Split of Classical Logic(draft)Tatsuya AbeFebruary 17, 2010∗

Abstract
Classical logic contains intuitionistic and paraconsistent logics. This study
clarifies that proofs in classical logic are not intricately interwined with intuitionistic and paraconsistent proofs, that is, there exists a constructive procedure ofextracting intuitionistic and paraconsistent proofs. Formally, this study claims thatfor any judgment in classical logic there exists some formula such that splits theclassical judgment into intuitionistic and paraconsistent ones.

1Introduction

This study deals with classical logic, the most primitive logic which has been studied
for a long time. While classical logic is the most immediate logic for us, it seems tohave something unknown yet. We dare to say that too elegance of classical logic is
one of the most difficulties to understand it. Although we believe that classical logic
has more remarkable and profound properties, we cannot notice many of them sinceclassical logic has such properties too naturally.
Intuitionistic logic is a fragment of classical logic (i.e., of less provability). Although intuitionistic logic is interesting itself, we use it as a tool of analyzing classicallogic in this study. The most discriminating difference between classical and intuitionistic logics is surely provability. The excluded middle ϕ ∨ ¬ ϕ can be proved in classicallogic, but cannot be done in intuitionistic logic. On the other hand, what is in common?
In this study, we focus on Glivenko’s theorem: if Γ derives contradiction in classicalpropositional logic if and only if so does Γ in intuitionistic propositional logic, whereΓ is a sequence of formulas.
Now, a natural question occurs. Does there exist a logic of provability (under noassumption) is the same as classical logic? Such a logic should be dual in a sense,for, it satisfies the statement dual to the one intuitionistic logic, i.e., co-Glivenko’s theorem. Such a dual intuitionistic logic is seen in [2, 3]. The dual intuitionistic logic
has the same provability (under no assumption) as the one of classical logic, but cannot derive contradiction from ¬ ϕ ∧ ϕ, dual to that intuitionistic logic cannot prove theexcluded middle. Therefore, the dual intuitionistic logic is sometimes called paraconsistent logic.
Classical logic contains intuitionistic and paraconsistent logics. Now, we would
like to raise the following two questions:∗ Revised: December 15, 20111

1. do intuitionistic and paraconsistent logics cover classical logic, and
2. are proofs in classical logic too scrambled to be constructively split into intuitionistic and paraconsistent proofs?
In this study, we answer yes to the former question and no to the latter.

2

Classical, Intuitionistic, and Paraconsistent Logics

First, we recall classical logic, Gentzen’s LK:ϕ`ϕΓ ` ∆, ϕϕ, Π ` Σ(cut)Γ, Π ` ∆, ΣΓ, ϕ, ψ, Π ` ∆Γ, ψ, ϕ, Π ` ∆Γ ` ∆, ϕ, ψ, Σ
Γ ` ∆, ψ, ϕ, Σϕ, ϕ, Γ ` ∆ϕ, Γ ` ∆Γ ` ∆, ϕ, ϕ
Γ ` ∆, ϕΓ`∆ϕ, Γ ` ∆Γ`∆Γ ` ∆, ϕΓ ` ∆, ϕ¬ ϕ, Γ ` ∆ϕ, Γ ` ∆Γ ` ∆, ¬ ϕ

