The Gate of Logic: Mastering Formal Systems and Set Theory

The shimmering portal before you is not made of stone or metal, but of pure reason. The Sphinx, guardian of the Gate of Logic, does not ask a single riddle—it presents a cascade of paradoxes that threaten to unravel the fabric of mathematics itself. "I am lying," it declares, a statement that is true if and only if it is false. "Consider the set of all sets that do not contain themselves," it challenges, conjuring Russell's paradox. To pass, you must master the formal languages that can precisely express such statements, the axiomatic systems that can consistently manage them, and the proof techniques that can navigate their depths. This chapter is your initiation into that mastery. We will begin with the bedrock of formal systems, ascend through propositional and predicate logic, build the edifice of set theory from the ZFC axioms, construct the very numbers we take for granted, and finally confront the profound limits revealed by Gödel's incompleteness theorems. Along the way, you will practice constructing rigorous proofs, resolving ancient paradoxes, and exploring the frontiers of mathematical logic.

The Architecture of Formal Systems

At the heart of mathematical rigor lies the formal system—a precise, mechanical framework for generating truths. A formal system consists of three components: a formal language (symbols and formation rules), a set of axioms (self-evident starting points), and a set of inference rules (mechanisms for deriving new statements). The power of this abstraction is that it removes ambiguity: every well-formed formula (wff) has an unambiguous syntactic structure, and proofs are finite sequences of formulas where each line follows from previous ones by an inference rule. This is the language in which the Sphinx speaks, and it is our first tool.

Syntax and Semantics: Two Worlds

Crucially, we must distinguish between syntax (the formal manipulation of symbols) and semantics (the assignment of meaning, typically truth values). A formal proof is a syntactic object; it need not refer to any "real" interpretation. Yet, we desire our proofs to yield true statements under intended interpretations. This tension is captured by two fundamental properties:

• **Soundness**: If a formula is provable from the axioms, then it is true in all intended models (i.e., the inference rules preserve truth).
• **Completeness**: If a formula is true in all intended models, then it is provable from the axioms.

For propositional logic, we will see that both hold. For stronger systems, Gödel's theorems will show that completeness fails in a precise sense.

Formal languages are built from an alphabet. For propositional logic, the alphabet includes propositional variables ($p, q, r, \dots$), logical connectives ($\neg, \land, \lor, \rightarrow, \leftrightarrow$), and parentheses. Formation rules define what strings are wffs: e.g., if $\phi$ and $\psi$ are wffs, then $(\neg \phi)$, $(\phi \land \psi)$, etc., are wffs. These rules allow recursive parsing, which is essential for defining proofs.

> Sidebar: Why Formalism? > The late 19th and early 20th centuries saw a crisis in mathematics: intuitive definitions (like "a set is any collection") led to contradictions. Formalism, championed by Hilbert, sought to place mathematics on a secure syntactic foundation, reducing it to symbol manipulation. This chapter's journey is a direct response to that crisis.

Propositional Logic: The Calculus of Truth

Propositional logic (or sentential logic) deals with truth-functional connectives. Its semantics is given by truth tables: each connective is defined by the truth value it outputs for every combination of input truth values. For example, the material conditional $p \rightarrow q$ is false only when $p$ is true and $q$ is false; otherwise true. This often surprises beginners, but it is equivalent to $\neg p \lor q$.

Truth Tables and Logical Equivalences

We can compute the truth value of any complex wff given an assignment of truth values to its atomic variables. Two wffs are logically equivalent if they have identical truth tables for all assignments. Key equivalences include:

• **De Morgan's Laws**: $\neg (p \land q) \equiv \neg p \lor \neg q$, $\neg (p \lor q) \equiv \neg p \land \neg q$
• **Distributive Laws**: $p \land (q \lor r) \equiv (p \land q) \lor (p \land r)$, and dually for $\lor$ over $\land$
• **Double Negation**: $\neg \neg p \equiv p$
• **Implication**: $p \rightarrow q \equiv \neg p \lor q$
• **Contrapositive**: $p \rightarrow q \equiv \neg q \rightarrow \neg p$

These equivalences are not mere curiosities; they are the bread and butter of simplifying logical expressions, a skill essential for designing digital circuits and verifying software conditions.

Functional Completeness and Minimal Connectives

A set of connectives is functionally complete if every truth function can be expressed using only those connectives. The set $\{\neg, \land, \lor\}$ is complete. Remarkably, even a single connective can be complete if it is not monotonic, not self-dual, not linear, and not truth-preserving. Two famous examples are NAND (Sheffer stroke, $p \mid q \equiv \neg (p \land q)$) and NOR (Peirce's arrow, $p \downarrow q \equiv \neg (p \lor q)$). Every other connective can be defined in terms of NAND:

• $\neg p \equiv p \mid p$
• $p \land q \equiv (p \mid q) \mid (p \mid q)$
• $p \lor q \equiv (p \mid p) \mid (q \mid q)$

This demonstrates the economy of logical primitives—a single operation suffices to build all of propositional logic.

Inference Rules and Proof Calculi

To derive conclusions from premises, we need inference rules. The most common are:

• **Modus Ponens (MP)**: From $p$ and $p \rightarrow q$, infer $q$.
• **Modus Tollens (MT)**: From $p \rightarrow q$ and $\neg q$, infer $\neg p$.
• **Hypothetical Syllogism (HS)**: From $p \rightarrow q$ and $q \rightarrow r$, infer $p \rightarrow r$.
• **Disjunctive Syllogism (DS)**: From $p \lor q$ and $\neg p$, infer $q$.
• **Conjunction Introduction (∧I)**: From $p$ and $q$, infer $p \land q$.
• **Conjunction Elimination (∧E)**: From $p \land q$, infer $p$ (or $q$).
• **Disjunction Introduction (∨I)**: From $p$, infer $p \lor q$ (for any $q$).
• **Resolution**: From $p \lor q$ and $\neg p \lor r$, infer $q \lor r$. This rule is the cornerstone of automated theorem proving in propositional logic.

A proof is a finite sequence of wffs where each wff is either an axiom, a premise, or follows from previous wffs by an inference rule. The final wff is the conclusion. To practice, consider the argument: 1. $p \rightarrow q$ 2. $q \rightarrow r$ 3. $\neg r$ Therefore, $\neg p$.

A natural deduction proof: 4. $p \rightarrow r$ (from 1,2 by HS) 5. $\neg p$ (from 4,3 by MT)

This mechanical process is exactly what the Sphinx demands: the ability to manipulate symbols according to rigid rules, leaving no room for intuitive leaps.

Semantic Tableaux and Decision Procedures

While truth tables provide a semantic method for checking validity (an argument is valid iff the conjunction of premises and negation of conclusion is unsatisfiable), they become impractical for many variables (complexity $O(2^n)$). Semantic tableaux (or truth trees) offer a more efficient syntactic method for testing satisfiability. Starting from the assumption that the premises are true and the conclusion false, we systematically break down complex formulas using rules that preserve satisfiability. If we derive a contradiction (a branch contains both $A$ and $\neg A$), the branch closes; if all branches close, the original set is unsatisfiable, hence the argument valid.

For propositional logic, tableaux always terminate, providing a decision procedure. This is not the case for predicate logic, as we will see.

Predicate Logic: Quantifying the World

Propositional logic cannot express the internal structure of statements. Predicate logic (first-order logic) introduces quantifiers