Traditional Logic Put in Contemporary Form

This is a reflection on John Bacon’s article “First Order Logic based on Inclusion and Abstraction”.

Aristotle’s syllogistic was a logic of general terms, and the same could still be said of traditional logic in the 19thcentury.  Writing in 1900, Bertrand Russell explained the failures he saw in Leibniz’s philosophy by the simple point that Leibniz was held back by the form of Aristotle’s syllogistic, the only logic then in play.  

Ironically, we still see the struggles and birth pangs of a new logic coming into being in Russell’s 1903 Principles of Mathematics.  What sense could there be in the new ideas about sets or classes?  A set is meant to be a collection.  But by the very meaning of the word, a collection is a collection of things, “things” plural.  Does it make sense to speak of a collection of just one thing?  What is the difference between “I put an orange on the table” and “I put a collection of one orange on the table”?   It does make sense to say “I put nothing on the table”, but what about “I put a collection of nothing on the table”? 

One might say, not unfairly, that all these puzzles were put behind us when Frege (in effect) introduced set-abstraction. (Even if he did so a little injudiciously, even inconsistently, the idea was soon tamed and made practical.)  Within limitations, x̂Fx denotes the set of all things F, the singleton or unit set appears as extension of x̂(x = y), and the empty set as x̂(x  x).  The Frege-Russell logic was able to develop through that major innovation.  

But then, can’t we imagine that traditional logic could have developed equally successfully, through that same innovation?

I read John Bacon’s paper as answering this question with a resounding Yes.  

As Bacon shows, the new logic that we enjoy today can be seen as a straightforward development of the very ‘logic of terms’ that Boole and De Morgan (and Schroeder and Peirce and …) turned into algebra. And so I would like to explain in a general way just how he does that.

To begin, it is a recurrent complaint about syllogistic that it is really only a logic of general terms, and has no good place for singular propositions.  “Socrates is mortal” is accommodated awkwardly and artificially .

But as soon as singletons are respectable denizens of the abstract world, there is no problem for a logic of terms:

 “Socrates is mortal” is true if and only if {Socrates} ⊆ {mortals}.

The three primitive notions that Bacon uses to simultaneously construct a contemporary form of the logic of terms and reconstruct first-order logic in just that form are these:  the relation of inclusion, an abstraction operator, and the empty set.  

Vocabulary: a set of variables, a set of constants, x̂, , and 0.   Grammar: variables and constants are terms, and andx̂A is a term if A is any sentence and x a variable; if X, Y are terms then X ⊆ Y is a sentence. 

The constants are names of sets, they cannot include “Socrates” but only a name for the set {Socrates}.  The variables stand for singletons.  So “Socrates is mortal” can be symbolized as “x ⊆ Y”.

Reconstruction of propositional calculus

If A is a sentence then x̂A is the set of all things x such that A.  In this part we’ll only look at the case where x does not occur in A or B, for example x̂[2 + 2 = 4].  All things are such that 2+2 = 4!  So that set is the universe of discourse, it has everything in it.  We have a neat way to introduce the truth values:

A is true if and only if x̂A = the universe

A is false if and only if x̂A = 0.

This already tells us how to denote the universe:

            U = x̂(O ⊆ 0)

A quick reflection shows that, accordingly, (x̂A ⊆ 0) always has the opposite truth-value of A.  So we define:

            ~A = (x̂A ⊆ 0)

What about material implication, the sentence A ⊃ B?  That is false only if A is true and B is false.  But that is so exactly and only if x̂A = U and x̂B = 0, so we define:

            (A ⊃ B) = (x̂A ⊆ x̂B)

Since nothing more is needed to define the other truth-functional connectives, we are finished.  It is at once useful to employ the definable conjunction & at once for a definition:

            X = Y iff (X ⊆ Y) & (Y ⊆ X)

Reconstruction of quantificational logic

Let’s to begin think only about unary predicates.  The variables here can occur in the sentences we are looking at.

“Something is F” we symbolize today as “(∃x)Fx”.  But this is clearly true if and only if the set x̂[Fx] is not empty.  We define:

            (X ≠Y) = ~(X = Y)

            (∃x)A = (x̂A ≠ 0)

Similarly, the universal quantification (∀x)Fx is true precisely if x̂A = U.

Symbolizing “All men are mortal”:

            x̂[(x ⊆ X) ⊃ (x ⊆ Y)] = U

Relations

The famous puzzle for 19th century logic was to symbolize

            If horses are animals then heads of horses are heads of animals.

