Editing Disjunction introduction

{{Short description|Inference introducing a disjunction in logical proofs}}
{{Infobox mathematical statement
| name = Disjunction introduction
| type = [[Rule of inference]]
| field = [[Propositional calculus]]
| statement = If <math>P</math> is true, then <math>P</math> or <math>Q</math> must be true.
| symbolic statement = <math>\frac{P}{\therefore P \lor Q}</math>
}}
{{Transformation rules}}

'''Disjunction introduction''' or '''addition''' (also called '''or introduction''')<ref>{{cite book |last1=Hurley |first1=Patrick J. |title=A Concise Introduction to Logic |date=2014 |publisher=Cengage |isbn=978-1-285-19654-1 |pages=401–402, 707 |edition=12th}}</ref><ref>{{cite book |last1=Moore |first1=Brooke Noel |last2=Parker |first2=Richard |title=Critical Thinking |date=2015 |publisher=McGraw Hill |location=New York |isbn=978-0-07-811914-9 |page=311 |edition=11th |chapter-url=https://archive.org/details/criticalthinking0000moor_t5e3/page/311/mode/1up |chapter-url-access=registration|chapter=Deductive Arguments II Truth-Functional Logic}}</ref><ref>{{cite book |last1=Copi |first1=Irving M. |last2=Cohen |first2=Carl |last3=McMahon |first3=Kenneth |title=Introduction to Logic|date=2014 |publisher=Pearson |isbn=978-1-292-02482-0 |edition=14th|pages=370, 618}}</ref> is a [[rule of inference]] of [[propositional calculus|propositional logic]] and almost every other [[deduction system]]. The rule makes it possible to introduce [[logical disjunction|disjunctions]] to [[formal proof|logical proofs]]. It is the [[inference]] that if ''P'' is true, then ''P or Q'' must be true.

An example in [[English language|English]]:
:Socrates is a man.
:Therefore, Socrates is a man or pigs are flying in formation over the English Channel.

The rule can be expressed as:
:<math>\frac{P}{\therefore P \lor Q}</math>

where the rule is that whenever instances of "<math>P</math>" appear on lines of a proof, "<math>P \lor Q</math>" can be placed on a subsequent line. 

More generally it's also a simple [[Validity (logic)|valid]] [[logical form|argument form]], this means that if the premise is true, then the conclusion is also true as any rule of inference should be, and an [[immediate inference]], as it has a single proposition in its premises. 

Disjunction introduction is not a rule in some [[paraconsistent logic]]s because in combination with other rules of logic, it leads to [[Principle of explosion|explosion]] (i.e. everything becomes provable) and paraconsistent logic tries to avoid explosion and to be able to reason with contradictions. One of the solutions is to introduce disjunction with over rules. See {{slink|Paraconsistent logic|Tradeoffs}}.

== Formal notation ==
The ''disjunction introduction'' rule may be written in [[sequent]] notation:

: <math>P \vdash (P \lor Q)</math>

where <math>\vdash</math> is a [[metalogic]]al symbol meaning that <math>P \lor Q</math> is a [[logical consequence|syntactic consequence]] of <math>P</math> in some [[formal system|logical system]];

and expressed as a truth-functional [[tautology (logic)|tautology]] or [[theorem]] of propositional logic:

:<math>P \to (P \lor Q)</math>

where <math>P</math> and <math>Q</math> are propositions expressed in some [[formal system]].

== References ==
{{reflist}}

{{DEFAULTSORT:Disjunction Introduction}}
[[Category:Rules of inference]]
[[Category:Paraconsistent logic]]
[[Category:Theorems in propositional logic]]