Return to Answer

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.

Edit. Let me now observe that ZFC and even PA already exhibit the power of what you had hoped to gain by your deduction rule, but in a slightly different sense. That is, let us consider matters as a theory, rather than as a change in the proof system, by considering over ZFC the axioms:

• $\varphi\to Con(\varphi)$

This axiom expresses something very like the content of your proposed deducton rule. But I claim that all of these axioms are already provable in ZFC! This is a consequence of the Reflection Theorem, which asserts of any finitely list of statements $varphi_0,\ldots,\varphi_n$ that there is some $\alpha$ such that $\varphi_i$ is absolute between $V_\alpha$ and $V$. In particular, for any sentence $\varphi$, the theory ZFC proves that if $\varphi$ is true, then it is consistent. (One can prove this claim only as a scheme, however, that is, separately of each $\varphi$, and so one cannot deduce $Con(ZFC)$ within ZFC this way.)

Thus, ZFC already seems to have much of the power that you had wanted to gain by your deduction rule.

Indeed, any theory that proves all of its finite subtheories consistent will have the same feature. This includes PA itself, because I believe that if one stratifies the PA induction scheme by complexity, then $\Sigma_{n+1}$ induction implies $Con(I\Sigma_n)$. This is one way people have deduced that PA is not finitely axiomatizable. Thus, PA also proves all of the above axioms in the language of arithmetic. But again, these proofs cannot be uniformized into a proof of $Con(PA)$, because of the counterexample model I mention above.

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.

Edit. Let me now observe that ZFC already exhibits much of the power of what you had hoped to gain by your deduction rule, but in a slightly different sense. That is, let us consider matters as a theory, rather than as a change in the proof system, by considering over ZFC the axioms:

• $\varphi\to Con(\varphi)$

This axiom expresses something very like the content of your proposed deducton rule. But I claim that all of these axioms are already provable in ZFC! This is a consequence of the Reflection Theorem, which asserts of any finitely list of statements $varphi_0,\ldots,\varphi_n$ that there is some $\alpha$ such that $\varphi_i$ is absolute between $V_\alpha$ and $V$. In particular, for any sentence $\varphi$, the theory ZFC proves that if $\varphi$ is true, then it is consistent. (One can prove this claim only as a scheme, however, that is, separately of each $\varphi$, and so one cannot deduce $Con(ZFC)$ within ZFC this way.)

Thus, ZFC already seems to have much of the power that you had wanted to gain by your deduction rule.

(Even PA itself proves all of its finite subtheories to be consistent. If one stratifies the PA induction scheme by complexity, then $\Sigma_{n+1}$ induction implies $Con(I\Sigma_n)$. This is one way people have deduced that PA is not finitely axiomatizable. This feature seems related to the scheme above, but I'd have to think further about whether PA actually proves every statement of the form $\varphi\to Con(\varphi)$, as ZFC does.)

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.

Edit. Let me now observe that ZFC in a sense already exhibits the power of what you had hoped to gain by your deduction rule. That is, let us consider matters as a theory, rather than as a change in the proof system, by considering over ZFC the axioms:

• $\varphi\to Con(\varphi)$

This axiom expresses something very like the content of your proposed deducton rule. But I claim that all of these axioms are already provable in ZFC! This is a consequence of the Reflection Theorem, which asserts of any finitely list of statements $varphi_0,\ldots,\varphi_n$ that there is some $\alpha$ such that $\varphi_i$ is absolute between $V_\alpha$ and $V$. In particular, for any sentence $\varphi$, the theory ZFC proves that if $\varphi$ is true, then it is consistent. (One can prove this claim only as a scheme, however, that is, separately of each $\varphi$, and so one cannot deduce $Con(ZFC)$ within ZFC this way.)

Thus, ZFC already seems to have much of the power that you had wanted to gain by your deduction rule.

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.

Edit. Let me now observe that ZFC and even PA already exhibit the power of what you had hoped to gain by your deduction rule, but in a slightly different sense. That is, let us consider matters as a theory, rather than as a change in the proof system, by considering over ZFC the axioms:

• $\varphi\to Con(\varphi)$

This axiom expresses something very like the content of your proposed deducton rule. But I claim that all of these axioms are already provable in ZFC! This is a consequence of the Reflection Theorem, which asserts of any finitely list of statements $varphi_0,\ldots,\varphi_n$ that there is some $\alpha$ such that $\varphi_i$ is absolute between $V_\alpha$ and $V$. In particular, for any sentence $\varphi$, the theory ZFC proves that if $\varphi$ is true, then it is consistent. (One can prove this claim only as a scheme, however, that is, separately of each $\varphi$, and so one cannot deduce $Con(ZFC)$ within ZFC this way.)

Thus, ZFC already seems to have much of the power that you had wanted to gain by your deduction rule.

Indeed, any theory that proves all of its finite subtheories consistent will have the same feature. This includes PA itself, because I believe that if one stratifies the PA induction scheme by complexity, then $\Sigma_{n+1}$ induction implies $Con(I\Sigma_n)$. This is one way people have deduced that PA is not finitely axiomatizable. Thus, PA also proves all of the above axioms in the language of arithmetic. But again, these proofs cannot be uniformized into a proof of $Con(PA)$, because of the counterexample model I mention above.

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.

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.

Edit. Let me now observe that ZFC in a sense already exhibits the power of what you had hoped to gain by your deduction rule. That is, let us consider matters as a theory, rather than as a change in the proof system, by considering over ZFC the axioms:

• $\varphi\to Con(\varphi)$

This axiom expresses something very like the content of your proposed deducton rule. But I claim that all of these axioms are already provable in ZFC! This is a consequence of the Reflection Theorem, which asserts of any finitely list of statements $varphi_0,\ldots,\varphi_n$ that there is some $\alpha$ such that $\varphi_i$ is absolute between $V_\alpha$ and $V$. In particular, for any sentence $\varphi$, the theory ZFC proves that if $\varphi$ is true, then it is consistent. (One can prove this claim only as a scheme, however, that is, separately of each $\varphi$, and so one cannot deduce $Con(ZFC)$ within ZFC this way.)

Thus, ZFC already seems to have much of the power that you had wanted to gain by your deduction rule.