Peano arithmetic — flashcards
Every card the map can derive about Peano arithmetic — definitions, statements, attribution, and the edges it sits on.
Theorems 5
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: 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 5
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
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 6
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 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
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 1
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