I recently learned that ZFC can prove $Con(PA)$ because it can give a model of PA, but I'm not given the technical details. (My teacher thinks it is too obvious to even mention.) What plagues me is that my naïve intuition tells me that the modeling procedures can be imitated in PA, exactly in the same way.

Here is my attempt: Let $eval_F$ and $eval_T$ be evaluation functions for Formulas and Terms. Let $e$ denote any variable assignment. We can define these functions recursively, exploiting Tarski's lemma. Explicitly,

\begin{align} eval_T(\ulcorner v_i\urcorner,e) &= e[i] \\ eval_T(\ulcorner o\urcorner,e) &= 0 \\ eval_T(\ulcorner s\tau \urcorner,e) &=eval_T(\ulcorner\tau\urcorner,e)+1 \\ eval_T(\ulcorner \tau_1 + \tau_2 \urcorner,e) &=eval_T(\ulcorner\tau_1\urcorner,e)+eval_T(\ulcorner\tau_2\urcorner,e) \\ eval_T(\ulcorner \tau_1 \cdot \tau_2 \urcorner,e) &=eval_T(\ulcorner\tau_1\urcorner,e) \cdot eval_T(\ulcorner\tau_2\urcorner,e) \end{align}


\begin{align} eval_F(\ulcorner \bot \urcorner,e) &=0 \\ eval_F(\ulcorner \tau_1 = \tau_2 \urcorner,e) &= \chi_=(eval_T(\ulcorner\tau_1\urcorner,e),eval_T(\ulcorner\tau_2\urcorner,e)) \\ eval_F(\ulcorner \Phi\to\Psi \urcorner,e) &= \mathrm{sgn}((1-eval_F(\ulcorner \Phi \urcorner,e))+eval_F(\ulcorner \Psi \urcorner,e)) \\ eval_F(\ulcorner \forall v_i.\Phi \urcorner,e) &=\begin{cases} 1 & (\forall n.eval_F (\ulcorner\Phi\urcorner,e[i\mapsto n]) = 1) \\ 0 & (\mathrm{otherwise})\\ \end{cases} \end{align}

Then $eval_T$ and $eval_F$ are $\Sigma_1^0$- and $\Sigma_2^0$-defined function respectively. Although $eval_F$ is not decidable, at least we know that $eval_F$ is total over coded PA-formulas and the value is either $0$ or $1$. If we show that every axiom in PA evaluates to $1$ and the inference rules are truth-preserving, then we can show the soundness of the model: $$ \forall \phi:\mathrm{Form}. (Provable(\phi) \to \forall e. (eval_F(\phi,e)=1)) $$ If so, we can conclude $Con(PA)$, which is $\neg Provable(\ulcorner \bot \urcorner)$, because $\bot$ evaluates to $0$.

Of course, this violates Gödel's second incompleteness theorem, so I must be wrong somewhere - but I couldn't find where. I am now suspecting three possibilities:

  • We cannot in fact well-define $eval_T$ and $eval_F$ in PA.
  • We cannot prove that $eval_F$ models the axioms of PA.
  • The inference rules does not preserve truth generated by $eval_F$.

I want to know where my argument fails. Thanks in advance.

P.S. The most suspicious one for me is the second one, especially induction scheme. Nonetheless I am convinced that induction scheme is provably evaluated to 1, since it reduces to \begin{align} \forall \phi:\mathrm{Form}.\forall e. &\forall i. \bigl( eval_F(\phi,e[i\mapsto 0])=1 \to \\ &\forall n. (eval_F(\phi,e[i\mapsto n])=1 \to eval_F(\phi,e[i\mapsto n+1])=1) \to \\ &\forall n. (eval_F(\phi,e[i\mapsto n])=1 )\bigr) \end{align}

which is an instance of induction scheme of outer PA.

  • 3
    $\begingroup$ The thing is, in formal logic you can't define formulas by recursion like you do like that. If you want to define a formula $A$, then you have to define using symbols which do not involve $A$ itself. The way this can be done in ZFC is by constructing not a single formula $eval_F$, but rather a set, call it $e_F$, which contains all the formulas. Sets can be defined iteratively like that, and we can say that $e_F$ is the set which satsifies the inductive properties you list. $\endgroup$ – Wojowu Jun 28 at 11:46
  • 4
    $\begingroup$ Why is $\mathit{eval}_F$ total? What is the PA formula that expresses $\mathit{eval}_F(n) = k$? If you use recursion to define a formula, you also have to explain how to eliminate the recursions, because in first-order logic there is no way to define formulas by recursion the way you do. $\endgroup$ – Andrej Bauer Jun 28 at 11:47
  • 1
    $\begingroup$ Perhaps the following comment will be helpful: you claim that the logical complexity of $\mathit{eval}_F(n) = k$ is $\Sigma^0_2$. If that were the case, then $\mathit{eval}(\lceil \forall v_i . \Phi\rceil) = k$ would have complexity $\Pi^0_3$, at least the way it's written in your definition. $\endgroup$ – Andrej Bauer Jun 28 at 13:15
  • 1
    $\begingroup$ @Wojowu See this Math SE answer. The fact that you can actually explicitize recursively defined predicates or functions even in PA, without any notions about sets, is the significant result of metamathematics from Gödel's famous paper. $\endgroup$ – Paul Sohn Jun 28 at 14:58
  • $\begingroup$ @AndrejBauer Now I got the point. I was bugged in the explicitization step. To evaluatie universal quantification, I need to make infinite sequence to prove the evaluation, which is impossible in PA. $\endgroup$ – Paul Sohn Jun 28 at 15:10

First-order logic does not provide for definitions of functions by recursion. For example, the transitive closure of a binary relation $R$, though definable from $R$ by recursion, is not in general first-order definable from $R$.

Peano Arithmetic, though formulated in first-order logic, does have enough axioms to support some definitions by recursion. Specifically, thanks to the availability in PA of sequence coding, a recursive definition can be reformulated as an explicit definition provided each step in the recursion depends on only finitely many previous results. For example, the natural definition of the factorial function ($0!=1$ and $(n+1)!=n!\cdot (n+1)$) can be rewritten as "$x!=y$ iff there is a sequence $a_0,a_1,\dots,a_x$ of length $x+1$ with $a_0=1$, $a_{n+1}=a_n\cdot(n+1)$ for all $n<x$, and $a_x=y$." This reformulation is expressible in PA because coding allows us to replace "there is a sequence" with "there is a number". But it's crucial here that all the "predecessors" of "$x!=y$" in this recursion can be coded into a single number, which requires that there be only finitely many of these predecessors. There's no way to code an infinite sequence of natural numbers into a single natural number.

In your recursive definition of $eval$, the clause for a universally quantified formula unfortunately involves infinitely many predecessors, namely the values for all the alternative assignments $e[i\mapsto n]$. This one clause prevents your recursion from being expressible in PA.

(Any extension of PA that would allow expressing this recursion --- whether by adding more axioms or by strengthening the logic --- and allow proofs by induction of formulas containing such an expression would also prove the consistency of PA along the lines you indicated. So it's a good thing that PA can't express this recursion; if it could, then it would prove its own consistency and therefore would be inconsistent by Gödel's second incompleteness theorem.)

| cite | improve this answer | |
  • $\begingroup$ That's why I assumed PA, not arbitrary first-order theory. Anyway, I overlooked that universal quantifier clause involves infinite predecessors, which requires sequences of countable ordinal lengths to encode it. Now I see how second-order arithmetic (sufficiently strong ones) proves Con(PA) and PA doesn't. Thanks! $\endgroup$ – Paul Sohn Jun 28 at 15:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.