Skip to main content

2017 | OriginalPaper | Buchkapitel

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

verfasst von : Yosuke Fukuda, Ryosuke Igarashi

Erschienen in: Logic, Rationality, and Interaction

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Fußnoten
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.
 
Literatur
2.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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
8.
9.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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
Metadaten
Titel
A Reconstruction of Ex Falso Quodlibet via Quasi-Multiple-Conclusion Natural Deduction
verfasst von
Yosuke Fukuda
Ryosuke Igarashi
Copyright-Jahr
2017
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-55665-8_38