A Reconstruction of Ex Falso Quodlibet via
Quasi-Multiple-Conclusion Natural Deduction
Yosuke Fukuda1 and Ryosuke Igarashi2
1 Graduate School of Informatics, Kyoto Univeristy, Japan
2 Graduate School of Letters, Kyoto University, Japan

LORI VI, September 12th, 2017

1 / 30Ex Falso Quodlibet
Ex Falso Quodlibet (EFQ) is a logical principle which states that:“From the absurdity ‘⊥’, an arbitrary formula A follows”
Boolean Algebra
AF
FTT

BFTFT Natural Deduction
A⊃BTTFT⊥ EFQA

It is now standard to view EFQ as a valid form of inference.
However, how can we believe that this principle is “valid”?

2 / 30Ex Falso Quodlibet
Ex Falso Quodlibet (EFQ) is a logical principle which states that:“From the absurdity ‘⊥’, an arbitrary formula A follows”Boolean Algebra
AF
FTT



BF
TFT

 Natural Deduction


A⊃B
T
TFT



⊥ EFQA

It is now standard to view EFQ as a valid form of inference.
However, how can we believe that this principle is “valid”?

2 / 30Ex Falso Quodlibet
Ex Falso Quodlibet (EFQ) is a logical principle which states that:“From the absurdity ‘⊥’, an arbitrary formula A follows”
Boolean Algebra
AFFTTBFTFT Natural Deduction

A⊃BTTFT⊥ EFQA

It is now standard to view EFQ as a valid form of inference.
However, how can we believe that this principle is “valid”?

2 / 30Our work

Aim To give an intuitive understanding of EFQ
Idea To combine two ideas from logic and computation:
1 “ ‘⊥’ is a logical dead-end in deductions” [Tennant ‘99]
2 The catch/throw mechanism [Nakano ‘94]
Result In our framework, EFQ can be viewed as:“a jump inference from a dead-end to other possibilites”

3 / 30Outline

1 Background: Meaning theory for formal logic
2 Several validations to EFQ and their problems
3 Our quasi-multiple-conclustion natural deduction: NQ
4 The corresponding typed λ-calculus: λNQ

4 / 30Outline

1 Background: Meaning theory for formal logic
2 Several validations to EFQ and their problems
3 Our quasi-multiple-conclustion natural deduction: NQ
4 The corresponding typed λ-calculus: λNQ

5 / 30How to define a formal deductive system?

To define a formal deductive system, one has to consider that:“How to define mathematical proofs as mathematical entities?”“How can we believe that a mathematical inference is correct?”6 / 30Meaning of mathematical statements“The meaning of a mathematicalstatement determines and is exhaustively determined by its ‘use’.
( The Philosophical Basis of Intuitionistic Logic, 1973 )”Michael Dummett

7 / 30One answer: Natural Deduction [Gentzen ‘34]
The meaning of inference rules of N.D. is determined by their “use”
The conjucntion rules as syntactic operations

AB∧IA∧BA ∧ B ∧ELAA ∧ B ∧ERB

Its “use” lets us know the meaning: the commutativity of ‘∧’A ∧ B ∧EA ∧ B ∧EL
R
B
A
∧IB∧A






8 / 30One answer: Natural Deduction [Gentzen ‘34]
The meaning of inference rules of N.D. is determined by their “use”
The conjucntion rules as syntactic operations

AB∧IA∧BA ∧ B ∧EL
AA ∧ B ∧ERB

Its “use” lets us know the meaning: the commutativity of ‘∧’

A ∧ B ∧EA ∧ B ∧ELRBA∧IB∧A


8 / 30Problematic connective: tonk [Prior ‘60]



The inference rules of tonk
Atonk-I
A tonk B

A tonk B
tonk-EB

tonk-I is equivalent to ∨I
tonk-E is equivalent to ∧E

An undesirable proof of “everything”[X ]⊃IX ⊃X
tonk-I(X ⊃ X ) tonk Y
tonk-EY
9 / 30Problematic connective: tonk [Prior ‘60]



The inference rules of tonk
Atonk-I
A tonk BA tonk B
tonk-EB

