Page 21 - Textos de Matemática Vol. 40

1.1. The logic of partial terms 9
Since we work with classical logic, ∨ (disjunction), → (implication), ↔ (equiv- alence), and ∃ (existential quantification) can be defined as usual. We will use the usual conventions of precedence for the connectives. For the quantifiers we use in analogy to λ terms a point notation which should be understood that the scope of a quantifier goes up to the next closing parenthesis which was not opened after the quantifier, or the end of the formula. The set of free variables FV(t) or FV(φ) of a term t or formula φ is defined as usual. We use the notation t[s/x] and φ[s/x] to indicate that all free occurrences of x in t and φ should be substituted by s. If the substitution variable is clear from the context, we also use φ(t) to indicate that t should be substituted for it in φ.
As abbreviation we will need the following partial equality relation: t≃s :⇔ t↓∨s↓→t=s.
Sometimes, we will use a “strong” inequality which differs from the negated equality by the fact that the definedness of the involved terms should be kept:
t̸=s :⇔ t↓∧s↓∧¬t=s. 1.1.2 The logical axioms
The logic of partial terms is defined in [Bee85, Section IV.1]. A detailed discus- sion, including its semantics, may be found in the lecture notes [J¨ag97, Chap- ter 1].
Using a Hilbert-style calculus1 we have the following logical axioms and rules:
I. A complete axiomatization of classical propositional logic.
II. Quantifier axioms.
(Q1) ∀x.φ ∧ t ↓ → φ[t/x],
(Q2) φ[t/x] ∧ t ↓ → ∃x.φ.
III. Equality axioms. (E1) x = x,
(E2) t≃s∧φ(t)→φ(s). IV. Strictness axioms.
(S1) R(t1,...,tn)→t1 ↓∧...∧tn ↓, (S2) ts↓→t↓∧s↓,
ifRisan-aryrelationsymbol,
1For metamathematical considerations it is some times convenient to consider reformula- tions of the theories as a sequent calculus or as a Tait calculus. This is done in this work for the proof of the upper bounds of truth theories with universes in Section 3.4.6.