λρ-Calculus: A Natural Deduction for Classical Logic

Yuichi KOMORI

                       komori@math.s.chiba-u.ac.jp

Department of Mathematics, Faculty of Science, Chiba University Inage-ku Chiba 263-8522 JAPAN

In this note, we will pose a new system, named λρ–calculus. While the type assignment system TA_{λ} gives a natural deduction for implicational intuitionistic logic, the type assignment system TA_{λρ} gives a natural deduction for classical implicational logic. Moreover for any classical implicational theorem α there exists a proof of α in TA_{λρ} enjoying the subformula property.

1 The type free λρ-calculus

1.1 Definition (λρ-terms). An infinite sequence of λ-variables is assumed to be given, and an infinite sequence of ρ-variables is assumed to be given. Then linguistic expressions called λρ-terms are defined thus:

1. each λ-variable is a λρ-terms, called an atom or atomic term;

2. if M and N are λρ-terms then (MN) is a λρ-term called an application;

3. if M is a λρ-term and a is a ρ-variable then aM is a λρ-term called an absurd;

4. if f is a λ-variable or a ρ-variable and M is a λρ-term then (λf.M) is a λρ-term called an abstract.

1.1.1 Notation. λ-variables are denoted by “u”,“v”,“w”,“x”, “y”,“z”, with or without number-subscripts. ρ-variables are denoted by “a”,“b”,“c”,“d”, with or without number-subscripts. A term-variable means a λ-variable or a ρ-variable. Term variables are denoted by “f”,“g”,“h”, with or without number-subscripts. Distinct letters denotes distinct variables unless otherwise stated.

A term λa.M is sometimes denoted by ρa.M if the variable a is a ρ-variable.

Arbitrary λρ-terms are denoted by “L”,“M”,“N”,“P ”,“Q”, “R”,“S”,“T ”, with or without numbersubscripts. For “λρ-term” we shall say just “term”.

1.2 Definition (Free, bound). A non-binding variable occurence \underline{f} in a term M is said to be bound in M iff it is in the scope of an occurrence of λf in M, otherwise it is free in M.

A variable f is said to be bound in M iff M contains an occurence of λf; and f is said to be free in M iff M contains a free occurence of f. The set of all variables free in M is called

F V (M).

1.3 Definition (ρβ-reduction). Any λρ-term of form aMN, (λx.M)N, (λa.M)N is called a ρβ-redex. ρβ-contracting an occurrence of a redex in a term U means replacing one occurence of

\begin{matrix}aMN & by & aM , \\ (λx.M)N & by & [N/x]M , \\ (λa.M)N & by & λa.([λx.a(xN)/a]M)N . \end{matrix}

If this changes U to V, we say U ρβ-contracts to V, or

U ⊳_{1ρβ} V.

We say U ρβ-reduces to V, or

U ⊳_{ρβ} V,

iff V is obtained from U by a finite (perhaps empty) series of ρβ-contractions and changes of bound variables.

1.4 Theorem ((Church-Rosser Theorem for ρβ)). If M ⊳_{ρβ} P and M ⊳_{ρβ} Q then there exist T such that

P ⊳_{ρβ} T, Q ⊳_{ρβ} T.

2 Assigning types to terms

Types are defined as usual.

2.1 Definition. A type-assignment is any expression

M : τ

where M is a λρ-term or a ρ-variable and τ is a type; we call M its subject and τ its predicate.

2.2 Definition. A type-context Γ is any finite, perhaps empty, set of type-assignments

Γ = {f_{1} : ρ_{1}, …, f_{m} : ρ_{m}}

whose subjects are term-variables which is consistent in the sense that no term-variable is the subject of more than one assignment. For any such Γ define

Subjects(Γ) = {f_{1}, …, f_{m}}.

2.2.1 Notation. The result of removing from Γ the assignment whose subject is f (if Γ has one) is called

Γ − f.

(If f ∉ Subjects(Γ) we define Γ − f = Γ.)

Γ_{λ} and Γ_{ρ} denote the subsets of Γ of all assignments whose subjects are λ-variables and ρ-variables respectively.

2.2.2 Note. A type-context Γ is a set, not a sequence. Hence it does not change when its members are permuted or repeated.

2.3 Definition. We say Γ_{1} is consistent with Γ_{2} iff Γ_{1} ∪Γ_{2} is consistent; and Γ_{1}, …, Γ_{n} are mutually consistent if their union is consistent.