tonk-I is equivalent to ∨I
tonk-E is equivalent to ∧EAn undesirable proof of “everything”[X ]⊃IX ⊃X
tonk-I(X ⊃ X ) tonk Y
tonk-EY
9 / 30Gentzen’s explanatation of logical connectives“The introduction rules represent,
as it were, the definition of thesymbol concerned, and the elimination rules are no more, in the
final analysis, than the consequences of these definitions.
( Investigations into Logical Inference, 1935 )Gerhard Gentzen”
10 / 30Harmony [Dummett ‘91][Pfenning&Davies ‘00]

Harmony Any consequence of a compound statement must bederived from its premises. Verified by local reductionΠ0Π1Π0AB∧I →A ∧ B ∧EAL
AThanks to the harmony, we can say that tonk is invalid

11 / 30

Outline

1 Background: Meaning theory for formal logic
2 Several validations to EFQ and their problems
3 Our quasi-multiple-conclustion natural deduction: NQ
4 The corresponding typed λ-calculus: λNQ

12 / 30

Several previous validations to EFQ

Several validations to EFQ have been proposed so far:
[Prawitz ‘07]: “There is no I-rule for ‘⊥’ ”
defSecond-order prop. logic validation: “⊥ = ∀A.A”[Dummett ‘91]: By the harmonious I-rule for ‘⊥’
Well-known validation: By the so-called disjunctive syllogism
However, all of these validation have an inadequacy

13 / 30

Dummett’s Validation to EFQ [Dummett ‘91]
Dummett introduced an I-rule for ‘⊥’ so as to achieve “harmony”
The “infinitary” I-rule for ⊥p0p1

p2···⊥⊥I

Harmony between ⊥I and ⊥EΠ0p0···

Πipi
⊥
pi ⊥E

···

⊥I

⇒Πipi

Problem:
We have to admit such “infinitary” deduction;
This does not explain why “ ‘⊥’ is what infers everything”
14 / 30

Dummett’s Validation to EFQ [Dummett ‘91]
Dummett introduced an I-rule for ‘⊥’ so as to achieve “harmony”
The “infinitary” I-rule for ⊥p0p1p2···

⊥

⊥I


Harmony between ⊥I and ⊥EΠ0p0···

Πipi⊥pi ⊥E

···

⊥I

⇒

Πipi

Problem:
We have to admit such “infinitary” deduction;
This does not explain why “ ‘⊥’ is what infers everything”
14 / 30

Dummett’s Validation to EFQ [Dummett ‘91]
Dummett introduced an I-rule for ‘⊥’ so as to achieve “harmony”
The “infinitary” I-rule for ⊥
p0

p1

p2···

⊥




⊥I



Harmony between ⊥I and ⊥EΠ0p0···

Πipi
⊥
pi ⊥E



···

⊥I



⇒

Πipi


Problem:
We have to admit such “infinitary” deduction;
This does not explain why “ ‘⊥’ is what infers everything”
14 / 30

Validation via Disjuctive Syllogism
According to [Priest ‘02], EFQ is historically validated by:
Disjunctive Syllogism
X ∨YY¬XDS

Disjuctive Syllogism implies the Ex Falso rule⊥∨IL⊥∨AA






[⊥]
⊥
¬I
¬⊥
DS


This validation is quite good, but DS does not fit Gentzen’s spirit

15 / 30

Validation via Disjuctive Syllogism
According to [Priest ‘02], EFQ is historically validated by:
Disjunctive Syllogism
X ∨YY¬XDS

Disjuctive Syllogism implies the Ex Falso rule⊥∨IL⊥∨AA[⊥]⊥
¬I
¬⊥
DS


This validation is quite good, but DS does not fit Gentzen’s spirit

15 / 30

Validation via Disjuctive Syllogism
According to [Priest ‘02], EFQ is historically validated by:
Disjunctive Syllogism
X ∨Y




Y

¬X

DS

Disjuctive Syllogism implies the Ex Falso rule⊥
∨IL
⊥∨AA






[⊥]
⊥
¬I
¬⊥
DS


This validation is quite good, but DS does not fit Gentzen’s spirit

15 / 30

Outline

