GetWiki

{{Short description|Branch of logic}}{{Distinguish|Propositional analysis}}{{Use dmy dates|date=February 2021}}The propositional calculus{{refn|group=lower-alpha|Many sources write this with a definite article, as the propositional calculus, while others just call it propositional calculus with no article.}} is a branch of logic.WEB, Propositional Logic {{!, Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/propositional-logic-sentential-logic/ |access-date=2024-03-22 |language=en-US}} It is also called propositional logic,{{Citation |last=Franks |first=Curtis |title=Propositional Logic |date=2023 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/fall2023/entries/logic-propositional/ |access-date=2024-03-22 |edition=Fall 2023 |publisher=Metaphysics Research Lab, Stanford University |editor2-last=Nodelman |editor2-first=Uri}} statement logic, sentential calculus,WEB, Weisstein, Eric W., Propositional Calculus,mathworld.wolfram.com/, 2024-03-22, mathworld.wolfram.com, en, sentential logic, or sometimes zeroth-order logic.BOOK, BÄ›lohlávek, Radim, Fuzzy logic and mathematics: a historical perspective, Dauben, Joseph Warren, Klir, George J., 2017, Oxford University Press, 978-0-19-020001-5, New York, NY, United States of America, 463, BOOK, Manzano, María, Extensions of first order logic, 2005, Cambridge University Press, 978-0-521-35435-6, Digitally printed first paperback version, Cambridge tracts in theoretical computer science, Cambridge, 180, It deals with propositions (which can be true or false){{Citation |last1=McGrath |first1=Matthew |title=Propositions |date=2023 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/win2023/entries/propositions/ |access-date=2024-03-22 |edition=Winter 2023 |publisher=Metaphysics Research Lab, Stanford University |last2=Frank |first2=Devin |editor2-last=Nodelman |editor2-first=Uri}} and relations between propositions,WEB, Predicate Logic,www3.cs.stonybrook.edu/~skiena/113/lectures/lecture26/lecture26.html, 2024-03-22, www3.cs.stonybrook.edu, including the construction of arguments based on them.WEB, Philosophy 404: Lecture Five,www.webpages.uidaho.edu/~morourke/404-phil/Summer-99/Lecture%20Notes/5.htm, 2024-03-22, www.webpages.uidaho.edu, Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, biconditional, and negation.WEB, 3.1 Propositional Logic,www.teach.cs.toronto.edu/~csc110y/fall/notes/03-logic/01-propositional-logic.html, 2024-03-22, www.teach.cs.toronto.edu, BOOK, Semantics: a reader, 2004, Oxford University Press, 978-0-19-513697-5, Davis, Steven, New York, Gillon, Brendan S., BOOK, Plato, Jan von, Elements of logical reasoning, 2013, Cambridge University press, 978-1-107-03659-8, 1. publ, Cambridge, 9,32,121, WEB, Propositional Logic,www.cs.miami.edu/home/geoff/Courses/CSC648-12S/Content/Propositional.shtml, 2024-03-22, www.cs.miami.edu, Some sources include other connectives, as in the table below.Unlike first-order logic, propositional logic does not deal with non-logical objects, predicates about them, or quantifiers. However, all the machinery of propositional logic is included in first-order logic and higher-order logics. In this sense, propositional logic is the foundation of first-order logic and higher-order logic.Propositional logic is typically studied with a formal language, in which propositions are represented by letters, which are called propositional variables. These are then used, together with symbols for connectives, to make compound propositions. Because of this, the propositional variables are called atomic formulas of a formal zeroth-order language. While the atomic propositions are typically represented by letters of the alphabet, there is a variety of notations to represent the logical connectives. The following table shows the main notational variants for each of the connectives in propositional logic.{| class=“wikitable”mathworld.wolfram.com/, 2024-03-22, mathworld.wolfram.com, en, ! Connective! Symbol

Logical conjunction>AND| A land B, A cdot B, AB, A & B, A && B

Logical biconditional>equivalent| A equiv B, A Leftrightarrow B, A leftrightharpoons B

Material conditional>implies| A Rightarrow B, A supset B, A rightarrow B

Sheffer stroke>NAND| A overline{land} B, A mid B, overline{A cdot B}

| nonequivalent| A notequiv B, A notLeftrightarrow B, A nleftrightarrow B

Logical NOR>NOR| A overline{lor} B, A downarrow B, overline{A+B}

Negation>NOT| neg A, -A, overline{A}, sim A

Logical disjunction>OR| A lor B, A + B, A mid B, A parallel B

XNOR gate>XNOR| A XNOR B

Exclusive or>XOR| A underline{lor} B, A oplus B

The most thoroughly researched branch of propositional logic is classical truth-functional propositional logic, in which formulas are interpreted as having precisely one of two possible truth values, the truth value of true or the truth value of false.WEB, Propositional Logic {{!, Brilliant Math & Science Wiki |url=https://brilliant.org/wiki/propositional-logic/ |access-date=2020-08-20 |website=brilliant.org |language=en-us}} The principle of bivalence and the law of excluded middle are upheld. By comparison with first-order logic, truth-functional propositional logic is considered to be zeroth-order logic.

History

Although propositional logic (also called propositional calculus) had been hinted by earlier philosophers, it was developed into a formal logic (Stoic logic) by Chrysippus in the 3rd century BCBOOK,plato.stanford.edu/archives/spr2016/entries/logic-ancient/, The Stanford Encyclopedia of Philosophy, Susanne, Bobzien, Ancient Logic, Edward N., Zalta, 1 January 2016, Metaphysics Research Lab, Stanford University, Stanford Encyclopedia of Philosophy, and expanded by his successor Stoics. The logic was focused on propositions. This was different from the traditional syllogistic logic, which focused on terms. However, most of the original writings were lostWEB, Propositional Logic {{!, Internet Encyclopedia of Philosophy|url=https://iep.utm.edu/prop-log/|access-date=2020-08-20|language=en-US}} and, at some time between the 3rd and 6th century CE, Stoic logic faded into oblivion, to be resurrected only in the 20th century, in the wake of the (re)-discovery of propositional logic.{{Citation |last=Bobzien |first=Susanne |title=Ancient Logic |date=2020 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/sum2020/entries/logic-ancient/ |access-date=2024-03-22 |edition=Summer 2020 |publisher=Metaphysics Research Lab, Stanford University}}Symbolic logic, which would come to be important to refine propositional logic, was first developed by the 17th/18th-century mathematician Gottfried Leibniz, whose calculus ratiocinator was, however, unknown to the larger logical community. Consequently, many of the advances achieved by Leibniz were recreated by logicians like George Boole and Augustus De Morgan, completely independent of Leibniz.BOOK,plato.stanford.edu/archives/spr2014/entries/leibniz-logic-influence/, The Stanford Encyclopedia of Philosophy, Volker, Peckhaus, Leibniz’s Influence on 19th Century Logic, Edward N., Zalta, 1 January 2014, Metaphysics Research Lab, Stanford University, Stanford Encyclopedia of Philosophy, Gottlob Frege’s predicate logic builds upon propositional logic, and has been described as combining “the distinctive features of syllogistic logic and propositional logic.“BOOK, A Concise Introduction to Logic 10th edition, Hurley, Patrick, 2007, Wadsworth Publishing, 392, Consequently, predicate logic ushered in a new era in logic’s history; however, advances in propositional logic were still made after Frege, including natural deduction, truth trees and truth tables. Natural deduction was invented by Gerhard Gentzen and StanisÅ‚aw JaÅ›kowski. Truth trees were invented by Evert Willem Beth.Beth, Evert W.; “Semantic entailment and formal derivability”, series: Mededlingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, Nieuwe Reeks, vol. 18, no. 13, Noord-Hollandsche Uitg. Mij., Amsterdam, 1955, pp. 309–42. Reprinted in Jaakko Intikka (ed.) The Philosophy of Mathematics, Oxford University Press, 1969 The invention of truth tables, however, is of uncertain attribution.Within works by Fregefrege.brown.edu/heck/pdf/unpublished/TruthInFrege.pdf" title="web.archive.org/web/20120807235445frege.brown.edu/heck/pdf/unpublished/TruthInFrege.pdf">Truth in Frege and Bertrand Russell,WEB,digitalcommons.mcmaster.ca/cgi/viewcontent.cgi?article=1219&context=russelljournal, Russell: the Journal of Bertrand Russell Studies, are ideas influential to the invention of truth tables. The actual tabular structure (being formatted as a table), itself, is generally credited to either Ludwig Wittgenstein or Emil Post (or both, independently). Besides Frege and Russell, others credited with having ideas preceding truth tables include Philo, Boole, Charles Sanders Peirce,JOURNAL, Anellis, Irving H., Irving Anellis, Peirce’s Truth-functional Analysis and the Origin of the Truth Table, History and Philosophy of Logic, 2012, 33, 87–97, 10.1080/01445340.2011.621702, 170654885, and Ernst Schröder. Others credited with the tabular structure include Jan Łukasiewicz, Alfred North Whitehead, William Stanley Jevons, John Venn, and Clarence Irving Lewis. Ultimately, some have concluded, like John Shosky, that “It is far from clear that any one person should be given the title of ‘inventor’ of truth-tables.”.

Sentences

Propositional logic, as currently studied in universities, is a specification of a standard of logical consequence in which only the meanings of propositional connectives are considered in evaluating the conditions for the truth of a sentence, or whether a sentence logically follows from some other sentence or group of sentences.

Declarative sentences

Propositional logic deals with statements, which are defined as declarative sentences having truth value.WEB, Part2Mod1: LOGIC: Statements, Negations, Quantifiers, Truth Tables,www.math.fsu.edu/~wooland/hm2ed/Part2Module1/Part2Module1.html, 2024-03-22, www.math.fsu.edu, Examples of statements might include:

• Pseudopedia is a free online encyclopedia that anyone can edit.
• London is the capital of England.
• All Pseudopedia editors speak at least three languages.

Declarative sentences are contrasted with questions, such as “What is Pseudopedia?”, and imperative statements, such as “Please add citations to support the claims in this article.”.WEB, Lecture Notes on Logical Organization and Critical Thinking,www2.hawaii.edu/~sugihara/courses/HCU2016s_TC/notes/CriticalThinking.html, 2024-03-22, www2.hawaii.edu, WEB, Logical Connectives,sites.millersville.edu/bikenaga/math-proof/logical-connectives/logical-connectives.html, 2024-03-22, sites.millersville.edu, Such non-declarative sentences have no truth value,WEB, Lecture1,www.cs.columbia.edu/~rgu/courses/e6998/fall2018/Lecture1.html, 2024-03-22, www.cs.columbia.edu, and are only dealt with in nonclassical logics, called erotetic and imperative logics.

Compounding sentences with connectives

{{See also|Atomic formula|Atomic sentence}}In propositional logic, a statement can contain one or more other statements as parts. Compound sentences are formed from simpler sentences and express relationships among the constituent sentences.WEB, Introduction to Logic - Chapter 2,intrologic.stanford.edu/chapters/chapter_02.html, 2024-03-22, intrologic.stanford.edu, This is done by combining them with logical connectives:BOOK, Beall, Jeffrey C., Logic: the basics, 2010, Routledge, 978-0-203-85155-5, 1. publ, London, 6, 8,14-16,19-20, 44-48, 50-53, 56, en, the main types of compound sentences are negations, conjunctions, disjunctions, implications, and biconditionals, which are formed by using the corresponding connectives to connect propositions.WEB, Watson,watson.latech.edu/book/intelligence/intelligenceApproaches2b1.html, 2024-03-22, watson.latech.edu, WEB, Introduction to Theoretical Computer Science, Chapter 1,www.cs.odu.edu/~toida/nerzic/390teched/math/logic.html, 2024-03-22, www.cs.odu.edu, In English, these connectives are expressed by the words “and” (conjunction), “or” (disjunction), “not” (negation), “if” (material conditional), and “if and only if” (biconditional). Examples of such compound sentences might include:

• Pseudopedia is a free online encyclopedia that anyone can edit, and millions (Help:Editing|already have). (conjunction)
• It is not true that all Pseudopedia editors speak at least three languages. (negation)
• Either London is the capital of England, or London is the capital of the United Kingdom, or both. (disjunction){{refn|group=lower-alpha|The “or both” makes it clear that it’s a logical disjunction, not an exclusive or, which is more common in English.}}

If sentences lack any logical connectives, they are called simple sentences, or atomic sentences; if they contain one or more logical connectives, they are called compound sentences, or molecular sentences.Sentential connectives are a broader category that includes logical connectives. Sentential connectives are any linguistic particles that bind sentences to create a new compound sentence, or that inflect a single sentence to create a new sentence. A logical connective, or propositional connective, is a kind of sentential connective with the characteristic feature that, when the original sentences it operates on are (or express) propositions, the new sentence that results from its application also is (or expresses) a proposition. Philosophers disagree about what exactly a proposition is, as well as about which sentential connectives in natural languages should be counted as logical connectives. Sentential connectives are also called sentence-functors, and logical connectives are also called truth-functors.

Arguments

An argument is defined as a pair of things, namely a set of sentences, called the premises,{{refn|group=lower-alpha|The set of premises may be the empty set; an argument from an empty set of premises is valid if, and only if, the conclusion is a tautology.}} and a sentence, called the conclusion.BOOK, Allen, Colin, Logic primer, Hand, Michael, 2022, The MIT Press, 978-0-262-54364-4, 3rd, Cambridge, Massachusetts, The conclusion is claimed to follow from the premises, and the premises are claimed to support the conclusion.

Example argument

The following is an example of an argument within the scope of propositional logic: The logical form of this argument is known as modus ponens, which is a classically valid form.JOURNAL, Stojnić, Una, 2017, One’s Modus Ponens: Modality, Coherence and Logic,www.jstor.org/stable/48578954, Philosophy and Phenomenological Research, 95, 1, 167–214, 48578954, 0031-8205, So, in classical logic, the argument is valid, although it may or may not be sound, depending on the meteorological facts in a given context. This example argument will be reused when explaining {{section link||Formalization}}.

Validity and soundness

An argument is valid if, and only if, it is necessary that, if all its premises are true, its conclusion is true.{{Citation |last=Dutilh Novaes |first=Catarina |title=Argument and Argumentation |date=2022 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/fall2022/entries/argument/ |access-date=2024-04-05 |edition=Fall 2022 |publisher=Metaphysics Research Lab, Stanford University |editor2-last=Nodelman |editor2-first=Uri}}WEB, Validity and Soundness {{!, Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/val-snd/ |access-date=2024-04-05 |language=en-US}} Alternatively, an argument is valid if, and only if, it is impossible for all the premises to be true while the conclusion is false.Validity is contrasted with soundness. An argument is sound if, and only if, it is valid and all its premises are true. Otherwise, it is unsound.Logic, in general, aims to precisely specify valid arguments. This is done by defining a valid argument as one in which its conclusion is a logical consequence of its premises, which, when this is understood as semantic consequence, means that there is no case in which the premises are true but the conclusion is not true – see {{section link||Semantics}} below.

Formalization

Propositional logic is typically studied through a formal system in which formulas of a formal language are interpreted to represent propositions. This formal language is the basis for proof systems, which allow a conclusion to be derived from premises if, and only if, it is a logical consequence of them. This section will show how this works by formalizing the {{section link||Example argument}}. The formal language for a propositional calculus will be fully specified in {{section link||Language}}, and an overview of proof systems will be given in {{section link||Proof systems}}.

Propositional variables

Since propositional logic is not concerned with the structure of propositions beyond the point where they cannot be decomposed any more by logical connectives, it is typically studied by replacing such atomic (indivisible) statements with letters of the alphabet, which are interpreted as variables representing statements (propositional variables). With propositional variables, the {{section link||Example argument}} would then be symbolized as follows: When {{mvar|P}} is interpreted as “It’s raining” and {{mvar|Q}} as “it’s cloudy” these symbolic expressions correspond exactly with the original expression in natural language. Not only that, but they will also correspond with any other inference with the same logical form.When a formal system is used to represent formal logic, only statement letters (usually capital roman letters such as P, Q and R) are represented directly. The natural language propositions that arise when they’re interpreted are outside the scope of the system, and the relation between the formal system and its interpretation is likewise outside the formal system itself.

Gentzen notation

If we assume that the validity of modus ponens has been accepted as an axiom, then the same {{section link||Example argument}} can also be depicted like this: This method of displaying it is Gentzen’s notation for natural deduction and sequent calculus.{{Citation |last1=Pelletier |first1=Francis Jeffry |title=Natural Deduction Systems in Logic |date=2024 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/spr2024/entries/natural-deduction/ |access-date=2024-03-22 |edition=Spring 2024 |publisher=Metaphysics Research Lab, Stanford University |last2=Hazen |first2=Allen |editor2-last=Nodelman |editor2-first=Uri}} The premises are shown above a line, called the inference line, separated by a comma, which indicates combination of premises.{{Citation |last=Restall |first=Greg |title=Substructural Logics |date=2018 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/spr2018/entries/logic-substructural/ |access-date=2024-03-22 |edition=Spring 2018 |publisher=Metaphysics Research Lab, Stanford University}} The conclusion is written below the inference line. The inference line represents syntactic consequence, sometimes called deductive consequence,WEB, Compactness {{!, Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/compactness/ |access-date=2024-03-22 |language=en-US}} which is also symbolized with ⊢.WEB, Lecture Topics for Discrete Math Students,math.colorado.edu/~kearnes/Teaching/Courses/F23/discretel.html, 2024-03-22, math.colorado.edu, So the above can also be written in one line as P to Q, P vdash Q.{{refn|group=lower-alpha|The turnstile (for syntactic consequence) is of a higher level than the comma (for premise combination), which is of a higher level than the arrow (for material implication), so no parentheses are needed to interpret this formula.}}Syntactic consequence is contrasted with semantic consequence,{{Citation |last1=Paseau |first1=Alexander |title=Deductivism in the Philosophy of Mathematics |date=2023 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/fall2023/entries/deductivism-mathematics/ |access-date=2024-03-22 |edition=Fall 2023 |publisher=Metaphysics Research Lab, Stanford University |last2=Pregel |first2=Fabian |editor2-last=Nodelman |editor2-first=Uri}} which is symbolized with ⊧. In this case, the conclusion follows syntactically because the natural deduction inference rule of modus ponens has been assumed. For more on inference rules, see the sections on proof systems below.

Language

{{Formal languages}}The language (commonly called mathcal{L})WEB, Compactness {{!, Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/compactness/ |access-date=2024-03-22 |language=en-US}}{{Citation |last1=Demey |first1=Lorenz |title=Logic and Probability |date=2023 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/fall2023/entries/logic-probability/ |access-date=2024-03-22 |edition=Fall 2023 |publisher=Metaphysics Research Lab, Stanford University |last2=Kooi |first2=Barteld |last3=Sack |first3=Joshua |editor2-last=Nodelman |editor2-first=Uri}} of a propositional calculus is defined in terms of:

1. a set of primitive symbols, called atomic formulas, atomic sentences, atoms,BOOK, Kleene, Stephen Cole, Mathematical logic, 2002, Dover Publications, 978-0-486-42533-7, Dover, Mineola, N.Y, placeholders, prime formulas, proposition letters, sentence letters, or variables, and
2. a set of operator symbols, called connectives, logical connectives, logical operators, truth-functional connectives, truth-functors, or propositional connectives.

A well-formed formula is any atomic formula, or any formula that can be built up from atomic formulas by means of operator symbols according to the rules of the grammar. The language mathcal{L}, then, is defined either as being identical to its set of well-formed formulas, or as containing that set (together with, for instance, its set of connectives and variables).Usually the syntax of mathcal{L} is defined recursively by just a few definitions, as seen next; some authors explicitly include parentheses as punctuation marks when defining their language’s syntax,BOOK, Smullyan, Raymond M., First-order logic, 1995, Dover, 978-0-486-68370-6, New York, 5,11,14, en, while others use them without comment.

Syntax

Given a set of atomic propositional variables p_1, p_2, p_3, ..., and a set of propositional connectives c_1^1, c_2^1, c_3^1, ..., c_1^2, c_2^2, c_3^2, ..., c_1^3, c_2^3, c_3^3, ..., a formula of propositional logic is defined recursively by these definitions:BOOK, Humberstone, Lloyd,www.worldcat.org/title/694679197, The connectives, 2011, MIT Press, 978-0-262-01654-4, Cambridge, Mass, 118,702, 694679197, {{refn|group=lower-alpha|A very general and abstract syntax is given here, following the notation in the SEP, but including the third definition, which is very commonly given explicitly by other sources, such as Gillon, Bostock, Allen & Hand, and many others. As noted elsewhere in the article, languages variously compose their set of atomic propositional variables from uppercase or lowercase letters (often focusing on P/p, Q/q, and R/r), with or without subscript numerals; and in their set of connectives, they may include either the full set of five typical connectives, { neg, land, lor, to, leftrightarrow }, or any of the truth-functionally complete subsets of it. (And, of course, they may also use any of the notational variants of these connectives.)}} Writing the result of applying c_n^m to langleA, B, C, …rangle in functional notation, as c_n^m(A, B, C, …), we have the following as examples of well-formed formulas:

• p_5
• c_3^2(p_2, p_9)
• c_3^2(p_1, c_2^1(p_3))
• c_1^3(p_4, p_6, c_2^2(p_1, p_2))
• c_4^2(c_1^1(p_7), c_3^1(p_8))
• c_2^3(c_1^2(p_3, p_4), c_2^1(p_5), c_3^2(p_6, p_7))
• c_3^1(c_1^3(p_2, p_3, c_2^2(p_4, p_5)))

What was given as Definition 2 above, which is responsible for the composition of formulas, is referred to by Colin Howson as the principle of composition.{{refn|group=lower-alpha|Note that the phrase “principle of composition” has referred to other things in other contexts, and even in the context of logic, since Bertrand Russell used it to refer to the principle that “a proposition which implies each of two propositions implies them both.“BOOK, Russell, Bertrand, Principles of mathematics, 2010, Routledge, 978-0-415-48741-2, Routledge classics, London, 17, }} It is this recursion in the definition of a language’s syntax which justifies the use of the word “atomic” to refer to propositional variables, since all formulas in the language mathcal{L} are built up from the atoms as ultimate building blocks. Composite formulas (all formulas besides atoms) are called molecules, or molecular sentences. (This is an imperfect analogy with chemistry, since a chemical molecule may sometimes have only one atom, as in monatomic gases.)The definition that “nothing else is a formula”, given above as Definition 3, excludes any formula from the language which is not specifically required by the other definitions in the syntax. In particular, it excludes infinitely long formulas from being well-formed.

CF grammar in BNF

An alternative to the syntax definitions given above is to write a context-free (CF) grammar for the language mathcal{L} in Backus-Naur form (BNF).BOOK, Hodges, Wilfrid, Logic, 1977, Penguin, 978-0-14-021985-2, Harmondsworth ; New York, 80–85, BOOK, Hansson, Sven Ove, Introduction to formal philosophy, Hendricks, Vincent F., 2018, Springer, 978-3-030-08454-7, Springer undergraduate texts in philosophy, Cham, 38, This is more common in computer science than in philosophy. It can be done in many ways, of which a particularly brief one, for the common set of five connectives, is this single clause:BOOK, Ayala-Rincón, Mauricio,link.springer.com/book/10.1007/978-3-319-51653-0, Applied Logic for Computer Scientists, de Moura, Flávio L.C., 2017, Springer, 2, en, 10.1007/978-3-319-51653-0, This clause, due to its self-referential nature (since phi is in some branches of the definition of phi), also acts as a recursive definition, and therefore specifies the entire language. To expand it to add modal operators, one need only add … | ~ Boxphi ~ | ~ Diamondphi to the end of the clause.

Constants and schemata

Mathematicians sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional constants represent some particular proposition,BOOK, Lande, Nelson P., Classical logic and its rabbit holes: a first course, 2013, Hackett Publishing Co., Inc, 978-1-60384-948-7, Indianapolis, Ind, 20, while propositional variables range over the set of all atomic propositions. Schemata, or schematic letters, however, range over all formulas.BOOK, Bostock, David, Intermediate logic, 1997, Clarendon Press ; Oxford University Press, 978-0-19-875141-0, Oxford : New York, 4-5, 8-13, 18-19, 22, 27, 29, (Schematic letters are also called metavariables.) It is common to represent propositional constants by {{mvar|A}}, {{mvar|B}}, and {{mvar|C}}, propositional variables by {{mvar|P}}, {{mvar|Q}}, and {{mvar|R}}, and schematic letters are often Greek letters, most often {{mvar|φ}}, {{mvar|ψ}}, and {{mvar|χ}}.However, some authors recognize only two “propositional constants” in their formal system: the special symbol top, called “truth”, which always evaluates to True, and the special symbol bot, called “falsity”, which always evaluates to False.BOOK, Goldrei, Derek, Propositional and predicate calculus: a model of argument, 2005, Springer, 978-1-85233-921-0, London, 69, en, WEB, Propositional Logic,www.cs.rochester.edu/u/nelson/courses/csc_173/proplogic/expressions.html, 2024-03-22, www.cs.rochester.edu, WEB, Propositional calculus,www.cs.cornell.edu/courses/cs671/1999fa/typed%20logic/node18.html, 2024-03-22, www.cs.cornell.edu, Other authors also include these symbols, with the same meaning, but consider them to be “zero-place truth-functors”, or equivalently, “nullary connectives”.

Semantics

To serve as a model of the logic of a given natural language, a formal language must be semantically interpreted. In classical logic, all propositions evaluate to exactly one of two truth-values: True or False.{{Citation |last1=Shramko |first1=Yaroslav |title=Truth Values |date=2021 |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/win2021/entriesruth-values/ |access-date=2024-03-23 |edition=Winter 2021 |publisher=Metaphysics Research Lab, Stanford University |last2=Wansing |first2=Heinrich |encyclopedia=The Stanford Encyclopedia of Philosophy}} For example, “Pseudopedia is a (Pseudopedia:Free encyclopedia|free) online encyclopedia that anyone can edit” (Pseudopedia:About|evaluates to True),JOURNAL, Metcalfe, David, Powell, John, 2011, Should doctors spurn Pseudopedia?, Journal of the Royal Society of Medicine, en, 104, 12, 488–489, 10.1258/jrsm.2011.110227, 0141-0768, 3241521, 22179287, while “Pseudopedia is a paper encyclopedia” (Pseudopedia:NOTPAPER|evaluates to False).BOOK, Ayers, Phoebe,www.worldcat.org/title/185698411, How Pseudopedia works: and how you can be a part of it, Matthews, Charles, Yates, Ben, 2008, No Starch Press, 978-1-59327-176-3, San Francisco, 22, 185698411, In other respects, the following formal semantics can apply to the language of any propositional logic, but the assumptions that there are only two semantic values (bivalence), that only one of the two is assigned to each formula in the language (noncontradiction), and that every formula gets assigned a value (excluded middle), are distinctive features of classical logic.{{Citation |last1=Shapiro |first1=Stewart |title=Classical Logic |date=2024 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/spr2024/entries/logic-classical/ |access-date=2024-03-25 |edition=Spring 2024 |publisher=Metaphysics Research Lab, Stanford University |last2=Kouri Kissel |first2=Teresa |editor2-last=Nodelman |editor2-first=Uri}} To learn about nonclassical logics with more than two truth-values, and their unique semantics, one may consult the articles on “Many-valued logic”, “Three-valued logic”, “Finite-valued logic”, and “Infinite-valued logic”.

Interpretation (case) and argument

For a given language mathcal{L}, an interpretation,JOURNAL, Landman, Fred, 1991, Structures for Semantics,doi.org/10.1007/978-94-011-3212-1, Studies in Linguistics and Philosophy, en, 45, 127, 10.1007/978-94-011-3212-1, 978-0-7923-1240-6, 0924-4662, or case,{{refn|group=lower-alpha|The name “interpretation” is used by some authors and the name “case” by other authors. This article will be indifferent and use either, since it is collaboratively edited and there is no consensus about which terminology to adopt.}} is an assignment of semantic values to each formula of mathcal{L}. For a formal language of classical logic, a case is defined as an assignment, to each formula of mathcal{L}, of one or the other, but not both, of the truth values, namely truth (T, or 1) and falsity (F, or 0).BOOK, Nascimento, Marco Antonio Chaer, Frontiers in quantum methods and applications in chemistry and physics: selected proceedings of QSCP-XVIII (Paraty, Brazil, December, 2013), 2015, Springer, International Workshop on Quantum Systems in Chemistry and Physics, 978-3-319-14397-2, Progress in theoretical chemistry and physics, Cham, 255, en, JOURNAL, Chowdhary, K.R., 2020, Fundamentals of Artificial Intelligence,doi.org/10.1007/978-81-322-3972-7, SpringerLink, en, 31–34, 10.1007/978-81-322-3972-7, 978-81-322-3970-3, An interpretation of a formal language for classical logic is often expressed in terms of truth tables.BOOK, Hunter, Geoffrey, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Press, 1971, 0-520-02356-0, Since each formula is only assigned a single truth-value, an interpretation may be viewed as a function, whose domain is mathcal{L}, and whose range is its set of semantic values mathcal{V} = {mathsf{T}, mathsf{F}}, or mathcal{V} = {1, 0}.For n distinct propositional symbols there are 2^n distinct possible interpretations. For any particular symbol a, for example, there are 2^1=2 possible interpretations: either a is assigned T, or a is assigned F. And for the pair a, b there are 2^2=4 possible interpretations: either both are assigned T, or both are assigned F, or a is assigned T and b is assigned F, or a is assigned F and b is assigned T. Since mathcal{L} has aleph_0, that is, denumerably many propositional symbols, there are 2^{aleph_0}=mathfrak c, and therefore uncountably many distinct possible interpretations of mathcal{L} as a whole.Where mathcal{I} is an interpretation and varphi and psi represent formulas, the definition of an argument, given in {{section link||Arguments}}, may then be stated as a pair langle {varphi_1, varphi_2, varphi_3, ..., varphi_n} , psi rangle, where {varphi_1, varphi_2, varphi_3, ..., varphi_n} is the set of premises and psi is the conclusion. The definition of an argument’s validity, i.e. its property that {varphi_1, varphi_2, varphi_3, ..., varphi_n} models psi, can then be stated as its absence of a counterexample, where a counterexample is defined as a case mathcal{I} in which the argument’s premises {varphi_1, varphi_2, varphi_3, ..., varphi_n} are all true but the conclusion psi is not true. As will be seen in {{section link||Semantic truth, validity, consequence}}, this is the same as to say that the conclusion is a semantic consequence of the premises.

Propositional connective semantics

An interpretation assigns semantic values to atomic formulas directly. Molecular formulas are assigned a function of the value of their constituent atoms, according to the connective used; the connectives are defined in such a way that the truth-value of a sentence formed from atoms with connectives depends on the truth-values of the atoms that they’re applied to, and only on those. This assumption is referred to by Colin Howson as the assumption of the truth-functionality of the connectives.{{Logical connectives sidebar}}Since logical connectives are defined semantically only in terms of the truth values that they take when the propositional variables that they’re applied to take either of the two possible truth values, the semantic definition of the connectives is usually represented as a truth table for each of the connectives, as seen below:{| class=“wikitable” style="margin:1em auto; text-align:center;”! p! q! p ∧ q! p ∨ q! p → q! p ↔ q! ¬p! ¬q

}}T	{{Success		}}T	{{Success		}}T	{{Success		}}F	{{Failure|}}F

}}T	{{Failure		}}F	{{Success		}}F	{{Failure		}}F	{{Success|}}T

}}F	{{Success		}}F	{{Success		}}T	{{Failure		}}T	{{Failure|}}F

}}F	{{Failure		}}F	{{Failure		}}T	{{Success		}}T	{{Success|}}T

