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:
Replying to
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
Show replies