i wrote a mathoverflow answer about godel's incompleteness theorem and nonstandard models of arithmetic that believe arithmetic is inconsistent that some of you might be interested in:
Conversation
Some people say that they believe that PA is consistent despite not being able to prove it and I still don't get that. It seems like we can only be in two states of knowledge about it. Either we are uncertain about the consistency of PA, or we know it is inconsistent.
1
3
so if you ask a mathematician who knows a little about this, the standard boilerplate answer is that ZF proves the consistency of PA because you can construct a model of PA in it (the standard natural numbers). of course then you can ask why they believe that ZF is consistent
2
3
Yeah that just passes the buck.
Do you know how much of model theory of PA and results like in the MO post are constructively provable?
1
2
nonstandard models of PA can't be computable so they don't really exist constructively:
1
2
the compactness theorem and the completeness theorem are equivalent to each other and to the ultrafilter lemma which is independent of ZF but strictly weaker than the axiom of choice:
1
2
Can you even say that if PA is consistent, then it has a model? (Maybe some sort of syntactic model??)
I'm trying to find stuff on constructive model theory and there's very little. Model theory seems to be very classical
1
2
so to set up model theory you need a metatheory which is in particular capable of talking about sets so that you can talk about a model as a set equipped with some functions and relations etc. if your metatheory believes ZF then you can just construct a model of PA in it
1
2
idk i feel like if you want to be really hardnosed about the natural numbers you can sort of just refuse to work with the “completed infinity” and stick to only increasingly large finite sets of integers as necessary. like instead of proving that addition is commutative by...
1
2
...induction you just note that for any particular finite n you can write down a finite proof that addition is commutative up to n, then run that proof whenever you need to cite commutativity of addition anywhere. of course most mathematicians would consider this crazy...
1
2
...because to them it’s clear that this procedure will always work so why not just do it all at once one time and then forget about it? and at least for something as simple as commutativity of addition i admit i find this argument pretty compelling
Replying to
Imo induction just encodes proofs like this, and types like N aren't these static completed things but have constructors for producing more elements, so I don't see problems with such infinite sets from a finitist/constructive perspective
1
1
If you used something like higher order HA_oo, which is equiconsistent with first order PA_1 and HA_1, then it shouldn't be able to outright prove that its own N type is a model of HA_1. I wonder if Con(HA_1) would allow it to do so though
1