This table covers each of the main five logical connectives: conjunction (here notated p ∧ q), disjunction (p ∨ q), implication (p → q), biconditional (p ↔ q) and negation, (¬p, or ¬q, as the case may be). It is sufficient for determining the semantics of each of these operators.{{Citation |last=Aloni |first=Maria |title=Disjunction |date=2023 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/spr2023/entries/disjunction/ |access-date=2024-03-23 |edition=Spring 2023 |publisher=Metaphysics Research Lab, Stanford University |editor2-last=Nodelman |editor2-first=Uri}} For more detail on each of the five, see the articles on each specific one, as well as the articles “Logical connective” and “Truth function”. For more truth tables for more different kinds of connectives, see the article “Truth table”.Some of these connectives may be defined in terms of others: for instance, implication, p â†’ q, may be defined in terms of disjunction and negation, as ¬p âˆ¨ q;BOOK, Levin, Oscar,discrete.openmathbooks.org/dmoi3/sec_propositional.html, Propositional Logic, en-US, and disjunction may be defined in terms of negation and conjunction, as ¬(¬p âˆ§ Â¬q). In fact, a truth-functionally complete system,{{refn|group=lower-alpha|A truth-functionally complete set of connectives is also called simply functionally complete, or adequate for truth-functional logic, or expressively adequate,{{citation | last1=Smith | first1=Peter | title=An introduction to formal logic | publisher=Cambridge University Press | isbn=978-0-521-00804-4 | year=2003}}. (Defines “expressively adequate”, shortened to “adequate set of connectives” in a section heading.) or simply adequate.}} in the sense that all and only the classical propositional tautologies are theorems, may be derived using only disjunction and negation (as Russell, Whitehead, and Hilbert did), or using only implication and negation (as Frege did), or using only conjunction and negation, or even using only a single connective for “not and” (the Sheffer stroke), as Jean Nicod did. A joint denial connective (logical NOR) will also suffice, by itself, to define all other connectives, but no other connectives have this property.Some authors, namely Howson and Cunningham,BOOK, Cunningham, Daniel W., Set theory: a first course, 2016, Cambridge University Press, 978-1-107-12032-7, Cambridge mathematical textbooks, New York, NY, distinguish equivalence from the biconditional. (As to equivalence, Howson calls it “truth-functional equivalence”, while Cunningham calls it “logical equivalence”.) Equivalence is symbolized with ⇔ and is a metalanguage symbol, while a biconditional is symbolized with ↔ and is a logical connective in the object language mathcal{L}. Regardless, an equivalence or biconditional is true if, and only if, the formulas connected by it are assigned the same semantic value under every interpretation. Other authors often do not make this distinction, and may use the word “equivalence”, and/or the symbol ⇔,BOOK, Genesereth, Michael,link.springer.com/10.1007/978-3-031-01801-5, Introduction to Logic, Kao, Eric J., 2017, Springer International Publishing, 978-3-031-00673-9, Synthesis Lectures on Computer Science, Cham, 18, en, 10.1007/978-3-031-01801-5, to denote their object language’s biconditional connective.

