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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 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.
- 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.
References
Cook, R.T., Cogburn, J.: What negation is not: intuitionism and ‘0=1’. Analysis 60(265), 5–12 (2000)
Dummett, M.: The Logical Basis of Metaphysics. Harvard University Press, Cambridge (1991)
Dummett, M.: Elements of Intuitionism. Oxford Logic Guides. Clarendon Press, Oxford (2000)
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)
Hand, M.: Antirealism and falsity. In: Gabbay, D.M., Wansing, H. (eds.) What is Negation?, pp. 185–198. Springer, Dordrecht (1999). doi:10.1007/978-94-015-9309-0_9
Kameyama, Y., Sato, M.: Strong normalizability of the non-deterministic catch/throw calculi. Theor. Comput. Sci. 272(1–2), 223–245 (2002)
Maehara, S.: Eine darstellung der intuitionistischen logik in der klassischen. Nagoya Math. J. 7, 45–64 (1954)
Nakano, H.: A constructive logic behind the catch and throw mechanism. Ann. Pure Appl. Logic 69(2), 269–301 (1994)
Nakano, H.: Logical structures of the catch and throw mechanism. Ph.D. thesis, The University of Tokyo (1995)
Onishi, T.: Proof-theoretic semantics and bilateralism. Ph.D. thesis, Kyoto University (2012). (Written in Japanese)
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
Prawitz, D.: Meaning approached via proofs. Synthese 148(3), 507–524 (2006)
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)
Read, S.: Harmony and autonomy in classical logic. J. Philos. Logic 29(2), 123–154 (2000)
Sørensen, H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Elsevier, Amsterdam (2006)
Steele, G.L.: Common LISP: The Language, 2nd edn. Digital Press, Newton (1990)
Tennant, N.: Negation, Absurdity and Contrariety. In: Gabbay, D.M., Wansing, H. (eds.) What is Negation?, pp. 199–222. Springer, Dordrecht (1999)
Tranchini, L.: The role of negation in proof-theoretic semantics: a proposal. Fuzzy Logics Interpret. Logics Resour. 9, 273–287 (2008)
van Dalen, D.: Kolmogorov and Brouwer on constructive implication and the Ex Falso rule. Russ. Math. Surv. 59(2), 247–257 (2004)
Acknowledgment
We appreciate the helpful comments of Atsushi Igarashi and Takuro Onishi that improved the presentation of this paper. We are also grateful to the anonymous referees for their helpful comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer-Verlag GmbH Germany
About this paper
Cite this paper
Fukuda, Y., Igarashi, R. (2017). A Reconstruction of Ex Falso Quodlibet via Quasi-Multiple-Conclusion Natural Deduction. In: Baltag, A., Seligman, J., Yamada, T. (eds) Logic, Rationality, and Interaction. LORI 2017. Lecture Notes in Computer Science(), vol 10455. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-55665-8_38
Download citation
DOI: https://doi.org/10.1007/978-3-662-55665-8_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-55664-1
Online ISBN: 978-3-662-55665-8
eBook Packages: Computer ScienceComputer Science (R0)
