6
$\begingroup$

I'm studying (independently) mathematical logic and in investigating self-referential statements I developed a result which I don't know how to interpret. I'll use the notation from Enderton's "A mathematical introduction to logic" (p 266-267):

Let $T$ be any sufficiently strong recursively axiomizable theory (PA or ZF will do) and let $\sf Prb_T \sigma$ (Here $\sf Prb_T$ abbreviates "provable in $T$") express that $\sigma$ has a deductive proof in $T$. (i.e. $\sf Prb_T \sigma$ means $T \vdash \sigma$). Let $\sf Cons T$ be a sentence expressing that $T$ is consistent (such as $\neg \sf Prb_T (0=1))$. Then using the fixed-point lemma we can get a sentence $\sigma$ such that:

$$T \vdash (\sigma \leftrightarrow \sf Prb_T (\sf Cons T \rightarrow \neg \sf Prb_T \sigma))$$

Now either $T \vdash \sigma$ or $T \nvdash \sigma$. I will show that we cannot have either assuming $T$ is consistent.

If $T \vdash \sigma$ then by our definition of $\sigma$ we have that $T \vdash \sf Prb_T (\sf Cons T \rightarrow \neg \sf Prb_T \sigma)$. This implies that $T \vdash (\sf Cons T \rightarrow \neg \sf Prb_T \sigma)$ But this means that we have a proof of $T$ being consistent implies $T \nvdash \sigma$ which contradicts this initial hypothesis of $T \vdash \sigma$. Therefore, assuming $T$ is consistent, we must have $T \nvdash \sigma$. But this too also leads to a contradiction, for by our construction of $\sigma$ we now have $T \nvdash \sf Prb_T (\sf Cons T \rightarrow \neg \sf Prb_T \sigma)$. This means that there is no proof of $T$ being consistent implying that $T \nvdash \sigma$. However, we just provided a proof (albeit meta-mathematical in nature) testifying to this fact.

So what should I logically conclude from this? I figure that this implies that $T$ is inconsistent. I guess there is another possibility: That this whole result/proof cannot be formalized thus removing the contradiction (or maybe not because then we might have a contradiction with the Completeness Theorem for first-order logic). I know that by Godel's Second Incompleteness Theorem assuming $T$ is consistent then $T \nvdash \sf Cons T$. However $T$ can still prove some facts about implications involving $\sf Cons T$ (In fact, Enderton gives one such example on the bottom of page 267). My understanding is that most meta-mathematical results such as Godel's incompleteness theorem and Tarski's undefinability theorem can be represented and proven in the deductive calculus. Am I wrong on this? If I'm not then what makes this result any different?

$\endgroup$

1 Answer 1

6
$\begingroup$

The problem with the argument, indeed with most of the claims of this sort is that the internalization of logic and proofs are only as good as your standard integers, but become uncontrollable when we move forward from them.

What do I mean by that? We know that every real, meta-theoretic, proof corresponds to a specific natural number. And we know that $T$ itself has a predicate that is interpreted as exactly the codes for the axioms of $T$.

But this only happens in models where the integers are standard. If you have non-standard integers, you invariably add new axioms to $T$ and you add new inference rules to your logic, and so you added new ways of proving that $0=1$.

So the way to reconcile this is to notice that indeed a model of $\sf ZFC+\lnot\operatorname{Con}(ZFC)$ must disagree with its meta-theory about the integers (namely, it must have non-standard integers which will witness this).

$\endgroup$
4
  • $\begingroup$ I apologize, but I'm just a novice and a little lost by your answer. Can you explain at all how I added new ways of proving $0=1$ but something like $T \vdash (\tau \leftrightarrow \neg \sf Prb_T \tau) \implies T \vdash (\sf Cons T \rightarrow \neg \sf Prb_T \tau)$ can be proven as Enterton demonstrates. $\endgroup$
    – Ari
    Commented Jan 19, 2016 at 17:07
  • $\begingroup$ You should perhaps read this before we start mincing words. It talks about a similar situation, but with $\sf PA$ instead. $\endgroup$
    – Asaf Karagila
    Commented Jan 19, 2016 at 17:09
  • $\begingroup$ I take that it helped? $\endgroup$
    – Asaf Karagila
    Commented Jan 19, 2016 at 18:03
  • $\begingroup$ Yes thank you. I didn't consider the fact that there are other models. However, I think I'll ask another question though (not one claiming ZF is inconsistent) just to get a better sense of proof techniques and how they are reflected (or not) in the deductive calculus. Thanks again! $\endgroup$
    – Ari
    Commented Jan 19, 2016 at 18:10

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .