Very weak metatheories

[Timothy Y. Chow]

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.

Tim