On Pudlak's "Life in an Inconsistent World"

Solution 1:

To talk about these things semantically, it is easier to work in the system $\mathsf{ACA}_0$ of second-order arithmetic. This system is a conservative extension of Peano arithmetic for sentences in the language of Peano arithmetic, but $\mathsf{ACA}_0$ is able to deal directly with satisfaction (truth) predicates. If you don't know the details, for the rest of this post you can just treat $\mathsf{ACA}_0$ as a second-order version of Peano arithmetic.

A key point about $\mathsf{ACA}_0$ is that it can be axiomatized with a finite set of axioms. So we do not need to worry about "nonstandard" axioms when we look at nonstandard models: we can just assume that the finite set of axioms is used. This is not true of Peano arithmetic, which complicates Pudlak's argument - Peano arithmetic is not finitely axiomatizable. The fact that $\mathsf{ACA}_0$ is finitely axiomatizable is a good reason to look at it instead.

Suppose $M$ is a model of $\mathsf{ACA}_0 + \lnot \text{Con}(\mathsf{ACA}_0)$. This means that, in $M$, there is a natural number $c$ that codes a proof of $\lnot \text{Con}(\mathsf{ACA}_0)$. The proof coded by $c$ uses normal first-order logic, using just the axioms from $\mathsf{ACA}_0$. Because we can use a deductive system for first-order logic that only has a finite number of deduction rules, and because $\mathsf{ACA}_0$ really is consistent, $c$ must code a proof of nonstandard length when viewed from outside $M$.

Following Pudlak, let's assume that someone living in $M$ recognizes that all of the (finite number of) axioms of $\mathsf{ACA}_0$ are true in $M$, but they also recognize that $c$ codes a proof of $0=1$ from these axioms. Why is this not a contradiction?

For the person in $M$ to see the contradiction, they would need to prove by induction that, for each coded proof and every $n$, if all the statements on lines $0, 1, \ldots, n$ of a proof are true, then so is the statement on line $n+1$ (assuming the proof has $n+1$ or more lines). If they could prove that, they would be able to prove that $0=1$ is true in $M$, even though they know $0=1$ is not true in $M$, because $M$ satisfies $\mathsf{ACA}_0$.

The problem for the person in $M$ is that the induction principle needed in that proof is part of the $\Sigma^1_1$ induction scheme, and that scheme is not provable from $\mathsf{ACA}_0$. In fact, $\mathsf{ACA}_0$ plus the $\Sigma^1_1$ induction scheme proves $\text{Con}(\mathsf{ACA}_0)$. So the person in $M$ will see that $\Sigma^1_1$ induction fails.

That could be interpreted as "logic fails" if the person in $M$ thinks that $\Sigma^1_1$ induction is part of logic. Put more sharply, the person in $M$ would certainly think that "first-order logic is not sound" in the sense that a false sentence may be derived from true sentences in a "finite" (in $M$) number of steps. (At the same time, we know that $\mathsf{ACA}_0$ proves the soundness theorem for first-order logic - but that refers to something else, in this context.)

Solution 2:

A (Hilbert style) proof of $\phi$ from a (first order) theory $T$ is a finite sequence of sentences $\phi_1,\dots,\phi_n$, where $\phi$ is $\phi_n$, and each $\phi_i$ is either an instance of a logical axiom, a sentence in $T$, or comes from previous sentences in the sequence via modus ponens or one of the logical rules dealing with quantifiers.

There are variants of this definition, but they are all very similar, and what follows can be straighforwardly adapted to apply to them as well.

