Very weak metatheories

[Pedro Sánchez Terraf]

Dear Tim and List,

Thank you very much for the pointer. That MO question was exactly on the 
spot; I was curious of what would be the views of someone like Nelson on 
the matter, and discussions around that. I'm also grateful for the 
references and comments provided by Riki Heck and David Auerbach.

I have another kinda follow-up question, that goes somewhat some sense 
in the opposite direction. It is also far more speculative.

With my team we've being working on a computer formalization of forcing. 
This was first achieved by Han & van Doorn by using the Lean proof 
assistant, based on type theory + universes. We worked in Isabelle/ZF, 
and we constructed the relevant ctms assuming ZF + a ctm of ZFC. It 
would obviously have been nicer to have the relative consistency results 
proved in PRA, PA, or at least something weaker than ZF.

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).

Thanks in advance for any new pointers (if there are any) on the 
discussion of this topic.

Best regards,

--
Pedro Sánchez Terraf
CIEM-FAMAF — Universidad Nacional de Córdoba
cs.famaf.unc.edu.ar/~pedro <https://cs.famaf.unc.edu.ar/~pedro>
On 28/7/22 17:04, Timothy Y. Chow wrote:
> Pedro Sanchez Terraf wrote:
>
>> It seems to be a standard practice to use Primitive Recursive 
>> Arithmetic as a "finitistic metatheory"; at least that is the take on 
>> Kunen's 2011 Set Theory book.
>>
>> My question, whose greatest sin is to have emerged out of sheer 
>> curiosity, is about what happens if one replaces PRA by a weaker, 
>> even ultrafinitist, metatheory.
>>
>>  * Do relative consistency results (CH, ~CH) go through as usual?
>>  * What about the Reflection Principle?
>>  * (Your metatheorem of choice)?
>
> A similar question came up on MathOverflow a couple of years ago. You 
> might find some relevant information in the answers and comments.
>
> https://mathoverflow.net/questions/378777/did-edward-nelson-accept-the-incompleteness-theorems 
>
>
> Tim
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220729/e13eab2c/attachment-0001.html>