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