Proofs of the properties of formal systems are commonly carried out in weak predicative arithmetic systems such as PRA (Primitive Recursive Arithmetic) using Gödel numberings (1931), an assignment of a unique natural number to each symbol and well-formed formula of some formal language. However the necessity to go through coding makes the proofs considerably more tedious and introduces a reasoning gap.
Recent advances in type theories allow to address these issues. Primitive recursive dependent type theory
Tᴾᴿ[BB24] is a conservative extentsion of the PRA supporting finitary
inductive types and type families comprising a small universe FData lacking function types, and one Π-closed
universe Type above.
Finitary inductive type families are direct representations of abstract formal languages and come with structural induction principles, a tidy and natural way to define translations and reason about expressions.
In Tᴾᴿ it is possible to define inductive types capturing the syntax of arithmetic and a proof calculus for classical first order logic. Then we can both prove the consistency of the Peano Arithmetic relative to the ε₀-induction principle (which can be stated in Tᴾᴿ very naturally, cf. the original paper) and define its Dialectica Interpretation in a very readable and fully mechanized way without reasoning gaps.
Tᴾᴿ can naturaly state (but not prove) its own consistency. Let Prf : FData be the inductive type of its own proofs
together with a type family Conclusion : Prf → Type. Hilbert-style consistency is a states that conclusion of
every proof is not false.
∀(prf : Prf) ¬¬Conclusion(prf)
Classically, it is equivalent to its constructively stronger form, a dependent function
eval : ∀(prf : Prf) Conclusion(prf)
Gödel’s second incompleteness theorem seems to rule out theories that can prove their own Hilbert-style consistency, but the recently developed finitary set theory H˂ʷ [Pakhomov19] uses a loophole of Gödel’s result and proves its own consistency. Its proof cannot be verified in its entirety because the syntactical encoding of the very proofs (“Gödel numbering”) lies outside the scope of set theoretic language. We want to address this shortcoming by developing a type-theoretic counterpart of Pakhomov’s finitary set theory.
We’ll be working in a type theory with subtyping with a universe FData : Type of finitary inductive types
lacking function types, and a universe Type ⊋ FData closed under П-types ∀(x : X) Y(x) and parametric
quantification ∀<x : X> Y(x).
Definition of an inductive type J also allows to define a family of its subtypes
ℬ︀J : J → FData, with each ℬ︀J e inhabited by subexpressions of e : J. For the type ℕ of natural numbers,
ℬ︀ℕ n is precisely the type of natural numbers below n also known as Fin n in literature. Note that ℬ︀ is
not a function on types, but an operator on type definitions; it produces non-equivalent results on isomorphic types.
In Tᴾᴿ elimination form inductive types is only allowed into the universe FData to ensure only primitive recursive
functions can be defined. We’ll be even more restrictive: unless result type is a finite type (like ℬ︀ℕ n),
elimination motive is not allowed to apply any constructors to non-constant terms. It is still possible to
define constant functions and enough non-increasing functions as usual:
def ultimateAnswer(n : ℕ) = 42
def id<T>(t : T) = t
def K<X, Y>(x : X, y : Y) = x
def monus(n m : ℕ) `n ∸ m` : ℕ
(0, _) ↦ 0
(n, 0) ↦ n
(n⁺, m⁺) ↦ (n ∸ m)
Yet we cannot construct addition (or successor, for that matter), unless we track construction costs:
def add<bound>(n : ℬ︀ℕ bound, m : ℬ︀ℕ (bound ∸ n)) : ℬ︀ℕ bound
In our theory, total functions are only those that cannot run out of memory.
It also seems that under our restrictions we can make the universe Type impredicative without introducing paradoxes.
Given a type U : Type and a type-falued function Dec : U → FData we can define a W-type W(t : U) Dec T of U-small hereditary multisets.
For U = FData and Dec = id<FDate> let us call the resulting type V := W(T : FData) T. It’s constructor will be denoted sup<T> (elements : T → V) : V.
Other than that we’ll be working with hereditary multiset types for finite types U, which are ordinary finitary inductive types inside FData.
To every inductive type definition J we can associate a hereditary multiset as follows:
𝒮[J] = sup { expr : J ↦ 𝒮[ℬ︀J] expr}
In particular, we have
𝒮[Void] = ∅
𝒮[Unit] = {∅}
𝒮[ℬ︀ℕ 2] = {∅, {∅}}
𝒮[ℬ︀ℕ 3] = {∅, {∅}, {∅, {∅}}
𝒮[ℕ] = {finite von Neumann numerals}
Note that 𝒮 is an operator on inductive definitions, not a function on types. It produces non-equivalent results on isomorphic types, e.g.
𝒮[Bool] = {∅, ∅} ≠ 𝒮[ℬ︀ℕ 2]
The type (ℬ︀V s) contains precisely the elements of s.
Given a finite inductive type F, (ℬ︀V 𝒮F) the von Neumann closure of 𝒮F.
For any term c : J of any inductive type J let’s write 𝒱e for
(ℬ︀V 𝒮[ℬ︀J c]).
𝒱c can be made into a finite universe closed under strongly bounded sums
and products and containing inductive types (ℬ︀J c’) for all c' : ℬ︀J c.
Inductive types J are defined by dependent polynomials P such that J = P(J).
Since finite universes are closed under strongly bounded sums and products, i.e.
strongly bounded dependent polynomials, for every inductive type definition
[J] : FData, and we have a canonical approximation ⌊J⌋c of J contained
inside 𝒱c.
We anticipate that just like in case of Pakhomov’s finitary set theory, the finite
universes 𝒱c will turn out to be partial models of our calculus BICC.
Given b : ℕ, 𝒱b is a finite universe where sets have at most b elements,
so the approximation ⌊ℕ²⌋b of the type of pairs of natural numbers only contains
pairs where each component is at most ⌊√b⌋, while the approximation of the disjoint
sum ⌊ℕ + ℕ⌋b only contains terms inl(n) and inr(n) where n is at most ⌊b/2⌋.
This way we can write signatures of growing functions much more concisely:
add<b, inl(h) : ⌊ℕ + ℕ⌋b>(n : ⌊ℕ⌋h,
m : ⌊ℕ⌋h) : ℬ︀ℕ b
mul<b, (_, h) : ⌊ℕ²⌋b>(n : ⌊ℕ⌋h,
m : ⌊ℕ⌋h) : ℬ︀ℕ b
The types ℕ + ℕ and ℕ² are special cases of ordinals governing recursive complexity of underlying functions.
With an appropriate inductive type ε₀, we should be able to construct the cut-elimination procedure for proofs in Peano arithmetic:
normalize<size, depth : ⌊ε₀⌋size> : ⌊PeanoPrf⌋depth → (CutFreePrf size)
In type theories, types containing other types are known as universes. A universe is called hereditary if the types it contains are (1) themselves universes (2) hereditary ones. Pure set theories can be understood as type theories where all types (besides the universe of proposition Prop) are hereditary universes. Well-founded pure set theories are the ones where ∈-induction for hereditary universes is derivable.
Type theories, in particular the ones with infinite universe hierarchies have rule schemata producing a (r.e.) infinite number of rules, e.g.
–––––————–––––(UH) –——––––————–––—(UC)
Γ ⊢ Uⁿ : Uⁿ⁺ Γ ⊢ Uⁿ ⊆ Uⁿ⁺
Finitary set theory H˂ʷ [Pakhomov19] features the schemes (UH) and (UA) from above defining a cumulative hierarchy of hereditary universes containing at least n elements for each finite n, the operation of completion V for hereditary universes U:
Γ ⊢ T : U U' ⊆ V(T)
–––––————––––––––————–––—
Γ ⊢ U' : V(U)
Additionally, it contains the type of propositions implementing classical predicate logic with equality and reflecting ∈-relation for hereditary universes. Hereditary universes can be filtered by predicates (separation). ∈-induction for predicates can be classically derived.
Older stuff; TODO: rewrite
A theory is called locally finite iff any of its finite subtheories (take any finite number of axioms generated by schemata) have finite models. It is precisely the locally finite theories that can evade the shackles of Gödel’s second incompleteness theorem. As exemplified by H˂ʷ, a locally finite theory can be powerful enough to define query functions on finite domains (think of database queries applicable to finite tables), but a locally finite type theory cannot feature provably infinite types, but it is still possible to allow inductive definitions. Instead of defining types, they will define inductive hierarchies, that is cumulative hierarchies of finite “bounded inductive” types approximating the intended inductive type.
Our idea is to use terms of other bounded inductive types as levels of approximation.
That is for every inductive definition J and some term n : T of some bounded inductive type,
we will have a bounded inductive type Jⁿ of J-terms
that can be constructed from n using non-increasing structural induction.
This way we will have
Γ, n : T ⊢ t' : Jⁿ
––––––––––––––––––––––––––––
Γ, n : T, t : Jⁿ ⊢ Jᵗ ⊆ Jⁿ
i.e. essentially we have t : Jᵗ.
We hope to generalize the completion operator V from hereditary universes to terms of arbitrary inductive types so that Vᵗ is precisely the finitary hereditary universe where all bounded inductive types Jᵗ can be modelled.
Since every proof t : Prfⁿ is finite,
it can be carried out already inside the finite partial model Vⁿ of our theory.
Checking a proof inside a finite model is a case of a query evaluation on a finite domain,
so it should be possible to define the level-polymorphic function evalⁿ : ∀(t : Prfⁿ) → Conclusion(prf),
yielding the strong Hilbert-style consistency eval : ∀(t : Prf) → Conclusion(prf).
We want to develop Bounded Inductive Construction Calculus to be a trusted finitistic core theory to carry out metamathematical proofs. It seems, in most cases bi-interpretability and conservativity proofs can be carried out unconditionally.
We intend to develop a logic-free formalization for the finitary set theory H˂ʷ and its intuitionistic variant CH˂ʷ (see https://akuklev.github.io/finitistic-core) and show their bi-interpretability with BICC. Then we intend to develop its extensions CH˂ᶿ for computable ordinals θ to gauge consistency strength of predicative theories, e.g. show bi-interpretability of Peano Arithmetic with CH˂ᵋ⁰ and thus its consistency modulo ε₀-induction. Consistency of impredicative theories is measured relative to set theories with some higher infinity axioms (existence of universes with given closure properties), so we hope to develop appropriate extensions of H˂ʷ with a fixed number, a countable hierarchy, or an ordinal-indexed hierarchy of universes with given properties to use for bi-interpretability proofs with impredicative theories.
We intend to use BICC to prove the soundness of HCCC, namely typechecking decidability, normalization, canonicity, and conservativity over M. Shulman’s “Set theory for category theory” ZMC/𝕊, which also yields relative consistency. The same should be carried out for restricted variants of HCCC, namely the one conservative over Tarski-Grothendieck set theory, the one conservative over ZFC and the strongest known predicative variant (extended predicative Mahlo universes, but no propositional resizing). Weak variants conservative over major reverse mathematics systems should be also isolated.
We hope BICC might be the right choice to develop an extensive body of mechanized proofs of major results regarding conservativity, relative consistency, independence, forcing, realizability, ordinal analysis, and reverse mathematics.