Semantic truth, validity, consequence

Given varphi and psi as formulas (or sentences) of a language mathcal{L}, and mathcal{I} as an interpretation (or case){{refn|group=lower-alpha|Some of these definitions use the word “interpretation”, and speak of sentences/formulas being true or false “under” it, and some will use the word “case”, and speak of sentences/formulas being true or false “in” it. Published reliable sources () have used both kinds of terminological convention, although usually a given author will use only one of them. Since this article is collaboratively edited and there is no consensus about which convention to use, these variations in terminology have been left standing.}} of mathcal{L}, then the following definitions apply:

• Truth-in-a-case: A sentence varphi of mathcal{L} is true under an interpretation mathcal{I} if mathcal{I} assigns the truth value T to varphi. If varphi is true under mathcal{I}, then mathcal{I} is called a model of varphi.
• Falsity-in-a-case: varphi is false under an interpretation mathcal{I} if, and only if, negvarphi is true under mathcal{I}. This is the “truth of negation” definition of falsity-in-a-case. Falsity-in-a-case may also be defined by the “complement” definition: varphi is false under an interpretation mathcal{I} if, and only if, varphi is not true under mathcal{I}. In classical logic, these definitions are equivalent, but in nonclassical logics, they are not.
• Semantic consequence: A sentence psi of mathcal{L} is a semantic consequence (varphi models psi) of a sentence varphi if there is no interpretation under which varphi is true and psi is not true.
• Valid formula (tautology): A sentence varphi of mathcal{L} is logically valid (modelsvarphi),{{refn|group=lower-alpha|Conventionally modelsvarphi, with nothing to the left of the turnstile, is used to symbolize a tautology. It may be interpreted as saying that varphi is a semantic consequence of the empty set of formulae, i.e., {}modelsvarphi, but with the empty brackets omitted for simplicity; which is just the same as to say that it is a tautology, i.e., that there is no interpretation under which it is false.}} or a tautology,WEB, 6. Semantics of Propositional Logic — Logic and Proof 3.18.4 documentation,leanprover.github.io/logic_and_proof/semantics_of_propositional_logic.html, 2024-03-28, leanprover.github.io, WEB, Knowledge Representation and Reasoning: Basics of Logics,www.emse.fr/~zimmermann/Teaching/KRR/generalities.html, 2024-03-28, www.emse.fr, if it is true under every interpretation, or true in every case.
• Consistent sentence: A sentence of mathcal{L} is consistent if it is true under at least one interpretation. It is inconsistent if it is not consistent. An inconsistent formula is also called self-contradictory, and said to be a self-contradiction, or simply a contradiction, although this latter name is sometimes reserved specifically for statements of the form (p land neg p).

