λρ-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

January 23, 2002

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.

Ryo Kashima has posed a Natural deduction system for the classical implicational logic. His system has three rules, the elimination of the implication, the introduction of the implication and the case rule. The author noticed that the introduction of the implication is derivable from the case rule and the weakening. So we have gotten the system TA_{μ} from Kashima’s system by replacing the introduction of implication by the weakening(cf. [3]). Then we have discovered the λρ–calculus.

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. (If f is a λ-variable or a ρ-variable, then it called a λ-abstract or a ρ-abstract respectively.)

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 (ρβ-contraction). A ρβ-redex is any λρ-term of form aMN, (λx.M)N or (λa.M)N; its contractum is aM, [N/x]M or λa.([λx.a(xN)/a]M)N respectively. The re-write rules are

\begin{matrix}aMN & ⊳_{1ρβ} & aM , \\ (λx.M)N & ⊳_{1ρβ} & [N/x]M , \\ (λa.M)N & ⊳_{1ρβ} & λa.([λx.a(xN)/a]M)N . \end{matrix}

Iff P contains a ρβ-redex-occurrence \underline{R} and Q is the result of replacing this by its contractum, we say P ρβ-contracts to Q (P ⊳_{1ρβ} Q) and we call the triple ⟨P, \underline{R}, Q⟩ a ρβ-contraction of P.

1.3.1 Lemma. P ⊳_{1ρβ} Q ⟹ F V (P) ⊇ F V (Q).

1.4 Definition (ρβ-reduction). A ρβ-reduction of a term P is a finite or infinite sequence of ρβcontractions with form

⟨P_{1}, \underline{R}_{1}, Q_{1}⟩, ⟨P_{2}, \underline{R}_{2}, Q_{2}⟩, …

where P_{1} ≡_{α} P and Q_{i} ≡_{α} P_{i+1} for i = 1, 2, . . .. (The empty sequence is allowed.) We say a finite reduction is from P to Q iff either it has n ≥ 1 contractions and Q_{n} ≡_{α} Q or it is empty and P ≡_{α} Q. A reduction from P to Q is said to terminate or end at Q. Iff there is a reduction from P to Q we say P ρβ-reduces to Q, or

P ⊳_{ρβ} Q.

Note that α-conversions are allowed in a ρβ-reduction.

1.5 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

2.1 Definition (Types). An infinite sequence of type-variables is assumed to be given, distinct from the term-variables. Types are linguistic expressions defined thus:

1. each type-variable is a type (called an atom);

2. if σ and τ are types then (σ → τ) is a type (called a composite type).

2.1.1 Notation. Type-variables are denoted by “p”, “q”, “r” with or without number-subscripts, and distinct letters denote distinct variables unless otherwise stated.

Arbitrary types are denoted by lower-case Greek letters except “λ” and “ρ”.

Parentheses will often (but not always) be omitted from types, and the reader should restore omitted ones in such a way that, for example,

ρ → σ → τ ≡ (ρ → (σ → τ))

This restoration rule is called association to the right.

2.2 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.

(“M : τ” should be read informally as “assign to M the type τ” or “M has type τ” or “M denotes a member of whatever set τ denotes”.)

2.3 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.3.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 = Γ.) The result of removing from Γ all assignments f_{i} : ρ_{i} with f_{i} ∉ F V (M) (where M is a given term) is called

Γ ↾ M

or “Γ restricted to M”. And Γ is called an “M-context” (for a given M) iff

Subjects(Γ) = F V (M).

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

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

2.4 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.5 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.5.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.6 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.6.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),

or in more compact style;

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

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

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

In the special case Γ = ∅ we shall say M has type τ in TA_{λρ}, or τ is a type of M in TA_{λρ}, or

⊢_{λρ} M : τ.

The phrase “in TA_{λρ}” may be omitted when no confusion is likely.

2.8 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.9 Theorem (Normalization Theorem for TA_{λρ}). Every T A_{λρ}-typable term has a ρβ-normal form.

2.10 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.11 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.

[3] Yuichi Komori. A natural deduction for classical logic, in which there exists a proof with the subformula property. In Proc. 33rd MLG meeting, pp. 3–6, Echigo Yuzawa, 2000. http://www.math.s.chibau.ac.jp/˜ komori/gakkai01-10/subform.dvi(tex).