Page 26 - Textos de Matemática Vol. 40

14 Chapter 1. Applicative theories
Proposition 1.2.3. Let T be an applicative theory, φ(x) and ψ(x) formulae of the language of T with the common free variable x. If negψ is a term of the language of T such that T proves φ(x) → (ψ(x) ↔ ¬ψ(negψ x)) and φ(t) → t ↓ for all terms t of T , then there exists a term notφ such that:
T ⊢ ¬φ(notφ).
Proof. Define notφ := rec (λf, x.negψ (f x)) 0. With the assumption φ(notφ) we get notφ ↓ and furthermore:
ψ(notφ) ↔
↔ ψ((λf, x.negψ (f x)) (rec (λf, x.negψ (f x))) 0)
↔ ψ(negψ (rec (λf, x.negψ (f x)) 0))
↔ ψ(negψ notφ)
↔ ¬ψ(notφ).
This is a contradiction, i.e., the assumption φ(notφ) is false. ⊣ 1.2.2 Some comments
Totality. As mentioned above, in the total setting the axiom I.(2) for the s com- binator can be simplified to s x y z = x z (y z). In this context, the Propositions about λ and recursion read as follows:
Proposition 1.2.4. 1. For every variable x and every term t of an applicative language L, there exists a term λx.t of L whose free variables are those of t, excluding x, such that (λx.t) x = t is provable.
2. There exists a term rec of L such that ∀x.rec x = x (rec x) is provable.
Extensionality. In particular from a mathematical point of view, it is reasonable to consider functions as extensional objects. This can be done in applicative theories by adding the following axiom of extensionality:
(Ext) (∀x.fx≃gx)→f =g.
However, this axiom cannot be verified in the recursion theoretic models of applicative theories.
Functional programming. By providing combinatory logic, applicative theories are closely related to the λ calculus. This advises to use them as theories for functional programming which is—in its core—an implementation of the λ calculus. Since the underlying logic is untyped and strict, applicative theories fit well with programming languages based on these properties, like lisp and scheme. In fact, Beeson [Bee85, p. 107] mentions lisp as a model for applicative theories, and Sta¨rk has worked out the close relationship between
ψ(rec (λf, x.negψ (f x)) 0)