Propositional Calculus

Here are some notes on the formal system for Propositional Calculus (PC) that is discussed in Chapter VII of GEB.

Interpretation

Here I discuss the interpretation of the PC system. There are several concepts that are useful to introduce:

Interpretation:

An interpretation of a set of formulas is an assignment of truth values to each of the atoms that appear in the formulas. The truth values of the formulas are then determined recursively using the following rules:

  1. "~x" is true iff "x" is false.
  2. "(x^y)" is true iff "x" and "y" are true.
  3. "(x|y)" is true iff "x" or "y" is true.
  4. "(x>y)" is true iff "x" is false or "y" is true.

For a set of formulas with n distinct atoms there are 2n possible interpretations.

Model:

A model for a set of formulas is an interpretation for which all the formulas in the set are true. For example, consider the set {"(P>Q)", "Q"}. As an example of a model for this set, consider an interpretation in which "P" is false and "Q" is true.

Tautology:

A tautology is a formula that is true under every interpretation. For example, the formula "(P|~P)" is a tautology.

Contradiction:

A contradiction is a formula that is false under every interpretation. For example, the formula "(P^~P)" is a contradiction.

The theorems of PC are all tautologies, so every interpretation is a model for the set PC-theorems.

Hofstadter does not introduce the notion of a tautology, and for this reason some of the statements made in chapter VII could perhaps be misinterpreted. For example:

"This system--the Propositional Calculus--steps neatly from truth to truth, carefully avoiding all falsities..." (page 187)
Unless a formula is a tautology or a contradiction, it is only true or false relative to a given interpretation. Thus, it is not the case that the PC system "avoids all falsities"; in fact, what it avoids is all non-tautologies. Hofstadter does, however, clarify this issue later on:
"...And that is the key idea of the Propositional Calculus: it produces theorems which, when semi-interpreted, are seen to be 'universally true semisentences', by which is meant that no matter how you complete the interpretation, the final result will be a true statement." (page 189)

Properties of the PC system

PC is semantically complete with respect to tautologies:

If a formula is a tautology, then it is a theorem.

PC is syntactically incomplete:

It is not the case that for every formula "x", either "x" or "~x" is a theorem. In other words, there are undecidable formulas. Some examples of undecidable formulas are "P", "~Q", "(P^Q)".

PC is syntactically consistent:

There is no formula "x" such that both "x" and "~x" are theorems.

PC is semantically consistent:

The set PC-theorems has at least one model (in fact, every interpretation is a model for the set PC-theorems).

PC is not categorical:

The set PC-theorems has more than one model (in fact, every interpretation is a model for the set PC-theorems).

PC is decidable:

There is an effective procedure that can decide, for any formula "x", whether or not "x" is a theorem.

PC has redundant rules of inference:

The rules of inference are not independent of one another.

PC is semantically complete

PC is semantically complete; that is, all tautologies are theorems.

To prove this, I will show that every theorem of L1 is also a theorem of PC, where L1 is a system known to be semantically complete (the proof that L1 is complete is given in [Mendelson, 1987]).

The axiom schemes for system L1 are

A1: "(A>(B>A))",

A2: "((A>(B>C))>((A>B)>(A>C)))",

A3: "((~B>~A)>((~B>A)>B))",

where "A", "B", and "C" are arbitrary formulas. The only rule of inference for L1 is Modus Ponens (MP), which is equivalent to Hofstadter's rule of detachment:
MP: If "A" and "(A>B)" are theorems, then "B" is a theorem.
Proof of A1: 
(1)  [                           push
(2)    A                         premise
(3)    [                         push
(4)      B                       premise
(5)      A                       carry-over of line 2
(6)    ]                         pop
(7)    (B>A)                     fantasy
(8)  ]                           pop
(9)  (A>(B>A))                   fantasy
Proof of A2: 
(1)   [                           push
(2)     (A>(B>C))                 premise
(3)     [                         push
(4)       (A>B)                   premise
(5)       [                       push
(6)         A                     premise
(7)         (A>(B>C))             carry-over of line 2
(8)         (B>C)                 detachment (lines 6 and 7)
(9)         (A>B)                 carry-over of line 4
(10)        B                     detachment (lines 6 and 9)
(11)        C                     detachment (lines 8 and 10)
(12)      ]                       pop
(13)       (A>C)                  fantasy
(14)    ]                         pop
(15)    ((A>B)>(A>C))             fantasy
(16)  ]                           pop
(17)  ((A>(B>C))>((A>B)>(A>C)))   fantasy
Proof of A3: 
(1)   [                           push
(2)     (~B>~A)                   premise
(3)     [                         push
(4)       (~B>A)                  premise
(5)       [                       push
(6)         ~B                    premise
(7)         (~B>A)                carry-over of line 4
(8)         (~B>~A)               carry-over of line 2
(9)         A                     detachment (lines 6 and 7)
(10)        ~A                    detachment (lines 6 and 8)
(11)        ~~A                   double-tilde (line 9)
(12)        (~A^~~A)              joining (lines 10 and 11)
(13)        ~(A|~A)               De Morgan
(14)      ]                       pop
(15)      (~B>~(A|~A))            fantasy
(16)      ((A|~A)>B)              contrapositive
(17)      [                       push
(18)        ~A                    premise
(19)      ]                       pop
(20)      (~A>~A)                 fantasy
(21)      (A|~A)                  switcheroo
(22)      B                       detachment (lines 16 and 20)
(23)    ]                         pop
(24)    ((~B>A)>B)                fantasy
(25)  ]                           pop
(26)  ((~B>~A)>((~B>A)>B))        fantasy
Thus, every theorem of L1 is theorem of PC.

