Layer 0 — Logic: The Foundation of Reasoning¶

Core Idea¶

Logic is the language and rulebook of valid reasoning. It answers two questions:

1. What counts as a well-formed statement? (syntax)
2. When does a statement follow from other statements? (semantics and proof theory)

Every mathematical proof — in every layer — is ultimately a chain of logical deductions. Logic does not tell us what to study; it tells us how to be certain about whatever we study.

Key Structures¶

Propositional Logic¶

Think of propositional logic as the mathematics of true/false reasoning. You start with simple statements that are either true or false — "it is raining," "I have an umbrella" — and combine them with words like "and," "or," "not," and "if...then." The formal symbols below are just shorthand for these everyday reasoning patterns.

The simplest formal system. Atomic propositions \(P, Q, R, \ldots\) are combined with connectives:

A tautology is a formula true under every truth-value assignment. The canonical example:

A formula is satisfiable if it is true under some assignment. The distinction between tautology and satisfiability is the seed of computational complexity theory (SAT is NP-complete).

Predicate Logic (First-Order Logic)¶

Propositional logic can only talk about whole statements being true or false. But we often need to say things like "every even number greater than 2 is the sum of two primes" or "there exists a solution to this equation." Predicate logic adds the ability to talk about individual objects and make claims about all or some of them.

Propositional logic cannot express "for all \(x\)" or "there exists an \(x\) such that." Predicate logic adds:

• Variables: \(x, y, z, \ldots\)
• Predicates: \(P(x)\), \(R(x, y)\)
• Quantifiers:
  • Universal: \(\forall x \, P(x)\) — "for every \(x\), \(P(x)\) holds"
  • Existential: \(\exists x \, P(x)\) — "there is some \(x\) for which \(P(x)\) holds"
• Functions and constants: \(f(x)\), \(c\)

The expressive leap is enormous. Predicate logic can formalize:

This is the \(\varepsilon\)-\(\delta\) definition of continuity — a statement in Layer 5 (Analysis) that is written in the language of Layer 0.

Proof Systems¶

A proof system is a set of rules for deriving conclusions from premises. Two major frameworks:

Natural Deduction (Gentzen, 1935): Rules are introduction and elimination rules for each connective. For example, \(\land\)-introduction says: from \(P\) and \(Q\), infer \(P \land Q\).

Sequent Calculus (Gentzen, 1935): Proofs manipulate sequents \(\Gamma \vdash \Delta\), meaning "from the assumptions \(\Gamma\), at least one of \(\Delta\) follows." The cut-elimination theorem shows that any proof can be transformed into one without "detours" — a foundational result for proof theory.

Model Theory¶

Model theory studies the relationship between formal languages and the structures that satisfy them.

A model (or structure) for a first-order language assigns:

• A non-empty domain (universe)
• Interpretations for each predicate, function, and constant symbol

A sentence \(\varphi\) is true in a model \(\mathcal{M}\) (written \(\mathcal{M} \models \varphi\)) if it holds under the model's interpretation. Key results:

Computability Theory¶

Turing machines (1936) formalize the intuitive notion of "mechanical computation." A Turing machine reads and writes symbols on an infinite tape according to a finite table of rules.

The halting problem is the first concrete example of an undecidable problem:

This is the computability-theoretic cousin of Gödel's incompleteness — both arise from self-referential diagonal arguments.

Historical Trigger¶

timeline
    title The Evolution of Formal Logic
    ~350 BCE : Aristotle's syllogistic logic
              : First systematic study of valid argument forms
    1847 : Boole's algebraic logic
         : Logic as algebraic computation
    1879 : Frege's Begriffsschrift
         : First complete system of predicate logic
    1901 : Russell's Paradox
         : Naive comprehension is inconsistent
    1910-13 : Principia Mathematica
             : Russell & Whitehead attempt a complete foundation
    1929 : Gödel's Completeness Theorem
         : First-order logic is complete
    1931 : Gödel's Incompleteness Theorems
         : No consistent system can prove all truths of arithmetic
    1936 : Church & Turing
         : Undecidability and the formalization of computation

The arc is: informal reasoning → formal syntax → a paradox forces axiomatization → the axiomatized system turns out to have inherent limits.

Key Proofs¶

Soundness of Propositional Logic Foundational¶

Why it matters: Soundness guarantees that the proof system never lies. Every theorem it produces is genuinely true. Without soundness, proofs would be meaningless symbol-pushing.

What it unlocks: The soundness of propositional logic is inherited by every system built on top of it. It is the warranty on the entire mathematical supply chain.

Gödel's Completeness Theorem (First-Order Logic) Foundational¶

This is the converse of soundness. Together, soundness and completeness say:

Provability and truth coincide — but only for first-order logic. Higher-order logics sacrifice completeness for expressiveness.

Gödel's First Incompleteness Theorem Insight¶

The Gödel sentence. The core idea is self-reference. Gödel constructs a sentence \(G_F\) that, when decoded, says:

If \(F\) could prove \(G_F\), then \(G_F\) would be false (it claims to be unprovable), contradicting the assumed soundness of \(F\). So \(G_F\) is not provable. But then what \(G_F\) says is true — there really is a true sentence \(F\) cannot prove.

What it means: No single formal system can capture all mathematical truth. There will always be true statements that escape the net. This is not a defect of any particular system — it is an intrinsic feature of sufficiently powerful formal reasoning.

Gödel's Second Incompleteness Theorem Insight¶

Why it matters: You cannot pull yourself up by your own bootstraps. If you want to know that \(F\) is consistent, you must use a stronger system — which then has its own unprovable consistency statement. The chain never terminates.

The Halting Problem and Church-Turing Insight¶

The undecidability of the halting problem (sketched above) is the computational mirror of incompleteness. Both results use diagonal arguments, and both establish inherent limits on formal methods:

Connections¶

Dependencies¶

None. Logic is Layer 0 — it presupposes no mathematical content. (It does presuppose a meta-language and informal reasoning, but these are pre-mathematical.)

Upward Impact¶

Logic is the only layer that every other layer depends on directly.

Worked Example¶

Applications¶

Sources & Further Reading¶

1. Enderton, H. B. A Mathematical Introduction to Logic (2^nd ed., 2001). — Standard undergraduate text covering propositional and predicate logic, completeness, and compactness.
2. Gödel, K. "On Formally Undecidable Propositions" (1931). — The original incompleteness paper. Difficult but historically essential.
3. Turing, A. M. "On Computable Numbers, with an Application to the Entscheidungsproblem" (1936). — Introduces Turing machines and proves the undecidability of the halting problem.
4. Smith, P. An Introduction to Gödel's Theorems (2^nd ed., 2013). — The most accessible modern treatment of incompleteness.
5. Marker, D. Model Theory: An Introduction (2002). — Graduate-level model theory; covers Löwenheim-Skolem and compactness in depth.

title: Glossary! tags: - reference - glossary

Glossary¶

A working reference of essential terms spanning all nine layers of the mathematical hierarchy. Terms are grouped alphabetically; hover-tooltip definitions are provided at the bottom for use across the knowledge base.

A¶

B¶

C¶

D¶

E¶

F¶

G¶

H¶

I¶

L¶

M¶

N¶

P¶

Q¶

R¶

S¶

T¶

U¶

V¶

Z¶