Working within $\mathsf{PA}$, where we have numbers but no sentences, or sequences, we need to make do via coding. This requires some care. The key property of $\mathsf{PA}$ being used is that we can carry out recursive constructions, as we can code finite sequences of numbers via numbers. This is not entirely obvious, see here for an example. We use this as follows: We start by selecting a recursive set of numbers to code the symbols of our language. Once this is done, we can code strings of symbols, formulas, and sequences of formulas. We can associate to $\mathsf{PA}$ a recursive set of numbers that code the sentences of $\mathsf{PA}$, and we have a formula $\psi(x,y)$ that holds iff $x$ is the code of a sentence, and $y$ is the code of a proof in $\mathsf{PA}$ of the sentence coded by $x$. (The way that recursive sets and recursive functions are represented in $\mathsf{PA}$ also requires some technical care. The references I mention in the link above address all these details carefully.) Moreover, whenever $\mathsf{PA}$ proves $\phi$, we can code the proof by a number $m$, and $\phi$ by a number $n$, and we can prove in $\mathsf{PA}$ that $\psi(n,m)$ holds. (More formally, the statement $\forall x\,\forall y\,(\tau_n(x)\land\tau_m(y)\to\psi(x,y))$ is provable. Here, $\tau_k(x)$ is "the" formula stating that $x$ "is" $k$.) Also, given any numbers $n,m$, if $n$ does not code a sentence, or if it does but $m$ does not code a proof of that sentence, then $\mathsf{PA}$ also proves $\lnot\psi(n,m)$.

Now, the point is this: In non-standard models, there will be non-standard numbers $n$ and $m$ such that $\psi(n,m)$ is satisfied in the model. This is what is meant when we say that the people of the model see a proof of "the sentence coded by $n$". In the model $\mathcal M$ Pudlak is describing, if $n$ is the code for $0=1$, there is a "proof" $m$ with $\psi(n,m)$ holding in $\mathcal M$. This $m$ is necessarily nonstandard. Maybe it has nonstandard length, so it is not really coding a sequence. Or maybe some of the "axioms" used in the "sequence" coded by $m$ are non-standard, so they are not really sentences. Or maybe both the length of the sequence and the lengths of some of the sentences used there are non-standard.

Solution 3:

It is a common figure of speech to re-present a proposition $P$ that is independent of a particular formal system $S$ and of a logical form that can be decided by examples (e.g., displaying a solution proves an equation is solvable, and writing down a proof of $0=1$ demonstrates inconsistency) as having examples that are "nonstandard" and exist in a "nonstandard model".

This kind of talk about nonstandard witnesses is the semantic equivalent restatement (by the completeness theorem) of the syntactic concept of a statement being undecidable. The completeness theorem is a correspondence between syntax and semantics for first-order theories.

Adding an independent statement to a system preserves consistency. The completeness theorem asserts that the system plus the independent statement (or its negation) has a model. If the addition is an undecidable existential statement $\exists x Q(x)$ that model will contain an element $x$ for which $Q(x)$ is true (a witness). If the addition is the negation of an undecidable universal statement $\forall y Q(y)$ that model will contain an element $y$ for which $Q(y)$ is false (a counterexample). For more complicated nested quantifiers the model might have to contain larger structures such as sets and functions and other collections of many $x$'s in order to (in)validate $P$, they no longer have to be single elements and there is not necessarily a simple word like "counterexample" to describe the relation of the truth/falsity certificate to the proposition.

The words true and standard refer to a situation where a more powerful supersystem of $S$ (such as a set theory, when $S$ is a theory of arithmetic) proves that $S$ has a preferred (thus "standard") type of model, perhaps a unique one, satisfying additional properties, and also can prove that the $S$-independent statement is true in that model (and, perhaps, also true in every model of the supersystem).

The nonstandard vocabulary is most common when the base system is a theory of arithmetic such as $PA$, since in that case developed language and intuitions of nonstandard models of arithmetic can be applied. These are not random extensions where you "add more stuff" to a standard model, but have very constrained order-types and a clear enough notion of the additional positive integers being infinitely large yet with well-defined properties.

In this metaphor, a nonstandard inconsistency proof can exist for a consistent system, but it has length $L$ for $L$ a nonstandard (therefore infinite) positive integer.

What is provable in the system $S$ only involves proofs whose lengths are measured by standard finite integers. That this coexists with nonstandard infinitely long proofs is because the latter reflect what is true in the model, and truth is a weaker property than being provable. Any nonstandard $L$ that is the length (or code) of an inconsistency proof would also admit proofs that $L >1$, $L > 2$, $L>3$ and $L > n$ for any finite $n$ that can be written down in a finite number of symbols.

From a more skeptical point of view, the passage from the book is merely an evocative reference to the undefined concept of people "seeing that their natural numbers are a model of Peano Arithmetic" (which also assumes it is well-defined to talk about "their natural numbers" separately from the PA-like system in their hypothetical world).