Page 10 - Textos de Matemática Vol. 38

2 FERNANDO FERREIRA
the following interpretation in mind: the base type 0 is the type constituted by the natural numbers, whereas τ → σ is the type of (total) functions of objects of type τ to objects of type σ.
To make the reading easier, we often omit brackets and associate the arrows to the right, e.g., 0 → 0 → 0 means 0 → (0 → 0). The pure types are defined inductively for each natural number: the pure type corresponding to the natural number 0 is the base type 0; the pure type n + 1 is n → 0.
The language of Heyting arithmetic in all finite types, denoted by Lω0 , is a sorted language with a sort for each finite type. There is a denumerable set of variables xσ, yσ, zσ, etc for each type σ. When convenient, we omit the type superscript. There are two kinds of constants:
(a) Logical constants or combinators. For each pair of types ρ,τ there is a combinator of type ρ → τ → ρ denoted by Πρ,τ ; for each triple of types δ, ρ, τ there is a combinator of type
(δ → ρ → τ) → (δ → ρ) → (δ → τ) denoted by Σδ,ρ,τ .
(b) Arithmetical constants. The constant 0 of type 0; the successor constant S of type 1; for each tuple of types ρ a recursor constant of type
0 → ρ → (ρ → 0 → ρ) → ρ denoted by Rρ.
Constants and variables of type ρ are terms of type ρ. If t is a term of type ρ→τ andqisatermsoftypeρthenApp(t,q)isatermoftypeτ.Theseareall the terms there are. A term with no variables is a closed term. We usually write tq or t(q) for App(t, q). When writing tqr without brackets we associate to the left (note the difference with the previous convention): (t(q))(r). We also write t(q, r) instead of (t(q))(r). In general, t(q, r, . . . , s) stands for (. . . ((t(q))(r)) . . .)(s).
Atomic formulas are formulas of the form t = q where t and q are terms of type 0. Note that, in the present setting, there is only one primitive equality symbol (infixing between terms of type 0). Formulas are obtained from atomic formulas by means of the usual propositional connectives ∧, ∨, →, ⊥ (falsum) and universal and existential quantifiers ∀xσ and ∃xσ for each type σ. As usual, ¬A abbreviates A → ⊥ and A ↔ B abbreviates (A → B) ∧ (B → A).
1.2 Heyting arithmetic in all finite types
The theory HAω0 is based on intuitionistic logic. It also has the following axioms for combinators and equality: