Propositional Calculus (GEB)

The Propositional Calculus as presented in Gödel, Escher, Bach by Douglas Hofstadter (Ch. VII). A formal system with no axioms, using a fantasy rule as its central device — essentially a natural deduction system disguised as a typographical game.

1. Alphabet

• Variables: $P,Q,R$ (and $P^{\prime },Q^{\prime },R^{\prime },P^{″}$, etc.)
• Connective symbols: $\sim$ (not), $\wedge$ (and), $\vee$ (or), $\supset$ (implies)
• Punctuation: $<$ and $>$

2. Formation Rules (Syntax)

A well-formed formula (WFF) is defined recursively:

1. Atoms: $P,Q,R$ (and any primed version) are atoms, and every atom is a WFF.
2. Negation: If $x$ is a WFF, then $\sim x$ is a WFF.
3. Conjunction: If $x$ and $y$ are WFFs, then $<x\wedge y>$ is a WFF.
4. Disjunction: If $x$ and $y$ are WFFs, then $<x\vee y>$ is a WFF.
5. Implication: If $x$ and $y$ are WFFs, then $<x\supset y>$ is a WFF.

• Examples of WFFs: $P$, $\sim Q$, $<<P\wedge Q>\supset P>$, $<P\vee \sim P>$
• Examples of non-WFFs: $P\wedge Q$ (missing angle brackets), $<P\wedge Q\wedge R>$ (binary connective only joins two), $<<<P$ (unbalanced brackets)

3. Axioms

There are none. The system has no axioms — all theorems are generated by the inference rules alone.

4. Rules of Inference

Joining Rule

From $x$ and $y$ (both theorems), deduce $<x\wedge y>$.
Analogous to $\wedge$-introduction.

Separation Rule

From $<x\wedge y>$ (a theorem), deduce $x$ and $y$ separately.
Analogous to $\wedge$-elimination.

Double-Tilde Rule

$\sim \sim x$ and $x$ are interchangeable — you may replace one by the other anywhere.
Analogous to double-negation elimination/introduction.

Fantasy Rule (the "regla fantasiosa")

You may start a fantasy (subproof) by assuming any WFF as a premise. Within the fantasy, you apply all the rules (including other fantasy rules). When the fantasy is closed, you obtain $<x\supset y>$, where $x$ is the premise and $y$ is any theorem derived inside.

This is how implication is introduced — analogous to $\supset$-introduction or the Deduction Theorem.

Carry-Over Rule

Any theorem proved outside a fantasy may be carried into the fantasy and used freely.

Rule of Detachment (Modus Ponens)

From $<x\supset y>$ and $x$, deduce $y$.
Analogous to $\supset$-elimination.

5. Key properties

• Soundness: Every theorem of this system is a tautology in classical logic.
• Completeness: Every tautology is a theorem — the system can prove all logical truths.
• Semantic independence: The symbols have no intrinsic meaning; they are manipulated purely typographically. The semantics (truth tables, models) is an interpretation superimposed from outside.

6. Comparison with MIU

References

• MIU-system
• formal system
• Godel theorems