Introduction to Propositional Calculus
In this chapter, Hofstadter explains a formal system which he calls propositional calculus (you may know about it if you’ve studied logic; it also goes by the name propositional logic).
In propositional calculus, the symbol ‘^’ is meant to be interpreted as the word ‘and’. The symbol ‘˅’ is meant to be interpreted as the word ‘or’ (the inclusive ‘or’, not the exclusive ‘or’). The symbol ‘~’ is meant to be interpreted as the word ‘not’. The symbols ‘<‘ and ‘>’ are meant to be interpreted as parentheses. The symbol ‘⊃’ is meant to be interpreted as the phrase “if … then …”.
The Rules of Propositional Calculus
Hofstadter lays out the rules of propositional calculus (which are isomorphic with the standard rules of logic). In all of these rules, x and y are assumed to be well-formed strings.
Joining Rule: If x and y are theorems, then <x^y> is a theorem.
Separation Rule: If <x^y> is a theorem, then x and y are theorems.
Double-Tilde Rule: The string ~~ can be deleted from or inserted into any theorem.
Detachment Rule: If x and <x⊃y> are theorems, then y is a theorem. (This rule often goes by the more common name: Modus Ponens).
Contrapositive Rule: <x⊃y> and <~x⊃~y> are interchangeable.
De Morgan’s Rule: <~x^~y> and ~<x˅y> are interchangeable.
Switcheroo Rule: <x˅y> and <~x⊃y> are interchangeable.
The Fantasy Rule
You may have noticed that so far, no axioms have been provided. This is because propositional calculus has no axioms; it is solely composed of rules. How can any theorems be derived if there are no axioms?
Hofstadter provides a rule called the Fantasy Rule, which produces theorems without taking any input. Thus, no axioms are needed. The Fantasy Rule is provided below:
Fantasy Rule: If y can be derived when x is assumed to be a theorem, then <x⊃y> is a theorem.
In derivations of theorems involving the Fantasy Rule, the steps that are performed while in the fantasy are by convention enclosed in square brackets: ‘[‘ and ‘]’.
While operating inside a fantasy, the user can choose to operate in another fantasy and, from there, yet another, through recursion. Hofstadter presents a rule here to govern how theorems can be used in recursive fantasies:
Carry-Over Rule: Inside a fantasy, any theorem from reality or a ‘higher’ fantasy can be used.
Cognitive Century 