Editing Propositional calculus (section)

== 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 name="ms47"/> although many authors prefer to read it as "entails",<ref name="BostockIntermediate" /><ref name="ms48"/> or as "models".<ref name="ms49"/>
{| 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"/>
| 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 of conjunction]]
| style="text-align:center;" | <math>((p \to q) \land (p \to r))</math> ⟚ <math>(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
|-
| [[Distributive property|Composition of disjunction]]
| style="text-align:center;" | <math>((p \to q) \lor (p \to r))</math> ⟚ <math>(p \to (q \lor r))</math>
| If {{mvar|p}} then {{mvar|q}}; or if {{mvar|p}} then {{mvar|r}}; therefore if {{mvar|p}} is true then {{mvar|q}} or {{mvar|r}} is 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 name="ms50"/>
| 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))\models((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}}
|}