Bacon had no difficulty explaining how the system can be extended to relational terms P2, Q3, and so on, with the superscript indicating the addicity.  The semantics can be straightforward in our modern view:  P2 is a set of couples, Q3 a set of triples, and so on,   with the simple idea that (ignoring use/mention):

            (*) Rab is true if and only if <a, b> is in R.

Then Bacon allows strings of variables as n-adic variables.  So if x stands for {Tom} and y for {jenny} then xy stands for {<Tom, Jenny>}.  The sentence (xy ⊆ P2) then means that {<Tom, Jenny>} ⊆ P2.

But Bacon does it in a particular way that has some limitations.  For example, in his formulation, inclusion is significant only between relations of the same degree.  That raises a difficulty for examples like:

            If Tom is older than Jenny then Tom is in age between Jenny and Lucy.

 But there is a simple way, Tarski-style, to do away with this limitation.  When Tarski introduced his style of semantics he gave each sentence as its semantic value the set of infinite sequences that satisfy that sentence. 

Above we took terms to stand for sets of things in the universe of discourse.  Now we can take them to stand for sets of countably infinite sequences of things in that universe.  For example, the predicate “is older than”  we take to stand, not for a set of couples, but for the set OLDER of infinite sequences s whose first element is older than its second element.  

We represent any finite sequence t by the set of infinite sequences of which t is the initial segment.   The notation <a, b> now stands  not for the ordered pair whose first and second members are a and b respectively, but for the set of all infinite sequences whose first and second member are a, b respectively.

The predicate “is in age between … and —” we take to stand for the set BETWEEN of infinite sequences whose first member is in age between its second and third member.   So the intersection of OLDER and BETWEEN is the set of sequences u such that the first element is older than the second, and the third element is someone older than both of them.  This intersection can be the extension of a predicate P2 and if Q3 has BETWEEN as its extension then P2 ⊆ Q3is true.

But this is a minor point.  There are always different, equally good, ways of doing things.  The important moral of Bacon’s article is that it is not right to say that our contemporary logic had to replace the deficient logic of the tradition.  Rather, the innovations that made our logic possible would equally improve the traditional logic, to precisely the same degree of adequacy.

REFERENCES

Bacon, John (1982) “First-Order Logic Based on Inclusion and Abstraction”. The Journal of Symbolic Logic 47: 793-808. 

Hilbert logics (2): Quine, quantifiers, and modalities

Thesis: all our most familiar logics, both sentential and quantificational, are Hilbert logics.

In Henkin’s paper (cited in the preceding post) his main target was not sentential but predicate logic. Given that the proof of the Deduction Theorem hinges on Modus Ponens being the sole rule of inference, there is an obvious question. Isn’t

Universal Generalization. from ⊢Fa to infer ⊢(x)Fx

an indispensable rule as well?

Moreover, Henkin indicates that his topic here is not just classical and intuitionistic quantification theory, but applies to quantified modal logic. At that time the concept of a normal modal logic had not yet been introduced. The main modal logics were Lewis and Langford’s S1 through S5, and in retrospect we can say that of these only S4 and S5 were normal. But as typically formulated now, the normal modal logics have a rule that is similar to Universal Generalization, namely

Necessitation. from ⊢A to infer ⊢□A

It is important, and easy to see, that these rules are quite different from Modus Ponens, which says

from A and A ⊃ B to infer B

or, using the deducibility symbol,

A, A ⊃ B ⊢ B

Universal Generalization and Necessitation do not provide inferences from premises to conclusions. Instead, what they do, in effect, is to add lots to the stock of axioms, that is, to the lines in a deduction that do not need to be inferred from previous lines.

It is in fact possible in both cases to have a formulation that is a Hilbert logic, and here I would like to explore one way in which that can be shown.

Quantifier logic a la Quine

For quantificational logic this was made this beautifully clear by Quine in his Mathematical Logic (revised edition 1951). His system of quantifier logic with identity, called ML, does not have the rule of Universal Generalization, and Modus Ponens is its only rule of inference. But he introduced a more nuanced notion of axiom schemata.

First he defines the notion of closure: if A is a well-formed formula which has in it free variables x, y, z, … then the closure of A is the statement which results when universal quantifiers are prefixed to A to bind those variables. So the closure of A looks like this: (x)(y)(z) …A.

Each axiom schema then defines a large class of statements, which are the closures of instances of the displayed form. For example for the class he calls C he displays the form

A ⊃ (x)A, where A is a formula in which x is not a free variable,

and C is the class of all closures of well-formed formulas that have this form. Examples would be (y)(Fy ⊃ (x)Fy), (z)(y)(Rzy ⊃ (x)Rzy), and so forth.

