Our earlier publications showed semantic tableau admits partial exceptions to the Second Incompleteness Theorem where a formalism recognizes its self consistency and views multiplication as a 3-way relation (rather than as a total function). We now show these boundary-case evasions will collapse if the Law of the Excluded Middle is treated by tableau as a schema of logical axioms (instead of as derived theorems).
From Tarski to Gödel. Or, how to derive the Second Incompleteness Theorem from the Undefinability of Truth without Self-reference
Rosser provability and the second incompleteness theorem
A mathematical commitment without computational strength
![QR code for arXiv:2006.01057 [math.LO]](http://oss.arxitics.com/images/favicon.svg)