Very weak metatheories
Timothy Y. Chow
tchow at math.princeton.edu
Fri Jul 29 18:30:37 EDT 2022
On Fri, 29 Jul 2022, Pedro Sánchez Terraf wrote:
> But actually, that "proof" is ultimately running in the computer
> hardware, which is a physical system. The question is, which is the
> consistency strength of that physical system?
> I'll try to make sense of the question, at least one interpretation of
> it (but I'd be interested in any other). The design of the components
> and circuitry of the computer respond to some mathematical model (laws,
> equations, etc.) of the underlying physics. Therefore, I should consider
> that my meta-meta-theory to be that supporting this model. Hence if the
> strength needed to support that model is supposedly stronger than PA,
> there is no point in lowering the intermediate meta level (that is, the
> logic of the proof-assisting software).
I think you're conflating a couple of different things here.
The word "assumption" can mean different things. It can mean a formal
axiom in a formal language. It can also mean something fuzzier, like an
assumption that there's no Cartesian demon messing with my mind, or that
cosmic rays aren't somehow zapping my computers at exactly the right times
to make my incorrect computations seem to be correct. Let's call the
latter type of "assumption" a "demonic assumption."
It sounds like you're arguing that there is no point in proving a theorem
using "assumptions" that are weaker than the "assumptions" that I must
make in order to justify my belief in the correctness of the physical
process of checking the proof. But the former assumptions are formal
axioms while the latter assumptions are demonic assumptions, and so they
are not comparable.
You might still have a nagging feeling that the demonic assumptions
include some formal axioms. But you never need to assume anything more
than that *one specific computer run behaved the way you expected*. This
is a completely finite calculation and so "consistency strength" never
enters into it.
Let's take an even more simple-minded scenario. Using pen and paper, I
verify that 34 + 47 = 81. At the conclusion of this calculation, I feel
confident that 34 + 47 = 81, but what assumptions am I making? I'm
certainly assuming that I'm not a brain in a vat that is being manipulated
into believing a false calculation, but am I making some *arithmetic*
assumptions? The point is that even if one wishes to argue that I am
making some arithmetic assumptions, I only need to assume enough
arithmetic to support the finite calculation 34 + 47 = 81, and that is an
extremely finite amount of arithmetic. I don't need to assume anything
infinitary, and so consistency strength doesn't enter into it.
More information about the FOM