Abstract
This chapter develops intuitionist sentential logic in a way suggested by Jaroslav Peregrin. It treats the intuitionist conditional as a device for affirming the correctness of certain inferences.
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.
The name ‘Peregrin’ is a tribute to Jaroslav Peregrin whose paper [7] outlines the approach to intuitionist logic we pursue in this chapter.
- 2.
The name ‘Ded’ recalls a result, known as the deduction theorem, of which our axiom is a special case. We still need to confirm the full deduction theorem: that is, we still need to confirm that \((\phi \vartriangleright \psi )\) is inferable when the derivation of \(\psi \) from \(\phi \) depends on additional premises \(\varPhi \):
$$ \varPhi \cup \{\phi \}\vdash \psi \quad \Rightarrow \quad \varPhi \vdash (\phi \vartriangleright \psi ). $$Axioms 7.7, 7.8, and 7.9 will help us do so. This will show that the Peregrins should accept the inference from \(\varPhi \) to \((\phi \vartriangleright \psi )\) whenever they accept the inference from \(\varPhi \cup \{\phi \}\) to \(\psi \). Perhaps we should have just adopted that as an axiom. I saw two reasons not to take that course. First, I thought Axiom 7.9 deserved separate discussion because of its special role in distinguishing between inferability and strict implication (to be discussed below). Second, I thought it quite evident that Axioms 7.7 and 7.8 belong in a logic of inferability, but less immediately evident that the deduction theorem does. Others may see the matter differently.
- 3.
‘MP’ stands for ‘modus ponens’.
- 4.
‘EFQ’ stands for ‘ex falso quodlibet’: “from a falsehood anything [follows].”
- 5.
This is just one of the many insights to be found in Martin [6]. I will be borrowing exercises from that book for the rest of this chapter.
- 6.
Charles Sanders Peirce (1839–1914) was an American logician, mathematician, philosopher, and scientist.
- 7.
If you can infer \(P\) from the inferability of \(Q\) from \(P\), can you safely infer \(P\)? That move may be justified; but its justifiability is not intrinsic to the very concept of inference. By the way, it is not obvious that ‘\((((P\vartriangleright Q)\vartriangleright P)\vartriangleright P)\)’ is unprovable in our system. There are proofs of its unprovability, but I will not supply any here. If you want to pursue this further, you might consult the WikipediA article on Heyting algebras (http://en.wikipedia.org/wiki/Heyting_algebra).
- 8.
I am not going to try to present ‘\(\bigtriangledown \)’ as a natural outgrowth of Peregrinese reflections on a logic-free conception of inference. Perhaps you can figure out a way to do so. You might start by looking into something called “multiple-conclusion logic.”
- 9.
Is it intrinsic to the concept of inference that, given any two sentences, one will be inferable from the other?
- 10.
For more on assimilators, see Pollard [8–10]. The first two papers are available via http://www.projecteuclid.org. You can find the third at http://www.philosophy.unimelb.edu.au/ajl/
- 11.
- 12.
- 13.
For a proof, see Martin [6, p. 168].
- 14.
The ‘H’ in HA commemorates the mathematician Arend Heyting (1898–1980).
- 15.
- 16.
The American logician Haskell Curry (1900–1982) noted this in [1] (http://www.jstor.org/stable/2269292).
References
Curry, H. B. (1942). The inconsistency of certain formal logics. Journal of Symbolic Logic, 7, 115–117.
Glivenko, V. (1929). Sur quelques points de la logique de M. Brouwer. Académie royale de Belgique, Bulletin de la classe des sciences, 15, 183–188.
Gödel, K. (1933). Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines mathematischen Kolloquiums, 4, 34–38.
Gödel, K. (1986). Collected Works (Vol. 1). New York: Oxford University Press.
Mancosu, P. (Ed.). (1998). From Brouwer to Hilbert. New York: Oxford University Press.
Martin, N. M. (1989). Systems of logic. Cambridge: Cambridge University Press.
Peregrin, J. (2008). What is the logic of inference? Studia Logica, 88, 263–294.
Pollard, S. (2002). The expressive truth conditions of two-valued logic. Notre Dame Journal of Formal Logic, 43, 221–230.
Pollard, S. (2005). The expressive unary truth functions of n-valued logic. Notre Dame Journal of Formal Logic, 46, 93–105.
Pollard, S. (2006). Expressive three-valued truth functions. Australasian Journal of Logic, 4, 226–243.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Pollard, S. (2014). Intuitionist Logic. In: A Mathematical Prelude to the Philosophy of Mathematics. Springer, Cham. https://doi.org/10.1007/978-3-319-05816-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-05816-0_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-05815-3
Online ISBN: 978-3-319-05816-0
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)