Skip to main content
1 of 4
Joel David Hamkins
  • 236.2k
  • 44
  • 777
  • 1.4k

The two most important properties of any formal proof system are soundness and completeness. A proof system is sound if it is truth-preserving, so that any model of the hypothesis of a derivation is also a model of the conclusion. A sound system is complete when any statement that holds in all models of a hypotheses is actually derivable in the system.

All of the usual proof systems are sound and complete. Soundness is typically easy to prove, for it usually amounts to observing that the logical axioms are valid and the derivation rules are truth-preserving. (Completeness proofs, in contrast, can be much deeper.)

Your proposed system, unfortunately, is not sound. The reason is that there can be models $M$ that think a theory $T$ is true, but not that it is consistent.

The easiest way to see that there are such models is to use the Incompleteness Theorem. Suppose that $PA$ is consistent, so that $Con(PA)$ is not provable in PA. Thus, $PA + \neg Con(PA)$ is consistent. If $M$ is a model of $PA + \neg Con(PA)$, then it satisfies $PA$, but not $Con(PA)$.

One can construct finitely axiomatizable examples in the same way, since the second incompletess theorem applies to sufficiently strong finitely axiomatizable theories, such as Robinson's $Q$. Thus, there are finite theories $T$, axiomatizing a sizable portion of arithmetic sufficient to do Goedel coding, such that there is a model of $T$ that is not a model of $Con(T)$. Your derivation rule is not truth-preserving with respect to these models, and so it is not a sound rule.

Joel David Hamkins
  • 236.2k
  • 44
  • 777
  • 1.4k