Skip to main content
SpringerLink
Log in

Propositional Logic: Proofs from Axioms and Inference Rules

    We’re sorry, something doesn't seem to be working properly.

    Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Logic, Mathematics, and Computer Science

We’re sorry, something doesn't seem to be working properly.

Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

  • 2647 Accesses

Abstract

This chapter introduces propositional logics, which consist of starting formulae called axioms and rules of inference to derive from the axioms other formulae called theorems. Axioms and rules of inference form a mathematical model of rational thinking processes; theorems are their consequences. Different such logics, which are also called calculi, rely on different axioms or different rules of inference. For example, the Pure Positive Implicational Propositional Calculus focuses only on the logical implication. The first few sections derive some of its theorems, for instance, the transitivity of the logical implication and the law of commutation, using the rule of Detachment with the laws of affirmation of the consequent and self-distributivity of the logical implication taken as axiom schemata from Frege and Łukasiewicz. A preliminary version of the Deduction Theorem for the propositional calculus provides a method for designing proofs. Another section shows the mutual equivalence of these axioms with Kleene’s axioms and Tarski’s axioms. Adding the converse law of contraposition, subsequent sections focus on the Classical Propositional Calculus, deriving the laws of double negation, reductio ad absurdum, proofs by contradiction, and proofs by cases. Yet another section outlines the equivalence of Frege and Łukasiewicz’s axioms with Church’s, Kleene’s, Tarski’s, and Rosser’s axioms, respectively. A final section demonstrates the contrast between logics that admit of a recipe for constructing proofs of all “valid” formulae, and logics where some formulae are “valid” but unprovable. The prerequisite for this chapter is the ability to read, compare, and substitute sequences and tables of symbols. The goal of this chapter is merely to develop a working knowledge of propositional logic:

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 69.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. V.I. Arnold, From Hilbert’s superposition problem to dynamical systems. Am. Math. Mon. 111(7), 608–624 (2004). ISSN 0002-9890

    Google Scholar 

  2. G.D.W. Berry, Peirce’s contributions to the logic of statements and quantifiers, in Studies in the Philosophy of Charles Sanders Peirce: First Series, ed. by P.P. Wiener, F.H. Young (Harvard University Press, Cambridge, 1952), pp. 153–165

    Google Scholar 

  3. R.T. Boute, How to calculate proofs: bridging the cultural divide. Not. Am. Math. Soc. 60(2), 173–191 (2013)

    Article  MathSciNet  Google Scholar 

  4. A. Church, Introduction to Mathematical Logic. Princeton Landmarks in Mathematics and Physics (Princeton University Press, Princeton, 1996). Tenth printing. ISBN 0-691-02906-7

    Google Scholar 

  5. P.J. Cohen, Set Theory and the Continuum Hypothesis (Dover, Mineola, 2008). ISBN-10 0-486-46921-2; QA248.C614 2008; LCCC No. 2008042847 511.3’22—dc22

    Google Scholar 

  6. C. Davis, The role of the untrue in mathematics. Math. Intell. 31(3), 4–8 (2009). Text of a talk presented at the Joint Mathematics Meeting in Toronto on Monday 5 January 2009

    Google Scholar 

  7. J.L.E. Dreyer, A History of Astronomy from Thales to Kepler, 2nd edn. (Dover, New York, 1953). SBN 486-60079-3; QB15.D77 1953; 53-12387

    Google Scholar 

  8. U. Dudley, Mathematical Cranks. MAA Spectrum (Mathematical Association of America, Washington, DC, 1992)

    Google Scholar 

  9. U. Dudley, The Trisectors. MAA Spectrum, revised edition (Mathematical Association of America, Washington, DC, 1994)

    Google Scholar 

  10. H.B. Enderton, A Mathematical Introduction to Logic (Academic Press, New York, 1972). LCCC No. 78-182659

    Google Scholar 

  11. J. Evans, The History and Practice of Ancient Astronomy (Oxford University Press, New York, 1998). ISBN 0-19-509539-1; QB16.E93 1998; LCCC No. 97-16539; 520’. 938–dc21

    Google Scholar 

  12. S. Feferman, Does mathematics need new axioms? Am. Math. Mon. 106(2), 99–111 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  13. G. Frege, Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens (Nebert, Halle, 1879)

    Google Scholar 

  14. G. Frege, Conceptual Notation, and Related Articles; Translated [from the German] and Edited with a Biography and Introduction by Terrell Ward Bynum (Clarendon Press, Oxford, 1972). ISBN 0198243596; B3245.F22 B94

    Google Scholar 

  15. K. Gödel, On formally Undecidable Propositions of Principia Mathematica and Related Systems (Dover, Mineola, 1992). ISBN 0-486-66980-7. QA248.G573 1992. LCCC No. 91-45947. 511.3–dc20

    Google Scholar 

  16. G. Gonthier, Formal proof—the four-color theorem. Not. Am. Math. Soc. 55(11), 1382–1393 (2008)

    MATH  MathSciNet  Google Scholar 

  17. T.C. Hales, Formal proof. Not. Am. Math. Soc. 55(11), 1370–1380 (2008)

    MATH  MathSciNet  Google Scholar 

  18. E.C. Hall, MIT’s role in project Apollo: final report on contracts NAS 9-163 and NAS 94065. Technical report R-700 (Charles Stark Draper Laboratory, MIT, Cambridge) (1972)

    Google Scholar 

  19. J. Harrison, Formal proof—theory and practice. Not. Am. Math. Soc. 55(11), 1395–1406 (2008)

    MATH  Google Scholar 

  20. J.R. Harrison, Handbook of Practical Logic and Automated Reasoning (Cambridge University Press, London, 2009). ISBN-13: 9780521899574

    Book  MATH  Google Scholar 

  21. D. Hilbert, Foundations of Geometry, 10th edn. (Open Court, La Salle, 1971). Eighth printing, 1996. Translated by Leo Unger and revised by Paul Bernays. ISBN 0-87548-164-7; LCCC No. 73-110344

    Google Scholar 

  22. D. Hilbert, W. Ackermann, Principles of Mathematical Logic (Chelsea Publishing Company, New York, 1950). BC135.H514. (Translation of David Hilbert & Wilhelm Ackermann, Grundzüge der theoretischen Logik, Julius Springer, Berlin, Germany, 1928 & 1938)

    Google Scholar 

  23. M. Kaku, Venus envy. Wall Street J. CCXLVIII(40), A8 (2006). Western Edition

    Google Scholar 

  24. H. Karttunen, P. Kröger, H. Oja, M. Poutanen, K.J. Donner (eds.), Fundamental Astronomy (Springer, New York, 1994). ISBN 0-387-57203; QB43.2.T2613 1993; 93-31098; 520–dc20 (second enlarged edition)

    Google Scholar 

  25. S.C. Kleene, Mathematical Logic (Dover, Mineola, 2002). ISBN 0-486-42533-9; QA9.A1 K54 2002; LCCC No. 2002034823 (originally published by Wiley in 1967)

    Google Scholar 

  26. S. Kortenkamp, Why Isn’t Pluto a Planet?: A Book about Planets (Capstone Press, Mankato, 2007). ISBN 0-7368-6753-8; QB701.K57 2007; LCCC No. 2006025648; 523.4–dc22

    Google Scholar 

  27. E. Lakdawalla, Pluto and the Kuiper belt. Sky Telesc. 127(2), 18–25 (2014)

    Google Scholar 

  28. J. Łukasiewicz, Zur vollen dreiwertigen Aussagenlogik. Erkenntniss 5, 176 (1935)

    Article  Google Scholar 

  29. J. Łukasiewicz, Zur Geschichte der Aussagenlogik. Erkenntniss 5, 111–131 (1935)

    Google Scholar 

  30. Y.I. Manin, A Course in Mathematical Logic (Springer, New York, 1977). ISBN 0-387-90243-0; QA9.M296; LCCC No. 77-1838; 511’.3

    Google Scholar 

  31. A. Margaris, First Order Mathematical Logic (Dover Publications Inc., New York, 1990). Corrected reprint of the 1967 edition

    Google Scholar 

  32. B. Mates, Elementary Logic, 2nd edn. (Oxford University Press, New York, 1972). BC135.M37 1972. LCCC No. 74-166004

    Google Scholar 

  33. O. Neugebauer, A History of Ancient Mathematical Astronomy. Part I. Studies in the History of Mathematics and Physical Sciences, vol. 1 (Springer, New York, 1975)

    Google Scholar 

  34. O. Neugebauer, A History of Ancient Mathematical Astronomy. Part III. Studies in the History of Mathematics and Physical Sciences, vol. 1 (Springer, New York, 1975)

    Google Scholar 

  35. Y. Nievergelt, The truth table of the logical implication. Math. Gaz. 94(531), 509–513 (2010). ISSN 0025-5572

    Google Scholar 

  36. Y. Nievergelt, H. Sullivan, Undecidability in fuzzy logic. UMAP J. 31(4), 323–359 (2010). Also reprinted as UMAP Unit 804

    Google Scholar 

  37. C.S. Peirce, On the algebra of logic: a contribution to the philosophy of notation. Am. J. Math. 7(2), 180–196 (1885)

    Article  MATH  MathSciNet  Google Scholar 

  38. J.W. Robbin, Mathematical Logic: A First Course (Dover, Mineola, 2006). SBN 486-61272-4; LCCC No. 65-12253 (originally published by W. A. Benjamin, New York, 1969)

    Google Scholar 

  39. J.B. Rosser, Logic For Mathematicians (McGraw-Hill, New York, 1953). BC135.R58; LCCC No. 51-12640

    Google Scholar 

  40. E. Schechter, Classical and Nonclassical Logics (Princeton University Press, Princeton 2005). ISBN 0-691-12279-2; QA9.3.S39 2005; 2004066030; 160–dc22

    Google Scholar 

  41. R.M. Smullyan, First-Order Logic (Dover, Mineola, 1995). ISBN 0-486-68370-2. QA9.S57 1994. LCCC No. 94-39736. 511.3–dc20

    Google Scholar 

  42. R.R. Stoll, Sets, Logic, and Axiomatic Theories (W. H. Freeman, San Francisco, 1961). LCCC No. 61-6784

    Google Scholar 

  43. A.A. Stolyar, Introduction to Elementary Mathematical Logic (Dover, Mineola, 1983). ISBN 0-486-64561-4. BC135.S7613 1983. LCCC No. 83-5223. 511.3

    Google Scholar 

  44. A. Tarski, Introduction to Logic and to the Methodology of Deductive Sciences (Oxford University Press, Oxford, 1941)

    Google Scholar 

  45. G. van Brummelen, The Mathematics of the Heavens and the Earth: The Early History of Trigonometry (Princeton University Press, Princeton, 2009). ISBN 978-0-691-12973-0; QA24.V36 2009; 516.2409–dc22; LCCC No. 2008032521

    Google Scholar 

  46. B.L. van der Waerden, Geometry and Algebra in Ancient Civilizations (Springer, Berlin, 1983). ISBN 3-540-12159-5. QA151.W34 1983. LCCC No. 83-501. 512’.009

    Google Scholar 

  47. D.A. Weintraub, Is Pluto a Planet?: A Historical Journey through the Solar System (Princeton University Press, Princeton, 2007). ISBN 0-691-12348-9; QB602.9.W45 2007; LCCC No. 2006929630

    Google Scholar 

  48. Westinghouse Electric Corporation, Surface Division, P.O. Box 1897, Baltimore, MD 21203. Technical Manual for DPS-2402 Computer, Volume I, 1 February 1966. http://www.bitsavers.org/pdf/westinghouse

    Google Scholar 

  49. F. Wiedijk, Formal proof—getting started. Not. Am. Math. Soc. 55(11), 1408–1417 (2008)

    MATH  MathSciNet  Google Scholar 

  50. S. Wolfram, The Mathematica Book, 3rd edn. (Wolfram Media, Champaign, 1996). ISBN 0-9650532-1-0; QA76.95.W65 1996; LCCC No. 96-7218; 510’.285’53–dc20

    Google Scholar 

  51. G. Zukav, The Dancing Wu Li Masters: An Overview of the New Physics (Morrow, New York, 1979). ISBN: 0-688-03402-0; QC173.98.Z84 1979; 530.1’2; LCCC No. 78-25827

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, Eastern Washington University, Cheney, WA, USA

    Yves Nievergelt

Authors
  1. Yves Nievergelt
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer Science+Business Media New York

About this chapter

Cite this chapter

Nievergelt, Y. (2015). Propositional Logic: Proofs from Axioms and Inference Rules. In: Logic, Mathematics, and Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-1-4939-3223-8_1

Download citation

Publish with us

Policies and ethics

Search

Navigation