PC has redundant rules of inference

Note that in the proof that PC is semantically complete, the separation rule was never used. Also, the double-tilde rule was only used to add '~~', not to remove it. We can show that the separation rule is not independent by deriving it from the other rules:

Proof of "((A^B)>A)": 

1.   [                           push
2.     ~A                        premise
3.     [                         push
4.       B                       premise
5.       ~A                      carry-over of line 2
6.     ]                         pop
7.     (B>~A)                    fantasy
8.     (~~A>~B)                  contrapositive
9.   ]                           pop    
10.  (~A>(~~A>~B))               fantasy
11.  (~(~~A>~B)>~~A)             contrapositive
12.  (~(~A|~B)>~~A)              switcheroo
13.  ((~~A^~~B)>~~A)             De Morgan
14.  ((A^B)>A)                   double-tilde

PC is syntactically consistent

PC is syntactically consistent; that is, there is no formula "x" such that both "x" and "~x" are theorems.

To show this, we first note that the axioms are all tautologies, and the rules of inference produce tautologies from tautologies. Thus, all the theorems of PC are tautologies. But it is impossible for both "x" and "~x" to both be tautologies, since if one is a tautology, the other is a contradiction. Thus, it is impossible for "x" and "~x" to both be theorems.

PC is decidable

PC is decidable; that is, there is an effective procedure for determining if an arbitrary string in PC-formulas is or is not a member of PC-theorems.

The decision procedure works as follows. Suppose we are given a formula "x". If there are n distinct atoms of "x", then there are 2n possible interpretations. Interpret "x" under each of these interpretations. If "x" is true under every interpretation then it is a tautology, and thus belongs to PC-theorems, otherwise it is not a tautology, and thus does not belong to PC-theorems.

I have written a computer program that implements this decision procedure.

Syntax

Here I summarize the syntax of the PC system.

Well-formed strings

There is a set PC-formulas of well-formed strings, which are defined recursively via the following rules:

Atoms:

The letters "P", "Q", and "R" are atoms. If "x" is an atom, then so is "x'". All atoms are well-formed.

Formation Rules:

If strings "x" and "y" are well-formed, then the strings "~x", "(x^y)", "(x|y)", and "(x>y)" are also well-formed.

Rules of production

There is a subset PC-theorems of PC-formulas, which is defined recursively via the following rules:

Joining Rule:

If "x" and "y" are theorems, then "(x^y)" is a theorem.

Separation Rule:

If "(x^y)" is a theorem, then both "x" and "y" are theorems.

Double-tilde Rule:

The string "~~" can be deleted from any theorem. It can also be inserted into any theorem, provided that the resulting string is itself well-formed.

Fantasy Rule:

If "y" can be derived when "x" is assumed to be a theorem, then "(x>y)" is a theorem.

Carry-over Rule:

Inside a fantasy, any theorem from "reality" one level higher can be brought in and used.

Rule of Detachment:

If "x" and "(x>y)" are both theorems, then "y" is a theorem.

Contrapositive Rule:

The formulas "(x>y)" and "(~y>~x)" are interchangeable.

De Morgan's Rule:

The formulas "(~x^~y)" and "~(x|y)" are interchangeable.

Switcheroo Rule:

The formulas "(x|y)" and "(~x>y)" are interchangeable.

Bibliography

Medelson, E., Introduction to Mathematical Logic, third edition. Pacific Grove, California: Wadsworth & Brooks/Cole, 1987.

David Boozer
Last modified 25 January 2009
boozer at caltech dot edu