Suppose that an effectively axiomatized consistent formal system P that contains enough arithmetic for Gödel's Incompleteness theorems to apply, proves for any undecidable formula φ in the language of the formal system :

P⊢ Con(⌈P⌉)⇔φ , or , P⊢ ¬Con(⌈P⌉)⇔φ

where 'Con' is a consistency statement (with the provability predicate therein satisfying the conditions for Gödel's second incompleteness theorem)

where ⌈·⌉ is a Gödel numbering

then there exists an effective procedure that cannot be carried out by any Turing Machine and hece Church-Turing's thesis is false , because then P is decidable but not Turing decidable ( i.e. not decidable in any Turing equivalent model of computation ) for remark that then the following is a draft of a procedure that effectively lists out all the unprovable formula's of P :

on any input of sequences of symbols/strings of the language of P, decide whether or not it is a proof of a formula of P

if no, then ⟦ write 2+2=5 on the list ⟧

if yes, then ⟦ decide whether or not the formula that is proved is a biconditional (i.e. has as it’s main connective the biconditional) and has Con(⌈P⌉) as one of it’s conditions

if yes then ⟦output the other condition together with it's negation on the list ⟧

if no then⟦ check whether or not the formula that is proved is a conjunction with 2+2=4 as one of it’s conjuncts.

if yes then ⟦output the negation of the other conjunct on the list⟧ if no then ⟦ output 2+2=5 on the list ⟧ ⟧ ⟧


Questions :

are there flaws in this reasoning? are there (easy) disproofs for P proving these biconditionals?

  • $\begingroup$ A set (or relation) is strongly representable in P if and only if it is Turing decidable. A set (or relation) is weakly representable if and only if it is Turing semi-decidable. hence the set of (Gödel numbers of) unprovable formula's in P being not weakly representable implies that it is not Turing semi-decidable , however if my reasoning above is correct then it is semi-decidable (but not Turing semi-decidable) $\endgroup$
    – Icon
    Commented Sep 2, 2021 at 21:01
  • $\begingroup$ What distinction are you drawing between 'semi-decidable' and 'Turing semi-decidable'? What does the former mean? $\endgroup$ Commented Sep 2, 2021 at 21:26
  • $\begingroup$ Why should it be impossible to enumerate the unprovable formulas of $P$? And in any event, you never stated a critical assumption: that $P$ is actually consistent. $\endgroup$ Commented Sep 2, 2021 at 21:30
  • $\begingroup$ Also, what does it mean for $P$ to be "effectively axiomatised"? The only definition of this that I know of is that $P \vdash \phi$ is Turing semi-decidable. $\endgroup$ Commented Sep 2, 2021 at 21:34
  • $\begingroup$ @Steven Stadnicki by Church-Turing thesis a set is decidable iff it is Turing decidable , and it is semi-decidable iff it is Turing semi-decidable. That is decidable is the intuitive notion of an effective procedure and Turing decidable is what can be decided by a Turing machine , CTT is the thesis that the latter accurately captures the former , however if my reasoning above is correct then CTT is false for then there exists an intuitive effective procedure that cannot be carried out by any TM $\endgroup$
    – Icon
    Commented Sep 2, 2021 at 21:37

1 Answer 1


What you've actually shown is that $P$ is not consistent.

Edit: sadly, my original answer did not work. But this answer does work.

Consider a Turing-decidable "proof predicate" $isProof(x, y)$. The meaning of $isProof(x, \ulcorner \psi \urcorner)$ is that $x$ is a proof of $\psi$. Because $P$ is effectively axiomatised, there is such a Turing-decidable predicate. In fact, without loss of generality we can take $isProof$ to be a primitive recursive predicate (using the power of Kleene's T Predicate). So $P \vdash \psi$ is exactly the metatheoretic statement that there exists $x$ such that $isProof(x, \ulcorner \psi \urcorner)$.

Without loss of generality, take $isProof$ to be a partial function. That is, if $isProof(x, y)$ and $isProof(x, z)$ then $y = z$. In other words, each $x$ can be the proof of at most one thing.

Explanation for why we can take $isProof$ to be a partial function: We can do this by coming up with some primitive recursive function $pair : \mathbb{N}^2 \to \mathbb{N}$ and primitive recursive functions $p_1, p_2 : \mathbb{N}^2 \to \mathbb{N}$ such that $pair(p_1(p), p_2(p)) = p$, $p_1(pair(x, y)) = x$, and $p_2(pair(x, y)) = y$ for all $x, y, p \in \mathbb{N}$. In other words, $pair$ is a primitive recursive bijection, and the function $(p_1, p_2) : \mathbb{N} \to \mathbb{N}^2$ is its primitive recursive inverse. Starting with a proof predicate $isProof'$, we can come up with another proof predicate $isProof(x, y) = isProof'(p_1(x), y) \land (p_2(x) = y)$. If $isProof'$ is Turing-decidable, then $isProof$ will also be Turing decidable. And if $isProof'$ is primitive recursive, then $isProof'$ will also be primitive recursive.

We need to also have functions $not$ and $equiv$, definable in $P$. $not$ must satisfy $not(\ulcorner q \urcorner) = \ulcorner \neg q \urcorner$, and $equiv$ must satisfy $equiv(\ulcorner q \urcorner, \ulcorner p \urcorner) = \ulcorner q \iff p \urcorner$. If you are working in a sufficiently weak theorem, you may need to be more careful about the definition of $not$ and $equiv$ (they may be strongly representable but not definable), but we won't worry about that here.

Now consider the diagonal theorem of Godel, which states that for all unary predicates $\phi$ there exists some statement $\psi$ such that $P \vdash \psi \iff \phi(\ulcorner \psi \urcorner)$.

Consider the predicate

$$\eta(p, x) = isProof(x, p) \lor isProof(x, not(p)) \lor isProof(x, equiv(p, \ulcorner Con(P) \urcorner)) \lor isProof(x, equiv(p, \ulcorner \neg Con(P) \urcorner))$$

Note that $\eta$ is a primitive recursive predicate. Now consider the predicate $\phi(p) = \ulcorner$there is some $k$ such that $\eta(k, p)$, and $k$ is the smallest $k$ such that $\eta(k, p)$, and $k$ is not a proof of $p\urcorner$.

Let $\psi$ be such that $P \vdash \psi \iff \phi(\ulcorner \psi \urcorner)$.

Suppose there actually exists $k$ such that $\eta(k, \ulcorner \psi \urcorner)$. Consider the smallest such $k$. Since $\eta$ is primitive recursive, it is strongly representable in $P$, and therefore we have $P \vdash \eta(k)$.

Let us note that for all $j < k$, we have $\neg \eta(j)$. Since $\eta$ is strongly representable in $P$, for all $j < k$, we have $P \vdash \neg \eta(j)$.

Furthermore, since $P$ contains enough arithmetic, we have $P \vdash \forall j (j < k \iff \bigvee\limits_{i < k} j = i)$.

Therefore, we have $P \vdash \forall j (j < k \implies \neg \eta(j))$. So we see that $P \vdash \ulcorner k$ is the smallest $k$ such that $\eta(k) \urcorner$.

Now, we consider cases.

Case 1: $isProof(k, \ulcorner \psi \urcorner)$. Then $P \vdash \psi$. Then $P \vdash \phi(\ulcorner \psi \urcorner)$. Then $P \vdash \neg isProof(k, \ulcorner \psi \urcorner)$. But $isProof$ is strongly representable in $P$, and therefore $P \vdash isProof(k, \ulcorner \psi \urcorner)$. We have proved $P$ is inconsistent.

Case 2: $\neg isProof(k, \ulcorner \psi \urcorner)$. Then $P \vdash \neg isProof(k, \ulcorner \psi \urcorner)$ by strong representability. Therefore, $P \vdash \phi(\ulcorner \psi \urcorner)$, and thus $P \vdash \psi$. We must do further case analysis.

Case 2a: $isProof(k, \ulcorner \neg \psi \urcorner)$. Then $P \vdash \neg \psi$, and we see that $P$ is inconsistent.

Case 2b: $isProof(k, \ulcorner \psi \iff Con(P) \urcorner)$. Then $P \vdash \psi \iff Con(P)$, and thus $P \vdash Con(P)$. By the second incompleteness theorem, we see that $P$ is inconsistent.

Case 2c: $isProof(k, \ulcorner \psi \iff \neg Con(P) \urcorner)$. Then $P \vdash \psi \iff \neg Con(P)$, and therefore $P \vdash \neg Con(P)$.

Then there are no statements which are independent of $P$. For if a statement $\xi$ were independent of $P$, then either $P \vdash \xi \iff Con(P)$, in which case we would have $P \vdash \neg \xi$, or we would have $P \vdash \xi \iff \neg Con(P)$, in which case we would have $P \vdash \xi$. By the first incompleteness theorem, $P$ is not consistent.

Thus, we see that if either $P \vdash \psi$, $P \vdash \neg \psi$, $P \vdash \psi \iff Con(P)$, or $P \vdash \psi \iff \neg Con(P)$, then there exists some $k$ such that $\eta(k)$, and therefore $P$ is not consistent.

Now suppose that $P$ were consistent. Then we see that $P \nvdash \psi$, and also $P \nvdash \neg \psi$. Therefore, either $P \vdash \psi \iff Con(P)$, or $P \vdash \psi \iff \neg Con(P)$. Then $P$ is not consistent. Contradiction.

Therefore, $P$ is not consistent.

  • $\begingroup$ That's a satisfying answer, thanks. $\endgroup$
    – Icon
    Commented Sep 2, 2021 at 22:28

You must log in to answer this question.

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