For interpretations (cases) mathcal{I} of mathcal{L}, these definitions are sometimes given:

• Complete case: A case mathcal{I} is complete if, and only if, either varphi is true-in-mathcal{I} or negvarphi is true-in-mathcal{I}, for any varphi in mathcal{L}.BOOK,www.worldcat.org/title/681481210, Computational logic in multi-agent systems: 10th international workshop, CLIMA X, Hamburg, Germany, September 9-10, 2009: revised selected and invited papers, 2010, Springer, 978-3-642-16866-6, Dix, J., Lecture notes in computer science, Berlin ; New York, 49, 681481210, Fisher, Michael, Novak, Peter,
• Consistent case: A case mathcal{I} is consistent if, and only if, there is no varphi in mathcal{L} such that both varphi and negvarphi are true-in-mathcal{I}.BOOK, Computational models of argument: proceedings of comma 2020, 2020, IOS Press, 978-1-64368-106-1, Prakken, Henry, Frontiers in artificial intelligence and applications, Washington, 252, Bistarelli, Stefano, Santini, Francesco, Taticchi, Carlo,

For classical logic, which assumes that all cases are complete and consistent, the following theorems apply:

• For any given interpretation, a given formula is either true or false under it.BOOK, Rogers, Robert L.,dx.doi.org/10.1016/c2013-0-11894-6, Mathematical Logic and Formalized Theories, 1971, Elsevier, 978-0-7204-2098-2, 38–39, 10.1016/c2013-0-11894-6, en,
• No formula is both true and false under the same interpretation.
• varphi is true under mathcal{I} if, and only if, negvarphi is false under mathcal{I}; negvarphi is true under mathcal{I} if, and only if, varphi is not true under mathcal{I}.
• If varphi and (varphi to psi) are both true under mathcal{I}, then psi is true under mathcal{I}.
• If modelsvarphi and models(varphi to psi), then modelspsi.
• (varphi to psi) is true under mathcal{I} if, and only if, either varphi is not true under mathcal{I}, or psi is true under mathcal{I}.
• varphi models psi if, and only if, (varphi to psi) is logically valid, that is, varphi models psi if, and only if, models(varphi to psi).

Proof systems

{{See also|Proof theory|Proof calculus}}Proof systems in propositional logic can be broadly classified into semantic proof systems and syntactic proof systems,BOOK, Rudolf carnap: studies in semantics: the collected works of rudolf carnap, volume 7, 2024, Oxford University Press, 978-0-19-289487-8, Awodey, Steve, New York, xxvii, Arnold, Greg Frost-, BOOK, Advances in Mathematics Education Research on Proof and Proving: An International Perspective, 2018, Springer International Publishing : Imprint: Springer, 978-3-319-70996-3, Harel, Guershon, 1st ed. 2018, ICME-13 Monographs, Cham, 181, Stylianides, Andreas J., JOURNAL, DeLancey, Craig, 2017, A Concise Introduction to Logic: §4. Proofs,milnepublishing.geneseo.edu/concise-introduction-to-logic/chapter/4-proofs/, 2024-03-23, Milne Publishing, according to the kind of logical consequence that they rely on: semantic proof systems rely on semantic consequence (varphi models psi),{{Citation |last1=Ferguson |first1=Thomas Macaulay |title=semantic consequence |date=2016-06-23 |work=A Dictionary of Logic |url=https://www.oxfordreference.com/display/10.1093/acref/9780191816802.001.0001/acref-9780191816802-e-387 |access-date=2024-03-23 |publisher=Oxford University Press |language=en |doi=10.1093/acref/9780191816802.001.0001 |isbn=978-0-19-181680-2 |last2=Priest |first2=Graham}} whereas syntactic proof systems rely on syntactic consequence (varphi vdash psi).{{Citation |last1=Ferguson |first1=Thomas Macaulay |title=syntactic consequence |date=2016-06-23 |work=A Dictionary of Logic |url=https://www.oxfordreference.com/display/10.1093/acref/9780191816802.001.0001/acref-9780191816802-e-440 |access-date=2024-03-23 |publisher=Oxford University Press |language=en |doi=10.1093/acref/9780191816802.001.0001 |isbn=978-0-19-181680-2 |last2=Priest |first2=Graham}} Semantic consequence deals with the truth values of propositions in all possible interpretations, whereas syntactic consequence concerns the derivation of conclusions from premises based on rules and axioms within a formal system.BOOK, Cook, Roy T., A dictionary of philosophical logic, 2009, Edinburgh University Press, 978-0-7486-2559-8, Edinburgh, 82,176, en, This section gives a very brief overview of the kinds of proof systems, with anchors to the relevant sections of this article on each one, as well as to the separate Pseudopedia articles on each one.

Semantic proof systems

File:Logische Verknuepfung Inhibition AB Truthtable.svg|200px|right|thumb|Example of a truth tabletruth tableFile:Partially built tableau.svg|thumb|200px|A graphical representation of a partially built propositional tableau ]]Semantic proof systems rely on the concept of semantic consequence, symbolized as varphi models psi, which indicates that if varphi is true, then psi must also be true in every possible interpretation.

Truth tables

A truth table is a semantic proof method used to determine the truth value of a propositional logic expression in every possible scenario.WEB, 2024-03-14, Truth table {{!, Boolean, Operators, Rules {{!}} Britannica |url=https://www.britannica.com/topic/truth-table |access-date=2024-03-23 |website=www.britannica.com |language=en}} By exhaustively listing the truth values of its constituent atoms, a truth table can show whether a proposition is true, false, tautological, or contradictory.WEB, MathematicalLogic,www.cs.yale.edu/homes/aspnes/pinewiki/MathematicalLogic.html, 2024-03-23, www.cs.yale.edu, See {{section link||Semantic proof via truth tables}}.

Semantic tableaux

A semantic tableau is another semantic proof technique that systematically explores the truth of a proposition.WEB, Analytic Tableaux,www3.cs.stonybrook.edu/~skiena/113/lectures/lecture5/lecture5.html, 2024-03-23, www3.cs.stonybrook.edu, It constructs a tree where each branch represents a possible interpretation of the propositions involved.WEB, Formal logic - Semantic Tableaux, Proofs, Rules {{!, Britannica |url=https://www.britannica.com/topic/formal-logic/Semantic-tableaux |access-date=2024-03-23 |website=www.britannica.com |language=en}} If every branch leads to a contradiction, the original proposition is considered to be a contradiction, and its negation is considered a tautology.BOOK, Howson, Colin, Logic with trees: an introduction to symbolic logic, 1997, Routledge, 978-0-415-13342-5, London ; New York, ix,x,5-6,15-16,20,24-29,38,42-43,47, See {{section link||Semantic proof via tableaux}}.

Syntactic proof systems

File:LK groupe logique.png|300px|right|thumb|Rules for the propositional sequent calculus LK, in Gentzen notation]]Syntactic proof systems, in contrast, focus on the formal manipulation of symbols according to specific rules. The notion of syntactic consequence, varphi vdash psi, signifies that psi can be derived from varphi using the rules of the formal system.

Axiomatic systems

An axiomatic system is a set of axioms or assumptions from which other statements (theorems) are logically derived.WEB, Axiomatic method {{!, Logic, Proofs & Foundations {{!}} Britannica |url=https://www.britannica.com/science/axiomatic-method |access-date=2024-03-23 |website=www.britannica.com |language=en}} In propositional logic, axiomatic systems define a base set of propositions considered to be self-evidently true, and theorems are proved by applying deduction rules to these axioms.WEB, Propositional Logic,mally.stanford.edu/tutorial/sentential.html, 2024-03-23, mally.stanford.edu, See the {{section link||Jan Łukasiewicz axiomatic proof system example}}.

Natural deduction

Natural deduction is a syntactic method of proof that emphasizes the derivation of conclusions from premises through the use of intuitive rules reflecting ordinary reasoning.WEB, Natural Deduction {{!, Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/natural-deduction/ |access-date=2024-03-23 |language=en-US}} Each rule reflects a particular logical connective and shows how it can be introduced or eliminated. See {{section link||Syntactic proof via natural deduction}}.

Sequent calculus

The sequent calculus is a formal system that represents logical deductions as sequences or “sequents” of formulas.WEB, Weisstein, Eric W., Sequent Calculus,mathworld.wolfram.com/, 2024-03-23, mathworld.wolfram.com, en, Developed by Gerhard Gentzen, this approach focuses on the structural properties of logical deductions and provides a powerful framework for proving statements within propositional logic.WEB, Interactive Tutorial of the Sequent Calculus,logitext.mit.edu/tutorial, 2024-03-23, logitext.mit.edu,

Semantic proof via truth tables

{{See also|Truth table}}Taking advantage of the semantic concept of validity (truth in every interpretation), it is possible to prove a formula’s validity by using a truth table, which gives every possible interpretation (assignment of truth values to variables) of a formula. If, and only if, all the lines of a truth table come out true, the formula is semantically valid (true in every interpretation). Further, if (and only if) negvarphi is valid, then varphi is inconsistent.WEB, 2021-09-09, 1.4: Tautologies and contradictions,math.libretexts.org/Bookshelves/Combinatorics_and_Discrete_Mathematics/Elementary_Foundations%3A_An_Introduction_to_Topics_in_Discrete_Mathematics_(Sylvestre)/01%3A_Symbolic_language/1.04%3A_Tautologies_and_contradictions, 2024-03-29, Mathematics LibreTexts, en, BOOK, Sylvestre, Jeremy,sites.ualberta.ca/~jsylvest/books/EF/section-symb-lang-taut-contra.html, EF Tautologies and contradictions, en-US, BOOK, DeLancey, Craig,intrologicimport.pressbooks.tru.ca/chapter/9-if-and-only-if-using-theorems-a-concise-introduction-to-logic/, Elementary Formal Logic, Woodrow, Jenna, Pressbooks, 2017, 1, For instance, this table shows that ”p → (q ∨ r → (r → ¬p))” is not valid:{| class=“wikitable” style="margin:1em auto; text-align:center;”! p! q! r! q ∨ r! r → ¬p! q ∨ r → (r → ¬p)! p → (q ∨ r → (r → ¬p))

}}T	{{Success		}}T	{{Success		}}F	{{Failure		}}F

}}T	{{Success		}}F	{{Success		}}T	{{Success		}}T

}}T	{{Failure		}}T	{{Success		}}F	{{Failure		}}F

}}T	{{Failure		}}F	{{Failure		}}T	{{Success		}}T

}}F	{{Success		}}T	{{Success		}}T	{{Success		}}T

}}F	{{Success		}}F	{{Success		}}T	{{Success		}}T

}}F	{{Failure		}}T	{{Success		}}T	{{Success		}}T

}}F	{{Failure		}}F	{{Failure		}}T	{{Success		}}T

