View source for Propositional calculus

{{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]].<ref name=":1">{{Cite web |title=Propositional Logic {{!}} Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/propositional-logic-sentential-logic/ |access-date=2024-03-22 |language=en-US}}</ref>  It is also called '''(first-order) propositional logic''',<ref name=":2">{{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}}</ref> '''statement logic''',<ref name=":1" /> '''sentential calculus''',<ref name=":18">{{Cite web |last=Weisstein |first=Eric W. |title=Propositional Calculus |url=https://mathworld.wolfram.com/ |access-date=2024-03-22 |website=mathworld.wolfram.com |language=en}}</ref> '''sentential logic''',<ref name=":1" /> or sometimes '''zeroth-order logic'''.<ref name=":10">{{Cite book |last1=Bělohlávek |first1=Radim |title=Fuzzy logic and mathematics: a historical perspective |last2=Dauben |first2=Joseph Warren |last3=Klir |first3=George J. |date=2017 |publisher=Oxford University Press |isbn=978-0-19-020001-5 |location=New York, NY, United States of America |pages=463}}</ref><ref name=":11">{{Cite book |last=Manzano |first=María |title=Extensions of first order logic |date=2005 |publisher=Cambridge University Press |isbn=978-0-521-35435-6 |edition=Digitally printed first paperback version |series=Cambridge tracts in theoretical computer science |location=Cambridge |pages=180}}</ref> It deals with [[propositions]]<ref name=":1" /> (which can be [[Truth value|true or false]])<ref name=":22">{{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}}</ref> and relations between propositions,<ref>{{Cite web |title=Predicate Logic |url=https://www3.cs.stonybrook.edu/~skiena/113/lectures/lecture26/lecture26.html |access-date=2024-03-22 |website=www3.cs.stonybrook.edu}}</ref> including the construction of arguments based on them.<ref>{{Cite web |title=Philosophy 404: Lecture Five |url=https://www.webpages.uidaho.edu/~morourke/404-phil/Summer-99/Lecture%20Notes/5.htm |access-date=2024-03-22 |website=www.webpages.uidaho.edu}}</ref> Compound propositions are formed by connecting propositions by [[logical connective]]s representing the [[truth function]]s of [[Logical conjunction|conjunction]], [[Logical disjunction|disjunction]], [[Material conditional|implication]], [[Logical biconditional|biconditional]], and [[negation]].<ref name=":5">{{Cite web |title=3.1 Propositional Logic |url=https://www.teach.cs.toronto.edu/~csc110y/fall/notes/03-logic/01-propositional-logic.html |access-date=2024-03-22 |website=www.teach.cs.toronto.edu}}</ref><ref name=":0">{{Cite book |title=Semantics: a reader |date=2004 |publisher=Oxford University Press |isbn=978-0-19-513697-5 |editor-last=Davis |editor-first=Steven |location=New York |editor-last2=Gillon |editor-first2=Brendan S.}}</ref><ref name=":3">{{Cite book |last=Plato |first=Jan von |title=Elements of logical reasoning |date=2013 |publisher=Cambridge University press |isbn=978-1-107-03659-8 |edition=1. publ |location=Cambridge |pages=9,32,121}}</ref><ref name=":12">{{Cite web |title=Propositional Logic |url=https://www.cs.miami.edu/home/geoff/Courses/CSC648-12S/Content/Propositional.shtml |access-date=2024-03-22 |website=www.cs.miami.edu}}</ref> 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 [[Quantifier (logic)|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 variable]]s''. These are then used, together with symbols for connectives, to make compound propositions. Because of this, the propositional variables are called ''[[atomic formula]]s'' of a formal zeroth-order language.<ref name=":0" /><ref name=":2" /> While the atomic propositions are typically represented by letters of the [[alphabet]],<ref name=":0" /> 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"
|+ Notational variants of the connectives<ref>{{Cite book |last=Plato |first=Jan von |title=Elements of logical reasoning |date=2013 |publisher=Cambridge University press |isbn=978-1-107-03659-8 |edition=1. publ |location=Cambridge |pages=9}}</ref><ref name=":23">{{Cite web |last=Weisstein |first=Eric W. |title=Connective |url=https://mathworld.wolfram.com/ |access-date=2024-03-22 |website=mathworld.wolfram.com |language=en}}</ref>
|-
! Connective
! Symbol
|-
| [[Logical conjunction|AND]]
| <math>A \land B</math>, <math>A \cdot B</math>, <math>AB</math>, <math>A \& B</math>, <math>A \&\& B</math>
|-
| [[Logical biconditional|equivalent]]
| <math>A \equiv B</math>, <math>A \Leftrightarrow B</math>, <math>A \leftrightharpoons B</math>
|-
| [[Material conditional|implies]]
| <math>A \Rightarrow B</math>, <math>A \supset B</math>, <math>A \rightarrow B</math>
|-
| [[Sheffer stroke|NAND]]
| <math>A \overline{\land} B</math>, <math>A \mid B</math>, <math>\overline{A \cdot B}</math>
|-
| nonequivalent
| <math>A \not\equiv B</math>, <math>A \not\Leftrightarrow B</math>, <math>A \nleftrightarrow B</math>
|-
| [[Logical NOR|NOR]]
| <math>A \overline{\lor} B</math>, <math>A \downarrow B</math>, <math>\overline{A+B}</math>
|-
| [[Negation|NOT]]
| <math>\neg A</math>, <math>-A</math>, <math>\overline{A}</math>, <math>\sim A</math>
|-
| [[Logical disjunction|OR]]
| <math>A \lor B</math>, <math>A + B</math>, <math>A \mid B</math>, <math>A \parallel B</math>
|-
| [[XNOR gate|XNOR]]
| <math>A \odot B</math>
|-
| [[Exclusive or|XOR]]
| <math>A \underline{\lor} B</math>, <math>A \oplus B</math>
|}

The most thoroughly researched branch of propositional logic is '''classical truth-functional propositional logic''',<ref name=":1" /> in which formulas are interpreted as having precisely one of two possible [[truth value]]s, the truth value of ''true'' or the truth value of ''false''.<ref>{{Cite web |title=Propositional Logic {{!}} Brilliant Math & Science Wiki |url=https://brilliant.org/wiki/propositional-logic/ |access-date=2020-08-20 |website=brilliant.org |language=en-us}}</ref> 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''.<ref name=":10" /><ref name=":11" />

== History ==
{{main|History of logic}}
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 BC<ref>{{cite book|url=http://plato.stanford.edu/archives/spr2016/entries/logic-ancient/|title=The Stanford Encyclopedia of Philosophy|first=Susanne|last=Bobzien|chapter=Ancient Logic |editor-first=Edward N.|editor-last=Zalta|date=1 January 2016|publisher=Metaphysics Research Lab, Stanford University |via=Stanford Encyclopedia of Philosophy}}</ref> and expanded by his successor [[Stoics]]. The logic was focused on [[proposition]]s. This was different from the traditional [[syllogism|syllogistic logic]], which focused on [[Syllogisms#Terms in syllogism|terms]]. However, most of the original writings were lost<ref>{{Cite web|title=Propositional Logic {{!}} Internet Encyclopedia of Philosophy|url=https://iep.utm.edu/prop-log/|access-date=2020-08-20|language=en-US}}</ref> 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.<ref>{{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}}</ref>

[[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.<ref>{{cite book|url=http://plato.stanford.edu/archives/spr2014/entries/leibniz-logic-influence/|title=The Stanford Encyclopedia of Philosophy|first=Volker|last=Peckhaus|chapter=Leibniz's Influence on 19th Century Logic |editor-first=Edward N.|editor-last=Zalta|date=1 January 2014|publisher=Metaphysics Research Lab, Stanford University |via=Stanford Encyclopedia of Philosophy}}</ref>

[[Gottlob Frege|Gottlob Frege's]] [[predicate logic]] builds upon propositional logic, and has been described as combining "the distinctive features of syllogistic logic and propositional logic."<ref>{{cite book |title=A Concise Introduction to Logic 10th edition |last=Hurley |first=Patrick |year=2007 |publisher=Wadsworth Publishing |page=392 }}</ref> 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]], [[Method of analytic tableaux|truth trees]] and [[truth-table|truth tables]]. Natural deduction was invented by [[Gerhard Gentzen]] and [[Stanisław Jaśkowski]]. Truth trees were invented by [[Evert Willem Beth]].<ref>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</ref> The invention of truth tables, however, is of uncertain attribution.

Within works by Frege<ref name="Truth in Frege">[https://web.archive.org/web/20120807235445/http://frege.brown.edu/heck/pdf/unpublished/TruthInFrege.pdf Truth in Frege]</ref> and [[Bertrand Russell]],<ref name="Russell Truth-Tables">{{cite web|url=http://digitalcommons.mcmaster.ca/cgi/viewcontent.cgi?article=1219&context=russelljournal|title=Russell: the Journal of Bertrand Russell Studies}}</ref> 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).<ref name="Truth in Frege" /> Besides Frege and Russell, others credited with having ideas preceding truth tables include Philo, Boole, [[Charles Sanders Peirce]],<ref>{{cite journal|last1=Anellis|first1=Irving H.|authorlink=Irving Anellis|title=Peirce's Truth-functional Analysis and the Origin of the Truth Table|journal=History and Philosophy of Logic|date=2012|volume=33|pages=87–97|doi=10.1080/01445340.2011.621702|s2cid=170654885 }}</ref> and [[Ernst Schröder (mathematician)|Ernst Schröder]]. Others credited with the tabular structure include [[Jan Łukasiewicz]], [[Alfred North Whitehead]], [[William Stanley Jevons]], [[John Venn]], and [[Clarence Irving Lewis]].<ref name="Russell Truth-Tables" /> 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.".<ref name="Russell Truth-Tables" />

==Sentences==
{{Main article|Proposition}}
Propositional logic, as currently studied in universities, is a specification of a standard of [[logical consequence]] in which only the meanings of [[Logical connective|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.<ref name=":2" />

=== Declarative sentences ===
Propositional logic deals with '''statements''', which are defined as declarative sentences having truth value.<ref>{{Cite web |title=Part2Mod1: LOGIC: Statements, Negations, Quantifiers, Truth Tables |url=https://www.math.fsu.edu/~wooland/hm2ed/Part2Module1/Part2Module1.html |access-date=2024-03-22 |website=www.math.fsu.edu}}</ref><ref name=":1" /> Examples of statements might include:

* ''[[Wikipedia]] is a free online encyclopedia that anyone can edit.''
* ''[[London]] is the capital of [[England]].''
* ''All [[Wikipedia community|Wikipedia editors]] speak at least three [[language]]s.''
Declarative sentences are contrasted with [[question]]s, such as "What is Wikipedia?", and [[Imperative mood|imperative]] statements, such as "Please add [[citation]]s to support the claims in this article.".<ref>{{Cite web |title=Lecture Notes on Logical Organization and Critical Thinking |url=https://www2.hawaii.edu/~sugihara/courses/HCU2016s_TC/notes/CriticalThinking.html |access-date=2024-03-22 |website=www2.hawaii.edu}}</ref><ref>{{Cite web |title=Logical Connectives |url=https://sites.millersville.edu/bikenaga/math-proof/logical-connectives/logical-connectives.html |access-date=2024-03-22 |website=sites.millersville.edu}}</ref> Such non-declarative sentences have no [[truth value]],<ref>{{Cite web |title=Lecture1 |url=https://www.cs.columbia.edu/~rgu/courses/e6998/fall2018/Lecture1.html |access-date=2024-03-22 |website=www.cs.columbia.edu}}</ref> and are only dealt with in [[Non-classical logic|nonclassical logics]], called [[Erotetics|erotetic]] and [[imperative logic]]s.

=== Compounding sentences with connectives ===
{{See also|Atomic formula|Atomic sentence}}
In propositional logic, a statement can contain one or more other statements as parts.<ref name=":1" /> ''Compound sentences'' are formed from simpler sentences and express relationships among the constituent sentences.<ref name=":4">{{Cite web |title=Introduction to Logic - Chapter 2 |url=http://intrologic.stanford.edu/chapters/chapter_02.html |access-date=2024-03-22 |website=intrologic.stanford.edu}}</ref> This is done by combining them with [[logical connective]]s:<ref name=":4" /><ref name=":21">{{Cite book |last=Beall |first=Jeffrey C. |title=Logic: the basics |date=2010 |publisher=Routledge |isbn=978-0-203-85155-5 |edition=1. publ |location=London |pages=6, 8, 14–16, 19–20, 44–48, 50–53, 56 |language=en}}</ref> the main types of compound sentences are [[negation]]s, [[Logical conjunction|conjunctions]], [[Logical disjunction|disjunctions]], [[Material conditional|implications]], and [[Logical biconditional|biconditionals]],<ref name=":4" /> which are formed by using the corresponding connectives to connect propositions.<ref>{{Cite web |title=Watson |url=http://watson.latech.edu/book/intelligence/intelligenceApproaches2b1.html |access-date=2024-03-22 |website=watson.latech.edu}}</ref><ref>{{Cite web |title=Introduction to Theoretical Computer Science, Chapter 1 |url=https://www.cs.odu.edu/~toida/nerzic/390teched/math/logic.html |access-date=2024-03-22 |website=www.cs.odu.edu}}</ref> In [[English language|English]], these connectives are expressed by the words "and" ([[logical conjunction|conjunction]]), "or" ([[logical disjunction|disjunction]]), "not" ([[negation]]), "if" ([[material conditional]]), and "if and only if" ([[Logical biconditional|biconditional]]).<ref name=":1" /><ref name=":5" /> Examples of such compound sentences might include:

* ''Wikipedia is a free online encyclopedia that anyone can edit, '''and''' [[1,000,000|millions]] [[Help:Editing|already have]].'' (conjunction)
* '''''It is not true that''' all Wikipedia 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<ref name=":21" /> 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'',<ref name=":1" /> or ''atomic sentences'';<ref name=":21" /> if they contain one or more logical connectives, they are called ''compound sentences'',<ref name=":4" /> or ''molecular sentences''.<ref name=":21" />

''Sentential connectives'' are a broader category that includes logical connectives.<ref name=":2" /><ref name=":21" /> Sentential connectives are any linguistic particles that bind sentences to create a new compound sentence,<ref name=":2" /><ref name=":21" /> or that inflect a single sentence to create a new sentence.<ref name=":2" /> 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) [[proposition]]s, the new sentence that results from its application also is (or expresses) a [[proposition]].<ref name=":2" /> Philosophers disagree about what exactly a proposition is,<ref name=":22" /><ref name=":2" /> as well as about which sentential connectives in natural languages should be counted as logical connectives.<ref name=":21" /><ref name=":2" /> Sentential connectives are also called ''sentence-functors'',<ref name="BostockIntermediate" /> and logical connectives are also called ''truth-functors''.<ref name="BostockIntermediate" />

== Arguments ==
{{Main article|Argument}}
An [[argument]] is defined as a [[2|pair]] of things, namely a set of sentences, called the '''premises''',{{refn|group=lower-alpha|The set of premises may be the [[empty set]];<ref name="BostockIntermediate" /><ref name=":35" /> an argument from an empty set of premises is ''valid'' if, and only if, the conclusion is a [[Tautology (logic)|tautology]].<ref name="BostockIntermediate" /><ref name=":35" />}} and a sentence, called the '''conclusion'''.<ref name=":35">{{Cite book |last1=Allen |first1=Colin |title=Logic primer |last2=Hand |first2=Michael |date=2022 |publisher=The MIT Press |isbn=978-0-262-54364-4 |edition=3rd |location=Cambridge, Massachusetts}}</ref><ref name=":21" /><ref name="BostockIntermediate" /> The conclusion is claimed to ''follow from'' the premises,<ref name="BostockIntermediate" /> and the premises are claimed to ''support'' the conclusion.<ref name=":21" />

=== Example argument ===
The following is an example of an argument within the scope of propositional logic:

:'''Premise 1:''' ''If'' it's raining, ''then'' it's cloudy.
:'''Premise 2:''' It's raining.
:'''Conclusion:''' It's cloudy.

The [[logical form]] of this argument is known as [[modus ponens]],<ref name=":13" /> which is a [[Classical logic|classically]] [[Validity (logic)|valid]] form.<ref>{{Cite journal |last=Stojnić |first=Una |date=2017 |title=One's Modus Ponens: Modality, Coherence and Logic |url=https://www.jstor.org/stable/48578954 |journal=Philosophy and Phenomenological Research |volume=95 |issue=1 |pages=167–214 |doi=10.1111/phpr.12307 |jstor=48578954 |issn=0031-8205}}</ref> So, in classical logic, the argument is ''valid'', although it may or may not be ''[[Soundness|sound]]'', depending on the [[Meteorology|meteorological]] facts in a given context. This '''example argument''' will be reused when explaining {{section link||Formalization}}.

=== Validity and soundness ===
{{Main article|Validity (logic)|Soundness}}
An argument is '''valid''' if, and only if, it is ''necessary'' that, if all its premises are true, its conclusion is true.<ref name=":35" /><ref>{{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}}</ref><ref name=":36">{{Cite web |title=Validity and Soundness {{!}} Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/val-snd/ |access-date=2024-04-05 |language=en-US}}</ref> Alternatively, an argument is valid if, and only if, it is ''impossible'' for all the premises to be true while the conclusion is false.<ref name=":36" /><ref name=":35" />

Validity is contrasted with ''soundness''.<ref name=":36" /> An argument is '''sound''' if, and only if, it is valid and all its premises are true.<ref name=":35" /><ref name=":36" /> Otherwise, it is ''unsound''.<ref name=":36" />

Logic, in general, aims to precisely specify valid arguments.<ref name=":21" /> This is done by defining a valid argument as one in which its conclusion is a [[logical consequence]] of its premises,<ref name=":21" /> 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<ref name=":21" /> – see {{section link||Semantics}} below.

== Formalization ==
Propositional logic is typically studied through a [[formal system]] in which [[well-formed formula|formulas]] of a [[formal language]] are [[interpretation (logic)|interpreted]] to represent [[propositions]]. This formal language is the basis for [[Proof calculus|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 ===
{{Main article|Propositional variable}}
Since propositional logic is not concerned with the structure of propositions beyond the point where they cannot be decomposed any more by logical connectives,<ref name=":13" /><ref name=":1" /> it is typically studied by replacing such ''atomic'' (indivisible) statements with letters of the alphabet, which are interpreted as variables representing statements ([[Propositional variable|''propositional variables'']]).<ref name=":1" /> With propositional variables, the {{section link||Example argument}} would then be symbolized as follows:

:'''Premise 1:''' <math>P \to Q</math>
:'''Premise 2:''' <math>P</math>
:'''Conclusion:''' <math>Q</math>

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 <math>P</math>, <math>Q</math> and <math>R</math>) 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:

:<math>\frac{P \to Q, P}{Q}</math>

This method of displaying it is [[Gerhard Gentzen|Gentzen]]'s notation for [[natural deduction]] and [[sequent calculus]].<ref name=":40">{{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}}</ref> The premises are shown above a line, called the '''inference line''',<ref name=":3" /> separated by a '''comma''', which indicates ''combination'' of premises.<ref name=":34">{{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}}</ref> The conclusion is written below the inference line.<ref name=":3" /> The inference line represents ''syntactic consequence'',<ref name=":3" /> sometimes called ''deductive consequence'',<ref name=":7">{{Cite web |title=Compactness {{!}} Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/compactness/ |access-date=2024-03-22 |language=en-US}}</ref> which is also symbolized with ⊢.<ref name=":6">{{Cite web |title=Lecture Topics for Discrete Math Students |url=https://math.colorado.edu/~kearnes/Teaching/Courses/F23/discretel.html |access-date=2024-03-22 |website=math.colorado.edu}}</ref><ref name=":7" /> So the above can also be written in one line as <math>P \to Q, P \vdash Q</math>.{{refn|group=lower-alpha|The turnstile, for syntactic consequence, is of lower [[Order of operations|precedence]] than the comma, which represents premise combination, which in turn is of lower precedence than the arrow, used for material implication; so no parentheses are needed to interpret this formula.<ref name=":34" />}}

Syntactic consequence is contrasted with ''semantic consequence'',<ref>{{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}}</ref> which is symbolized with ⊧.<ref name=":6" /><ref name=":7" /> In this case, the conclusion follows ''syntactically'' because the [[natural deduction]] [[Rule of inference|inference rule]] of [[modus ponens]] has been assumed. For more on inference rules, see the sections on proof systems below.

==Language==
{{Formal languages}}
The [[formal language|language]] (commonly called <math>\mathcal{L}</math>)<ref name=":7"/><ref name=":25">{{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}}</ref><ref name=":21" /> of a propositional calculus is defined in terms of:<ref name=":2" /><ref name=":0" />
<!-- If you add more alternative names, let's keep them in alphabetical order -->
# a set of primitive symbols, called ''[[atomic formula]]s'', ''atomic sentences'',<ref name=":13" /><ref name=":21" /> ''atoms,''<ref name=":8">{{Cite book |last=Kleene |first=Stephen Cole |title=Mathematical logic |date=2002 |publisher=Dover Publications |isbn=978-0-486-42533-7 |edition=Dover |location=Mineola, N.Y}}</ref> ''placeholders'', ''prime formulas'',<ref name=":8" /> ''proposition letters'', ''sentence letters'',<ref name=":13" /> or ''variables'', and
# a set of operator symbols, called ''connectives'',<ref name=":23" /><ref name=":1" /><ref name=":33" /> ''[[logical connective]]s'',<ref name=":1" /> ''logical operators'',<ref name=":1" /> ''truth-functional connectives,''<ref name=":1" /> ''truth-functors'',<ref name="BostockIntermediate" /> or ''propositional connectives''.<ref name=":2" />

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 <math>\mathcal{L}</math>, then, is defined either as being ''identical to'' its set of well-formed formulas,<ref name=":25" /> or as ''containing'' that set (together with, for instance, its set of connectives and variables).<ref name=":0" /><ref name=":21" />

Usually the syntax of <math>\mathcal{L}</math> 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,<ref name=":21" /><ref name=":29">{{Cite book |last=Smullyan |first=Raymond M. |title=First-order logic |date=1995 |publisher=Dover |isbn=978-0-486-68370-6 |location=New York |pages=5, 10–11, 14 |language=en}}</ref> while others use them without comment.<ref name=":2" /><ref name=":0" />

=== Syntax ===
Given a set of atomic propositional variables <math>p_1</math>, <math>p_2</math>, <math>p_3</math>, ..., and a set of propositional connectives <math>c_1^1</math>, <math>c_2^1</math>, <math>c_3^1</math>, ..., <math>c_1^2</math>, <math>c_2^2</math>, <math>c_3^2</math>, ..., <math>c_1^3</math>, <math>c_2^3</math>, <math>c_3^3</math>, ..., a formula of propositional logic is [[Recursive definition|defined recursively]] by these definitions:<ref name=":2" /><ref name=":0" /><ref name=":33">{{Cite book |last=Humberstone |first=Lloyd |url=https://www.worldcat.org/title/694679197 |title=The connectives |date=2011 |publisher=MIT Press |isbn=978-0-262-01654-4 |location=Cambridge, Mass |pages=118, 702 |oclc=694679197}}</ref>{{refn|group=lower-alpha|A very general and abstract syntax is given here, following the notation in the SEP,<ref name=":2" /> but including the third definition, which is very commonly given explicitly by other sources, such as Gillon,<ref name=":0" /> Bostock,<ref name="BostockIntermediate" /> Allen & Hand,<ref name=":35" /> 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, <math>\{ \neg, \land, \lor, \to, \leftrightarrow \}</math>, 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.)}}

:'''Definition 1''': Atomic propositional variables are formulas.

:'''Definition 2''': If <math>c_n^m</math> is a propositional connective, and <math>\langle</math>A, B, C, …<math>\rangle</math> is a sequence of m, possibly but not necessarily atomic, possibly but not necessarily distinct, formulas, then the result of applying <math>c_n^m</math> to <math>\langle</math>A, B, C, …<math>\rangle</math> is a formula.
:'''Definition 3:''' Nothing else is a formula.

Writing the result of applying <math>c_n^m</math> to <math>\langle</math>A, B, C, …<math>\rangle</math> in functional notation, as <math>c_n^m</math>(A, B, C, …), we have the following as examples of well-formed formulas:

* <math>p_5</math>
* <math>c_3^2(p_2, p_9)</math>
* <math>c_3^2(p_1, c_2^1(p_3))</math>
* <math>c_1^3(p_4, p_6, c_2^2(p_1, p_2))</math>
* <math>c_4^2(c_1^1(p_7), c_3^1(p_8))</math>
* <math>c_2^3(c_1^2(p_3, p_4), c_2^1(p_5), c_3^2(p_6, p_7))</math>
* <math>c_3^1(c_1^3(p_2, p_3, c_2^2(p_4, p_5)))</math>

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''.<ref name=":13" />{{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."<ref>{{Cite book |last=Russell |first=Bertrand |title=Principles of mathematics |date=2010 |publisher=Routledge |isbn=978-0-415-48741-2 |series=Routledge classics |location=London |pages=17}}</ref>}} It is this [[recursion]] [[recursive definition|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 <math>\mathcal{L}</math> are built up from the atoms as ultimate building blocks.<ref name=":2" /> Composite formulas (all formulas besides atoms) are called ''molecules'',<ref name=":8" /> or ''molecular sentences''.<ref name=":21" /> (This is an imperfect analogy with [[chemistry]], since a chemical molecule may sometimes have only one atom, as in [[monatomic gas]]es.)<ref name=":8" />

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.<ref name="BostockIntermediate" /> In particular, it excludes ''infinitely long'' formulas from being [[Well-formed formula|well-formed]].<ref name="BostockIntermediate" />

==== CF grammar in BNF ====
An alternative to the syntax definitions given above is to write a [[Context-free grammar|context-free (CF) grammar]] for the language <math>\mathcal{L}</math> in [[Backus–Naur form|Backus-Naur form]] (BNF).<ref name=":41">{{Cite book |last=Hodges |first=Wilfrid |title=Logic |date=1977 |publisher=Penguin |isbn=978-0-14-021985-2 |location=Harmondsworth; New York |pages=80–85}}</ref><ref name=":42">{{Cite book |last1=Hansson |first1=Sven Ove |title=Introduction to formal philosophy |last2=Hendricks |first2=Vincent F. |date=2018 |publisher=Springer |isbn=978-3-030-08454-7 |series=Springer undergraduate texts in philosophy |location=Cham |pages=38}}</ref> This is more common in [[computer science]] than in [[philosophy]].<ref name=":42" /> It can be done in many ways,<ref name=":41" /> of which a particularly brief one, for the common set of five connectives, is this single clause:<ref name=":42" /><ref name=":02">{{Cite book |last1=Ayala-Rincón |first1=Mauricio |url=https://link.springer.com/book/10.1007/978-3-319-51653-0 |title=Applied Logic for Computer Scientists |last2=de Moura |first2=Flávio L.C. |series=Undergraduate Topics in Computer Science |date=2017 |publisher=Springer |pages=2 |language=en |doi=10.1007/978-3-319-51653-0|isbn=978-3-319-51651-6 }}</ref>
:<math>\phi ::= a_1, a_2, \ldots  ~ | ~  \neg\phi  ~ | ~  \phi ~ \& ~ \psi  ~ | ~  \phi \vee \psi  ~ | ~  \phi \rightarrow \psi  ~ | ~  \phi \leftrightarrow \psi</math>
This clause, due to its [[Self-reference|self-referential]] nature (since <math>\phi</math> is in some branches of the definition of <math>\phi</math>), also acts as a [[recursive definition]], and therefore specifies the entire language. To expand it to add [[modal operator]]s, one need only add … <math>| ~ \Box\phi ~ | ~ \Diamond\phi</math> to the end of the clause.<ref name=":42" />

=== Constants and schemata ===
Mathematicians sometimes distinguish between propositional constants, [[propositional variable]]s, and schemata. ''Propositional constants'' represent some particular proposition,<ref name=":9">{{Cite book |last=Lande |first=Nelson P. |title=Classical logic and its rabbit holes: a first course |date=2013 |publisher=Hackett Publishing Co., Inc |isbn=978-1-60384-948-7 |location=Indianapolis, Ind |pages=20}}</ref> while ''propositional variables'' range over the set of all atomic propositions.<ref name=":9" /> Schemata, or ''schematic letters'', however, range over all formulas.<ref name="BostockIntermediate">{{Cite book |last=Bostock |first=David |title=Intermediate logic |date=1997 |publisher=Clarendon Press; Oxford University Press |isbn=978-0-19-875141-0 |location=Oxford : New York |pages=4–5, 8–13, 18–19, 22, 27, 29, 191, 194}}</ref><ref name=":1" /> (Schematic letters are also called ''metavariables''.)<ref name=":35" /> 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|χ}}.<ref name="BostockIntermediate" /><ref name=":1" />

However, some authors recognize only two "propositional constants" in their formal system: the special symbol <math>\top</math>, called "truth", which always evaluates to ''True'', and the special symbol <math>\bot</math>, called "falsity", which always evaluates to ''False''.<ref>{{Cite book |last=Goldrei |first=Derek |title=Propositional and predicate calculus: a model of argument |date=2005 |publisher=Springer |isbn=978-1-85233-921-0 |location=London |pages=69 |language=en}}</ref><ref>{{Cite web |title=Propositional Logic |url=https://www.cs.rochester.edu/u/nelson/courses/csc_173/proplogic/expressions.html |access-date=2024-03-22 |website=www.cs.rochester.edu}}</ref><ref>{{Cite web |title=Propositional calculus |url=https://www.cs.cornell.edu/courses/cs671/1999fa/typed%20logic/node18.html |access-date=2024-03-22 |website=www.cs.cornell.edu}}</ref> Other authors also include these symbols, with the same meaning, but consider them to be "zero-place truth-functors",<ref name="BostockIntermediate" /> or equivalently, "[[nullary]] connectives".<ref name=":33" />

== Semantics ==
{{Main article|Semantics of logic|Model theory}}
To serve as a model of the logic of a given [[natural language]], a formal language must be semantically interpreted.<ref name=":21" /> In [[classical logic]], all propositions evaluate to exactly one of two [[Truth value|truth-values]]: ''True'' or ''False''.<ref name=":1" /><ref name=":26">{{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}}</ref> For example, "[[Wikipedia]] is a [[Wikipedia:Free encyclopedia|free]] [[online encyclopedia]] that anyone can edit" [[Wikipedia:About|evaluates to ''True'']],<ref>{{Cite journal |last1=Metcalfe |first1=David |last2=Powell |first2=John |date=2011 |title=Should doctors spurn Wikipedia? |journal=Journal of the Royal Society of Medicine |language=en |volume=104 |issue=12 |pages=488–489 |doi=10.1258/jrsm.2011.110227 |issn=0141-0768 |pmc=3241521 |pmid=22179287}}</ref> while "Wikipedia is a [[paper]] [[encyclopedia]]" [[Wikipedia:NOTPAPER|evaluates to ''False'']].<ref>{{Cite book |last1=Ayers |first1=Phoebe |url=https://www.worldcat.org/title/185698411 |title=How Wikipedia works: and how you can be a part of it |last2=Matthews |first2=Charles |last3=Yates |first3=Ben |date=2008 |publisher=No Starch Press |isbn=978-1-59327-176-3 |location=San Francisco |pages=22 |oclc=185698411}}</ref>

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 ([[Principle of bivalence|''bivalence'']]), that only one of the two is assigned to each formula in the language ([[Law of noncontradiction|''noncontradiction'']]), and that every formula gets assigned a value ([[Law of excluded middle|''excluded middle'']]), are distinctive features of classical logic.<ref name=":26" /><ref>{{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}}</ref><ref name="BostockIntermediate" /> To learn about [[Non-classical logic|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 ===
{{Main|Interpretation (logic)}}
For a given language <math>\mathcal{L}</math>, an '''interpretation''',<ref name=":24">{{Cite journal |last=Landman |first=Fred |date=1991 |title=Structures for Semantics |url=https://doi.org/10.1007/978-94-011-3212-1 |journal=Studies in Linguistics and Philosophy |language=en |volume=45 |pages=127 |doi=10.1007/978-94-011-3212-1 |isbn=978-0-7923-1240-6 |issn=0924-4662}}</ref> '''valuation''',<ref name=":29" /> or '''case''',<ref name=":21" />{{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 (mathematical logic)|assignment]] of ''semantic values'' to each formula of <math>\mathcal{L}</math>.<ref name=":21" /> For a formal language of classical logic, a case is defined as an ''assignment'', to each formula of <math>\mathcal{L}</math>, of one or the other, but not both, of the [[truth value]]s, namely [[truth]] ('''T''', or 1) and [[false (logic)|falsity]] ('''F''', or 0).<ref>{{Cite book |last=Nascimento |first=Marco Antonio Chaer |title=Frontiers in quantum methods and applications in chemistry and physics: selected proceedings of QSCP-XVIII (Paraty, Brazil, December, 2013) |date=2015 |publisher=Springer |others=International Workshop on Quantum Systems in Chemistry and Physics |isbn=978-3-319-14397-2 |series=Progress in theoretical chemistry and physics |location=Cham |pages=255 |language=en}}</ref><ref name=":19">{{Cite journal |last=Chowdhary |first=K.R. |date=2020 |title=Fundamentals of Artificial Intelligence |url=https://doi.org/10.1007/978-81-322-3972-7 |journal=SpringerLink |language=en |pages=31–34 |doi=10.1007/978-81-322-3972-7|isbn=978-81-322-3970-3 }}</ref> An interpretation that follows the rules of classical logic is sometimes called a '''Boolean valuation'''.<ref name=":29" /><ref>{{Cite book |last1=Restall |first1=Greg |url=https://books.google.com/books?id=IJVnEAAAQBAJ |title=Logical Methods |last2=Standefer |first2=Shawn |date=2023-01-03 |publisher=MIT Press |isbn=978-0-262-54484-9 |pages=76 |language=en}}</ref> An interpretation of a formal language for classical logic is often expressed in terms of [[truth tables]].<ref name="metalogic">{{Cite book |last=Hunter |first=Geoffrey |title=Metalogic: An Introduction to the Metatheory of Standard First-Order Logic |publisher=University of California Press |year=1971 |isbn=0-520-02356-0}}</ref><ref name=":1" /> Since each formula is only assigned a single truth-value, an interpretation may be viewed as a [[Function (mathematics)|function]], whose [[Domain of a function|domain]] is <math>\mathcal{L}</math>, and whose [[Range of a function|range]] is its set of semantic values <math>\mathcal{V} = \{\mathsf{T}, \mathsf{F}\}</math>,<ref name=":2" /> or <math>\mathcal{V} = \{1, 0\}</math>.<ref name=":21" />

For <math>n</math> distinct propositional symbols there are <math>2^n</math> distinct possible interpretations. For any particular symbol <math>a</math>, for example, there are <math>2^1=2</math> possible interpretations: either <math>a</math> is assigned '''T''', or <math>a</math> is assigned '''F'''. And for the pair <math>a</math>, <math>b</math> there are <math>2^2=4</math> possible interpretations: either both are assigned '''T''', or both are assigned '''F''', or <math>a</math> is assigned '''T''' and <math>b</math> is assigned '''F''', or <math>a</math> is assigned '''F''' and <math>b</math> is assigned '''T'''.<ref name="metalogic" /> Since <math>\mathcal{L}</math> has <math>\aleph_0</math>, that is, [[Denumerably infinite|denumerably]] many propositional symbols, there are <math>2^{\aleph_0}=\mathfrak c</math>, and therefore [[Cardinality of the continuum|uncountably many]] distinct possible interpretations of <math>\mathcal{L}</math> as a whole.<ref name="metalogic" />

Where <math>\mathcal{I}</math> is an interpretation and <math>\varphi</math> and <math>\psi</math> represent formulas, the definition of an ''argument'', given in {{section link||Arguments}}, may then be stated as a pair <math>\langle \{\varphi_1, \varphi_2, \varphi_3, ..., \varphi_n\} , \psi \rangle</math>, where <math>\{\varphi_1, \varphi_2, \varphi_3, ..., \varphi_n\}</math> is the set of premises and <math>\psi</math> is the conclusion. The definition of an argument's ''validity'', i.e. its property that <math>\{\varphi_1, \varphi_2, \varphi_3, ..., \varphi_n\} \models \psi</math>, can then be stated as its ''absence of a counterexample'', where a '''counterexample''' is defined as a case <math>\mathcal{I}</math> in which the argument's premises <math>\{\varphi_1, \varphi_2, \varphi_3, ..., \varphi_n\}</math> are all true but the conclusion <math>\psi</math> is not true.<ref name=":21" /><ref name=":13" /> 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 ===
{{Main article|Logical connective|Truth function}}An interpretation assigns semantic values to [[atomic formula]]s directly.<ref name=":24" /><ref name=":21" /> Molecular formulas are assigned a ''function'' of the value of their constituent atoms, according to the connective used;<ref name=":24" /><ref name=":21" /> the connectives are defined in such a way that the [[Truth value|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.<ref name=":24" /><ref name=":21" /> This assumption is referred to by [[Colin Howson]] as the assumption of the ''[[Truth function|truth-functionality]] of the [[Logical connective|connectives]]''.<ref name=":13" />

==== Semantics via truth tables ====
{{Logical connectives sidebar}}
Since logical connectives are defined semantically only in terms of the [[truth value]]s that they take when the [[propositional variable]]s that they're applied to take either of the [[Principle of bivalence|two possible]] truth values,<ref name=":1" /><ref name=":21" /> the semantic definition of the connectives is usually represented as a [[truth table]] for each of the connectives,<ref name=":1" /><ref name=":21" /><ref name=":37" /> as seen below:

{| class="wikitable" style="margin:1em auto; text-align:center;"
|-
! ''p''
! ''q''
! ''p'' ∧ ''q''
! ''p'' ∨ ''q''
! ''p'' → ''q''
! ''p'' ↔ ''q''
! ''¬p''
! ''¬q''
|-
| {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Failure|}}F || {{Failure|}}F
|-
| {{Success|}}T || {{Failure|}}F || {{Failure|}}F || {{Success|}}T || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Success|}}T
|-
| {{Failure|}}F || {{Success|}}T || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Failure|}}F || {{Success|}}T || {{Failure|}}F
|-
| {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T
|}

This table covers each of the main five [[logical connective]]s:<ref name=":5" /><ref name=":0" /><ref name=":3" /><ref name=":12" /> [[Logical conjunction|conjunction]] (here notated p ∧ q), [[Logical disjunction|disjunction]] (p ∨ q), [[Material conditional|implication]] (p → q), [[Logical biconditional|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.<ref name=":1" /><ref>{{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}}</ref><ref name=":21" /> For more truth tables for more different kinds of connectives, see the article "[[Truth table]]".

==== Semantics via assignment expressions ====
Some authors (viz., all the authors cited in this subsection) write out the connective semantics using a list of statements instead of a table. In this format, where <math>\mathcal{I}(\varphi)</math> is the interpretation of <math>\varphi</math>, the five connectives are defined as:<ref name="BostockIntermediate" /><ref name=":29" />

* <math>\mathcal{I}(\neg P) = \mathsf{T}</math> if, and only if, <math>\mathcal{I}(P) = \mathsf{F}</math>
* <math>\mathcal{I}(P \land Q) = \mathsf{T}</math> if, and only if, <math>\mathcal{I}(P) = \mathsf{T}</math> and <math>\mathcal{I}(Q) = \mathsf{T}</math>
* <math>\mathcal{I}(P \lor Q) = \mathsf{T}</math> if, and only if, <math>\mathcal{I}(P) = \mathsf{T}</math> or <math>\mathcal{I}(Q) = \mathsf{T}</math>
* <math>\mathcal{I}(P \to Q) = \mathsf{T}</math> if, and only if, it is true that, if <math>\mathcal{I}(P) = \mathsf{T}</math>, then <math>\mathcal{I}(Q) = \mathsf{T}</math>
* <math>\mathcal{I}(P \leftrightarrow Q) = \mathsf{T}</math> if, and only if, it is true that <math>\mathcal{I}(P) = \mathsf{T}</math> if, and only if, <math>\mathcal{I}(Q) = \mathsf{T}</math>
Instead of <math>\mathcal{I}(\varphi)</math>, the interpretation of <math>\varphi</math> may be written out as <math>|\varphi|</math>,<ref name="BostockIntermediate" /><ref>{{Cite book |last=Makridis |first=Odysseus |title=Symbolic logic |date=2022 |publisher=Palgrave Macmillan |isbn=978-3-030-67395-6 |series=Palgrave philosophy today |location=Cham, Switzerland |pages=119}}</ref> or, for definitions such as the above, <math>\mathcal{I}(\varphi) = \mathsf{T}</math> may be written simply as the English sentence "<math>\varphi</math> is given the value <math>\mathsf{T}</math>".<ref name=":29" /> Yet other authors<ref>{{Cite book |last=Burgess |first=John P. |url=https://www.worldcat.org/title/276141382 |title=Philosophical logic |date=2009 |publisher=Princeton University Press |isbn=978-0-691-13789-6 |series=Princeton foundations of contemporary philosophy |location=Princeton |pages=5 |oclc=276141382}}</ref><ref name=":43">{{Cite book |last1=Beall |first1=J. C. |url=https://books.google.com/books?id=qrUUDAAAQBAJ |title=Logical Pluralism |last2=Restall |first2=Greg |date=2006 |publisher=Clarendon Press |isbn=978-0-19-928840-3 |pages=38 |language=en}}</ref> may prefer to speak of a [[Model theory|Tarskian model]] <math>\mathfrak{M}</math> for the language, so that instead they'll use the notation <math>\mathfrak{M} \models \varphi</math>, which is equivalent to saying <math>\mathcal{I}(\varphi) = \mathsf{T}</math>, where <math>\mathcal{I}</math> is the interpretation function for <math>\mathfrak{M}</math>.<ref name=":43" />

==== Connective definition methods ====
Some of these connectives may be defined in terms of others: for instance, implication, p&nbsp;→&nbsp;q, may be defined in terms of disjunction and negation, as ¬p&nbsp;∨&nbsp;q;<ref>{{Cite book |last=Levin |first=Oscar |url=https://discrete.openmathbooks.org/dmoi3/sec_propositional.html |title=Propositional Logic |language=en-US}}</ref> and disjunction may be defined in terms of negation and conjunction, as ¬(¬p&nbsp;∧&nbsp;¬q).<ref name=":29" /> In fact, a ''[[Functional completeness|truth-functionally complete]]'' system,{{refn|group=lower-alpha|A truth-functionally complete set of connectives<ref name=":2" /> is also called simply ''[[Functional completeness|functionally complete]]'', or ''adequate for truth-functional logic'',<ref name=":13" /> or ''expressively adequate'',<ref name="Smith2003">{{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.)</ref> or simply ''adequate''.<ref name=":13" /><ref name="Smith2003" />}} in the sense that all and only the classical propositional tautologies are theorems, may be derived using only disjunction and negation (as [[Bertrand Russell|Russell]], [[Alfred North Whitehead|Whitehead]], and [[David Hilbert|Hilbert]] did),<ref name=":2" /> or using only implication and negation (as [[Gottlob Frege|Frege]] did),<ref name=":2" /> or using only conjunction and negation,<ref name=":2" /> or even using only a single connective for "not and" (the [[Sheffer stroke]]),<ref name=":18" /><ref name=":2" /> as [[Jean Nicod]] did.<ref name=":2" /> A ''joint denial'' connective ([[logical NOR]]) will also suffice, by itself, to define all other connectives,<ref name=":29" /> but no other connectives have this property.<ref name=":29" />

Some authors, namely [[Colin Howson|Howson]]<ref name=":13" /> and Cunningham,<ref>{{Cite book |last=Cunningham |first=Daniel W. |title=Set theory: a first course |date=2016 |publisher=Cambridge University Press |isbn=978-1-107-12032-7 |series=Cambridge mathematical textbooks |location=New York, NY}}</ref> 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 <math>\mathcal{L}</math>. 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",<ref name=":3" /> and/or the symbol ⇔,<ref>{{Cite book |last1=Genesereth |first1=Michael |url=https://link.springer.com/10.1007/978-3-031-01801-5 |title=Introduction to Logic |last2=Kao |first2=Eric J. |date=2017 |publisher=Springer International Publishing |isbn=978-3-031-00673-9 |series=Synthesis Lectures on Computer Science |location=Cham |pages=18 |language=en |doi=10.1007/978-3-031-01801-5}}</ref> to denote their object language's biconditional connective.

=== Semantic truth, validity, consequence ===
Given <math>\varphi</math> and <math>\psi</math> as [[formula (mathematical logic)|formulas]] (or sentences) of a language <math>\mathcal{L}</math>, and <math>\mathcal{I}</math> 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'' ([[WP:RS]]) 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 <math>\mathcal{L}</math>, then the following definitions apply:<ref name="metalogic" /><ref name=":19" />

* '''Truth-in-a-case:'''<ref name=":21" /> A sentence <math>\varphi</math> of <math>\mathcal{L}</math> is ''true under an interpretation'' <math>\mathcal{I}</math> if <math>\mathcal{I}</math> assigns the truth value '''T''' to <math>\varphi</math>.<ref name=":19" /><ref name="metalogic" /> If <math>\varphi</math> is [[logical truth|true]] under <math>\mathcal{I}</math>, then <math>\mathcal{I}</math> is called a ''model'' of <math>\varphi</math>.<ref name="metalogic" />
* '''Falsity-in-a-case:<ref name=":21" />''' <math>\varphi</math> is ''false under an interpretation'' <math>\mathcal{I}</math> if, and only if, <math>\neg\varphi</math> is true under <math>\mathcal{I}</math>.<ref name="metalogic" /><ref name=":20" /><ref name=":21" /> This is the "truth of negation" definition of falsity-in-a-case.<ref name=":21" /> Falsity-in-a-case may also be defined by the "complement" definition: <math>\varphi</math> is ''false under an interpretation'' <math>\mathcal{I}</math> if, and only if, <math>\varphi</math> is not true under <math>\mathcal{I}</math>.<ref name=":19" /><ref name="metalogic" /> In [[classical logic]], these definitions are equivalent, but in [[Non-classical logic|nonclassical logics]], they are not.<ref name=":21" />
* '''Semantic consequence:''' A sentence <math>\psi</math> of <math>\mathcal{L}</math> is a ''[[Logical consequence|semantic consequence]]'' (<math>\varphi \models \psi</math>) of a sentence <math>\varphi</math> if there is no interpretation under which <math>\varphi</math> is true and <math>\psi</math> is not true.<ref name=":19" /><ref name="metalogic" /><ref name=":21" />
* '''Valid formula (tautology):''' A sentence <math>\varphi</math> of <math>\mathcal{L}</math> is ''logically valid'' (<math>\models\varphi</math>),{{refn|group=lower-alpha|Conventionally <math>\models\varphi</math>, with nothing to the left of the turnstile, is used to symbolize a tautology. It may be interpreted as saying that <math>\varphi</math> is a semantic consequence of the empty set of formulae, i.e., <math>\{\}\models\varphi</math>, but with the empty brackets omitted for simplicity;<ref name="BostockIntermediate" /> 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.<ref name="BostockIntermediate" />}} or a ''tautology'',<ref>{{Cite web |title=6. Semantics of Propositional Logic — Logic and Proof 3.18.4 documentation |url=https://leanprover.github.io/logic_and_proof/semantics_of_propositional_logic.html |access-date=2024-03-28 |website=leanprover.github.io}}</ref><ref>{{Cite web |title=Knowledge Representation and Reasoning: Basics of Logics |url=https://www.emse.fr/~zimmermann/Teaching/KRR/generalities.html |access-date=2024-03-28 |website=www.emse.fr}}</ref><ref name=":29" /> if it is true under every interpretation,<ref name=":19" /><ref name="metalogic" /> or ''true in every case.''<ref name=":21" />
* '''Consistent sentence:''' A sentence of <math>\mathcal{L}</math> is ''[[Consistency|consistent]]'' if it is true under at least one interpretation. It is ''inconsistent'' if it is not consistent.<ref name=":19" /><ref name="metalogic" /> An inconsistent formula is also called ''self-contradictory'',<ref name=":1" /> and said to be a ''self-contradiction'',<ref name=":1" /> or simply a ''contradiction'',<ref name=":30" /><ref name=":31" /><ref name=":32" /> although this latter name is sometimes reserved specifically for statements of the form <math>(p \land \neg p)</math>.<ref name=":1" />

For interpretations (cases) <math>\mathcal{I}</math> of <math>\mathcal{L}</math>, these definitions are sometimes given:

* '''Complete case:''' A case <math>\mathcal{I}</math> is ''complete'' if, and only if, either <math>\varphi</math> is true-in-<math>\mathcal{I}</math> or <math>\neg\varphi</math> is true-in-<math>\mathcal{I}</math>, for any <math>\varphi</math> in <math>\mathcal{L}</math>.<ref name=":21" /><ref>{{Cite book |url=https://www.worldcat.org/title/681481210 |title=Computational logic in multi-agent systems: 10th international workshop, CLIMA X, Hamburg, Germany, September 9-10, 2009: revised selected and invited papers |date=2010 |publisher=Springer |isbn=978-3-642-16866-6 |editor-last=Dix |editor-first=J. |series=Lecture notes in computer science |location=Berlin; New York |pages=49 |oclc=681481210 |editor-last2=Fisher |editor-first2=Michael |editor-last3=Novak |editor-first3=Peter}}</ref>
* '''Consistent case:''' A case <math>\mathcal{I}</math> is ''consistent'' if, and only if, there is no <math>\varphi</math> in <math>\mathcal{L}</math> such that both <math>\varphi</math> and <math>\neg\varphi</math> are true-in-<math>\mathcal{I}</math>.<ref name=":21" /><ref>{{Cite book |title=Computational models of argument: proceedings of comma 2020 |date=2020 |publisher=IOS Press |isbn=978-1-64368-106-1 |editor-last=Prakken |editor-first=Henry |series=Frontiers in artificial intelligence and applications |location=Washington |pages=252 |editor-last2=Bistarelli |editor-first2=Stefano |editor-last3=Santini |editor-first3=Francesco |editor-last4=Taticchi |editor-first4=Carlo}}</ref>

For [[classical logic]], which assumes that all cases are complete and consistent,<ref name=":21" /> the following theorems apply:

* For any given interpretation, a given formula is either true or false under it.<ref name="metalogic" /><ref name=":20">{{Cite book |last=Rogers |first=Robert L. |url=http://dx.doi.org/10.1016/c2013-0-11894-6 |title=Mathematical Logic and Formalized Theories |date=1971 |publisher=Elsevier |isbn=978-0-7204-2098-2 |pages=38–39 |doi=10.1016/c2013-0-11894-6 |language=en}}</ref>
* No formula is both true and false under the same interpretation.<ref name="metalogic" /><ref name=":20" />
* <math>\varphi</math> is true under <math>\mathcal{I}</math> if, and only if, <math>\neg\varphi</math> is false under <math>\mathcal{I}</math>;<ref name="metalogic" /><ref name=":20" /> <math>\neg\varphi</math> is true under <math>\mathcal{I}</math> if, and only if, <math>\varphi</math> is not true under <math>\mathcal{I}</math>.<ref name="metalogic" />
* If <math>\varphi</math> and <math>(\varphi \to \psi)</math> are both true under <math>\mathcal{I}</math>, then <math>\psi</math> is true under <math>\mathcal{I}</math>.<ref name="metalogic" /><ref name=":20" />
* If <math>\models\varphi</math> and <math>\models(\varphi \to \psi)</math>, then <math>\models\psi</math>.<ref name="metalogic" />
* <math>(\varphi \to \psi)</math> is true under <math>\mathcal{I}</math> if, and only if, either <math>\varphi</math> is not true under <math>\mathcal{I}</math>, or <math>\psi</math> is true under <math>\mathcal{I}</math>.<ref name="metalogic" />
* <math>\varphi \models \psi</math> if, and only if, <math>(\varphi \to \psi)</math> is [[logically valid]], that is, <math>\varphi \models \psi</math> if, and only if, <math> \models(\varphi \to \psi)</math>.<ref name="metalogic" /><ref name=":20" />

==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'',<ref>{{Cite book |title=Rudolf carnap: studies in semantics: the collected works of rudolf carnap, volume 7 |date=2024 |publisher=Oxford University Press |isbn=978-0-19-289487-8 |editor-last=Awodey |editor-first=Steve |location=New York |pages=xxvii |editor-last2=Arnold |editor-first2=Greg Frost-}}</ref><ref>{{Cite book |title=Advances in Mathematics Education Research on Proof and Proving: An International Perspective |date=2018 |publisher=Springer International Publishing : Imprint: Springer |isbn=978-3-319-70996-3 |editor-last=Harel |editor-first=Guershon |edition=1st ed. 2018 |series=ICME-13 Monographs |location=Cham |pages=181 |editor-last2=Stylianides |editor-first2=Andreas J.}}</ref><ref>{{Cite journal |last=DeLancey |first=Craig |date=2017 |title=A Concise Introduction to Logic: §4. Proofs |url=https://milnepublishing.geneseo.edu/concise-introduction-to-logic/chapter/4-proofs/ |access-date=2024-03-23 |website=Milne Publishing}}</ref> according to the kind of [[logical consequence]] that they rely on: semantic proof systems rely on semantic consequence (<math>\varphi \models \psi</math>),<ref>{{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}}</ref> whereas syntactic proof systems rely on syntactic consequence (<math>\varphi \vdash \psi</math>).<ref>{{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}}</ref> 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.<ref name=":16">{{Cite book |last=Cook |first=Roy T. |title=A dictionary of philosophical logic |date=2009 |publisher=Edinburgh University Press |isbn=978-0-7486-2559-8 |location=Edinburgh |pages=82,176 |language=en}}</ref> This section gives a very brief overview of the kinds of proof systems, with [[Anchor (HTML)|anchors]] to the relevant sections of this article on each one, as well as to the separate Wikipedia articles on each one.

===Semantic proof systems===
[[File:Logische Verknuepfung Inhibition AB Truthtable.svg|200px|right|thumb|Example of a [[truth table]]]]
[[File:Partially built tableau.svg|thumb|200px|A graphical representation of a partially built [[Method of analytic tableaux|propositional tableau]]]]
Semantic proof systems rely on the concept of semantic consequence, symbolized as <math>\varphi \models \psi</math>, which indicates that if <math>\varphi</math> is true, then <math>\psi</math> must also be true in every possible interpretation.<ref name=":16" />

====Truth tables====
{{Main article|Truth table}}
A [[truth table]] is a semantic proof method used to determine the truth value of a propositional logic expression in every possible scenario.<ref>{{Cite web |date=2024-03-14 |title=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}}</ref> By exhaustively listing the truth values of its constituent atoms, a truth table can show whether a proposition is true, false, tautological, or contradictory.<ref name=":27">{{Cite web |title=MathematicalLogic |url=https://www.cs.yale.edu/homes/aspnes/pinewiki/MathematicalLogic.html |access-date=2024-03-23 |website=www.cs.yale.edu}}</ref> See {{section link||Semantic proof via truth tables}}.

====Semantic tableaux====
{{Main article|Method of analytic tableaux}}
A [[semantic tableau]] is another semantic proof technique that systematically explores the truth of a proposition.<ref>{{Cite web |title=Analytic Tableaux |url=https://www3.cs.stonybrook.edu/~skiena/113/lectures/lecture5/lecture5.html |access-date=2024-03-23 |website=www3.cs.stonybrook.edu}}</ref> It constructs a tree where each branch represents a possible interpretation of the propositions involved.<ref>{{Cite web |title=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}}</ref> If every branch leads to a contradiction, the original proposition is considered to be a contradiction, and its negation is considered a [[Tautology (logic)|tautology]].<ref name=":13">{{Cite book |last=Howson |first=Colin |title=Logic with trees: an introduction to symbolic logic |date=1997 |publisher=Routledge |isbn=978-0-415-13342-5 |location=London; New York |pages=ix, x,5–6, 15–16, 20, 24–29, 38, 42–43, 47}}</ref> 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 [[Gerhard Gentzen|Gentzen]] notation]]
Syntactic proof systems, in contrast, focus on the formal manipulation of symbols according to specific rules. The notion of syntactic consequence, <math>\varphi \vdash \psi</math>, signifies that <math>\psi</math> can be derived from <math>\varphi</math> using the rules of the formal system.<ref name=":16" />

====Axiomatic systems====
{{Main article|Axiomatic system (logic)}}
An [[axiomatic system]] is a set of axioms or assumptions from which other statements (theorems) are logically derived.<ref>{{Cite web |title=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}}</ref> 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.<ref>{{Cite web |title=Propositional Logic |url=https://mally.stanford.edu/tutorial/sentential.html |access-date=2024-03-23 |website=mally.stanford.edu}}</ref> See {{section link||Syntactic proof via axioms}}.

====Natural deduction====
{{Main article|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.<ref name=":14">{{Cite web |title=Natural Deduction {{!}} Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/natural-deduction/ |access-date=2024-03-23 |language=en-US}}</ref> Each rule reflects a particular logical connective and shows how it can be introduced or eliminated.<ref name=":14" /> See {{section link||Syntactic proof via natural deduction}}.

====Sequent calculus====
{{Main article|Sequent calculus}}
The [[sequent calculus]] is a formal system that represents logical deductions as sequences or "sequents" of formulas.<ref name=":15">{{Cite web |last=Weisstein |first=Eric W. |title=Sequent Calculus |url=https://mathworld.wolfram.com/ |access-date=2024-03-23 |website=mathworld.wolfram.com |language=en}}</ref> 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.<ref name=":15" /><ref>{{Cite web |title=Interactive Tutorial of the Sequent Calculus |url=http://logitext.mit.edu/tutorial |access-date=2024-03-23 |website=logitext.mit.edu}}</ref>

== 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.<ref name=":27" /><ref name=":8" /><ref name="BostockIntermediate" /> If, and only if, all the lines of a truth table come out true, the formula is semantically valid (true in every interpretation).<ref name=":27" /><ref name=":8" /> Further, if (and only if) <math>\neg\varphi</math> is valid, then <math>\varphi</math> is inconsistent.<ref name=":30">{{Cite web |date=2021-09-09 |title=1.4: Tautologies and contradictions |url=https://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 |access-date=2024-03-29 |website=Mathematics LibreTexts |language=en}}</ref><ref name=":31">{{Cite book |last=Sylvestre |first=Jeremy |url=https://sites.ualberta.ca/~jsylvest/books/EF/section-symb-lang-taut-contra.html |title=EF Tautologies and contradictions |language=en-US}}</ref><ref name=":32">{{Cite book |last1=DeLancey |first1=Craig |url=https://intrologicimport.pressbooks.tru.ca/chapter/9-if-and-only-if-using-theorems-a-concise-introduction-to-logic/ |title=Elementary Formal Logic |last2=Woodrow |first2=Jenna |publisher=Pressbooks |year=2017 |edition=1}}</ref>

For instance, this table shows that "''p → (q ∨ r → (r → ¬p))''" is not valid:<ref name=":8" />

{| 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''))
|-
| {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F
|-
| {{Success|}}T || {{Success|}}T || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T
|-
| {{Success|}}T || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F
|-
| {{Success|}}T || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T
|-
| {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T
|-
| {{Failure|}}F || {{Success|}}T || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T
|-
| {{Failure|}}F || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T
|-
| {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T
|}

The computation of the last column of the third line may be displayed as follows:<ref name=":8" />

{| 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
| T
|}

Further, using the theorem that <math>\varphi \models \psi</math> if, and only if, <math>(\varphi \to \psi)</math> is valid,<ref name="metalogic" /><ref name=":20" /> we can use a truth table to prove that a formula is a semantic consequence of a set of formulas: <math>\{\varphi_1, \varphi_2, \varphi_3, ..., \varphi_n\} \models \psi</math> if, and only if, we can produce a truth table that comes out all true for the formula <math>\left( \left(\bigwedge _{i=1}^n \varphi_i \right) \rightarrow \psi \right)</math> (that is, if <math>\models \left( \left(\bigwedge _{i=1}^n \varphi_i \right) \rightarrow \psi \right)</math>).<ref>{{Cite book |last1=Lucas |first1=Peter |url=https://www.cs.ru.nl/P.Lucas/teaching/KeR/logicintro.pdf |title=Principles of expert systems |last2=Gaag |first2=Linda van der |date=1991 |publisher=Addison-Wesley |isbn=978-0-201-41640-4 |series=International computer science series |location=Wokingham, England; Reading, Mass |pages=26}}</ref><ref>{{Cite web |last=Bachmair |first=Leo |date=2009 |title=CSE541 Logic in Computer Science |url=https://www3.cs.stonybrook.edu/~cse541/Spring2009/cse541PropLogic.pdf |website=Stony Brook University}}</ref>

== Semantic proof via tableaux ==
{{Main article|Method of analytic tableaux}}
Since truth tables have 2<sup>n</sup> lines for n variables, they can be tiresomely long for large values of n.<ref name=":13" /> Analytic tableaux are a more efficient, but nevertheless mechanical,<ref name=":37">{{Cite book |last=Restall |first=Greg |title=Logic: an introduction |date=2010 |publisher=Routledge |isbn=978-0-415-40068-8 |series=Fundamentals of philosophy |location=London |pages=5, 36–41, 55–60, 69}}</ref> 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."<ref name=":13" />

Analytic tableaux for propositional logic are fully specified by the rules that are stated in schematic form below.<ref name=":29" /> These rules use "signed formulas", where a signed formula is an expression <math>TX</math> or <math>FX</math>, where <math>X</math> is a (unsigned) formula of the language <math>\mathcal{L}</math>.<ref name=":29" />  (Informally, <math>TX</math> is read "<math>X</math> is true", and <math>FX</math> is read "<math>X</math> is false".)<ref name=":29" />  Their formal semantic definition is that "under any interpretation, a signed formula <math>TX</math> is called true if <math>X</math> is true, and false if <math>X</math> is false, whereas a signed formula <math>FX</math> is called false if <math>X</math> is true, and true if <math>X</math> is false."<ref name=":29" />

<math>
\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}
</math>

In this notation, rule 2 means that <math>T(X \land Y)</math> yields both <math>TX, TY</math>, whereas <math>F(X \land Y)</math> ''branches'' into <math>FX, FY</math>. The notation is to be understood analogously for rules 3 and 4.<ref name=":29" /> Often, in tableaux for [[classical logic]], the ''signed formula'' notation is simplified so that <math>T\varphi</math> is written simply as <math>\varphi</math>, and <math>F\varphi</math> as <math>\neg\varphi</math>, which accounts for naming rule 1 the "''Rule of Double Negation''".<ref name=":13" /><ref name=":37" />

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 <math>TX</math> and <math>FX</math> for some <math>X</math>, which is to say, a contradiction. In that case, the branch is said to '''close'''.<ref name=":13" /> If every branch in a tree closes, the tree itself is said to close.<ref name=":13" /> 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.<ref name=":13" /> Conversely, a tableau can also prove that a logical formula is [[Tautology (logic)|tautologous]]: if a formula is tautologous, its negation is a contradiction, so a tableau built from its negation will close.<ref name=":13" />

To construct a tableau for an argument <math>\langle \{\varphi_1, \varphi_2, \varphi_3, ..., \varphi_n\} , \psi \rangle</math>, one first writes out the set of premise formulas, <math>\{\varphi_1, \varphi_2, \varphi_3, ..., \varphi_n\}</math>, with one formula on each line, signed with <math>T</math> (that is, <math>T\varphi</math> for each <math>T\varphi</math> in the set);<ref name=":37" /> and together with those formulas (the order is unimportant), one also writes out the conclusion, <math>\psi</math>, signed with <math>F</math> (that is, <math>F\psi</math>).<ref name=":37" /> One then produces a truth tree (analytic tableau) by using all those lines according to the rules.<ref name=":37" /> A closed tree will be proof that the argument was valid, in virtue of the fact that <math>\varphi \models \psi</math> if, and only if, <math>\{ \varphi, \sim\psi \}</math> is inconsistent (also written as <math>\varphi, \sim\psi \models</math>).<ref name=":37" />

== 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.<ref name="BostockIntermediate" /> We use <math>\varphi</math> ⟚ <math>\psi</math> to denote equivalence of <math>\varphi</math> and <math>\psi</math>, that is, as an abbreviation for both <math>\varphi \models \psi</math> and <math>\psi \models \varphi</math>;<ref name="BostockIntermediate" /> 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,<ref name="BostockIntermediate" /><ref>{{Cite book |last=Lawson |first=Mark V. |title=A first course in logic |date=2019 |publisher=CRC Press, Taylor & Francis Group |isbn=978-0-8153-8664-3 |location=Boca Raton |pages=example 1.58}}</ref> although many authors prefer to read it as "entails",<ref name="BostockIntermediate" /><ref>{{Cite book |last=Dean |first=Neville |title=Logic and language |date=2003 |publisher=Palgrave Macmillan |isbn=978-0-333-91977-4 |location=Basingstoke |pages=66}}</ref> or as "models".<ref>{{Cite book |last1=Chiswell |first1=Ian |title=Mathematical logic |last2=Hodges |first2=Wilfrid |date=2007 |publisher=Oxford university press |isbn=978-0-19-857100-1 |series=Oxford texts in logic |location=Oxford |pages=3}}</ref>
{| class="wikitable" style="margin:auto;"
|- "
! Name
! Sequent
! Description
|-
| [[Modus Ponens]]
| style="text-align:center;" | <math>((p \to q) \land p) \models q</math><ref name=":21" />
| If {{mvar|p}} then {{mvar|q}}; {{mvar|p}}; therefore {{mvar|q}}
|-
| [[Modus Tollens]]
| style="text-align:center;" | <math>((p \to q) \land \neg q) \models \neg p</math><ref name=":21" />
| If {{mvar|p}} then {{mvar|q}}; not {{mvar|q}}; therefore not {{mvar|p}}
|-
| [[Hypothetical Syllogism]]
| style="text-align:center;" | <math>((p \to q) \land (q \to r)) \models (p \to r)</math><ref name=":35" />
| If {{mvar|p}} then {{mvar|q}}; if {{mvar|q}} then {{mvar|r}}; therefore, if {{mvar|p}} then {{mvar|r}}
|-
| [[Disjunctive syllogism|Disjunctive Syllogism]]
| style="text-align:center;" | <math>((p \lor q) \land \neg p) \models q</math><ref name=":28">{{Cite book |last=Hodges |first=Wilfrid |title=Logic |date=2001 |publisher=Penguin Books |isbn=978-0-14-100314-6 |edition=2 |location=London |pages=130–131 |language=en}}</ref>
| Either {{mvar|p}} or {{mvar|q}}, or both; not {{mvar|p}}; therefore, {{mvar|q}}
|-
| [[Constructive dilemma|Constructive Dilemma]]
| style="text-align:center;" | <math>((p \to q) \land (r \to s) \land (p \lor r)) \models (q \lor s)</math><ref name=":35" />
| If {{mvar|p}} then {{mvar|q}}; and if {{mvar|r}} then {{mvar|s}}; but {{mvar|p}} or {{mvar|r}}; therefore {{mvar|q}} or {{mvar|s}}
|-
| [[Destructive dilemma|Destructive Dilemma]]
| style="text-align:center;" | <math>((p \to q) \land (r \to s) \land(\neg q \lor \neg s)) \models (\neg p \lor \neg r)</math>
| If {{mvar|p}} then {{mvar|q}}; and if {{mvar|r}} then {{mvar|s}}; but not {{mvar|q}} or not {{mvar|s}}; therefore not {{mvar|p}} or not {{mvar|r}}
|-
| Bidirectional Dilemma
| style="text-align:center;" | <math>((p \to q) \land (r \to s) \land(p \lor \neg s)) \models (q \lor \neg r)</math>
| If {{mvar|p}} then {{mvar|q}}; and if {{mvar|r}} then {{mvar|s}}; but {{mvar|p}} or not {{mvar|s}}; therefore {{mvar|q}} or not {{mvar|r}}
|-
| [[Conjunction elimination|Simplification]]
| style="text-align:center;" | <math>(p \land q) \models p</math><ref name=":21" />
| {{mvar|p}} and {{mvar|q}} are true; therefore {{mvar|p}} is true
|-
| [[Logical conjunction|Conjunction]]
| style="text-align:center;" | <math>p, q \models (p \land q)</math><ref name=":21" />
| {{mvar|p}} and {{mvar|q}} are true separately; therefore they are true conjointly
|-
| [[Logical disjunction|Addition]]
| style="text-align:center;" | <math>p \models (p \lor q)</math><ref name=":21" /><ref name=":28" />
| {{mvar|p}} is true; therefore the disjunction ({{mvar|p}} or {{mvar|q}}) is true
|-
| [[Distributive property|Composition]]
| style="text-align:center;" | <math>((p \to q) \land (p \to r)) \models (p \to (q \land r))</math>
| If {{mvar|p}} then {{mvar|q}}; and if {{mvar|p}} then {{mvar|r}}; therefore if {{mvar|p}} is true then {{mvar|q}} and {{mvar|r}} are true
|-
| [[De Morgan's laws|De Morgan's Theorem]] (1)
| style="text-align:center;" | <math>\neg (p \land q)</math> ⟚ <math>(\neg p \lor \neg q)</math><ref name=":21" />
| The negation of ({{mvar|p}} and {{mvar|q}}) is equiv. to (not {{mvar|p}} or not {{mvar|q}})
|-
| [[De Morgan's laws|De Morgan's Theorem]] (2)
| style="text-align:center;" | <math>\neg (p \lor q)</math> ⟚ <math>(\neg p \land \neg q)</math><ref name=":21" />
| The negation of ({{mvar|p}} or {{mvar|q}}) is equiv. to (not {{mvar|p}} and not {{mvar|q}})
|-
| [[Commutative property|Commutation]] (1)
| style="text-align:center;" | <math>(p \lor q)</math> ⟚ <math>(q \lor p)</math><ref name=":28" />
| ({{mvar|p}} or {{mvar|q}}) is equiv. to ({{mvar|q}} or {{mvar|p}})
|-
| [[Commutative property|Commutation]] (2)
| style="text-align:center;" | <math>(p \land q)</math> ⟚ <math>(q \land p)</math><ref name=":28" />
| ({{mvar|p}} and {{mvar|q}}) is equiv. to ({{mvar|q}} and {{mvar|p}})
|-
| [[Commutative property|Commutation]] (3)
| style="text-align:center;" | <math>(p \leftrightarrow q)</math> ⟚ <math>(q \leftrightarrow p)</math><ref name=":28" />
| ({{mvar|p}} iff {{mvar|q}}) is equiv. to ({{mvar|q}} iff {{mvar|p}})
|-
| [[Associative property|Association]] (1)
| style="text-align:center;" | <math>(p \lor (q \lor r))</math> ⟚ <math>((p \lor q) \lor r)</math><ref name=":13" />
| {{mvar|p}} or ({{mvar|q}} or {{mvar|r}}) is equiv. to ({{mvar|p}} or {{mvar|q}}) or {{mvar|r}}
|-
| [[Associative property|Association]] (2)
| style="text-align:center;" | <math>(p \land (q \land r))</math> ⟚ <math>((p \land q) \land r)</math><ref name=":13" />
| {{mvar|p}} and ({{mvar|q}} and {{mvar|r}}) is equiv. to ({{mvar|p}} and {{mvar|q}}) and {{mvar|r}}
|-
| [[Distributive property|Distribution]] (1)
| style="text-align:center;" | <math>(p \land (q \lor r))</math> ⟚ <math>((p \land q) \lor (p \land r))</math><ref name=":28" />
| {{mvar|p}} and ({{mvar|q}} or {{mvar|r}}) is equiv. to ({{mvar|p}} and {{mvar|q}}) or ({{mvar|p}} and {{mvar|r}})
|-
| [[Distributive property|Distribution]] (2)
| style="text-align:center;" | <math>(p \lor (q \land r))</math> ⟚ <math>((p \lor q) \land (p \lor r))</math><ref name=":28" />
| {{mvar|p}} or ({{mvar|q}} and {{mvar|r}}) is equiv. to ({{mvar|p}} or {{mvar|q}}) and ({{mvar|p}} or {{mvar|r}})
|-
| [[Double negation elimination|Double Negation]]
| style="text-align:center;" | <math>p</math> ⟚ <math>\neg \neg p</math><ref name=":21" /><ref name=":28" />
| {{mvar|p}} is equivalent to the negation of not {{mvar|p}}
|-
| [[Transposition (logic)|Transposition]]
| style="text-align:center;" | <math>(p \to q)</math> ⟚ <math>(\neg q \to \neg p)</math><ref name=":21" />
| If {{mvar|p}} then {{mvar|q}} is equiv. to if not {{mvar|q}} then not {{mvar|p}}
|-
| [[Material implication (rule of inference)|Material Implication]]
| style="text-align:center;" | <math>(p \to q)</math> ⟚ <math>(\neg p \lor q)</math><ref name=":28" />
| If {{mvar|p}} then {{mvar|q}} is equiv. to not {{mvar|p}} or {{mvar|q}}
|-
| [[Material equivalence|Material Equivalence]] (1)
| style="text-align:center;" | <math>(p \leftrightarrow q)</math> ⟚ <math>((p \to q) \land (q \to p))</math><ref name=":28" />
| ({{mvar|p}} {{not a typo|iff}} {{mvar|q}}) is equiv. to (if {{mvar|p}} is true then {{mvar|q}} is true) and (if {{mvar|q}} is true then {{mvar|p}} is true)
|-
| [[Material equivalence|Material Equivalence]] (2)
| style="text-align:center;" | <math>(p \leftrightarrow q)</math> ⟚ <math>((p \land q) \lor (\neg p \land \neg q))</math><ref name=":28" />
| ({{mvar|p}} {{not a typo|iff}} {{mvar|q}}) is equiv. to either ({{mvar|p}} and {{mvar|q}} are true) or (both {{mvar|p}} and {{mvar|q}} are false)
|-
| [[Material equivalence|Material Equivalence]] (3)
| style="text-align:center;" | <math>(p \leftrightarrow q)</math> ⟚ <math>((p \lor \neg q) \land (\neg p \lor q))</math>
| ({{mvar|p}} {{not a typo|iff}} {{mvar|q}}) is equiv to., both ({{mvar|p}} or not {{mvar|q}} is true) and (not {{mvar|p}} or {{mvar|q}} is true)
|-
| [[Exportation (logic)|Exportation]]
| style="text-align:center;" | <math>((p \land q) \to r) \models (p \to (q \to r))</math><ref>{{cite web |last=Toida |first=Shunichi |date=2 August 2009 |title=Proof of Implications |url=http://www.cs.odu.edu/~toida/nerzic/content/logic/prop_logic/implications/implication_proof.html |access-date=10 March 2010 |work=CS381 Discrete Structures/Discrete Mathematics Web Course Material |publisher=Department of Computer Science, [[Old Dominion University]]}}</ref>
| from (if {{mvar|p}} and {{mvar|q}} are true then {{mvar|r}} is true) we can prove (if {{mvar|q}} is true then {{mvar|r}} is true, if {{mvar|p}} is true)
|-
| [[Exportation (logic)|Importation]]
| style="text-align:center;" | <math>(p \to (q \to r))</math> ⟚ <math>((p \land q) \to r)</math><ref name=":35" />
| If {{mvar|p}} then (if {{mvar|q}} then {{mvar|r}}) is equivalent to if {{mvar|p}} and {{mvar|q}} then {{mvar|r}}
|-
| [[Tautology (rule of inference)|Idempotence of disjunction]] 
| style="text-align:center;" | <math>p</math> ⟚ <math>(p \lor p)</math><ref name=":28" />
| {{mvar|p}} is true is equiv. to {{mvar|p}} is true or {{mvar|p}} is true
|-
| [[Tautology (rule of inference)|Idempotence of conjunction]]
| style="text-align:center;" | <math>p</math> ⟚ <math>(p \land p)</math><ref name=":28" />
| {{mvar|p}} is true is equiv. to {{mvar|p}} is true and {{mvar|p}} is true
|-
| [[Law of excluded middle|Tertium non datur (Law of Excluded Middle)]]
| style="text-align:center;" | <math>\models (p \lor \neg p)</math><ref name=":21" /><ref name=":28" />
| {{mvar|p}} or not {{mvar|p}} is true
|-
| [[Law of noncontradiction|Law of Non-Contradiction]]
| style="text-align:center;" | <math>\models \neg (p \land \neg p)</math><ref name=":21" /><ref name=":28" />
| {{mvar|p}} and not {{mvar|p}} is false, is a true statement
|-
|[[Principle of explosion|Explosion]]
| style="text-align:center;" | <math>(p \land \neg p) \models q</math><ref name=":21" />
| {{mvar|p}} and not {{mvar|p}}; therefore {{mvar|q}}
|}

== Syntactic proof via natural deduction ==
{{Main article|Natural deduction}}{{Transformation rules}}[[Natural deduction]], since it is a method of syntactical proof, is specified by providing ''inference rules'' (also called ''rules of proof'')<ref name=":35" /> for a language with the typical set of connectives <math>\{ -, \&, \lor, \to, \leftrightarrow \}</math>; no axioms are used other than these rules.<ref name=":38">{{Cite book |last=Lemmon |first=Edward John |title=Beginning logic |date=1998 |publisher=Chapman & Hall/CRC |isbn=978-0-412-38090-7 |location=Boca Raton, FL |pages=passim, especially 39–40}}</ref> 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<ref name=":40" /><ref name=":3" />—not to be confused with "truth trees", which is another name for [[Method of analytic tableaux|analytic tableaux]].<ref name=":37" /> There is also a style due to [[Stanisław Jaśkowski]], where the formulas in the proof are written inside various nested boxes,<ref name=":40" /> and there is a simplification of Jaśkowski's style due to [[Frederic Fitch|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.<ref name=":40" /> Lastly, there is the only notation style which will actually be used in this article, which is due to [[Patrick Suppes]],<ref name=":40" /> but was much popularized by [[John Lemmon|E.J. Lemmon]] and [[Benson Mates]].<ref>{{Cite web |title=Natural Deduction Systems in Logic > Notes (Stanford Encyclopedia of Philosophy) |url=https://plato.stanford.edu/entries/natural-deduction/notes.html#note-21 |access-date=2024-04-19 |website=plato.stanford.edu |language=en}}</ref> This method has the advantage that, graphically, it is the least intensive to produce and display, which made it a natural choice for the [[Wikipedia community|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,<ref name=":40" /> is a sequence of lines containing sentences,<ref name=":35" /> where each sentence is either an assumption, or the result of applying a rule of proof to earlier sentences in the sequence.<ref name=":35" /> Each '''line of proof''' is made up of a '''sentence of proof''', together with its '''annotation''', its '''assumption set''', and the current '''line number'''.<ref name=":35" /> The assumption set lists the assumptions on which the given sentence of proof depends, which are referenced by the line numbers.<ref name=":35" /> The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence.<ref name=":35" /> See the {{section link||Natural deduction proof example}}.

=== Inference rules ===
Natural deduction inference rules, due ultimately to [[Gerhard Gentzen|Gentzen]], are given below.<ref name=":38" /> 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''.<ref name=":35" /> Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination,<ref name=":35" /> and MTT and DN are commonly given rules,<ref name=":38" /> although they are not primitive.<ref name=":35" />

{| class="wikitable" style="margin:auto;"

|+ List of Inference Rules
|-
! Rule Name
! Alternative names
! Annotation
!Assumption set
! Statement
|-
| Rule of Assumptions<ref name=":38" />|| Assumption<ref name=":35" />|| '''A<ref name=":38" /><ref name=":35" />'''
|The current line number.<ref name=":35" />|| At any stage of the argument, introduce a proposition as an assumption of the argument.<ref name=":38" /><ref name=":35" />
|-
| Conjunction introduction|| Ampersand introduction,<ref name=":38" /><ref name=":35" /> conjunction (CONJ)<ref name=":35" /><ref name=":39">{{Cite book |last=Arthur |first=Richard T. W. |url=https://www.worldcat.org/title/962129086 |title=An introduction to logic: using natural deduction, real arguments, a little history, and some humour |date=2017 |publisher=Broadview Press |isbn=978-1-55481-332-2 |edition=2nd |location=Peterborough, Ontario |oclc=962129086}}</ref>|| '''m, n &I<ref name=":35" /><ref name=":38" />'''
|The union of the assumption sets at lines '''m''' and '''n'''.<ref name=":35" />|| From <math>\varphi</math> and <math>\psi</math> at lines '''m''' and '''n''', infer <math>\varphi ~ \& ~ \psi</math>.<ref name=":38" /><ref name=":35" />
|-
| Conjunction elimination|| Simplification (S),<ref name=":35" /> ampersand elimination<ref name=":38" /><ref name=":35" />|| '''m &E<ref name=":35" /><ref name=":38" />'''
|The same as at line '''m'''.<ref name=":35" />|| From <math>\varphi ~ \& ~ \psi</math> at line '''m''', infer <math>\varphi</math> and <math>\psi</math>.<ref name=":35" /><ref name=":38" />
|-
| Disjunction introduction<ref name=":38" />|| Addition (ADD)<ref name=":35" />|| '''m ∨I<ref name=":35" /><ref name=":38" />'''
|The same as at line '''m'''.<ref name=":35" />|| From <math>\varphi</math> at line '''m''', infer <math>\varphi \lor \psi</math>, whatever <math>\psi</math> may be.<ref name=":35" /><ref name=":38" />
|-
| Disjunction elimination|| Wedge elimination,<ref name=":38" /> dilemma (DL)<ref name=":39" />|| '''j,k,l,m,n ∨E<ref name=":38" />'''
|The lines '''j,k,l,m,n'''.<ref name=":38" />|| From <math>\varphi \lor \psi</math> at line '''j''', and an assumption of <math>\varphi</math> at line '''k''', and a derivation of <math>\chi</math> from <math>\varphi</math> at line '''l''', and an assumption of <math>\psi</math> at line '''m''', and a derivation of <math>\chi</math> from <math>\psi</math> at line '''n''', infer <math>\chi</math>.<ref name=":38" />
|-
|Disjunctive Syllogism
|Wedge elimination (∨E),<ref name=":35" /> modus tollendo ponens (MTP)<ref name=":35" />
|'''m,n DS<ref name=":35" />'''
|The union of the assumption sets at lines '''m''' and '''n'''.<ref name=":35" />
|From <math>\varphi \lor \psi</math> at line '''m''' and <math>- \varphi</math> at line '''n''', infer <math>\psi</math>; from <math>\varphi \lor \psi</math> at line '''m''' and <math>- \psi</math> at line '''n''', infer <math>\varphi</math>.<ref name=":35" />
|-
| Arrow elimination<ref name=":35" />|| Modus ponendo ponens (MPP),<ref name=":38" /><ref name=":35" /> modus ponens (MP),<ref name=":39" /><ref name=":35" /> conditional elimination || '''m, n →E<ref name=":35" /><ref name=":38" />'''
|The union of the assumption sets at lines '''m''' and '''n'''.<ref name=":35" />|| From <math>\varphi \to \psi</math> at line '''m''', and <math>\varphi</math> at line '''n''', infer <math>\psi</math>.<ref name=":35" />
|-
| Arrow introduction<ref name=":35" />|| Conditional proof (CP),<ref name=":39" /><ref name=":38" /><ref name=":35" /> conditional introduction || '''n, →I (m)<ref name=":35" /><ref name=":38" />'''
|Everything in the assumption set at line '''n''', excepting '''m''', the line where the antecedent was assumed.<ref name=":35" />|| From <math>\psi</math> at line '''n''', following from the assumption of <math>\varphi</math> at line '''m''', infer <math>\varphi \to \psi</math>.<ref name=":35" />
|-
| Reductio ad absurdum<ref name=":38" />|| Indirect Proof (IP),<ref name=":35" /> negation introduction (−I),<ref name=":35" /> negation elimination (−E)<ref name=":35" />|| '''m,'''&nbsp;'''n'''&nbsp;'''RAA'''&nbsp;'''(k)<ref name=":35" />'''
|The union of the assumption sets at lines '''m''' and '''n''', excluding '''k''' (the denied assumption).<ref name=":35" />|| From a sentence and its denial{{refn|group=lower-alpha|To simplify the statement of the rule, the word "denial" here is used in this way: the ''denial'' of a formula <math>\varphi</math> that is not a ''negation'' is <math>- \varphi</math>, whereas a ''negation'', <math>- \varphi</math>, has two ''denials'', viz., <math>\varphi</math> and <math>- - \varphi</math>.<ref name=":35" />}} at lines '''m''' and '''n''', infer the denial of any assumption appearing in the proof (at line '''k''').<ref name=":35" />
|-
| Double arrow introduction<ref name=":35" />|| Biconditional definition (''Df'' ↔),<ref name=":38" /> biconditional introduction|| '''m, n ↔ I<ref name=":35" />'''
|The union of the assumption sets at lines '''m''' and '''n'''.<ref name=":35" />|| From <math>\varphi \to \psi</math> and <math>\psi \to \varphi</math> at lines '''m''' and '''n''', infer <math>\varphi \leftrightarrow \psi</math>.<ref name=":35" />
|-
| Double arrow elimination<ref name=":35" />|| Biconditional definition (''Df'' ↔),<ref name=":38" /> biconditional elimination|| '''m ↔ E<ref name=":35" />'''
|The same as at line '''m'''.<ref name=":35" />|| From <math>\varphi \leftrightarrow \psi</math> at line '''m''', infer either <math>\varphi \to \psi</math> or <math>\psi \to \varphi</math>.<ref name=":35" />
|-
| Double negation<ref name=":38" /><ref name=":39" />|| Double negation elimination|| '''m DN<ref name=":38" />'''
|The same as at line '''m'''.<ref name=":38" />|| From <math>- - \varphi</math> at line '''m''', infer <math>\varphi</math>.<ref name=":38" />
|-
| Modus tollendo tollens<ref name=":38" />|| Modus tollens (MT)<ref name=":39" />|| '''m, n MTT<ref name=":38" />'''
|The union of the assumption sets at lines '''m''' and '''n'''.<ref name=":38" />|| From <math>\varphi \to \psi</math> at line '''m''', and <math>- \psi</math> at line '''n''', infer <math>- \varphi</math>.<ref name=":38" />
|}

=== Natural deduction proof example ===
The proof below'''<ref name=":35" />''' derives <math>-P</math> from <math>P \to Q</math> and <math>-Q</math> 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
|-
| {{EquationRef|1}}|| {{EquationRef|1}} || <math>P \to Q</math> || A
|-
| {{EquationRef|2}} || {{EquationRef|2}} || <math>-Q</math> || A
|-
| {{EquationRef|3}} || {{EquationRef|3}} || <math>P</math> || A
|-
| {{EquationRef|1}}, {{EquationRef|3}} || {{EquationRef|4}} || <math>Q</math> || {{EquationRef|1}}, {{EquationRef|3}} →E
|-
| {{EquationRef|1}}, {{EquationRef|2}} || {{EquationRef|5}} || <math>-P</math> || {{EquationRef|2}}, {{EquationRef|4}} RAA
|}

== Syntactic proof via axioms ==
{{Main article|Axiomatic system (logic)}}
It is possible to perform proofs axiomatically, which means that certain [[Tautology (logic)|tautologies]] are taken as self-evident and various others are deduced from them using [[modus ponens]] as an [[Rule of inference|inference rule]], as well as a ''rule of [[Substitution (logic)|substitution]]'', which permits replacing any [[well-formed formula]] with any {{glossary link|substitution-instance|glossary=Glossary of logic}} of it.<ref name=":44" /> Alternatively, one uses axiom schemas instead of axioms, and no rule of substitution is used.<ref name=":44" />

This section gives the axioms of some historically notable axiomatic systems for propositional logic. For more examples, as well as metalogical theorems that are specific to such axiomatic systems (such as their completeness and consistency), see the article [[Axiomatic system (logic)]].

=== Frege's ''Begriffsschrift'' ===
Although axiomatic proof has been used since the famous [[Ancient Greek]] textbook, [[Euclid]]'s ''[[Euclid's Elements|Elements of Geometry]]'', in propositional logic it dates back to [[Gottlob Frege]]'s [[1879]] ''[[Begriffsschrift]]''.<ref name="BostockIntermediate" /><ref name=":44">{{Cite book |last=Smullyan |first=Raymond M. |url=https://books.google.com/books?id=n6S-AwAAQBAJ |title=A Beginner's Guide to Mathematical Logic |date=2014-07-23 |publisher=Courier Corporation |isbn=978-0-486-49237-7 |pages=102–103 |language=en}}</ref> Frege's system used only [[Material conditional|implication]] and [[negation]] as connectives,<ref name=":2" /> and it had six axioms,<ref name=":44" /> which were these ones:<ref name=":45">{{Cite book |last=Mendelsohn |first=Richard L. |url=https://books.google.com/books?id=G6_90xFwUbUC |title=The Philosophy of Gottlob Frege |date=2005-01-10 |publisher=Cambridge University Press |isbn=978-1-139-44403-3 |pages=185 |language=en}}</ref><ref name=":46">{{Cite book |last=Łukasiewicz |first=Jan |url=https://books.google.com/books?id=Jb_zOwAACAAJ |title=Jan Lukasiewicz: Selected Works |date=1970 |publisher=North-Holland |pages=136 |language=en}}</ref>

* Proposition 1: <math>a \supset (b \supset a)</math>
* Proposition 2: <math>(c \supset (b \supset a)) \supset ((c \supset b) \supset (c \supset a))</math>
* Proposition 8: <math>(d \supset (b \supset a)) \supset (b \supset (d \supset a))</math>
* Proposition 28: <math>(b \supset a) \supset (\neg a \supset \neg b)</math>
* Proposition 31: <math>\neg \neg a \supset a</math>
* Proposition 41: <math>a \supset \neg \neg a</math>

These were used by Frege together with modus ponens and a rule of substitution (which was used but never precisely stated) to yield a complete and consistent axiomatization of classical truth-functional propositional logic.<ref name=":45" />

=== Łukasiewicz's P<sub>2</sub> ===
[[Jan Łukasiewicz]] showed that, in Frege's system, "the third axiom is superfluous since it can be derived from the preceding two axioms, and that the last three axioms can be replaced by the single sentence <math>CCNpNqCpq</math>".<ref name=":46" /> Which, taken out of Łukasiewicz's [[Polish notation]] into modern notation, means <math>(\neg p \rightarrow \neg q) \rightarrow (p \rightarrow q)</math>. Hence, Łukasiewicz is credited<ref name=":44" /> with this system of three axioms:

* <math>p \to (q \to p)</math>
* <math>(p \to (q \to r)) \to ((p \to q) \to (p \to r))</math>
* <math>(\neg p \to \neg q) \to (q \to p)</math>

Just like Frege's system, this system uses a substitution rule and uses modus ponens as an inference rule.<ref name=":44" /> The exact same system was given (with an explicit substitution rule) by [[Alonzo Church]],<ref name=":47">{{Cite book |last=Church |first=Alonzo |url=https://books.google.com/books?id=JDLQOMKbdScC |title=Introduction to Mathematical Logic |date=1996 |publisher=Princeton University Press |isbn=978-0-691-02906-1 |pages=119 |language=en}}</ref> who referred to it as the system P<sub>2</sub><ref name=":47" /><ref name=":48">{{Cite web |title=Proof Explorer - Home Page - Metamath |url=https://us.metamath.org/mpegif/mmset.html#scaxioms |access-date=2024-07-02 |website=us.metamath.org |language=EN-US}}</ref> and helped popularize it.<ref name=":48" />

==== Schematic form of P<sub>2</sub> ====
One may avoid using the rule of substitution by giving the axioms in schematic form, using them to generate an infinite set of axioms. Hence, using Greek letters to represent schemata (metalogical variables that may stand for any [[well-formed formula]]s), the axioms are given as:<ref name="BostockIntermediate" /><ref name=":48" />

* <math>\varphi \to (\psi \to \varphi)</math>
* <math>(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))</math>
* <math>(\neg \varphi \to \neg \psi) \to (\psi \to \varphi)</math>

The schematic version of P<sub>2</sub> is attributed to [[John von Neumann]],<ref name=":44" /> and is used in the [[Metamath]] "set.mm" formal proof database.<ref name=":48" /> It has also been attributed to [[David Hilbert|Hilbert]],<ref name=":49">{{Cite book |last=Walicki |first=Michał |title=Introduction to mathematical logic |date=2017 |publisher=World Scientific |isbn=978-981-4719-95-7 |edition=Extended |location=New Jersey |pages=126}}</ref> and named <math>\mathcal{H}</math> in this context.<ref name=":49" />

====Proof example in P<sub>2</sub>====
As an example, a proof of <math> A \to A </math> in P<sub>2</sub> is given below. First, the axioms are given names:
:(A1) <math>(p \to (q \to p))</math>
:(A2) <math>((p \to (q \to r)) \to ((p \to q) \to (p \to r)))</math>
:(A3) <math>((\neg p \to \neg q) \to (q \to p))</math>

And the proof is as follows:
# <math> A \to ((B \to A) \to A)</math> &nbsp; &nbsp; &nbsp; (instance of (A1))
# <math> (A \to ((B \to A) \to A)) \to ((A \to (B \to A)) \to (A \to A))</math> &nbsp; &nbsp; &nbsp; (instance of (A2))
# <math> (A \to (B \to A)) \to (A \to A)</math> &nbsp; &nbsp; &nbsp; (from (1) and (2) by [[modus ponens]])
# <math> A \to (B \to A)</math> &nbsp; &nbsp; &nbsp; (instance of (A1))
# <math> A \to A </math> &nbsp; &nbsp; &nbsp; (from (4) and (3) by modus ponens)

==Solvers==
One notable difference between propositional calculus and predicate calculus is that satisfiability of a propositional formula is [[Decidable set|decidable]].<ref>W. V. O. Quine, ''Mathematical Logic'' (1980), p.81. Harvard University Press, 0-674-55451-5</ref> 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 expression]]s; these are the [[SMT solver]]s.

==See also==
{{Portal|Philosophy}}

===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]]
* [[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.
* [[Chen Chung Chang|Chang, C.C.]] and [[Howard Jerome Keisler|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.
* [[Robert R. Korfhage|Korfhage, Robert R.]] (1974), ''Discrete Computational Structures'', Academic Press, New York, NY.
* [[Joachim Lambek|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===
* {{Cite book|last=Hofstadter |first=Douglas |author-link=Douglas Hofstadter |title=[[Gödel, Escher, Bach|Gödel, Escher, Bach: An Eternal Golden Braid]] |year=1979 |publisher=[[Basic Books]] |isbn=978-0-465-02656-2 }}

==External links==
{{Commons category}}
*[[Kevin C. Klement|Klement, Kevin C.]] (2006), "Propositional Logic", in James Fieser and Bradley Dowden (eds.), ''[[Internet Encyclopedia of Philosophy]]'', [http://www.iep.utm.edu/p/prop-log.htm Eprint].
*[http://www.qedeq.org/current/doc/math/qedeq_formal_logic_v1_en.pdf Formal Predicate Calculus], contains a systematic formal development with axiomatic proof
* ''[http://www.fecundity.com/logic/ forall x: an introduction to formal logic]'', by [[P.D. Magnus]], covers formal semantics and [[proof theory]] for sentential logic.
*[http://logicinaction.org/docs/ch2.pdf Chapter 2 / Propositional Logic] from [http://logicinaction.org Logic In Action]
*[https://www.nayuki.io/page/propositional-sequent-calculus-prover Propositional sequent calculus prover] on Project Nayuki. (''note'': implication can be input in the form <code>!X|Y</code>, and a sequent can be a single formula prefixed with <code>></code> and having no commas)
*[https://docs.google.com/document/d/1DhtRAPcMwJmiQnbdmFcHWaOddQ7kuqqDnWp2LZcGlnY/edit?usp=sharing Propositional Logic - A Generative Grammar]
*[https://propositional-calculator.com/ A Propositional Calculator that helps to understand simple expressions]

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

[[Category:Propositional calculus| ]]
[[Category:Logical calculi]]
[[Category:Boolean algebra]]
[[Category:Classical logic]]
[[Category:Analytic philosophy]]