Wolfgang Schwarz

Speculations on the Origin of "Incorrect" Quantifier Rules

The fact that it turned out so difficult to explain my question in sci.logic made me have a closer look at common axiomatic systems of the kind I was critizising. This was a good idea, because I found out that the systems used by Mendelson and Hodges are not of that kind after all. The only such system is the one used by Kutschera and Breitkopf, and as their logic book is German (and post-war), it is not surprising that nobody understood my problem. It is however interesting to compare the Kutschera/Breitkopf system with the systems of Mendelson, Hodges and others:

In the Kutschera/Breitkopf system, only closed sentences are allowed among premises and conclusions of a deduction. The axioms of the system are standard, its rules are Modus Ponens and

HG) From A B(x/t) one may deduce A x B provided that t does not occur in B and A.

Here t represents any individual constant, and B(x/t) is B, with every occurrence of x replaced by t.

This rule is "incorrect", because it justifies deductions like these:

1. Fa |- x Fx
2. Fa |- Fb
3. Fa Fb |- Fa Fa

In compensation, Kutschera and Breitkopf redefine "soundness" and restrict the Deduction Theorem:

The system is defined to be sound iff whenever M |- A, then M |= A, provided that in the deduction of A from M the rule (HG) is never applied for a constant t that occurs in M.

DT') If M,A |- B then A |- A B, provided that in the deduction of B from M,A the rule (HG) is never applied for a constant t that occurs in A.

(These are only roughly their redefinitions since I don't have the book here now.)

Now let's compare this to systems like Mendelson's and Hodges'. These systems allow open formulas in premises and conclusions. So they either have to restrict the equivalence of "|-" and "|=", or they have to provide a reading on which "|=" also makes sense when there are open formulas to its left or right. In practice, this choice doesn't matter because from the axioms and rules one can always read off a semantic relation that holds between M and A iff M |- A. The question whether or not this relation is officially assigned to "|=" is quite unimportant.

The semantic relation matching "|-" in Mendelson's and Hodges' system is this one: M |- A iff whenever every element of M is true under every valuation of an interpretation I, then A is also true under every valuation of I. So open formulas are basically treated like their universal closures.

These systems contain axioms and rules that look very much like the Kutschera/Breitkopf rules, except that they have variables where Kutschera and Breitkopf have constants. In particular, the following rule holds (maybe only as a derived rule):

HGV) From A B one may deduce A x B.

Under the proposed reading of "|-" this is unproblematic, because the deduced formula contains a quantifier that was already implicit in the premise. However, only a restricted version of the Deduction Theorem can be proved in these systems: E.g. it's true that

Fx |- x Fx

but not that

|- Fx x Fx.

Again, this is obvious under the proposed reading of "|-". However, the Deduction Theorem holds provided that in the deduction the rule (HGV) has not been applied for a variable x that occurs in the sentence that is taken from the left of "|-" to the right. That is,

DTV') If M,A |- B then M |- A B, provided that in the deduction of B from M,A the rule (HGV) is never applied for a constant x that occurs in A.

It seems that what Kutschera and Breitkopf did was to take such a system and then, to get rid of open formulas, replace all free variables occurring in the relata of the |- relation by constants.

This is why all the "incorrect" results of their system are correct if all individual constants in premises and conlusions are replaced by variables, and bound by universal quantifiers. E.g. the three examples above then become:

1. x Fx |- x Fx
2. x Fx |- x Fx
3. x y (Fx Fy) |- x (Fx Fx)

Of course they could hardly justify this reading of "|-" in their soundness proof. But once they had the restricted Deduction Theorem, it was quite easy to come up with a parallel restriction on sound deductions.

All this is rather unfortunate because the role of free variables in the systems they picked is so unlike the role of constants. There are other axiomatic systems where free variables are treated much more name-like, like the system used in Machover's Set Theory, Logic and their Limitations (Section 8.9.3 in this book contains a very brief comparison of the two kinds of system). Here, a different semantic relation matches |-: M |- A iff whenever every element of M is true under a valuation V of an interpretation I, then A is also true under V of I.

Replacing all free variables in the relata of |- by constants in such a system yields a nice, elegant and correct system that requires no redefinition of soundness and no restriction of the deduction theorem. The only thing that has to be restricted is HG: Under the proposed reading

(x=y) |- x=x (x=y)

is true, but not

(x=y) |- x=x x (x=y)

HG therefore has to be restricted to cases where the free variable bound by the newly introduced quantifier does not occur (freely) in the premises of the deduction.

Hm. Should I also add a "tedious" button?