The computation of the last column of the third line may be displayed as follows:{| class=“wikitable” style="margin:1em auto; text-align:center;”! p ! → ! (q ! ∨ ! r ! → ! (r ! → ! ¬ ! p))| T | → | (F | ∨ | T | → | (T | → | ¬ | T))| T | → | ( | T | | → | (T | → | F | ))| T | → | ( | T | | → | | F | | )| T | → | | | | F | | | | | | F | | | | | | | | | T | F | F | T | T | F | T | F | F| TFurther, using the theorem that varphi models psi if, and only if, (varphi to psi) is valid, we can use a truth table to prove that a formula is a semantic consequence of a set of formulas: {varphi_1, varphi_2, varphi_3, ..., varphi_n} models psi if, and only if, we can produce a truth table that comes out all true for the formula left( left(bigwedge _{i=1}^n varphi_i right) rightarrow psi right) (that is, if models left( left(bigwedge _{i=1}^n varphi_i right) rightarrow psi right)).BOOK, Lucas, Peter,www.cs.ru.nl/P.Lucas/teaching/KeR/logicintro.pdf, Principles of expert systems, Gaag, Linda van der, 1991, Addison-Wesley, 978-0-201-41640-4, International computer science series, Wokingham, England ; Reading, Mass, 26, WEB, Bachmair, Leo, 2009, CSE541 Logic in Computer Science,www3.cs.stonybrook.edu/~cse541/Spring2009/cse541PropLogic.pdf, Stony Brook University,

Semantic proof via tableaux

Since truth tables have 2n lines for n variables, they can be tiresomely long for large values of n. Analytic tableaux are a more efficient, but nevertheless mechanical,BOOK, Restall, Greg, Logic: an introduction, 2010, Routledge, 978-0-415-40068-8, Fundamentals of philosophy, London, 5,55-60,69, semantic proof method; they take advantage of the fact that “we learn nothing about the validity of the inference from examining the truth-value distributions which make either the premises false or the conclusion true: the only relevant distributions when considering deductive validity are clearly just those which make the premises true or the conclusion false.“Analytic tableaux for propositional logic are fully specified by the rules that are stated in schematic form below. These rules use “signed formulas”, where a signed formula is an expression TX or FX, where X is a (unsigned) formula of the language mathcal{L}. (Informally, TX is read “X is true”, and FX is read “X is false”.) Their formal semantic definition is that “under any interpretation, a signed formula TX is called true if X is true, and false if X is false, whereas a signed formula FX is called false if X is true, and true if X is false.” begin{align}&1) quad frac{T sim X}{FX} quad &&frac{F sim X}{TX} phantom{spacer} &2) quad frac{T(X land Y)}{begin{matrix} TX TY end{matrix}} quad &&frac{F(X land Y)}{FX | FY} phantom{spacer} &3) quad frac{T(X lor Y)}{TX | TY} quad &&frac{F(X lor Y)}{begin{matrix} FX FY end{matrix}} phantom{spacer} &4) quad frac{T(X supset Y)}{FX | TY} quad &&frac{F(X supset Y)}{begin{matrix} TX FY end{matrix}}end{align}In this notation, rule 2 means that T(X land Y) yields both TX, TY, whereas F(X land Y) branches into FX, FY. The notation is to be understood analogously for rules 3 and 4. Often, in tableaux for classical logic, the signed formula notation is simplified so that Tvarphi is written simply as varphi, and Fvarphi as negvarphi, which accounts for naming rule 1 the ”Rule of Double Negation”.One constructs a tableau for a set of formulas by applying the rules to produce more lines and tree branches until every line has been used, producing a complete tableau. In some cases, a branch can come to contain both TX and FX for some X, which is to say, a contradiction. In that case, the branch is said to close. If every branch in a tree closes, the tree itself is said to close. In virtue of the rules for construction of tableaux, a closed tree is a proof that the original formula, or set of formulas, used to construct it was itself self-contradictory, and therefore false. Conversely, a tableau can also prove that a logical formula is tautologous: if a formula is tautologous, its negation is a contradiction, so a tableau built from its negation will close.To construct a tableau for an argument langle {varphi_1, varphi_2, varphi_3, ..., varphi_n} , psi rangle, one first writes out the set of premise formulas, {varphi_1, varphi_2, varphi_3, ..., varphi_n}, with one formula on each line, signed with T (that is, Tvarphi for each Tvarphi in the set); and together with those formulas (the order is unimportant), one also writes out the conclusion, psi, signed with F (that is, Fpsi). One then produces a truth tree (analytic tableau) by using all those lines according to the rules. A closed tree will be proof that the argument was valid, in virtue of the fact that varphi models psi if, and only if, { varphi, simpsi } is inconsistent (also written as varphi, simpsi models).

List of classically valid argument forms

Using semantic checking methods, such as truth tables or semantic tableaux, to check for tautologies and semantic consequences, it can be shown that, in classical logic, the following classical argument forms are semantically valid, i.e., these tautologies and semantic consequences hold. We use varphi ⟚ psi to denote equivalence of varphi and psi, that is, as an abbreviation for both varphi models psi and psi models varphi; as an aid to reading the symbols, a description of each formula is given. The description reads the symbol ⊧ (called the “double turnstile“) as “therefore”, which is a common reading of it,BOOK, Lawson, Mark V., A first course in logic, 2019, CRC Press, Taylor & Francis Group, 978-0-8153-8664-3, Boca Raton, example 1.58, although many authors prefer to read it as “entails”,BOOK, Dean, Neville, Logic and language, 2003, Palgrave Macmillan, 978-0-333-91977-4, Basingstoke, 66, or as “models”.BOOK, Chiswell, Ian, Mathematical logic, Hodges, Wilfrid, 2007, Oxford university press, 978-0-19-857100-1, Oxford texts in logic, Oxford, 3, {| class=“wikitable” style="margin:auto;” “! Name! Sequent! Description| Modus Ponens| Modus Tollens| Hypothetical Syllogism| Bidirectional Dilemma

Disjunctive syllogism>Disjunctive Syllogism
Constructive dilemma>Constructive Dilemma
Destructive dilemma>Destructive Dilemma
Conjunction elimination>Simplification
Logical conjunction>Conjunction
Logical disjunction>Addition
Distributive property>Composition
De Morgan’s laws>De Morgan’s Theorem (1)
De Morgan’s laws>De Morgan’s Theorem (2)
Commutative property>Commutation (1)
Commutative property>Commutation (2)
Commutative property>Commutation (3)
Associative property>Association (1)
Associative property>Association (2)
Distributive property>Distribution (1)
Distributive property>Distribution (2)
Double negation elimination>Double Negation
Transposition (logic)>Transposition
Material implication (rule of inference)>Material Implication
Material equivalence>Material Equivalence (1)
Material equivalence>Material Equivalence (2)
Material equivalence>Material Equivalence (3)
Exportation (logic)>Exportation	OLD DOMINION UNIVERSITY,	p}} and {{mvar	r}} is true) we can prove (if {{mvar	r}} is true, if {{mvar|p}} is true)

Exportation (logic)>Importation
Tautology (rule of inference)>Tautology (1)
Tautology (rule of inference)>Tautology (2)
Law of excluded middle>Tertium non datur (Law of Excluded Middle)
Law of noncontradiction>Law of Non-Contradiction
Principle of explosion>Explosion	Natural deduction, since it is a method of syntactical proof, is specified by providing inference rules (also called rules of proof) for a language with the typical set of connectives { -, &, lor, to, leftrightarrow }; no axioms are used other than these rules.BOOK, Lemmon, Edward John, Beginning logic, 1998, Chapman & Hall/CRC, 978-0-412-38090-7, Boca Raton, FL, passim, especially 39-40, The rules are covered below, and a proof example is given afterwards. Notation styles Different authors vary to some extent regarding which inference rules they give, which will be noted. More striking to the look and feel of a proof, however, is the variation in notation styles. The {{section link||Gentzen notation}}, which was covered earlier for a short argument, can actually be stacked to produce large tree-shaped natural deduction proofs—not to be confused with “truth trees”, which is another name for analytic tableaux. There is also a style due to StanisÅ‚aw JaÅ›kowski, where the formulas in the proof are written inside various nested boxes, and there is a simplification of JaÅ›kowski’s style due to Fredric Fitch (Fitch notation), where the boxes are simplified to simple horizontal lines beneath the introductions of suppositions, and vertical lines to the left of the lines that are under the supposition. Lastly, there is the only notation style which will actually be used in this article, which is due to Patrick Suppes, but was much popularized by E.J. Lemmon and Benson Mates.WEB, Natural Deduction Systems in Logic > Notes (Stanford Encyclopedia of Philosophy),plato.stanford.edu/entries/natural-deduction/notes.html#note-21, 2024-04-19, plato.stanford.edu, en, This method has the advantage that, graphically, it is the least intensive to produce and display, which made it a natural choice for the editor who wrote this part of the article, who did not understand the complex LaTeX commands that would be required to produce proofs in the other methods.A proof, then, laid out in accordance with the Suppes–Lemmon notation style, is a sequence of lines containing sentences, where each sentence is either an assumption, or the result of applying a rule of proof to earlier sentences in the sequence. Each line of proof is made up of a sentence of proof, together with its annotation, its assumption set, and the current line number. The assumption set lists the assumptions on which the given sentence of proof depends, which are referenced by the line numbers. The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence. See the {{section link||Natural deduction proof example}}. Inference rules Natural deduction inference rules, due ultimately to Gentzen, are given below. There are ten primitive rules of proof, which are the rule assumption, plus four pairs of introduction and elimination rules for the binary connectives, and the rule reductio ad adbsurdum. Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination, and MTT and DN are commonly given rules, although they are not primitive.{| class=“wikitable” style="margin:auto;“|+ List of Inference Rules