2.4 Definition (TA_{λρ}-formulae). For any type-context Γ and any type-assignment M : τ, the pair ⟨Γ; M : τ⟩ is called TA_{λρ}-formula and is written as

Γ_{λ} ↦ Γ_{ρ}, M : τ

(or just ↦ M : τ when Γ is empty). We shall call M the subject of this formula and τ its predicate.

2.4.1 Notation. The following abbreviations will often be used:

f_{1} : σ_{1}, …, f_{n} : σ_{n} for {f_{1} : σ_{1}, …, f_{n} : σ_{n}},
Γ, f_{1} : σ_{1}, …, f_{n} : σ_{n} for Γ ∪ {f_{1} : σ_{1}, …, f_{n} : σ_{n}}.

2.5 Definition (The system TA_{λρ}). TA_{λρ} has an infinite set of axioms and four deduction-rules (called (→E) or →-elimination, (→I) or →-introduction, (Absurd) and (Rati)), as follows.

Axioms of TA_{λρ}: for every term-variable x and every type τ, TA_{λρ} has an axiom

x : τ ↦ x : τ.

Deduction-rules of TA_{λρ}:

\begin{matrix}⟨Γ_{1}; P : σ → τ⟩ & ⟨Γ_{2}; Q : σ⟩ \\ ⟨Γ_{1} ∪ Γ_{2}; P Q : τ⟩ \end{matrix} (→ E) [if Γ_{1} ∪ Γ_{2} is consistent],

{⟨Γ; P : τ⟩ \atop ⟨Γ − x; λx.P : σ → τ⟩} (→ I) [if Γ is consistent with x : σ],

{⟨Γ; P : τ⟩ \atop ⟨Γ, a : τ; aP : σ⟩} (Absurd) [if Γ is consistent with a : τ],

{⟨Γ; P : τ⟩ \atop ⟨Γ − a; λa.P : τ⟩} (Rati) [if Γ is consistent with a : τ].

2.5.1 Example (((α → β) → α) → α).

\begin{matrix}y : (α → β) → α ↦ y : (α → β) → α & \begin{matrix}{x : α ↦ x : α \atop x : α ↦ a : α, ax : β} & (Absurd) \\ ↦ a : α, λx.ax : α → β \end{matrix} ; (→ I) \\ y : (α → β) → α ↦ a : α, y(λx.ax) : α \end{matrix} ; (→ E) ; y : (α → β) → α ↦ ρa.y(λx.ax) : α ; (Rati) ; ↦ λy.ρa.y(λx.ax) : ((α → β) → α) → α ; (→ I)

The above TA_{λρ}-deduction is often written as the below.

\begin{matrix}y : (α → β) → α & \begin{matrix}{x : α \atop ax : β} & (Absurd) \\ λx.ax : α → β \end{matrix} ; (→ I) \\ y(λx.ax) : α \end{matrix} ; (→ E) ; ρa.y(λx.ax) : α ; (Rati) ; λy.ρa.y(λx.ax) : ((α → β) → α) → α ; (→ I)

2.6 Definition. Let Γ be a type-context. Iff there is a TA_{λρ}-deduction of a formula ⟨Γ′; M : τ⟩ for some Γ′ ⊆ Γ we shall say

Γ_{λ} ⊢_{λρ} Γ_{ρ}, M : τ.

2.7 Theorem (A λρ-term is a proof of classical implicational logic). α is a classical implicational theorem if and only if there exists a closed λρ-term M such that ⊢_{λρ} M : α.

2.8 Theorem (Normalization Theorem for TA_{λρ}). Every T A_{λρ}-typable term has a ρβ-normal form.

2.9 Theorem (Subformula Property for TA_{λρ}). Let λρ-term M be a ρβ-normal form and Δ a T A_{λρ}-deduction of ⟨Γ; M : α⟩. Then every type in Δ has an occurence in α or in a type in Γ.

2.10 Theorem (Subject-reduction Theorem). If Γ ⊢_{λρ} Θ, P : τ and P ⊳_{ρβ} Q then

Γ ⊢_{λρ} Θ, Q : τ.

References

[1] J. Roger Hindley. Basic Simple Type Theory, Vol. 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997.

[2] J. Roger Hindley and Jonathan P. Seldin. Introduction to combinators and λ–calculus, Vol. 1 of London Mathematical Society Student Texts. Cambridge University Press, 1986.