The Phenomenology of Second-Level Inference: Perfumes in The Deductive Garden

David Makinson

doi:10.18778/0138-0680.2020.23

Authors

David Makinson Les Etangs, B2 Domaine de la Ronce 92410 Ville d'Avray France

DOI:

https://doi.org/10.18778/0138-0680.2020.23

Keywords:

second-level inference, suppositions, indirect inference, goal simplification, goal preservation, wlog, premise preservation

Abstract

We comment on certain features that second-level inference rules commonly used in mathematical proof sometimes have, sometimes lack: suppositions, indirectness, goal-simplification, goal-preservation and premise-preservation. The emphasis is on the roles of these features, which we call 'perfumes', in mathematical practice rather than on the space of all formal possibilities, deployment in proof-theory, or conventions for display in systems of natural deduction.

References

[1] G. Gentzen, Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, vol. 23 (1934), pp. 176–210, 405–431, DOI: http://dx.doi.org/10.1007/BF01201353 English translation: Investigation into logical deduction, pp. 68–131 of The Collected Papers of Gerhard Gentzen, ed. M. E. Szabo. North-Holland, Amsterdam, 1969.
Google Scholar DOI: https://doi.org/10.1016/S0049-237X(08)70822-X

[2] J. Harrison, Without loss of generality, [in:] S. Berghofer, T. Nipkow (eds.), Theorem-Proving in Higher Order Logics, vol. 5674 of Lecture Notes in Computer Science, Springer, Berlin (2009), pp. 43–59, DOI: http://dx.doi.org/10.1007/978-3-642-03359-9_3
Google Scholar DOI: https://doi.org/10.1007/978-3-642-03359-9_3

[3] A. Indrzejczak, Natural Deduction, Hybrid Systems and Modal Logic, Springer, Dordrecht (2010), DOI: http://dx.doi.org/10.1007/978-90481-8785-0
Google Scholar DOI: https://doi.org/10.1007/978-90-481-8785-0

[4] A. Indrzejczak, Natural Deduction, Internet Encyclopedia of Philosophy, (2015), URL: https://iep.utm.edu/nat-ded/ consulted 16.07.2020.
Google Scholar

[5] S. Ja_skowski, On the rules of suppositions in formal logic, Studia Logica, vol. 1 (1934), pp. 1–32.
Google Scholar

[6] D. Kalish, R. Montague, Logic: Techniques of Formal Reasoning, Harcourt Brace, New York (1964), also second edition with co-author G. Mar, Oxford University Press, 2001.
Google Scholar

[7] J. Lucas, Introduction to Abstract Mathematics, 2nd ed., Rowman & Little_eld, Maryland, USA (1990).
Google Scholar

[8] D. Makinson, Sets, Logic and Maths for Computing, 3rd ed., Undergraduate Topics in Computer Science, Springer, London (2020), DOI: http://dx.doi.org/10.1007/978-1-4471-2500-6
Google Scholar DOI: https://doi.org/10.1007/978-3-030-42218-9_1

[9] D. Makinson, Relevance-sensitive truth-trees, [in:] Alasdair Urquhart on Nonclassical and Algebraic Logic and Complexity of Proofs, Outstanding Contributions to Logic, Springer, Berlin (2021), to appear.
Google Scholar DOI: https://doi.org/10.1007/978-3-030-71430-7_2

[10] J. Pelletier, A brief history of natural deduction, History and Philosophy of Logic, vol. 20 (1999), pp. 1–31, DOI: http://dx.doi.org/10.1080/014453499298165
Google Scholar DOI: https://doi.org/10.1080/014453499298165

[11] J. Pelletier, A. P. Hazen, A history of natural deduction, [in:] D. Gabbay, F. J. Pelletier, E. Woods (eds.), Handbook of the History of Logic, vol. 11, North-Holland, Amsterdam (2012), pp. 341–414, DOI: http://dx.doi.org/10.1016/B978-0-444-52937-4.50007-1
Google Scholar DOI: https://doi.org/10.1016/B978-0-444-52937-4.50007-1

[12] E. Schechter, Constructivism is di_cult, American Mathematical Monthly, vol. 108 (2001), pp. 50–54, DOI: http://dx.doi.org/10.1080/00029890.2001.11919720
Google Scholar DOI: https://doi.org/10.1080/00029890.2001.11919720

[13] R. Sikorski, Boolean Algebras, 2nd ed., Springer, Berlin (1964), DOI: http://dx.doi.org/10.1007/978-3-662-01507-0
Google Scholar DOI: https://doi.org/10.1007/978-3-662-01507-0