! Rule Name! Alternative names! Annotation!Assumption set! Statement

	| A	| At any stage of the argument, introduce a proposition as an assumption of the argument.

		URL=HTTPS://WWW.WORLDCAT.ORG/TITLE/962129086	DATE=2017	ISBN=978-1-55481-332-2	LOCATION=PETERBOROUGH, ONTARIO	| m, n &I	m and n.>| From varphi and psi at lines m and n, infer varphi ~ & ~ psi.

	| m &E	m.>| From varphi ~ & ~ psi at line m, infer varphi and psi.

	| m ∨I	m.>| From varphi at line m, infer varphi lor psi, whatever psi may be.

	| j,k,l,m,n ∨E	j,k,l,m,n.>| From varphi lor psi at line j, and an assumption of varphi at line k, and a derivation of chi from varphi at line l, and an assumption of psi at line m, and a derivation of chi from psi at line n, infer chi.

|Disjunctive Syllogism|Wedge elimination (∨E), modus tollendo ponens (MTP)|m,n DS|The union of the assumption sets at lines m and n.|From varphi lor psi at line m and - varphi at line n, infer psi; from varphi lor psi at line m and - psi at line n, infer varphi.

	| m, n →E	m and n.>| From varphi to psi at line m, and varphi at line n, infer psi.

	| n, →I (m)	n, excepting m, the line where the antecedent was assumed.>| From psi at line n, following from the assumption of varphi at line m, infer varphi to psi.

	| m, n RAA (k)	m and n, excluding k (the denied assumption).>	group=lower-alpha|To simplify the statement of the rule, the word “denial” here is used in this way: the denial of a formula varphi that is not a negation is - varphi, whereas a negation, - varphi, has two denials, viz., varphi and - - varphi.}} at lines m and n, infer the denial of any assumption appearing in the proof (at line k).

	Df ↔), biconditional introduction>| m, n ↔ I	m and n.>| From varphi to psi and psi to varphi at lines m and n, infer varphi leftrightarrow psi.

	Df ↔), biconditional elimination>| m ↔ E	m.>| From varphi leftrightarrow psi at line m, infer either varphi to psi or psi to varphi.

	| m DN	m.>| From - - varphi at line m, infer varphi.

	| m, n MTT	m and n.>| From varphi to psi at line m, and - psi at line n, infer - varphi.

Natural deduction proof example

The proof below derives -P from P to Q and -Q using only MPP and RAA, which shows that MTT is not a primitive rule, since it can be derived from those two other rules.{| class=“wikitable” style="margin:auto;“|+ Derivation of MTT from MPP and RAA! Assumption set! Line number! Sentence of proof! Annotation

1}}	{{EquationRef		| A

2}}	{{EquationRef		| A

3}}	{{EquationRef		| A

1}}, {{EquationRef		4}}	Q	{{EquationRef	3}} →E

1}}, {{EquationRef		5}}	-P	{{EquationRef	4}} RAA

Other example syntactic proof systems

{{Unreferenced section|date=March 2024}}Consider again the logical form of the {{section link||Example argument}}, formalized as in {{section link||Formalization}}: begin{array}{rl}1. & P to Q 2. & P hlinetherefore & Qend{array}The logical form of this argument is modus ponens, which is a classically valid form. It generalizes schematically. Thus, where {{mvar|φ}} and {{mvar|ψ}} may be any propositions at all, rather than only atomic propositions (cf. {{section link||Constants and schemata}}): begin{array}{rl}1. & varphi to psi 2. & varphi hlinetherefore & psiend{array}Other argument forms are convenient, but not necessary. Given a complete set of axioms (see below for one such set), modus ponens is sufficient to prove all other argument forms in propositional logic, thus they may be considered to be a derivative. Note, this is not true of the extension of propositional logic to other logics like first-order logic. First-order logic requires at least one additional rule of inference in order to obtain completeness.The significance of argument in formal logic is that one may obtain new truths from established truths. In the first example above, given the two premises, the truth of {{mvar|Q}} is not yet known or stated. After the argument is made, {{mvar|Q}} is deduced. In this way, we define a deduction system to be a set of all propositions that may be deduced from another set of propositions. For instance, given the set of propositions A = { P lor Q, neg Q land R, (P lor Q) to R }, we can define a deduction system, {{math|Γ}}, which is the set of all propositions which follow from {{mvar|A}}. Reiteration is always assumed, so P lor Q, neg Q land R, (P lor Q) to R in Gamma. Also, from the first element of {{mvar|A}}, last element, as well as modus ponens, {{mvar|R}} is a consequence, and so R in Gamma. Because we have not included sufficiently complete axioms, though, nothing else may be deduced. Thus, even though most deduction systems studied in propositional logic are able to deduce (P lor Q) leftrightarrow (neg P to Q), this one is too weak to prove such a proposition.

Formal structure for example systems

One of the main uses of a propositional calculus, when interpreted for logical applications, is to determine relations of logical equivalence between propositional formulas. These relationships are determined by means of the available transformation rules, sequences of which are called derivations or proofs.The following examples of proof systems for a propositional calculus will assume a calculus defined as a formal system mathcal{L} = mathcal{L} left( Alpha, Omega, Zeta, Iota right), where:

• The alpha set Alpha is a countably infinite set of mathcal{L}’s atomic formulas or propositional variables. In the examples to follow, the elements of Alpha are typically the letters {{mvar|p}}, {{mvar|q}}, {{mvar|r}}, and so on.
• The omega set {{math|Ω}} is a finite set of elements called operator symbols or logical connectives. The set {{math|Ω}} is partitioned into disjoint subsets as Omega = Omega_0 cup Omega_1 cup cdots cup Omega_j cup cdots cup Omega_m., where, Omega_j is the set of operator symbols of arity {{mvar|j}}. For instance, a partition of {{math|Ω}} for the typical five connectives would have Omega_1 = { lnot }, and Omega_2 subseteq { land, lor, to, leftrightarrow }. Also, the constant logical values are treated as operators of arity zero, so that Omega_0 = { bot, top }.

• The zeta set Zeta is a finite set of transformation rules, called inference rules when they acquire logical applications.
• The iota set Iota is a countable set of initial points that are called axioms when they receive logical interpretations.

The language mathcal{L} is its set of well-formed formulas, inductively defined by the following rules:

1. Base: Any element of the alpha set Alpha is a formula of mathcal{L}.
2. If p_1, p_2, ldots, p_j are formulas and f is in Omega_j, then f p_1 p_2 ldots p_j is a formula.
3. Closed: Nothing else is a formula of mathcal{L}.

Repeated applications of these rules permits the construction of complex formulas. Examples of formulas that follow these rules include “{{mvar|p}}” (by rule 1), “neg p” (by rule 2), “{{mvar|q}}” (by rule 1), and “neg p lor q ” (by rule 2).{{refn|group=lower-alpha|Formally, rule 2 obtains formulas in Polish notation, i.e. lor neg p q in this example. For convenience, we will use the common infix notation instead in this and all following examples.}}In the discussion to follow, after a proof system is defined, a proof is presented as a sequence of numbered lines, with each line consisting of a single formula followed by a reason or justification for introducing that formula. Each premise of the argument, that is, an assumption introduced as a hypothesis of the argument, is listed at the beginning of the sequence and is marked as a “premise” in lieu of other justification. The conclusion is listed on the last line. A proof is complete if every line follows from the previous ones by the correct application of a transformation rule. (For a contrasting approach, see proof-trees).

Jan Łukasiewicz axiomatic proof system example

Let mathcal{L}_{Ax} = mathcal{L}(Alpha,Omega,Zeta,Iota), where Alpha, Omega, Zeta, Iota are defined as follows:

• The set Alpha, the countably infinite set of symbols that serve to represent logical propositions: Alpha = {p, q, r, s, t, u, p_2, ldots }.
• The functionally complete set Omega of logical operators (logical connectives and negation) is as follows. Of the three connectives for conjunction, disjunction, and implication (wedge, lor, and {{math|→}}), one can be taken as primitive and the other two can be defined in terms of it and negation ({{math|¬}}).Wernick, William (1942) “Complete Sets of Logical Functions,” Transactions of the American Mathematical Society 51, pp. 117–132. Alternatively, all of the logical operators may be defined in terms of a sole sufficient operator, such as the Sheffer stroke (nand). The biconditional (a leftrightarrow b) can of course be defined in terms of conjunction and implication as (a to b) land (b to a). Adopting negation and implication as the two primitive operations of a propositional calculus is tantamount to having the omega set Omega = Omega_1 cup Omega_2 partitioned as Omega_1 = { lnot }, and Omega_2 = { to }. Then a lor b is defined as neg a to b, and a land b is defined as neg(a to neg b).

• The set Iota (the set of initial points of logical deduction, i.e., logical axioms) is the axiom system proposed by Jan Łukasiewicz, and used as the propositional-calculus part of a Hilbert system. The axioms are all substitution instances of:
  • p to (q to p)
  • (p to (q to r)) to ((p to q) to (p to r))
  • (neg p to neg q) to (q to p)
• The set Zeta of transformation rules (rules of inference) is the sole rule modus ponens (i.e., from any formulas of the form varphi and (varphi to psi), infer psi).

This system is used in Metamath set.mm formal proof database.

Example of a proof in an axiomatic propositional calculus system

We now prove the same theorem A to A in the axiomatic system by Jan Łukasiewicz described above, which is an example of a Hilbert-style deductive system for the classical propositional calculus.The axioms are: And the proof is as follows:

1. A to ((B to A) to A)       (instance of (A1))
2. (A to ((B to A) to A)) to ((A to (B to A)) to (A to A))       (instance of (A2))
3. (A to (B to A)) to (A to A)       (from (1) and (2) by modus ponens)
4. A to (B to A)       (instance of (A1))
5. A to A       (from (4) and (3) by modus ponens)

Soundness and completeness of the rules

The crucial properties of this set of rules are that they are sound and complete. Informally this means that the rules are correct and that no other rules are required. These claims can be made more formal as follows.The proofs for the soundness and completeness of the propositional logic are not themselves proofs in propositional logic; these are theorems in ZFC used as a metatheory to prove properties of propositional logic.We define a truth assignment as a function that maps propositional variables to true or false. Informally such a truth assignment can be understood as the description of a possible state of affairs (or possible world) where certain statements are true and others are not. The semantics of formulas can then be formalized by defining for which “state of affairs” they are considered to be true, which is what is done by the following definition.We define when such a truth assignment {{mvar|A}} satisfies a certain well-formed formula with the following rules:

