Derivation rules and Godel theorem

Question

Every formal theory is a collection of alphabet, axioms and derivation rules. My question is - what kind of "derivation rules" are acceptable here. For example, "from A B it follows $A \cup B$" is a valid derivation rule. But what about, say, D: "from K it follows Cons (T(K))" where K is any collection of axioms, T(K) is the theory with axioms K and some prespecified alphabet and derivation rules? If alphabet of T(K) is reach enough to express the statement "Cons (T(K))", I see no reason why D is not a valid derivation rule.

But if it is, let us add this derivation rule D to ZFC, and denote the resulting theory ZFC+. Now, sets of axioms in ZFC and ZFC+ coincide, so it is recognizable. Next, if we believe that all axioms in ZFC are sound, all theorems in ZFC+ are also sound, and hence ZFC+ is consistent. Finally, if we apply D with K = "all axioms in ZFC+" we derive Cons (ZFC+) in one step. This is a contradiction with Godel Theorem. So, D is not a valid derivation rule? If so, why?

Answer 1

There are several issues here. The easiest one to resolve is the "contradiction" with Gödel's incompleteness theorem. This theorem does not concern arbitrary formal systems in your sense, but only arbitrary (effective) theories in first-order logic. These theories may specify axioms, but they cannot specify additional rules of deduction.

The deeper issue is that a rule of deduction is not "valid" on its own, it can only be valid with respect to some semantics. A semantics for a general formal system is a collection of "interpretations" of the system. The essential property is that each sentence of the formal system is assigned a truth value by each interpretation.

The usual semantics for first-order logic uses so-called "structures", each of which consists of a domain of discourse and interpretations of the non-logical symbols of the formal theory. Gödel's completeness theorem shows that the usual deduction rules for first-order logic are sound and complete for this class of interpretations: anything that is provable is true in every structure (soundness) and everything that is true in every structure is provable (completeness).

Your proposed additional deduction rule "from K deduce Con(T(K))" is not sound under usual first-order semantics. Essentially, any model Robinson arithmetic, Q, that does not satisfy Con(Q) is a counterexample to your deduction rule. (The reason for chooing Robinson arithmetic is that it is finitely axiomatizable.)

However, it is trivial to obtain a semantics for which your deduction rule is sound: simply limit the allowed interpretations to those that satisfy your deduction rule! This is a common technique in other settings. For example, when Liebniz's rule of equality is treated as a deduction rule rather than an axiom, we must restrict the class of allowable interpretations to the ones that validate Liebniz's rule to ensure that our deduction rules are sound. Liebniz's rule says, informally, that if an interpretation makes $\Phi(a)$ true and makes $a=b$ true then the interpretation must also make $\Phi(b)$ true.

The downside of limiting the class of allowable interpretations is that, although it guarantees soundness, it can cause completeness to fail. For example, if I limit the interpretations of Peano arithmetic to just the standard model, the usual deductive rules are still sound, but they are no longer complete, because many things are true in the standard model but unprovable.

There are other classes of interpretations used outside first-order logic. One important example is the class of Kripke models used to study modal logic and intuitionistic logic. There are completeness theorems in these contexts that say that certain deductive systems are sound and complete with respect to these semantics.

Answer 2

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.)

Answer 3

Here is another way to answer your question: by Cons(T), you mean the consistency of the first order theory generated by the set T of axioms. But the theory ZFC+ is not first order any more, since you have added a new inference rule. So it is not true that ZFC+ proves its consistency.

Answer 4

First, a short answer similar to Pierre Simon's but in different words: In your definition of D, you did not state the exact derivation rules that T(K) was supposed to contain. However you make the definition of D precise, T(K) cannot contain your new rule D, since that is what you are defining.

But I think your question is interesting because, to me, it shows that the widespread view that "every formal theory is a collection of alphabet, axioms and derivation rules" can be harmful sometimes. Such a view suggests that the concepts of "axioms" and "derivation rules" are somehow inherent in the concepts of "formal systems/languages/theories." What's wrong with taking a step back and defining "formal system" in more general terms? There are many ways to do so; I would propose something along the lines of "a formal system is essentially the same as any self-contained data structure of a computer program, together with a function that validates a given instance of that data structure." (The idea being that the data structure describes "proofs" of "theorems" in some arbitrary coding.)

Please don't read too much into those intentionally vague words. My point is just that such a definition would apply to a much wider class of formal systems than just predicate logic, and in particular also to formal systems that don't know about "axioms." Interestingly enough, Gödel's incompleteness theorems seem to apply to all such systems that can encode Peano arithmetic in some way. (I'm writing "seem" only because I have often read that claim but haven't seen any proof or even a precise statement of it. I guess I should ask an MO question about this.) AFAIK, the system from Principia Mathematica which Gödel was talking about wasn't actually based on predicate logic either.

So I think your question stems from a common but somewhat artificial distinction between "axioms" and "rules." In principle, every axiom is also a rule: the rule that a given formula can be assumed without proof. (I'm only talking about foundational systems, of course, not about axioms describing mathematical structures -- though some argue that there is no difference.) In some sense, Gödel's theorems are about computability, not about axioms and rules. You cannot evade them by trying to turn axioms into rules.

Answer 5

Just because you are willing to accept the rule that for any (finite) set of axioms, you can infere that the set is consistent, doesn't mean it is actually consistent. The rule is valid only if the axioms are already consistent. So all you can prove this way is that if ZFC is consistent then the inference rule is valid and then ZFC is consistent. So you can prove that ZFC is consistent if ZFC is. We know from Gödel exactly that one cannot prove the soundness of the inference rule from ZFC.

Moreover, adding the inference rule D gives you some kind of infinitary logic. Your argument requires that K can be infinite. I'm sure this can bring other complications.