Page 22 - Textos de Matemática Vol. 40

10
Chapter 1.
Applicative theories
(S3) (S4)
c ↓, if c is a constant symbol, x ↓.
V. Modus Ponens. (MP)φ→ψ φ
ψ
VI. Quantifier rules. (Q3) ψ → φ
x ̸∈ FV(ψ), x ̸∈ FV(ψ).
ψ → ∀x.φ (Q4) φ → ψ
(∃x.φ) → ψ
Originally, applicative theories were formulated with intuitionistic logic, cf. [Fef75, Fef79]. Nowadays, however, they are usually studied in a classical set- ting. For many intuitionistic aspects of this subject we refer to Beeson [Bee85] and Troelstra and van Dalen [TvD88b], see also the work of Gordeev, [Gor88], and, more recently, Tupailo, [Tup01, Tup03, Tup04].
1.1.3 Some comments.
The ternary predicate App. In the original work of Feferman about explicit mathematics and in some later work of other authors the theories are developed based on usual first order logic instead of the logic of partial terms (which was introduced later). In this case, one uses a fundamental predicate App(t, r, s) for the application which may intuitively be translated into the logic of partial terms by t r ≃ s. In fact, the latter expression is introduced as abbreviation for the former one in [Fef79, p. 80], but there are terms defined only as constants and variables. In fact, an “usual” application term t s has to be broken down in a context of an partial equation ts ≃ y by ∃x1,x2.t ≃ x1 ∧s ≃ x2 ∧App(x1,x2,y). This treatment is given in detail in [Fef75, Section 2.4]. Conversely, it is some- times convenient to model the application operation by a ternary application relation which corresponds to the predicate App(t, r, s). This requires the same procedure as for the abbreviation of t s ≃ y in terms of App, now as part of the interpretation, cf. e.g., [FJ93, Section 5.2].
Partial Scott logic. Beside the logic of partial terms there is also a partial logic introduced by Scott in [Sco79]. This logic differs from LPT in the way that variables are not presupposed as defined, and therefore, the quantifiers are treated differently. A presentation of both logics may be found in [TvD88a, Chapter 2, Section 2] where the Scott logic is called E, while the logic of partial terms corresponds to E+ logic with strictness and equality. Comparisons of these two logics may also be found in Strahm [Str92] and Feferman [Fef95].
Basic Logic of Partial Terms. Identifying definedness with termination, the strictness axioms correspond obviously to a call-by-value evaluation strategy.