The Gateway: Foundations and Logical Architecture
The Gateway: Foundations and Logical Architecture
The journey into advanced mathematical concepts demands a careful examination of the ground upon which we build. Just as an expedition requires establishing base camps and supply lines before ascending peaks, the study of higher mathematics necessitates a thorough grounding in the logical architecture that supports the entire edifice. This chapter serves as that essential foundation—a systematic treatment of the formal systems, set-theoretic underpinnings, and structural frameworks that mathematicians have developed over centuries to codify reasoning and organize mathematical knowledge. The concepts introduced here will recur throughout this expedition, providing the vocabulary and conceptual toolkit necessary for exploring the realms that follow.
The Architecture of Formal Logic
Propositional Logic: The Language of Truth Values
At the most fundamental level, mathematical reasoning operates through statements that can be classified as true or false. Propositional logic provides the formal framework for manipulating such statements, treating them as atomic units whose internal structure is abstracted away for purposes of logical analysis.
Definition (Propositional Language). A propositional language $\mathcal{L}_P$ consists of:
- A countably infinite set $\text{Var} = \{p_0, p_1, p_2, \ldots\}$ of propositional variables
- Propositional connectives: $\neg$ (negation), $\wedge$ (conjunction), $\vee$ (disjunction), $\rightarrow$ (implication), $\leftrightarrow$ (biconditional)
- Punctuation: parentheses $(,)$
The syntax of propositional logic is defined recursively:
Definition (Well-Formed Formula). The set $\text{WFF}(\mathcal{L}_P)$ of well-formed formulas is the smallest set satisfying:
1. Every propositional variable $p \in \text{Var}$ is in $\text{WFF}(\mathcal{L}_P)$ 2. If $\varphi \in \text{WFF}(\mathcal{L}_P)$, then $\neg\varphi \in \text{WFF}(\mathcal{L}_P)$ 3. If $\varphi, \psi \in \text{WFF}(\mathcal{L}_P)$, then $(\varphi \circ \psi) \in \text{WFF}(\mathcal{L}_P)$ for each binary connective $\circ \in \{\wedge, \vee, \rightarrow, \leftrightarrow\}$
The semantics of propositional logic are given by truth valuations—functions assigning truth values to propositional variables and propagating these values through the connectives according to truth tables.
Definition (Truth Valuation). A valuation is a function $v: \text{Var} \to \{T, F\}$ extended to all well-formed formulas by:
- $v(\neg\varphi) = T$ if and only if $v(\varphi) = F$
- $v(\varphi \wedge \psi) = T$ if and only if $v(\varphi) = T$ and $v(\psi) = T$
- $v(\varphi \vee \psi) = T$ if and only if $v(\varphi) = T$ or $v(\psi) = T$ (inclusive or)
- $v(\varphi \to \psi) = T$ if and only if $v(\varphi) = F$ or $v(\psi) = T$
- $v(\varphi \leftrightarrow \psi) = T$ if and only if $v(\varphi) = v(\psi)$
These definitions yield the familiar truth tables:
| $\varphi$ | $\psi$ | $\neg\varphi$ | $\varphi \wedge \psi$ | $\varphi \vee \psi$ | $\varphi \to \psi$ | $\varphi \leftrightarrow \psi$ | |:---------:|:------:|:-------------:|:--------------------:|:-------------------:|:------------------:|:-----------------------------:| | T | T | F | T | T | T | T | | T | F | F | F | T | F | F | | F | T | T | F | T | T | F | | F | F | T | F | F | T | T |
Definition (Tautology, Contradiction, Contingent Formula). A formula $\varphi$ is a:
- **Tautology** if $v(\varphi) = T$ for every valuation $v$
- **Contradiction** if $v(\varphi) = F$ for every valuation $v$
- **Contingent** if it is neither a tautology nor a contradiction
The notion of logical consequence emerges naturally from these semantic definitions.
Definition (Logical Consequence). A formula $\psi$ is a logical consequence of a set of formulas $\Gamma$, written $\Gamma \models \psi$, if every valuation that makes all formulas in $\Gamma$ true also makes $\psi$ true. When $\Gamma = \emptyset$, we write $\models \psi$, indicating that $\psi$ is a tautology.
Proof Systems for Propositional Logic
While semantic definitions clarify the meaning of logical consequence, proof systems provide syntactic mechanisms for deriving conclusions from premises. The three principal approaches—Hilbert systems, natural deduction, and sequent calculus—each offer distinct advantages.
Hilbert Systems employ a minimal set of axiom schemas combined with a detachment rule (modus ponens):
Axiom Schemas (Standard Hilbert System): 1. $\varphi \to (\psi \to \varphi)$ 2. $(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))$ 3. $(\neg\varphi \to \neg\psi) \to (\psi \to \varphi)$
Rule: From $\varphi$ and $\varphi \to \psi$, infer $\psi$.
A proof from premises $\Gamma$ is a finite sequence of formulas where each formula is either a premise, an axiom, or follows from previous formulas by modus ponens. When a proof exists from $\Gamma$ to $\varphi$, we write $\Gamma \vdash \varphi$.
Natural Deduction provides a more intuitive proof system organized around introduction and elimination rules for each connective.
| Connective | Introduction | Elimination | |------------|--------------|-------------| | $\wedge$ | From $\varphi$ and $\psi$, infer $\varphi \wedge \psi$ | From $\varphi \wedge \psi$, infer $\varphi$ (and $\psi$) | | $\vee$ | From $\varphi$, infer $\varphi \vee \psi$ | From $\varphi \vee \psi$, $\varphi \to \chi$, and $\psi \to \chi$, infer $\chi$ | | $\to$ | Assume $\varphi$, derive $\psi$, discharge assumption to infer $\varphi \to \psi$ | From $\varphi$ and $\varphi \to \psi$, infer $\psi$ | | $\neg$ | Assume $\varphi$, derive $\bot$, discharge assumption to infer $\neg\varphi$ | From $\neg\neg\varphi$, infer $\varphi$ (or other strategies) |
The sequent calculus, developed by Gerhard Gentzen, organizes proofs as sequences of formulas (sequents) of the form $\Gamma \Rightarrow \Delta$, read as "the conjunction of $\Gamma$ entails the disjunction of $\Delta$."
The fundamental soundness and completeness theorems establish the correspondence between these syntactic proof systems and the semantic notion of logical consequence.
Theorem (Soundness of Hilbert System). If $\Gamma \vdash \varphi$, then $\Gamma \models \varphi$.
Theorem (Completeness of Hilbert System). If $\Gamma \models \varphi$, then $\Gamma \vdash \varphi$.
The proofs of these theorems represent milestones in mathematical logic. The soundness proof proceeds by induction on the structure of proofs, verifying that axioms are tautologies and that modus ponens preserves semantic entailment. The completeness proof, originally due to Gödel, typically employs either the Henkin construction or a canonical model argument.
From Propositions to Predicates: First-Order Logic
Propositional logic, while valuable for studying logical relationships, cannot capture the internal structure of statements involving individuals and their properties. First-order predicate logic extends the expressive power to encompass quantification over individuals.
Definition (First-Order Language). A first-order language $\mathcal{L}$ consists of:
- Logical symbols: variables $x_0, x_1, x_2, \ldots$; connectives $\neg, \wedge, \vee, \to, \leftrightarrow$; quantifiers $\forall, \exists$; equality $=$; parentheses
- Non-logical symbols: function symbols (each with an arity), relation/predicate symbols (each with an arity), constant symbols
- An arity is a natural number specifying the number of arguments
Definition (Term). Terms are defined recur