論理

Chapter I · Of Propositions

Propositional Logic

The most elementary chamber in the great library of logic concerns itself with whole declarative sentences — the propositions — and the connectives that bind them together into compound assertions.

A proposition is a statement that admits of being either true or false, and nothing else. From this austere starting point one builds a complete deductive calculus by introducing five connectives: negation (¬), conjunction (∧), disjunction (∨), implication (→), and biconditional (↔).¹

With these tools a remarkable architecture emerges. Modus ponens permits one to pass from P → Q and P to Q; the rules of inference, when carefully chosen, yield a system that is both sound and complete with respect to the truth-functional semantics of the propositional connectives.²

1.  P → Q                assumption
2.  P                         assumption
3.  Q                         1, 2, modus ponens
                    

The completeness theorem of propositional logic, first established by Post and refined by countless hands since, assures us that every valid argument has a formal proof and every formal proof corresponds to a valid argument. It is the first miracle in the discipline.

Chapter II · Of Quantifiers

Predicate Logic

Where propositional logic treats sentences as atomic, predicate logic dissects them — revealing within each declarative sentence a structure of terms, predicates, and the binding power of quantifiers.

The universal quantifier ∀ ranges over a domain of discourse, asserting that some property holds of every element. Its dual, the existential quantifier ∃, asserts that the property holds of at least one element. Together they articulate statements of striking subtlety.¹

∀x (Human(x) → Mortal(x))
Human(socrates)
∴ Mortal(socrates)
                    

First-order logic, the most studied predicate calculus, is also sound and complete (Gödel, 1929) but no longer decidable (Church, Turing, 1936). The price of expressive power is the loss of an effective decision procedure — a tension that runs through every subsequent chapter of this codex.²

Higher-order extensions allow quantification over predicates themselves and over sets, opening vistas of expressive power at the cost of further metatheoretic complications.

Chapter III · Of Necessity & Possibility

Modal Logic

Modal logic enriches the predicate calculus with two further operators — □ for necessity and ◊ for possibility — and so admits propositions about how things might be, not merely how they are.

The semantics, due to Kripke, interprets these operators over a frame of possible worlds connected by an accessibility relation. □P holds at a world w if P holds at every world accessible from w; ◊P holds if P holds at some accessible world.¹

□P → P                    axiom T (reflexive)
□P → □□P                axiom 4 (transitive)
◊P → □◊P                axiom 5 (Euclidean)
                    

Different choices of accessibility relation yield different modal systems: K, T, S4, S5, each with its own characteristic axioms and theorems. The plurality of systems is itself a philosophical statement — modality admits no single answer.²

Tense logic, deontic logic, and epistemic logic are all modal systems with the operators reinterpreted: time, obligation, knowledge. The framework is one of remarkable generality.

Chapter IV · Of Constructive Proof

Intuitionistic Logic

At the heart of the codex lies a quiet heresy: the rejection of the law of excluded middle. Brouwer's intuitionism insists that a mathematical statement is true only when one possesses a construction attesting to its truth.

In classical logic, P ∨ ¬P is a tautology — one of the two must hold, even if we cannot say which. Intuitionistic logic disallows this move. To assert P ∨ ¬P one must either produce a proof of P or produce a proof of ¬P; mere appeal to the completeness of truth is insufficient.¹

¬¬P              does NOT entail P
P ∨ ¬P           not a theorem
P → ¬¬P    is a theorem
                    

The Curry–Howard correspondence reveals an astonishing identity: intuitionistic proofs are programs. Every constructive proof of A → B is a function transforming proofs of A into proofs of B. Thus logic, computation, and category theory meet in a single edifice.²

Intuitionistic logic provides the foundation for type theory and for the proof assistants that increasingly verify the deepest results of mathematics. The constructivist scruple has become a practical instrument.