Considering this question, we know that a first order theory that admits a model has to be consistent.
A model for a theory $T$ in a language $\mathcal L$ is an interpretation of $\mathcal L$ in which all the axioms of $T$ are true.
In my introductory course to mathematical logic we discussed "minimal arithmetic" (better known as "Robinson arithmetic"), which is a theory in the language $\{0,1,+,\cdot\}$ satisfying a finite set of axioms, cfr. Robinson arithmetic. We also discussed $DLO$ theory.
My question is, in the case of $DLO$, which is the theory of "dense linear order without endpoints" we stated that, for example, $\mathcal Q=\{\mathbb{Q},\lt\}$ is a model for this theory, where $\mathbb{Q}$ are the rationals and $\lt$ is interpreted as usual.
Therefore, this should tell us that $DLO$, since it has a model, must be consistent, right?
For minimal arithmetic, which we denoted as $MA$, wouldn't we have some "obvious" models, for example the ring of natural numbers $\mathbb N$ with the usual operations of $+$ and $\cdot$. Now, take for example Peano arithmetic, there are discussions about "standard models" and "non-standard models", cfr. this question, in any case we are discussing models, shouldn't this immediately tell us that these theories are consistent? On the other hand it is a celebrated fact that Peano arithmetic cannot prove it's own consistency, according to Gödel's second theorem of incompleteness, but why would we even investigate this if the existence of a model is sufficient. I feel like I'm missing or misunderstanding some crucial point in the discussion, any help would be appreciated.
Best Answer
Yes, if you believe everything makes sense and checks out regarding the basic ideas of model theory and $\mathbb N$ being a model of PA, then you believe in the consistency of PA.
Most people are comfortable with all this. Not everyone is. (The sticking point is usually either the meaningfulness of $\mathbb N$ or the validity of induction for formulas arbitrarily high up in the arithmetical hierarchy. The latter wouldn't apply to MA and more generally, I’ve never heard anyone seriously doubt the consistency of MA.)
In any event, you are proving the consistency of PA using resources like model theory and set theoretical constructions that are more elaborate than arithmetic, so a proof like Gentzen's with fewer philosophical commitments has some appeal (and may also satisfy skeptics of the model theory proof, if we care about persuading them).
The original importance of the 'celebrated fact' was that it had been originally hoped that the consistency of very strong systems could be proven in very weak systems, and this rendered that impossible. So it's not really that PA can't prove Con(PA) that's important from this perspective, it's that PA can't prove Con(ZFC), or that not even ZFC can prove Con(ZFC). (And note that it is comparatively unclear that ZFC has a model.)
The emphasis on PA not proving Con(PA) is just an unfortunate turn some expositions have taken, though it's not exactly useless to know that we shouldn't go rooting about for a proof of Con(PA) in PA.