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 ⟧ ⟧ ⟧
End
Questions :
are there flaws in this reasoning? are there (easy) disproofs for P proving these biconditionals?
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.