Foundation — flashcards
Everything on this map that touches Foundation: its own shape, its concepts, the statements resting on them, and the lens edges crossing into it.
Theorems 8
State: The Euclidean algorithm terminates.
For positive integers a and b, the remainder sequence is strictly decreasing and non-negative, so it reaches zero after finitely many steps.
derived from st/euclid-terminates by the statement rule
State: √2 is irrational.
Anthyphairesis on a 1 by √2 rectangle never terminates, which is exactly the statement that √2 is not a ratio of integers.
derived from st/sqrt2-irrational by the statement rule
State: Gödel's first incompleteness theorem.
Any consistent, effectively axiomatised theory interpreting arithmetic contains a sentence neither provable nor refutable in it.
derived from st/godel-1 by the statement rule
State: Independence of the continuum hypothesis.
If ZFC is consistent, then neither CH nor its negation is provable from ZFC — Gödel 1940 for one direction, Cohen 1963 for the other.
derived from st/ch-independent by the statement rule
State: Independence of the axiom of choice.
If ZF is consistent, both ZFC and ZF plus the negation of choice are consistent. In Lean, choice is an axiom rather than a theorem, which makes the dependency mechanically visible.
derived from st/ac-independent by the statement rule
State: The Curry–Howard correspondence.
Propositions correspond to types, proofs to terms, and proof normalisation to evaluation. In a dependently typed proof assistant this is not an analogy but the implementation.
derived from st/curry-howard by the statement rule
State: Faulhaber's formula.
The sum of the kth powers of the first n integers is a polynomial in n of degree k+1 whose coefficients are the Bernoulli numbers. The defining system is lower triangular and dense: each Bernoulli number depends on every earlier one.
derived from st/faulhaber by the statement rule
State: Legendre's formula for v_p(n!).
v_p(n!) = Σ_{i≥1} ⌊n/pⁱ⌋, which grows like n/(p−1). So Σ n! converges p-adically for every prime while diverging in every real sense.
derived from st/legendre-formula by the statement rule
Names and dates 8
The Euclidean algorithm terminates — who, and when?
Euclid, c. 300 BC.
derived from st/euclid-terminates by the attribution rule
√2 is irrational — who, and when?
the Pythagorean school, c. 450 BC.
derived from st/sqrt2-irrational by the attribution rule
Gödel's first incompleteness theorem — who, and when?
Kurt Gödel, 1931.
derived from st/godel-1 by the attribution rule
Independence of the continuum hypothesis — who, and when?
Paul Cohen, 1963.
derived from st/ch-independent by the attribution rule
Independence of the axiom of choice — who, and when?
Paul Cohen, 1963.
derived from st/ac-independent by the attribution rule
The Curry–Howard correspondence — who, and when?
Haskell Curry, then William Howard, 1934 (Curry), 1969 (Howard).
derived from st/curry-howard by the attribution rule
Faulhaber's formula — who, and when?
Leonhard Euler, 1735.
derived from st/faulhaber by the attribution rule
Legendre's formula for v_p(n!) — who, and when?
Hasse, Schnirelmann, Teichmüller and others, 1920s–1930s.
derived from st/legendre-formula by the attribution rule
Formalisation 2
What is √2 is irrational called in Mathlib?
irrational_sqrt_two — Mathlib.NumberTheory.Real.Irrational
derived from st/sqrt2-irrational by the binding rule
What is Legendre's formula for v_p(n!) called in Mathlib?
sub_one_mul_padicValNat_factorial — Mathlib.NumberTheory.Padics.PadicVal.Basic
derived from st/legendre-formula by the binding rule
Connections 9
Under the Information cost lens, how do Bernoulli numbers & power sums and Peano arithmetic relate? [Information cost]
Every Bernoulli number depends on all the earlier ones: the defining system is lower triangular and dense. This is the worst case, and it is the baseline the sparse recurrences get compared against.
derived from information-cost:bernoulli-numbers→peano by the connection rule
Under the Degeneracy lens, how do Ostrowski's theorem and Peano arithmetic relate? [Degeneracy]
Being an integer is what survives every valuation at once — a condition imposed on a larger object, not a starting point that everything else is built up from.
derived from degeneracy:ostrowski→peano by the connection rule
Under the Degeneracy lens, how do Orbits & itineraries and Peano arithmetic relate? [Degeneracy]
Studying iteration in general and recovering the integer facts as corollaries, rather than building up from the integers and meeting iteration late. A claim about the right order to learn things in, not about what is true.
derived from degeneracy:dynamical-systems→peano by the connection rule
What is the correspondence between Propositional & predicate calculus and Typed λ-calculus? [Correspondences]
Propositions ↔ types, proofs ↔ programs, proof normalisation ↔ program evaluation. Logic and computation turn out to be the same subject written twice.
derived from correspondences:propositional-calculus→lambda-calculus by the connection rule
What is the correspondence between Propositional & predicate calculus and Peano arithmetic? [Correspondences]
Formulas and proofs ↔ natural numbers, so that provability becomes an arithmetic relation. This is what lets arithmetic talk about itself.
derived from correspondences:propositional-calculus→peano by the connection rule
Zermelo–Fraenkel set theory and Axiom of choice look like one thing. What separates them? [Forks]
The third return, and the one where you named the schema explicitly rather than just using it. ZFC and ZF¬C are both consistent if ZF is.
derived from forks:set-theory→axiom-of-choice by the connection rule
Zermelo–Fraenkel set theory and Continuum hypothesis look like one thing. What separates them? [Forks]
Same shape again: Gödel showed CH cannot be disproved, Cohen that it cannot be proved. A fork you reached for but did not develop — the thread stalled for want of forcing.
derived from forks:set-theory→continuum-hypothesis by the connection rule
Between Peano arithmetic and Hyperoperation hierarchy, which way does the reasoning actually run? [Direction]
From below, succession is an axiom and addition is defined from it. From above, addition is one rung of the hyperoperation ladder and the Peano axioms read as theorems about the bottom of it. Same content, opposite direction of justification.
derived from direction:peano→hyperoperations by the connection rule
In Mathlib, what is the import relation between p-adic numbers and Peano arithmetic? [Dependency (Mathlib)]
`Mathlib.NumberTheory.Padics.PadicVal.Basic` imports `Mathlib.Data.Nat.MaxPowDiv`, `Mathlib.Data.Nat.Multiplicity`, `Mathlib.Data.Nat.Prime.Int`. Read off Mathlib/NumberTheory/Padics/PadicVal/Basic.html. No human asserted this edge.
derived from dependency:p-adic-numbers→peano by the connection rule
Concepts 6
What is Peano arithmetic, in one sentence?
The natural numbers axiomatised: zero, successor, and induction. The base object almost everything else is eventually built on or compared to.
derived from peano by the concept rule
What is Effective procedure, in one sentence?
The pre-formal idea of a method you could just follow step by step — the intuition later made rigorous.
derived from effective-procedure by the concept rule
What is Typed λ-calculus, in one sentence?
Computation as function abstraction and application, with types constraining what may be applied to what.
derived from lambda-calculus by the concept rule
What is Propositional & predicate calculus, in one sentence?
Formal systems for reasoning, and the proofs expressible inside them.
derived from propositional-calculus by the concept rule
What is Zermelo–Fraenkel set theory, in one sentence?
The standard foundation: sets built from the empty set by a short list of construction axioms.
derived from set-theory by the concept rule
What is Axiom of choice, in one sentence?
Given any family of nonempty sets, a set can be formed by picking one element from each. Independent of ZF: assuming it and denying it both give consistent theories.
derived from axiom-of-choice by the concept rule