Skip to main content
Top

2017 | OriginalPaper | Chapter

A Reconstruction of Ex Falso Quodlibet via Quasi-Multiple-Conclusion Natural Deduction

Authors : Yosuke Fukuda, Ryosuke Igarashi

Published in: Logic, Rationality, and Interaction

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

This paper is intended to offer a philosophical analysis of the propositional intuitionistic logic formulated as \(\textit{NJ}\). This system has been connected to Prawitz and Dummett’s proof-theoretic semantics and its computational counterpart. The problem is, however, there has been no successful justification of ex falso quodlibet (EFQ): “From the absurdity ‘\(\bot \)’, an arbitrary formula follows.” To justify this rule, we propose a novel intuitionistic natural deduction with what we call quasi-multiple conclusion. In our framework, EFQ is no longer an inference deriving everything from ‘\(\bot \)’, but rather represents a “jump” inference from the absurdity to the other possibility.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
There is another formalization by using second-order propositional logic, but it seems that the formalization has the same problem.
 
2
At this point, our system avoids the problem of multiple conclusion pointed out by Dummett [2]. However, we will not go further into this debate.
 
3
An intuition behind here is Tennant’s remark [17]: “‘\(\bot \)’ represents a logical deadend, and thus there are no further inferences after it appears within deductions.”
 
4
In this sense, this rule is not well expressed its name, i.e., “from contradiction, anything” (ex falso quodlibet). In the following, however, we will continue to use this name for the sake of simplicity.
 
5
We recommend some text (e.g., Sørensen and Urzyczyn’s [15]) for people who are not familiar with these definitions, although the precise one is determined by Definition 6.
 
6
\(L'_{c/t}\) was named as \(L_{c/t}\) in their paper, which is the same name as Nakano’s calculus. In this paper, we use \(L'_{c/t}\) to denote Kameyama and Sato’s calculus.
 
7
It is equal to say, also through the Curry–Howard correspondence, that: “if \( \varGamma \vdash \bot \) holds in \(\textit{NJ}\), then the proof must depend on some assumption consisted of ‘\(\bot \)’.”
 
8
A term M is said to be in normal form if there is no further reduction from M.
 
Literature
2.
go back to reference Dummett, M.: The Logical Basis of Metaphysics. Harvard University Press, Cambridge (1991) Dummett, M.: The Logical Basis of Metaphysics. Harvard University Press, Cambridge (1991)
3.
go back to reference Dummett, M.: Elements of Intuitionism. Oxford Logic Guides. Clarendon Press, Oxford (2000)MATH Dummett, M.: Elements of Intuitionism. Oxford Logic Guides. Clarendon Press, Oxford (2000)MATH
4.
go back to reference Griffin, T.G.: A formulae-as-type notion of control. In: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 47–58 (1990) Griffin, T.G.: A formulae-as-type notion of control. In: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 47–58 (1990)
6.
go back to reference Kameyama, Y., Sato, M.: Strong normalizability of the non-deterministic catch/throw calculi. Theor. Comput. Sci. 272(1–2), 223–245 (2002)MathSciNetCrossRefMATH Kameyama, Y., Sato, M.: Strong normalizability of the non-deterministic catch/throw calculi. Theor. Comput. Sci. 272(1–2), 223–245 (2002)MathSciNetCrossRefMATH
9.
go back to reference Nakano, H.: Logical structures of the catch and throw mechanism. Ph.D. thesis, The University of Tokyo (1995) Nakano, H.: Logical structures of the catch and throw mechanism. Ph.D. thesis, The University of Tokyo (1995)
10.
go back to reference Onishi, T.: Proof-theoretic semantics and bilateralism. Ph.D. thesis, Kyoto University (2012). (Written in Japanese) Onishi, T.: Proof-theoretic semantics and bilateralism. Ph.D. thesis, Kyoto University (2012). (Written in Japanese)
11.
go back to reference Parigot, M.: \(\uplambda \upmu \)-Calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992). doi:10.1007/BFb0013061 CrossRef Parigot, M.: \(\uplambda \upmu \)-Calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992). doi:10.​1007/​BFb0013061 CrossRef
13.
go back to reference Prawitz, D.: Pragmatist and verificationist theories of meaning. In: Auxier, R.E., Hahn, L.E. (eds.) The Philosophy of Michael Dummett. Open Court Publishing Company (2007) Prawitz, D.: Pragmatist and verificationist theories of meaning. In: Auxier, R.E., Hahn, L.E. (eds.) The Philosophy of Michael Dummett. Open Court Publishing Company (2007)
15.
go back to reference Sørensen, H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier, Amsterdam (2006)MATH Sørensen, H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier, Amsterdam (2006)MATH
16.
go back to reference Steele, G.L.: Common LISP: The Language, 2nd edn. Digital Press, Newton (1990)MATH Steele, G.L.: Common LISP: The Language, 2nd edn. Digital Press, Newton (1990)MATH
17.
go back to reference Tennant, N.: Negation, Absurdity and Contrariety. In: Gabbay, D.M., Wansing, H. (eds.) What is Negation?, pp. 199–222. Springer, Dordrecht (1999)CrossRef Tennant, N.: Negation, Absurdity and Contrariety. In: Gabbay, D.M., Wansing, H. (eds.) What is Negation?, pp. 199–222. Springer, Dordrecht (1999)CrossRef
18.
go back to reference Tranchini, L.: The role of negation in proof-theoretic semantics: a proposal. Fuzzy Logics Interpret. Logics Resour. 9, 273–287 (2008) Tranchini, L.: The role of negation in proof-theoretic semantics: a proposal. Fuzzy Logics Interpret. Logics Resour. 9, 273–287 (2008)
19.
go back to reference van Dalen, D.: Kolmogorov and Brouwer on constructive implication and the Ex Falso rule. Russ. Math. Surv. 59(2), 247–257 (2004)CrossRef van Dalen, D.: Kolmogorov and Brouwer on constructive implication and the Ex Falso rule. Russ. Math. Surv. 59(2), 247–257 (2004)CrossRef
Metadata
Title
A Reconstruction of Ex Falso Quodlibet via Quasi-Multiple-Conclusion Natural Deduction
Authors
Yosuke Fukuda
Ryosuke Igarashi
Copyright Year
2017
Publisher
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-55665-8_38

Premium Partner