It is clear then that no axiom, and hence no theorem, has free variables in it. Quine’s language did not have individual constants. So it is not even possible to formulate a non-trivial version of Universal Generalization for ML itself. But more to the point, if individual constants are added, we have a choice, and for each choice we arrive at a complete quantificational logic without adding the Universal Generalization rule. If we add the axiom schema

(Ey)(y = a)

the result is the familiar classical predicate logic. Intuitively, each individual constant is the name of a real thing. If we do not add anything then the result is free logic. In that logic, again intuitively, the only existence assumption built it (as it was for Quine) is that there is something rather than nothing. But the individual constants can be non-referring terms, like our “Pegasus”.

In both cases it is provable as a meta-theorem that if ⊢Fa then ⊢(x)Fx. The need for the rule of Universal Generalization has been neatly by-passed by Quine’s tactic.

Modal logic

So how does it stand with the modal logics? Ruth Barcan Marcus wrote the seminal papers on quantified modal logic in the years 1946-1953. She proved the usual Deduction Theorem for material implication for S4 and S5, as formulated by Lewis and Langford, and showed that it could not be proved for S1 or S2.

In our present context, where the family of normal modal logics has a standard formulation, the rule Necessitation plays a salient role. Can Quine’s tactic be implemented here, mutatis mutandis?

The weakest normal logic is system K, formulated as follows with one axiom schema and three rules:

R0. If p is a theorem of classical propositional logic then ⊢ p

R1. p, p ⊃ q ⊢ q

R2. If ⊢ p then ⊢ p

A1. ⊢ (p ⊃q) ⊃ (□p ⊃ □q)

Only R1, modus ponens, is an ordinary rule of inference. Rule R0 can be replaced by the axiom schemata of a Hilbert logic formulation of sentential logic. But R2 is Necessitation.

Let’s adapt Quine’s tactic as follows. If A is a formula then call the necessitations of A all formulas that consist of A preceded by zero or more symbols □. And introduce the more nuanced notion of the use of schemata as follows: each axiom schema introduces a large class of axioms, namely all the necessitations of instances of the displayed form. So for example the schemata that can replace R0 include the form (p ⊃ p), and this means that the axioms include all sentences of form (p ⊃ p), □(p ⊃ p), □□(p⊃p), …, and do forth.

Lets say that K* is the modal logic which is like K except for lacking rule R2, but with the axiom schemata understood in this new way. Then it is easy to prove that K* and K have the same theorems (see Appendix). And K* is a Hilbert logic, that is, a Hilbert logic formulation of K.

The same can be done, in the same way, for the other normal modal logics.So, it follows from this that Henkin was quite right, if we read him anachronistically as referring to the normal modal logics: the Deduction Theorem is provable for all of them.

Conclusion Both the normal modal logics and quantificational logics (classical, normal modal, and intuitionistic) are Hilbert logics.

Historical note. Ruth Barcan Marcus who pioneered quantified modal logic, proved the Deduction Theorem for S4 and S5, and showed that it could not be proved for S1 or S2 (Journal of Symbolic Logic 18 (1953): 234-236). For the completeness of ML with names added as free logic, van Fraassen (Zeitschr. Math. Logic und Grundl. der Math. 12 (1966): 219-234).

APPENDIX

K* and K have precisely the same theorems. The proof is by induction.

Suppose A is a theorem of K; then there is a proof S = S(1), …., S(n) in K which has A as its last line. Change this proof into the sequence T = T(1), …, T(k), … , T(n) by moving the axioms that appear in S to the beginning, though kept in the same order they had in S: these are the lines T(1) …, T(k). The lines T(k+1), … , T(n) are the remaining lines of S in the same order in which they appeared in S.

T is also a proof of A in K, for the axioms need no justification, and if another line of S followed from preceding lines by modus ponens, that same line appearing in T follows from lines that precede it by modus ponens as well.

Claim: There is a proof in K* of □A.

Proof.

Each of □T(i), for in = 1, …, k is an axiom, for T(i) is a necessitation of axiom schema A1, and therefore so is □T(i).

Hypothesis of induction: for k < m ≤ n, and for all j < m, there is a proof of □T(j) in K*.

In S the line S(c) which appears as T(j) in T came from preceding lines S(a) and S(b) by modus ponens, so S(b) was [S(a) ⊃ S(c)]. Thus by hypothesis there are also proofs of □S(a) and □[S(a) ⊃ S(c)]. From these, by an instance of axiom A1. and two applications of modus ponens, □S(c) follows. That conclusion is the same as □T(j).

Therefore, by induction, there is a proof in K* of □T(i), for 1 ≤ i ≤ n; hence of □T(n), which is □A.