Gödel's beta function #
This file formalizes Gödel's beta function, and proves its properties in Q and PA. Gödel's beta
function enables encoding of finite sequences, which is a crucial step towards the representation
theorem.
In Q, we only prove its representability (beta_ofNat). In PA, we also prove its uniqueness
(beta_unique), totality (beta_total), and the comprehension theorem (beta_comprehension). The
comprehension theorem allows us to encode a finite sequence described by a formula; to prove that,
we have to formalize the Chinese remainder theorem in PA.
References #
- A Concise Introduction to Mathematical Logic (third edition), Wolfgang Rautenberg.
Equations
- v.unbeta = Nat.unbeta (List.ofFn v)
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Chinese remainder theorem formalized in PA: if p(x, i) and q(x, i) uniquely describe two
sequences of numbers a₀, ⋯, aₗ₋₁ and d₀, ⋯, dₗ₋₁ with aᵢ < dᵢ for each i, and
d₀, ⋯, dₗ₋₁ are coprime, then there exists a number m such that m % dᵢ = aᵢ for each i.
Comprehension theorem for Gödel's beta function: if p(x, i) uniquely describes a sequence of
numbers a₀, ⋯, aₗ₋₁, then there exists a number m that encodes this sequence, i.e.
β(m, i) = aᵢ for each i.
Proof sketch: let lcm(1, 2, ⋯, l) ∣ A, B ≥ max(a₀, ⋯, aₗ₋₁) and dᵢ = (i + 1) * A * B + 1,
then d₀, ⋯, dₗ₋₁ are coprime. By Chinese remainder theorem, there exists a C such that
C % dᵢ = aᵢ, i.e. β(⟪C, A * B⟫, i) = aᵢ.
With minimization, the description formula p in beta_comprehension does not have to be unique.