ϕ, Γ ` ∆ϕ ∧ ψ, Γ ` ∆ψ, Γ ` ∆ϕ ∧ ψ, Γ ` ∆Γ ` ∆, ϕΓ ` ∆, ψΓ ` ∆, ϕ ∧ ψϕ, Γ ` ∆ψ, Γ ` ∆ϕ ∨ ψ, Γ ` ∆Γ ` ∆, ϕΓ ` ∆, ϕ ∨ ψΓ ` ∆, ψΓ ` ∆, ϕ ∨ ψΓ ` ∆, ϕψ, Π ` Σϕ ⊃ ψ, Γ, Π ` ∆, Σϕ, Γ ` ∆, ψΓ ` ∆, ϕ ⊃ ψϕ(a), Γ ` ∆∀x.ϕ(x), Γ ` ∆Γ ` ∆, ϕ(a)(∗)Γ ` ∆, ∀x.ϕ(x)ϕ(a), Γ ` ∆(∗)∃x.ϕ(x), Γ ` ∆Γ ` ∆, ϕ(a)Γ ` ∆, ∃x.ϕ(x)where a does not occur in Γ, ∆, and ϕ(x) at (∗). The so-called eigenvariable conditionis satisfied. Note that any language and logic in this paper does not contain > and ⊥.
We also recall that ϕ ⊃ ψ is equivalent to ¬ ϕ ∨ ψ in LK.
Next, we recall intuitionistic logic, Gentzen’s LJ. The intuitionistic logic is derived
from being restricted its judgments’ succedents to consisting of at most one formulawhere the inference rules of ⊃ are replaced byΓ`ϕψ, Π ` Σ(⊃ `I )ϕ ⊃ ψ, Γ, Π ` Σϕ, Γ ` ψ(`I ⊃)Γ`ϕ⊃ψ.

In LJ, ϕ ⊃ ψ is known to be inequivalent to ¬ ϕ ∨ ψ.
Here, we add a logical connective ⊂ and the following inference rules:2Γ`ψ(⊂ `I )ϕ ⊂ ψ, Γ `ϕ, Γ ` ∆(⊂ `I )ϕ ⊂ ψ, Γ ` ∆Γ`ϕψ, Π `(`I ⊂) .
Γ, Π ` ϕ ⊂ ψ
We call classical and intuitionistic logics in this paper C and I, respectively, foravoiding confusion with Gentzen’s original LK and LJ. I is also called LJ−̇ in [3].
ϕ ⊂ ψ is just a syntax sugar of ϕ ∧ ¬ ψ (sometimes called the but not connective) in
C and I, i.e., these sequent calculi are definitional extensions as follows,Proposition 2.1. The judgment ϕ, ¬ ψ `I ϕ ⊂ ψ is derivable.
Readers may think it useless to add ⊂ since it is just a syntax sugar. However, it isindeed not! We give a paraconsistent logic P dual to I at the end in the section. The dualcorrespondence (seen in [1]) maps formulas out of intuitionistic logic in derivability.
But the dual correspondence cannot map formulas outside in the sense of language if
we introduce ⊂. This is the reason for adding ⊂.
Finally, we define a paraconsistent logic. Similarly to the intuitionistic logic, theparaconsistent logic is derived from being restricted its judgments’ antecedents to consisting of at most one formula where the inference rules of ⊃ and ⊂ are as follows,` Γ, ϕψ`∆(⊃ `P )ϕ ⊃ ψ ` Γ, ∆ϕ`∆(`P ⊃)` ∆, ϕ ⊃ ψΓ ` ∆, ψ(`P ⊃)Γ ` ∆, ϕ ⊃ ψϕ ` ∆, ψ(⊂ `P )ϕ⊂ψ`∆Γ ` ∆, ϕψ`Σ(`P ⊂)Γ ` ∆, Σ, ϕ ⊂ ψ.

We call this paraconsistent logic P (called LDJ−̇ in [3]).
Similarly, ϕ ⊃ ψ is a syntax sugar of ¬ ϕ ∨ ψ in P as follows,Proposition 2.2. The judgment ϕ ⊃ ψ `P ¬ ϕ, ψ is derivable.

3Split

The following is the main theorem in this study.
Theorem 3.1. Any judgment in classical logic has a splitter. That is, if Γ `C ∆ isderivable, then there exists ϕ such that Γ `I ϕ and ϕ `P ∆ are cut-freely1 derivable.
Proof. By induction on derivation and case analysis of the last inference rule.
(cut). First, we check it the so-called cut-rule:Γ `C ∆, ϕϕ, Π `C ΣΓ, Π `C ∆, Σ
By induction hypothesis, there exist χ and υ such that
Γ `I χ,χ `P ∆, ϕ,ϕ, Π `I υ,andυ `P Σare derivable. Then,1 Kojima suggests that the theorem in the original version (without referring to the cut-freedom) is trivial.

3χ `P ∆, ϕ`P ∆, χ ⊃ ϕυ `P Σ(χ ⊃ ϕ) ⊃ υ `P ∆, ΣΓ `I χϕ, Π `I υχ ⊃ ϕ, Γ, Π `I υΓ, Π `I (χ ⊃ ϕ) ⊃ υ

are derivable. Hence, we check it in the case of the cut-rule. In the following, we show
derivations only.

(¬).

Proposition 2.1
I.H.
Γ `I ψψ, ¬ ϕ `I ψ ⊂ ϕψ ⊃ ψ, Γ, ¬ ϕ `I ψ ⊂ ϕΓ, ¬ ϕ `I (ψ ⊃ ψ) ⊃ ψ ⊂ ϕ¬ ϕ, Γ `I (ψ ⊃ ψ) ⊃ (ψ ⊂ ϕ)

ψ `P ψψ `P ψ ⊃ ψI.H.
ψ `P ∆, ϕ`P ψ ⊃ ψ, ψ ⊃ ψ`P ψ ⊃ ψψ ⊂ ϕ `P ∆(ψ ⊃ ψ) ⊃ (ψ ⊂ ϕ) `P ∆ψ `I ψψ ⊂ ψ `I ψI.H.
ϕ, Γ `I ψψ ⊂ ψ, ψ ⊂ ψ `IΓ `I ϕ ⊃ ψψ ⊂ ψ `I
Γ `I (ϕ ⊃ ψ) ⊂ (ψ ⊂ ψ)

Proposition 2.2
I.H.
ϕ ⊃ ψ `P ¬ ϕ, ψψ `P ∆ϕ ⊃ ψ `P ¬ ϕ, ∆, ψ ⊂ ψ(ϕ ⊃ ψ) ⊂ (ψ ⊂ ψ) `P ¬ ϕ, ∆(ϕ ⊃ ψ) ⊂ (ψ ⊂ ψ) `P ∆, ¬ ϕI.H.
ϕ `I ϕψ, Π `I υϕ ⊃ ψ, ϕ, Π `I υI.H.
ϕ, ϕ ⊃ ψ, Π `I υ(⊃). Γ `I χχ ⊃ ϕ, Γ, ϕ ⊃ ψ, Π `I υΓ, ϕ ⊃ ψ, Π `I (χ ⊃ ϕ) ⊃ υϕ ⊃ ψ, Γ, Π `I (χ ⊃ ϕ) ⊃ υI.H.
χ `P ∆, ϕχ `P ∆, χ ⊃ ϕ`P ∆, χ ⊃ ϕ, χ ⊃ ϕ
I.H.
`P ∆, χ ⊃ ϕυ `P Σ(χ ⊃ ϕ) ⊃ υ `P ∆, Σϕ `P ϕ
I.H.
χ `P ∆, ψ`P ϕ, ϕ ⊃ ψ`P ϕ ⊃ ψ, ϕ
χ `P ∆, ϕ ⊃ ψϕ ⊃ χ `P ϕ ⊃ ψ, ∆, ϕ ⊃ ψI.H.
ϕ, Γ `I χΓ `I ϕ ⊃ χϕ ⊃ χ `P ∆, ϕ ⊃ ψ(∃).

I.H.
ϕ(a), Γ `I ψ(a)ϕ(a), Γ `I ∃x.ψ(x)(∗)∃x.ϕ(x), Γ `I ∃x.ψ(x)I.H.
ψ(a) `P ∆(∗)∃x.ψ(x) `P ∆I.H.
Γ `I ψI.H.
ψ `P ∆, ϕ(a)ψ `P ∆, ∃x.ϕ(x)where remark the eigenvariable condition at (∗).
The other cases are similar or trivial. That is, it is sufficient to consider dual derivations and splitters, e.g., ⊂’s ones are dual to ⊃’s ones. Therefore, we omit the details.
We conclude this paper with the following three remarks.
The splitters are the so-called cut-formulas, and the cut-rules are lowered to thebottom judgment in derivation. This is the converse to cut-elimination that uppers all
the cut-formulas in derivation to the top judgments in derivation.
4

In classical logic, the connective ⊃ is just a syntax sugar in provability. However, inintuitionistic logic (a weaker logic than classical logic) ϕ ⊃ ψ is not equivalent to ¬ ϕ ∨ψ, and the connective ⊃ shows its original character to us. Similarly, the connective ⊂(out of many logicians’ main interest) also shows its character by being located at notclassical and intuitionistic logics but paraconsistent logic. In this study, we clarify thatany judgment in classical logic can be split into intuitionistic and paraconsistent ones
using the full connectives containing ⊂.
In giving a proof of a theorem, we usually think that any proof in intuitionistic
logic becomes that in classical logic when we use reductio ad absurdum. However,this study claims that P suffices the inferences after reductio ad absurdum in C. That is,
this study clarifies that C is a hybrid of I and P, and exactly one time suffices switchingof logics in number.
Acknowledgment.

The author thanks Kensuke Kojima for the suggestion.

References[1] J. Czermak. A remark on Gentzen’s calculus of sequents. Notre Dame Journal ofFormal Logic, 18(3):471–474, 1977.
[2] N. D. Goodman. The logic of contradiction. Zeitschrift für mathematische Logik
und Grundlagen der Mathematik, 27:119–126, 1981.
[3] I. Urbas. Dual-intuitionistic logic.
37(3):440–451, 1996.

Notre Dame Journal of Formal Logic,

5