1 Background: Meaning theory for formal logic
2 Several validations to EFQ and their problems
3 Our quasi-multiple-conclustion natural deduction: NQ
4 The corresponding typed λ-calculus: λNQ

16 / 30

Our key observation and how ‘⊥’/EFQ work
Our obs.: EFQ is only used for “disjunctive syllogism”-like proofs
An informal proof of the disjunctive syllogism: “X ∨ Y , ¬X ` Y ”
1We have X ∨ Y , that is, two possibilites that X or Y holds.

2Firstly, focus on X . Considering that we also have ¬X , ‘⊥’follows and hence this is not the case.

3

Therefore, Y holds.

This underlined inference is usually interpreted by depending on:“ ‘⊥’ is what infers everything”
but an important point here is that:
there seems to be a “global” relevance in the last two steps
17 / 30

Our key observation and how ‘⊥’/EFQ work
Our obs.: EFQ is only used for “disjunctive syllogism”-like proofs
An informal proof of the disjunctive syllogism: “X ∨ Y , ¬X ` Y ”
1

We have X ∨ Y , that is, two possibilites that X or Y holds.

2Firstly, focus on X . Considering that we also have ¬X , ‘⊥’follows and hence this is not the case.

3Therefore, Y holds.

This underlined inference is usually interpreted by depending on:“ ‘⊥’ is what infers everything”
but an important point here is that:
there seems to be a “global” relevance in the last two steps
17 / 30

Our key observation and how ‘⊥’/EFQ work
Our obs.: EFQ is only used for “disjunctive syllogism”-like proofs
An informal proof of the disjunctive syllogism: “X ∨ Y , ¬X ` Y ”
1

We have X ∨ Y , that is, two possibilites that X or Y holds.

2Firstly, focus on X . Considering that we also have ¬X , ‘⊥’follows and hence this is not the case.

3

Therefore, Y holds.

This underlined inference is usually interpreted by depending on:“ ‘⊥’ is what infers everything”
but an important point here is that:
there seems to be a “global” relevance in the last two steps
17 / 30

Our key observation and how ‘⊥’/EFQ work
Our obs.: EFQ is only used for “disjunctive syllogism”-like proofs
An informal proof of the disjunctive syllogism: “X ∨ Y , ¬X ` Y ”
1We have X ∨ Y , that is, two possibilites that X or Y holds.

2Firstly, focus on X . Considering that we also have ¬X , ‘⊥’follows and hence this is not the case.

3Therefore, Y holds.

This underlined inference is usually interpreted by depending on:“ ‘⊥’ is what infers everything”
but an important point here is that:
there seems to be a “global” relevance in the last two steps
17 / 30

