λρ-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 T A_{λ} gives a natural deduction for implicational intuitionistic logic, the type assignment system T A_{λρ} gives a natural deduction for classical implicational logic. Moreover for any classical implicational theorem α there exists a proof of α in T A_{λρ} 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 T A_{μ} from Kashima’s system by replacing the introduction of implication by the weakening. Then we have discovered the λρ–calculus.

DEFINITION 0.1 (λρ-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 x is a λ-variable and M is a λρ-term then (λx.M) is a λρ-term called an abstract or a λ-abstract;

5. if a is a ρ-variable and M is a λρ-term then (ρa.M) is a λρ-term called a rationalization.

DEFINITION 0.2 (ρβ-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.

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

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

Types are defined as usual.

DEFINITION 0.4 (The type-assignment system T A_{λρ}) T A_{λ}ρ is a Natural Deduction system. Its formulas are arbitrary expressions M : α, where M is a λρ-term and α is a type.

\begin{matrix}{Π_{1} \atop M : α → β} & {Π_{2} \atop N : α} \\ MN : β \end{matrix} (→ E),  {x : α \atop Π} ; M : β ; λx.M : α → β (→ I),

{Π \atop M : α} ; aM : β (Absurd),  {Π \atop M : α} ; ρa.M : α (Rati).

EXAMPLE 0.5 (((α → β) → α) → α)

\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)

FACT 0.6 (T A_{λρ} 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 : α.

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

FACT 0.8 (Subformula Property for T A_{λρ}) 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 predicate of undischarged assumptions.

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.