• {{mvar|A}} satisfies the propositional variable {{mvar|P}} if and only if {{math|A(P) {{=}} true}}
• {{mvar|A}} satisfies {{math|¬φ}} if and only if {{mvar|A}} does not satisfy {{mvar|φ}}
• {{mvar|A}} satisfies {{math|(φ ∧ ψ)}} if and only if {{mvar|A}} satisfies both {{mvar|φ}} and {{mvar|ψ}}
• {{mvar|A}} satisfies {{math|(φ ∨ ψ)}} if and only if {{mvar|A}} satisfies at least one of either {{mvar|φ}} or {{mvar|ψ}}
• {{mvar|A}} satisfies {{math|(φ → ψ)}} if and only if it is not the case that {{mvar|A}} satisfies {{mvar|φ}} but not {{mvar|ψ}}
• {{mvar|A}} satisfies {{math|(φ ↔ ψ)}} if and only if {{mvar|A}} satisfies both {{mvar|φ}} and {{mvar|ψ}} or satisfies neither one of them

With this definition we can now formalize what it means for a formula {{mvar|φ}} to be implied by a certain set {{mvar|S}} of formulas. Informally this is true if in all worlds that are possible given the set of formulas {{mvar|S}} the formula {{mvar|φ}} also holds. This leads to the following formal definition: We say that a set {{mvar|S}} of well-formed formulas semantically entails (or implies) a certain well-formed formula {{mvar|φ}} if all truth assignments that satisfy all the formulas in {{mvar|S}} also satisfy {{mvar|φ}}.Finally we define syntactical entailment such that {{mvar|φ}} is syntactically entailed by {{mvar|S}} if and only if we can derive it with the inference rules that were presented above in a finite number of steps. This allows us to formulate exactly what it means for the set of inference rules to be sound and complete:Soundness: If the set of well-formed formulas {{mvar|S}} syntactically entails the well-formed formula {{mvar|φ}} then {{mvar|S}} semantically entails {{mvar|φ}}.Completeness: If the set of well-formed formulas {{mvar|S}} semantically entails the well-formed formula {{mvar|φ}} then {{mvar|S}} syntactically entails {{mvar|φ}}.For the above set of rules this is indeed the case.

Sketch of a soundness proof

(For most logical systems, this is the comparatively “simple” direction of proof)Notational conventions: Let {{mvar|G}} be a variable ranging over sets of sentences. Let {{mvar|A, B}} and {{mvar|C}} range over sentences. For “{{mvar|G}} syntactically entails {{mvar|A}}” we write “{{mvar|G}} proves {{mvar|A}}”. For “{{mvar|G}} semantically entails {{mvar|A}}” we write “{{mvar|G}} implies {{mvar|A}}”.We want to show: {{math|(A)(G)}} (if {{mvar|G}} proves {{mvar|A}}, then {{mvar|G}} implies {{mvar|A}}).We note that “{{mvar|G}} proves {{mvar|A}}” has an inductive definition, and that gives us the immediate resources for demonstrating claims of the form “If {{mvar|G}} proves {{mvar|A}}, then ...”. So our proof proceeds by induction.{{ordered list|list-style-type=upper-romanA}} is a member of {{mvarG}} implies {{mvar|A}}. A}} is an axiom, then {{mvarA}}. n}}, the length of the proof):{hide}ordered list|list-style-type=lower-alpha }}Notice that Basis Step II can be omitted for natural deduction systems because they have no axioms. When used, Step II involves showing that each of the axioms is a (semantic) logical truth.The Basis steps demonstrate that the simplest provable sentences from {{mvar|G}} are also implied by {{mvar|G}}, for any {{mvar|G}}. (The proof is simple, since the semantic fact that a set implies any of its members, is also trivial.) The Inductive step will systematically cover all the further sentences that might be provable—by considering each case where we might reach a logical conclusion using an inference rule—and shows that if a new sentence is provable, it is also logically implied. (For example, we might have a rule telling us that from “{{mvar|A}}” we can derive “{{mvar|A}} or {{mvar|B}}”. In III.a We assume that if {{mvar|A}} is provable it is implied. We also know that if {{mvar|A}} is provable then “{{mvar|A}} or {{mvar|B}}” is provable. We have to show that then “{{mvar|A}} or {{mvar|B}}” too is implied. We do so by appeal to the semantic definition and the assumption we just made. {{mvar|A}} is provable from {{mvar|G}}, we assume. So it is also implied by {{mvar|G}}. So any semantic valuation making all of {{mvar|G}} true makes {{mvar|A}} true. But any valuation making {{mvar|A}} true makes “{{mvar|A}} or {{mvar|B}}” true, by the defined semantics for “or”. So any valuation which makes all of {{mvar|G}} true makes “{{mvar|A}} or {{mvar|B}}” true. So “{{mvar|A}} or {{mvar|B}}” is implied.) Generally, the Inductive step will consist of a lengthy but simple case-by-case analysis of all the rules of inference, showing that each “preserves” semantic implication.By the definition of provability, there are no sentences provable other than by being a member of {{mvar|G}}, an axiom, or following by a rule; so if all of those are semantically implied, the deduction calculus is sound.

Sketch of completeness proof

(This is usually the much harder direction of proof.)We adopt the same notational conventions as above.We want to show: If {{mvar|G}} implies {{mvar|A}}, then {{mvar|G}} proves {{mvar|A}}. We proceed by contraposition: We show instead that if {{mvar|G}} does not prove {{mvar|A}} then {{mvar|G}} does not imply {{mvar|A}}. If we show that there is a model where {{mvar|A}} does not hold despite {{mvar|G}} being true, then obviously {{mvar|G}} does not imply {{mvar|A}}. The idea is to build such a model out of our very assumption that {{mvar|G}} does not prove {{mvar|A}}.{{ordered list|list-style-type=upper-romanG}} does not prove {{mvar|A}}. (Assumption) G}} does not prove {{mvarmaximal set, {{math>G∗}}, which is a superset of {{mvarA}}. G∗}} is a maximal set with respect to {{mvartruth-like. This means that it contains {{mvar>C}} if and only if it does not contain {{mvarC}} and contains “If {{mvarB}}” then it also contains {{mvar|B}}; and so forth. In order to show this, one has to show the axiomatic system is strong enough for the following:

• For any formulas {{mvar|C}} and {{mvar|D}}, if it proves both {{mvar|C}} and {{mvar|¬C}}, then it proves {{mvar|D}}. From this it follows, that a maximal set with respect to {{mvar|A}} cannot prove both {{mvar|C}} and {{mvar|¬C}}, as otherwise it would prove {{mvar|A}}.
• For any formulas {{mvar|C}} and {{mvar|D}}, if it proves both {{mvar|C}}→{{mvar|D}} and {{mvar|¬C}}→{{mvar|D}}, then it proves {{mvar|D}}. This is used, together with the deduction theorem, to show that for any formula, either it or its negation is in {{math|G∗}}: Let {{mvar|B}} be a formula not in {{math|G∗}}; then {{math|G∗}} with the addition of {{mvar|B}} proves {{mvar|A}}. Thus from the deduction theorem it follows that {{math|G∗}} proves {{mvar|B}}→{{mvar|A}}. But suppose {{mvar|¬B}} were also not in {{math|G∗}}, then by the same logic {{math|G∗}} also proves {{mvar|¬B}}→{{mvar|A}}; but then {{math|G∗}} proves {{mvar|A}}, which we have already shown to be false.
• For any formulas {{mvar|C}} and {{mvar|D}}, if it proves {{mvar|C}} and {{mvar|D}}, then it proves {{mvar|C}}→{{mvar|D}}.
• For any formulas {{mvar|C}} and {{mvar|D}}, if it proves {{mvar|C}} and {{mvar|¬D}}, then it proves ¬({{mvar|C}}→{{mvar|D}}).
• For any formulas {{mvar|C}} and {{mvar|D}}, if it proves {{mvar|¬C}}, then it proves {{mvar|C}}→{{mvar|D}}.

If additional logical operation (such as conjunction and/or disjunction) are part of the vocabulary as well, then there are additional requirement on the axiomatic system (e.g. that if it proves {{mvar|C}} and {{mvar|D}}, it would also prove their conjunction).G∗}} is truth-like there is a {{mathG∗}}-Canonical valuation of the language: one that makes every sentence in {{math>G∗}} true and everything outside {{math|G∗}} false while still obeying the laws of semantic composition in the language. The requirement that it is truth-like is needed to guarantee that the laws of semantic composition in the language will be satisfied by this truth assignment.G∗}}-canonical valuation will make our original set {{mvarA}} false. G}} are true and {{mvarG}} does not (semantically) imply {{mvar|A}}. }}Thus every system that has modus ponens as an inference rule, and proves the following theorems (including substitutions thereof) is complete:

• p to (neg p to q)
• (p to q) to ((neg p to q) to q)
• p to (q to (p to q))
• p to (neg q to neg (p to q))
• neg p to (p to q)
• p to p
• p to (q to p)
• (p to (q to r)) to ((p to q) to (p to r))

The first five are used for the satisfaction of the five conditions in stage III above, and the last three for proving the deduction theorem.

Example

As an example, it can be shown that as any other tautology, the three axioms of the classical propositional calculus system described earlier can be proven in any system that satisfies the above, namely that has modus ponens as an inference rule, and proves the above eight theorems (including substitutions thereof). Out of the eight theorems, the last two are two of the three axioms; the third axiom, (neg q to neg p) to (p to q), can be proven as well, as we now show.For the proof we may use the hypothetical syllogism theorem (in the form relevant for this axiomatic system), since it only relies on the two axioms that are already in the above set of eight theorems.The proof then is as follows:

1. q to (p to q)       (instance of the 7th theorem)
2. (q to (p to q)) to ((neg q to neg p) to (q to (p to q)))       (instance of the 7th theorem)
3. (neg q to neg p) to (q to (p to q))       (from (1) and (2) by modus ponens)
4. (neg p to (p to q)) to ((neg q to neg p) to (neg qto (pto q)))       (instance of the hypothetical syllogism theorem)
5. (neg p to (p to q))       (instance of the 5th theorem)
6. (neg q to neg p) to (neg qto (pto q))       (from (5) and (4) by modus ponens)
7. (q to (p to q)) to ((neg q to (p to q)) to (p to q))       (instance of the 2nd theorem)
8. ((q to (p to q)) to ((neg q to (p to q)) to (p to q)) ) to ((neg q to neg p) to ((q to (p to q)) to ((neg q to (p to q)) to (p to q))))       (instance of the 7th theorem)
9. (neg q to neg p) to ((q to (p to q)) to ((neg q to (p to q)) to (p to q)))       (from (7) and (8) by modus ponens)
10. ((neg q to neg p) to ((q to (p to q)) to ((neg q to (p to q)) to (p to q)))) to
11. :: (((neg q to neg p) to (q to (p to q))) to ((neg q to neg p) to ((neg q to (p to q)) to (p to q))))       (instance of the 8th theorem)
12. ((neg q to neg p) to (q to (p to q))) to ((neg q to neg p) to ((neg q to (p to q)) to (p to q)))       (from (9) and (10) by modus ponens)
13. (neg q to neg p) to ((neg q to (p to q)) to (p to q))       (from (3) and (11) by modus ponens)
14. ((neg q to neg p) to ((neg q to (p to q)) to (p to q))) to (((neg q to neg p) to (neg q to (p to q))) to ((neg q to neg p) to (p to q)))       (instance of the 8th theorem)
15. ((neg q to neg p) to (neg q to (p to q))) to ((neg q to neg p) to (p to q))       (from (12) and (13) by modus ponens)
16. (neg q to neg p) to (p to q)       (from (6) and (14) by modus ponens)

Verifying completeness for the classical propositional calculus system

We now verify that the classical propositional calculus system described earlier can indeed prove the required eight theorems mentioned above. We use several lemmas proven here: We also use the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.

