Page 80 - Textos de Matemática Vol. 40

68 Chapter 2. Explicit Mathematics
By choosing the codes for the generators according to these conditions, the axioms about uniqueness of generators are obviously satisfied.
To interpret the second order part of NEM we define three relations Typ, In and In, using appropriate operator forms. The meaning of these predicates and their relation to LEM is as follows. Let s,t be terms of ID1 interpreting types S,T of LEM, respectively, and let r be the interpretation of an arbitrary LEM term, then we have:
• Typ(t) represents that t is a code of a type.
• In(r, t) interprets the formula r ∈ T .
• In(r,t) holds for ¬r ∈ T.
• We have to introduce the relation In in order to guarantee that the defining operator forms are positive. As a consequence, we have to prove that In(r, t) is equivalent to ¬In(r, t).
• T = S is interpreted by Typ(t) ∧ Typ(s) ∧ ∀x.In(x, t) ↔ In(x, s), i.e., as extensional equality.
• R(t, S) is also modelled by Typ(t) ∧ Typ(s) ∧ ∀x.In(x, t) ↔ In(x, s).
In order to define Typ(x), In(x,y) and In(x,y) we need some coding. Let us use φ0(x), φ1(x, y) and φ2(x, y) as abbreviations for φ(⟨0, x⟩), φ(⟨1, ⟨x, y⟩⟩) and φ(⟨2, ⟨x, y⟩⟩), respectively. With this notation we can define Typ(x), In(x, y) and In(x,y) as the “projections” Pφ0 (x), Pφ1 (x,y) and Pφ2 (x,y) of the fixed point Pφ of the positive operator form:
φ(ψ,z) := (∃y.z=⟨0,y⟩∧CTyp(ψ,y))∨
(∃x, y.z = ⟨1, ⟨x, y⟩⟩ ∧ CIn(ψ, x, y)) ∨
(∃x, y.z = ⟨2, ⟨x, y⟩⟩ ∧ CIn(ψ, x, y))
with the following closure conditions (where it is helpful to keep in mind the intended meanings of ψ0, ψ1 and ψ2, namely Typ, In and In, respectively). CTyp(ψ,z) is the disjunction of the following clauses:
• z=⟨1⟩,
• z=⟨2⟩,
• ∃x.z=⟨3,x⟩∧ψ0(x),
• ∃x,y.z=⟨4,x,y⟩∧ψ0(x)∧ψ0(x),
• ∃x.z=⟨5,x⟩∧ψ0(x),
• ∃f,x.z=⟨6,f,x⟩∧ψ0(x),
• ∃f,x.z=⟨7,x,f⟩∧ψ0(x)∧∀y.¬ψ2(y,x)→ψ0({f}(y)).