Our Quasi-Multiple-Conclusion Natural Deduction NQ
We introduce our intuitionistic natural deduction NQ, based on
Nakano’s constructive minimal logic [Nakano ‘94]
Definition (Formulae)
A, B ::= p | ⊥ | A ∨ B | A ∧ B | A ⊃ BDefinition (Judgment [Nakano ‘94][Maehara ‘54])
A judgment of NQ , quasi-multiple-coclusion judgment, is a triple:Γ ` A; ∆where A is a formula; each of Γ and ∆ is a multi-set of formulae

18 / 30

An intuitive meaning of judgment

For a judgment Γ ` A; ∆, the conclusion “A; ∆” expresses that:
we are now “focusing” on a possibility A in reasoning proecss;
and “putting aside” the other possibilities to ∆Remark: The “constructive” meaning of judgment
Γ ` A; ∆ means that: “From the constructions of Γ, there exists atleast one construction of the formula of {A} ∪ ∆”19 / 30

An intuitive meaning of judgment

For a judgment Γ ` A; ∆, the conclusion “A; ∆” expresses that:
we are now “focusing” on a possibility A in reasoning proecss;
and “putting aside” the other possibilities to ∆Remark: The “constructive” meaning of judgment
Γ ` A; ∆ means that: “From the constructions of Γ, there exists atleast one construction of the formula of {A} ∪ ∆”19 / 30

EFQ as an “jump” inference

Following [Tennant ‘99]’s remark s.t. “ ‘⊥’ is a logical dead-end”,
we formalize EFQ in our NQ by:Γ ` ⊥; A, ∆Γ ` A; ∆Therefore EFQ in our formalization is …
is no longer the inference deriving everything from ‘⊥’; but rather,represents a “jump” from a dead-end ‘⊥’ to the other possibility A

20 / 30

EFQ as an “jump” inference

Following [Tennant ‘99]’s remark s.t. “ ‘⊥’ is a logical dead-end”,
we formalize EFQ in our NQ by:Γ ` ⊥; A, ∆Γ ` A; ∆Therefore EFQ in our formalization is …
is no longer the inference deriving everything from ‘⊥’; but rather,represents a “jump” from a dead-end ‘⊥’ to the other possibility A20 / 30

Example: A proof of disjunctive syllogism

Theorem (Disjunctive Syllogism)¬A, A ∨ B ` B; ∅ is derivable
Proof.
By the following derivation:
Ax
A ∨ B ` A ∨ B; ∅∨E 0Ax¬A ` ¬A; ∅A ∨ B ` A; B
⊃E
¬A, A ∨ B ` ⊥; B
EFQ
¬A, A ∨ B ` B; ∅21 / 30

Property of NQ

Our NQ logically corresponds to NJ as follows:
Theorem (Soundness and completeness w.r.t. NJ)
The followings are equivalent:Γ `NQ A; ∆W
Γ `NJ ({A} ∪ ∆),However, we can not yet conclude that NQ is a “good” system

22 / 30

Property of NQ

Our NQ logically corresponds to NJ as follows:
Theorem (Soundness and completeness w.r.t. NJ)
The followings are equivalent:Γ `NQ A; ∆W
Γ `NJ ({A} ∪ ∆),However, we can not yet conclude that NQ is a “good” system

22 / 30

What is a “good” deductive system?

It is hard to say that some system is good in a general way, but
Dummett proposed a criterion, called harmony [Dummett ‘91]
The notion of harmony is roughly summarized as follows:
Reducibility of proof detour
Normalizability of deduction
and these can be captured by the Curry–Howard correspondence

23 / 30

What is a “good” deductive system?

It is hard to say that some system is good in a general way, but
Dummett proposed a criterion, called harmony [Dummett ‘91]
The notion of harmony is roughly summarized as follows:
Reducibility of proof detour
Normalizability of deduction
and these can be captured by the Curry–Howard correspondence

23 / 30

Outline

1 Background: Meaning theory for formal logic
2 Several validations to EFQ and their problems
3 Our quasi-multiple-conclustion natural deduction: NQ
4 The corresponding typed λ-calculus: λNQ

24 / 30

Background: The Curry–Howard correspondence
The Curry–Howard correspondence [Curry ‘34][Howard ‘69] isa general correspondence between logic and computation:
Deductive Systemformuladerivation
proof normalizationComputational Model
type
well-typed term
term reduction

Π0
Π1
Γ`M:A
Γ`N :B∧IΓ ` hM, N i : A ∧ B∧ELΓ ` πL hM, N i : A

Term Reduction of PairΠ0Γ`M:A

25 / 30

Background: The Curry–Howard correspondence
The Curry–Howard correspondence [Curry ‘34][Howard ‘69] isa general correspondence between logic and computation:Deductive Systemformuladerivation
proof normalization
Computational Model
type
well-typed term
term reduction

Π0
Π1
Γ`M:A
Γ`N :B∧IΓ ` hM, N i : A ∧ B∧ELΓ ` πL hM, N i : A

Term Reduction of Pair

Π0
Γ`M:A

25 / 30

The Corresponding Typed λ-Calculus: λNQ
We introduce our calculus, λNQ , an extension of [Nakano ‘94]Definition (Term/Judgment)(Term)M, N , L ::= x | λx.M | MN | hM, N i | πL M | πR M | ιL M | ιR M
| case M of [x]N or [y]L | u | throw u M | catch u M(Judg.) Γ ` M : A; ∆Reduction examples
1

πL hM, N iM

2catch u (πL hM, (throw u N )i)

N

Theorem (The Curry–Howard Correspondence)1

Γ `NQ A; ∆ iﬀ Γ `λNQ M : A; ∆ for some M

2

NQ’s proof normalization corresponds to λNQ ’s reduction
26 / 30

