Page 11 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 3
(a) Axioms for combinators. A[Π(x,y)/w] ↔ A[x/w] and A[Σ(x,y,z)/w] ↔ A[x(z, yz)/w], where A is an atomic formula with a distinguished variable w and A[t/w] is obtained from A by replacing the occurrences of w by t.
(b) Equality axioms. x = x (reflexivity); x = y ∧ A[x/w] → A[y/w], where A is an atomic formula with a distinguished (type zero) variable w.
and the arithmetical axioms:
(c) Successoraxioms.Sx̸=0andSx=Sy→x=y.
(d) Axioms for recursors. A[R(0, y, z A[z(R(x, y, z
] ↔ A[y/w
)/w] ↔
)/w
),x)/w], where A is an atomic formula with distinguished
] and A[R(Sx, y, z
variables w.
(e) Induction scheme. A(0)∧∀x0(A(x) → A(Sx)) → ∀xA(x), for each formula
A of the language.
It can be shown that equality is symmetric and transitive and, moreover, the conditional x = y ∧ A[x/w] → A[y/w] also holds for every formula of the language (provided that there is no clash of variables). Similarly, the axioms for combinators and recursors extend to every formula A.
Equalityisdecidableinthefollowingsense:HAω0 ⊢∀x0(x=0∨x̸=0).This is easily proven by induction. Equality for higher types is defined inductively: s =ρ→τ t is ∀xρ(sx =τ tx). Equality in higher types is not decidable any longer. Full extensionality is the scheme of axioms ∀z∀x, y(x = y → zx = zy). It should be noted that we are not assuming full extensionality in the theory HAω0 . The theory obtained by its inclusion is denoted by E-HAω.
1.3 Combinatorial completeness
The combinators Π and Σ are instrumental in proving the following im- portant property:
Theorem 1.1 (Combinatorial completeness). For each term t[xρ] of type τ with a distinguished variable x of type ρ, we can construct a term q of type ρ → τ whose variables are those of t except for x such that, for every term s of type ρ and atomic formula A with a distinguished variable wτ ,
HAω0 ⊢A[t[s/x]/w]↔A[qs/w].
For instance, if t is of type 0, then qs = t[s/x]. The term q is usually denoted by λx.t and the above equation can now be written (λx.t)s = t[s/x] (β-reduction). Of course, the proposition extends to all formulas A (provided that there is no clash of variables), i.e., we may substitute the term t[s/x] by (λx.t)s in any formula.