Very weak metatheories
Pedro Sánchez Terraf
sterraf at famaf.unc.edu.ar
Fri Jul 29 16:57:40 EDT 2022
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>
More information about the FOM
mailing list