Example: A Typing of Disjunctive Syllogism

Axy B ` y B;
Π1Ax BThrowΓ0 ` N A∨B ; x A ` x A ;y ` (throw u y)A ; u BΠ0∨EΓ ` M¬A ;Γ0 ` (case N of [x]x or [y](throw u y))A ; u B⊃EΓ, Γ0 ` (M(case N of [x]x or [y](throw u y)))⊥ ; u BEFQ
Γ, Γ0 ` (catch u (M(case N of [x]x or [y](throw u y))))B ;27 / 30

The computational behaviour of EFQ
The computational behaviour can be described by case analysis:
1If N ≡ ιR (L) s.t. L’s type is B:catch u (M(case (ιR (L)) of [x]x or [y](throw u y)))catch u (M(throw u L))
L2

If N ≡ ιL (L) s.t. L’s type is A:
catch u (M(case (ιL (L)) of [x]x or [y](throw u y)))catch u (ML). . . (stuck)

28 / 30

Properties
The followings gurantee the well-definedness of NQ
Theorem (Subject reduction)
If Γ ` M : A; ∆ and M

M0 , then Γ ` M0 : A; ∆Theorem (Strong normalization)
For every typable term M, there is no infinite reduction sequence
starting from M
Thanks to the above theorems, we can finally achieve the harmony:
Corollary (Harmony)
All the logical rules of NQ are in “harmony”

29 / 30

Conclusion and Future work

Conclusion: We have proposed NQ to reconstruct EFQ
In our NQ , EFQ is no longer the inference deriving everything,but is a jump inference from ‘⊥’ to the other possibilities
The justification of NQ is given by λNQ so as to achieve harmony
The work indicates the single-conclusion N.D. is not enough tocapture the reasoning structures of I.L.

Future work: It is interesting as a further direction to …
To investigate a gap between our system and classical logic
To investigate a relationship with relevance logic
To establish a meaning theory through computational models

30 / 30

Appendix

31 / 30

Another Problematic Connective: “poor” conjunction“poor” conjunction
AB ♥I
A♥B
♥EA♥BA♥I is equivalent to ∧I♥E is equivalent to ∧EL

32 / 30

Stability [Dummett ‘91][Pfenning&Davies ‘00]

Stability The elimination rule must be as “strong” as possible.
Achieved by local expansion.
ΠΠΠA
∧
BA
∧ B ∧E→∧ELRA∧BAB∧IA∧B
Thanks to the stability, we can invalidate the poor conjunction

33 / 30

A problem of disjunction rules

Similar to EFQ, the usual I-rules of disjuction has a problem, as
mental logicians and relevant logicians discussed
The disjunction rules produces an artbitary formulaΓ ` A ∨IL
Γ`A∨B

Γ`B
∨IR
Γ`A∨B





34 / 30

Example: Reconstruction of disjunction

Theorem (Another formalization of disjunction)
The following I- and E-rules for disjunction are derivable:Γ ` A; B, ∆Γ ` A ∨ B; ∆∨I 0∨E 0Γ ` A ∨ B; ∆Γ ` A; B, ∆By the following derivations, respectively:Γ ` A; B, ∆∨ILAx
Γ ` A ∨ B; B, ∆B ` B; ∅ExAxThrowΓ ` B; A ∨ B, ∆Γ ` A ∨ B; ∆ A ` A; ∅B ` A; B∨IR∨EΓ ` A ∨ B; A ∨ B, ∆Γ ` A; B, ∆CatchΓ ` A ∨ B; ∆where Ex is a derivable rule

35 / 30

Inference rules of NQ and λNQ
NQ’s inference rulesΓ ` ⊥; A, ∆Γ ` A; A, ∆Γ ` A; ∆EFQCatchThrowΓ ` A; ∆Γ ` A; ∆Γ ` B; A, ∆

λNQ ’s typing rulesΓ ` M : ⊥; u : A, ∆EFQΓ ` catch u M : A; ∆Γ ` M : A; u : A, ∆CatchΓ ` catch u M : A; ∆Γ ` M : A; ∆ThrowΓ ` throw u M : B; u : A, ∆36 / 30