Gödel's incompleteness tells us no consistent formal system can prove its own consistency. I understand that we can add an axiom to formal system $A$ stating "$A$ is consistent" and get a new system $A + Cons(A)$ which still fails to prove its own consistency if consistent, but why can't we add an axiom to $A$ stating that "$A$ with this new axiom is consistent"? Where do I go wrong in the following?
$A$ is a recursively enumerable set of axioms for a formal system capable of expressing any algorithm $x$, and the sentences $halts(x)$ and $\lnot halts(x)$. $A$ happens to be consistent. Then,
- You could have an algorithm printing theorems of $A$, halting if it finds a contradiction.
- You could have an algorithm which first prints its own source code $a$ then prints theorems of $A$, halting if it finds a contradiction.
- You could have an algorithm which first prints its own source code $a$, then adds in the axiom $\lnot halts(a)$ to its list of axioms, then prints theorems of $A + \lnot halts(a)$, halting if it finds a contradiction.
- The algorithm in 3. proves its own consistency since it will print $\lnot halts(a)$.
- The algorithm in 3. halts because it proves Gödel's result and its own consistency, yet the algorithm in 1. does not halt?
It seems problematic to think that adding the information "this axiom set is consistent" to an axiom set which happened to already be consistent will create a contradiction. Is there a way to justify this?