A Natural Deduction for Classical Logic, in which there exists a proof with the Subformula Property

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. λ–calculus can be simulated in μ–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 has 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.

1 The type-free μ-calculus and its type assignment

DEFINITION 1.1 (μ-terms) An infinite sequence of term-variables is assmed to be given. Then linguistic expression called μ-terms are defined thus:

1. each term-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 then KM is a μ-term called a weakening;

4. if x is a term-variable and M and N are μ-terms then (μx.M ∗ N) is a μ-term called an abstract or a μ-abstract.

DEFINITION 1.2 (β-reduction) Any μ-term of form KMN, (μx.M∗N)R, μx.[xMN/z]P ∗Q (where z ∈ F V (P) and x ∉ F V (MP)) or μx.xM ∗ N (where x ∉ F V (M)) is called a β-redex. β-contracting an occurrence of a redex in a term U means replacing one occurence of

KMN  by M ,
(μx.M ∗ N)R by μx.MR ∗ NR (we α-convert (μx.M ∗ N) if necessary),
μx.[xMN/z]P ∗ Q by μx.[xM/z]P ∗ Q (where z ∈ F V (P) and x ∉ F V (MP)),
μx.xM ∗ N  by [M/x]N  (where x ∉ F V (M)).

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.

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

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

We can consider different types of reductions that have logical reasons, for example,

R(μx.M ∗ N) ⊳_{1} μx.RM ∗ RN.

But the reduction obtained from β-reduction adding the above reduction does not enjoy the Church-Rosser property.

ABBREVIATION 1.4 (λx.M) ≡ (μx.x ∗ KM).

FACT 1.5 (μ-calculus simulates λ-calculus)

(λx.M)N ⊳_{β} [M/x]N.

DEFINITION 1.6 (η-reduction) Any μ-term of form μx.x∗K(Nx) or μx.M ∗N (where x ∉ F V (N)) is called a η-redex. η-Contracting an occurrence of a η-redex in a term U means replacing one occurence of

μx.x ∗ K(Nx) by μx.x ∗ N ,
μx.M ∗ N  by N  (where x ∉ F V (N)) .

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.

CONJECTURE 1.7 (or FACT (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 1.8 (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),  {Π \atop M : β} ; KM : α → β (W eakening),

\begin{matrix}{k \atop x : α → β} ; Π_{1} ; M : γ & {k \atop x : α} ; Π_{2} ; N : γ \\ μx.M ∗ N : γ \end{matrix} k(Case).

FACT 1.9 (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 : α.

2 The type-free λA-calculus and its type assignment

We will next introduce an auxiliary type type-assignment system T A_{λA} to prove the subformula property of the system T A_{μ}.

DEFINITION 2.1 (λA-terms) An infinite sequence of term-variables is assmed to be given. Then linguistic expression called λA-terms are defined thus:

1. each term-variable is a λA-terms, called an atom or atomic term; 2. if M and N are λA-terms then (MN) is a λA-term called an application;

3. if M is a λA-term then AM is a λA-term called a r-weakening;

4. if x is a term-variable and M is a λA-terms then (λx.M) is a λA-term called an abstract or a λ-abstract.

DEFINITION 2.2 (Aβ-reduction) Any λA-term of form AMN and (λx.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. \end{matrix}

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

U ⊳_{1Aβ} V.

We say U Aβ-reduces to V, or

U ⊳_{Aβ} V,

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

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

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

A ⊥-type is a type constructed from variables and a type constant ’⊥’.

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

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

{Π \atop M : ⊥} ; AM : α (R − W eakening).

FACT 2.5 (T A_{λA} is a proof of intutionistic logic) α is a theorem of intutionistic {→, ⊥}-fragment logic if and only if there exists a closed λA-term M such that ⊢_{λA} M : α.

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

FACT 2.7 (Subformula Property for T A_{λA}) Let λA-term M be a Aβ-normal form and Δ a T A_{λA}- deduction of M : α. Then every type in Δ has an occurence in α or in a predicate of undischarged assumptions.

3 Transelation of λA-terms to μ-terms

In this section we will define a translation 𝒯 of λA-terms to μ-terms. At first, we define a simple translation 𝒯 ^{∗} of λA-terms without occurences of A to μ-terms.

DEFINITION 3.1 (Translation 𝒯 ^{∗}) We define recursively the translation 𝒯 ^{∗} of λA-terms, in which no A occurs, to μ-terms, as follows:

1. 𝒯 ^{∗}(x) ≡ x,

2. 𝒯 ^{∗}(MN) ≡ (𝒯 ^{∗}(M)𝒯 ^{∗}(N)),

3. 𝒯 ^{∗}(λx.M) ≡ (μx.x ∗ K𝒯 ^{∗}(M)).

DEFINITION 3.2 (Translation 𝒯 ) We define recursively the translation 𝒯 of λA-terms of the form AM to μ-terms, as follows:

1. 𝒯 (AM) ≡ 𝒯 ^{∗}(M) if no A occurs in N,

2. 𝒯 (AM) ≡ 𝒯 (AN) if M is of the form (⋯ AN ⋯) where this A is the leftmost occurence and no free variable in N is bounded in M,

3. 𝒯 (AM) ≡ μx.𝒯 (AN) ∗ 𝒯 (AR) if M is of the form (⋯ (λx. · · · AQ ⋯) ⋯) where this A is the leftmost occurence and this ’λx’ is the leftmost occurence which bounds a free variable in Q and N is obtained from M by replacing (λx. · · · AQ ⋯) by x (we α-convert M if necessary) and R ≡ (⋯ (λz. · · · AQ ⋯) ⋯) and the variable z is new.

4 Proof of Subformula Property

LEMMA 4.1 Let M be a Aβ-normal term without occurences A, Γ ⊢_{λA} M : α and g be a new type variable. Then

1. [g/⊥]Γ ⊢_{μ} 𝒯 ^{∗}(M) : [g/⊥]α,

2. every type in T A_{μ}-deduction of 𝒯 ^{∗}(M) : [g/⊥]α has an occurence in [g/⊥]α or in a type in [g/⊥]Γ.

LEMMA 4.2 Let AM be a Aβ-normal term, Γ ⊢_{λA} M : ⊥ and g be a new type variable. Then

1. [g/⊥]Γ ⊢_{μ} 𝒯 (AM) : g,

2. every type in T A_{μ}-deduction of 𝒯 (AM) : g is g or has an occurence in a type in [g/⊥]Γ.

LEMMA 4.3 Let α be a implicational formula and g be the rightmost variable in α. Then α is a classical teorem if and only if [⊥/g]α is an intuitionistic theorem.

THEOREM 4.4 (Subformula Property of T A_{μ}) If a type α is a classical implicational theorem, then there exists a closed μ-term M such that

1. ⊢_{μ} M : α,

2. for any T A_{μ}-deduction Δ of M : α, every type in Δ has an occurence in α.

Acknowledgement. The author would like to thank Ryo Kashima for informing him of Kashima’s Natural deduction system.

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.