• p to (neg p to q) - proof:
  • p to (neg q to p)       (instance of (A1))
  • (neg q to p) to (neg p to negneg q)       (instance of (TR1))
  • p to (neg p to negneg q)       (from (1) and (2) using the hypothetical syllogism metatheorem)
  • negneg q to q       (instance of (DN1))
  • (negneg q to q) to ((neg p to negneg q) to (neg p to q))       (instance of (HS1))
  • (neg p to negneg q) to (neg p to q)       (from (4) and (5) using modus ponens)
  • p to (neg p to q)       (from (3) and (6) using the hypothetical syllogism metatheorem)
• (p to q) to ((neg p to q) to q) - proof:
  • (p to q) to ((neg q to p) to (neg q to q))       (instance of (HS1))
  • (neg q to q) to q       (instance of (L3))
  • ((neg q to q) to q) to (((neg q to p) to (neg q to q)) to ((neg q to p) to q))       (instance of (HS1))
  • ((neg q to p) to (neg q to q)) to ((neg q to p) to q)       (from (2) and (3) by modus ponens)
  • (p to q) to ((neg q to p) to q)       (from (1) and (4) using the hypothetical syllogism metatheorem)
  • (neg p to q) to (neg q to p)       (instance of (TR2))
  • ((neg p to q) to (neg q to p)) to (((neg q to p) to q) to ((neg p to q) to q))       (instance of (HS2))
  • ((neg q to p) to q) to ((neg p to q) to q)       (from (6) and (7) using modus ponens)
  • (p to q) to ((neg p to q) to q)       (from (5) and (8) using the hypothetical syllogism metatheorem)
• p to (q to (p to q)) - proof:
  • q to (p to q)       (instance of (A1))
  • (q to (p to q)) to (p to (q to (p to q)))       (instance of (A1))
  • p to (q to (p to q))       (from (1) and (2) using modus ponens)
• p to (neg q to neg (p to q)) - proof:
  • p to ((p to q) to q)       (instance of (L1))
  • ((p to q) to q) to (neg q to neg (p to q))       (instance of (TR1))
  • p to (neg q to neg (p to q))       (from (1) and (2) using the hypothetical syllogism metatheorem)
• neg p to (p to q) - proof:
  • neg p to (neg q to neg p)       (instance of (A1))
  • (neg q to neg p) to (p to q)       (instance of (A3))
  • neg p to (p to q)       (from (1) and (2) using the hypothetical syllogism metatheorem)
• p to p - proof given in the proof example above
• p to (q to p) - axiom (A1)
• (p to (q to r)) to ((p to q) to (p to r)) - axiom (A2)

Another outline for a completeness proof

If a formula is a tautology, then there is a truth table for it which shows that each valuation yields the value true for the formula. Consider such a valuation. By mathematical induction on the length of the subformulas, show that the truth or falsity of the subformula follows from the truth or falsity (as appropriate for the valuation) of each propositional variable in the subformula. Then combine the lines of the truth table together two at a time by using “({{mvar|P}} is true implies {{mvar|S}}) implies (({{mvar|P}} is false implies {{mvar|S}}) implies {{mvar|S}})”. Keep repeating this until all dependencies on propositional variables have been eliminated. The result is that we have proved the given tautology. Since every tautology is provable, the logic is complete.

More complex axiomatic proof system example

It is possible to define another version of propositional calculus, which defines most of the syntax of the logical operators by means of axioms, and which uses only one inference rule.

Axioms

Let {{mvar|φ}}, {{mvar|χ}}, and {{mvar|ψ}} stand for well-formed formulas. (The well-formed formulas themselves would not contain any Greek letters, but only capital Roman letters, connective operators, and parentheses.) Then the axioms are as follows:{| style="margin:auto;” class=“wikitable”|+ Axioms! Name! Axiom Schema! Description

THEN-1}}| phi to (chi to phi)	χ}}, implication introduction

THEN-2}}| (phi to (chi to psi)) to ((phi to chi) to (phi to psi))| Distribute hypothesis phi over implication

AND-1}}| phi land chi to phi| Eliminate conjunction

AND-2}}| phi land chi to chi|

AND-3}}| phi to (chi to (phi land chi))| Introduce conjunction

OR-1}}| phi to phi lor chi| Introduce disjunction

OR-2}}| chi to phi lor chi|

OR-3}}| (phi to psi) to ((chi to psi) to (phi lor chi to psi))| Eliminate disjunction

NOT-1}}| (phi to chi) to ((phi to neg chi) to neg phi)| Introduce negation

NOT-2}}| phi to (neg phi to chi)| Eliminate negation

NOT-3}}| phi lor neg phi| Excluded middle, classical logic

IFF-1}}| (phi leftrightarrow chi) to (phi to chi)| Eliminate equivalence

IFF-2}}| (phi leftrightarrow chi) to (chi to phi)|

IFF-3}}| (phi to chi) to ((chi to phi) to (phi leftrightarrow chi))| Introduce equivalence

• Axiom {{EquationNote|THEN-2}} may be considered to be a “distributive property of implication with respect to implication.”
• Axioms {{EquationNote|AND-1}} and {{EquationNote|AND-2}} correspond to “conjunction elimination”. The relation between {{EquationNote|AND-1}} and {{EquationNote|AND-2}} reflects the commutativity of the conjunction operator.
• Axiom {{EquationNote|AND-3}} corresponds to “conjunction introduction.”
• Axioms {{EquationNote|OR-1}} and {{EquationNote|OR-2}} correspond to “disjunction introduction.” The relation between {{EquationNote|OR-1}} and {{EquationNote|OR-2}} reflects the commutativity of the disjunction operator.
• Axiom {{EquationNote|NOT-1}} corresponds to “reductio ad absurdum.”
• Axiom {{EquationNote|NOT-2}} says that “anything can be deduced from a contradiction.”
• Axiom {{EquationNote|NOT-3}} is called “tertium non-datur” (Latin: “a third is not given“) and reflects the semantic valuation of propositional formulas: a formula can have a truth-value of either true or false. There is no third truth-value, at least not in classical logic. Intuitionistic logicians do not accept the axiom {{EquationNote|NOT-3}}.

Inference rule

The inference rule is modus ponens:

Meta-inference rule

Let a demonstration be represented by a sequence, with hypotheses to the left of the turnstile and the conclusion to the right of the turnstile. Then the deduction theorem can be stated as follows: This deduction theorem (DT) is not itself formulated with propositional calculus: it is not a theorem of propositional calculus, but a theorem about propositional calculus. In this sense, it is a meta-theorem, comparable to theorems about the soundness or completeness of propositional calculus.On the other hand, DT is so useful for simplifying the syntactical proof process that it can be considered and used as another inference rule, accompanying modus ponens. In this sense, DT corresponds to the natural conditional proof inference rule which is part of the first version of propositional calculus introduced in this article.The converse of DT is also valid: in fact, the validity of the converse of DT is almost trivial compared to that of DT: The converse of DT has powerful implications: it can be used to convert an axiom into an inference rule. For example, by axiom AND-1 we have, which can be transformed by means of the converse of the deduction theorem into which tells us that the inference rule is admissible. This inference rule is conjunction elimination, one of the ten inference rules used in the first version (in this article) of the propositional calculus.

Example of a proof in the more complex axiomatic system

The following is an example of a (syntactical) demonstration, involving only axioms {{EquationNote|THEN-1}} and {{EquationNote|THEN-2}}:Prove: A to A (Reflexivity of implication).Proof:

1. (A to ((B to A) to A)) to ((A to (B to A)) to (A to A))
2. : Axiom {{EquationNote|THEN-2}} with phi = A, chi = B to A, psi = A
3. A to ((B to A) to A)
4. : Axiom {{EquationNote|THEN-1}} with phi = A, chi = B to A
5. (A to (B to A)) to (A to A)
6. : From (1) and (2) by modus ponens.
7. A to (B to A)
8. : Axiom {{EquationNote|THEN-1}} with phi = A, chi = B
9. A to A
10. : From (3) and (4) by modus ponens.

Solvers

One notable difference between propositional calculus and predicate calculus is that satisfiability of a propositional formula is decidable.W. V. O. Quine, Mathematical Logic (1980), p.81. Harvard University Press, 0-674-55451-5 Deciding satisfiability of propositional logic formulas is an NP-complete problem. However, practical methods exist (e.g., DPLL algorithm, 1962; Chaff algorithm, 2001) that are very fast for many useful cases. Recent work has extended the SAT solver algorithms to work with propositions containing arithmetic expressions; these are the SMT solvers.

See also

Higher logical levels

• First-order logic
• Second-order propositional logic
• Second-order logic
• Higher-order logic

Related topics

{{Div col|colwidth=20em}}

• Boolean algebra (logic)
• Boolean algebra (structure)
• Boolean algebra topics
• Boolean domain
• Boolean function
• Boolean-valued function
• Categorical logic
• Combinational logic
• Combinatory logic
• Conceptual graph
• Disjunctive syllogism
• Entitative graph
• Equational logic
• Existential graph
• Frege’s propositional calculus
• Implicational propositional calculus
• Intuitionistic propositional calculus
• Jean Buridan
• Laws of Form
• List of logic symbols
• Logical graph
• Logical NOR
• Logical value
• Mathematical logic
• Operation (mathematics)
• Paul of Venice
• Peirce’s law
• Peter of Spain (author)
• Propositional formula
• Symmetric difference
• Tautology (rule of inference)
• Truth function
• Truth table
• Walter Burley
• William of Sherwood

{{Div col end}}

Notes

{{reflist|group=lower-alpha}}

References

{{Reflist|30em}}

Further reading

• Brown, Frank Markham (2003), Boolean Reasoning: The Logic of Boolean Equations, 1st edition, Kluwer Academic Publishers, Norwell, MA. 2nd edition, Dover Publications, Mineola, NY.
• Chang, C.C. and Keisler, H.J. (1973), Model Theory, North-Holland, Amsterdam, Netherlands.
• Kohavi, Zvi (1978), Switching and Finite Automata Theory, 1st edition, McGraw–Hill, 1970. 2nd edition, McGraw–Hill, 1978.
• Korfhage, Robert R. (1974), Discrete Computational Structures, Academic Press, New York, NY.
• Lambek, J. and Scott, P.J. (1986), Introduction to Higher Order Categorical Logic, Cambridge University Press, Cambridge, UK.
• Mendelson, Elliot (1964), Introduction to Mathematical Logic, D. Van Nostrand Company.

Related works

• BOOK, Hofstadter, Douglas, Douglas Hofstadter, (Gödel, Escher, Bach, Gödel, Escher, Bach: An Eternal Golden Braid), 1979, Basic Books, 978-0-465-02656-2,

External links

{{Commons category}}

• Klement, Kevin C. (2006), “Propositional Logic”, in James Fieser and Bradley Dowden (eds.), Internet Encyclopedia of Philosophy, Eprint.
• Formal Predicate Calculus, contains a systematic formal development with axiomatic proof
• forall x: an introduction to formal logic, by P.D. Magnus, covers formal semantics and proof theory for sentential logic.
• Chapter 2 / Propositional Logic from Logic In Action
• Propositional sequent calculus prover on Project Nayuki. (note: implication can be input in the form !X|Y, and a sequent can be a single formula prefixed with > and having no commas)
• Propositional Logic - A Generative Grammar
• A Propositional Calculator that helps to understand simple expressions

{{Classical logic}}{{Formal Fallacy}}{{Mathematical logic}}{{Authority control}}