Editing Disjunctive normal form (section)

==Disjunctive Normal Form Theorem==
It is a theorem that all consistent formulas in [[Propositional calculus|propositional logic]] can be converted to disjunctive normal form.<ref name=":0">{{Cite book |last=Halbeisen |first=Lorenz |title=Gödel´s theorems and zermelo´s axioms: a firm foundation of mathematics |last2=Kraph |first2=Regula |date=2020 |publisher=Birkhäuser |isbn=978-3-030-52279-7 |location=Cham |pages=27}}</ref><ref name=":13" /><ref name=":1">{{Cite book |last=Cenzer |first=Douglas |title=Set theory and foundations of mathematics: an introduction to mathematical logic |last2=Larson |first2=Jean |last3=Porter |first3=Christopher |last4=Zapletal |first4=Jindřich |date=2020 |publisher=World Scientific |isbn=978-981-12-0192-9 |location=New Jersey |pages=19–21}}</ref><ref name=":2">{{Cite book |last=Halvorson |first=Hans |title=How logic works: a user's guide |date=2020 |publisher=Princeton University Press |isbn=978-0-691-18222-3 |location=Princeton Oxford |pages=195}}</ref> This is called the '''Disjunctive Normal Form Theorem'''.<ref name=":0" /><ref name=":13" /><ref name=":1" /><ref name=":2" /> The formal statement is as follows:<blockquote>'''Disjunctive Normal Form Theorem:''' Suppose <math>X</math> is a sentence in a propositional language <math>\mathcal{L}</math> with <math>n</math> sentence letters, which we shall denote by <math>A_1,...,A_n</math>. If <math>X</math> is not a contradiction, then it is truth-functionally equivalent to a disjunction of conjunctions of the form <math>\pm A_1 \land ... \land \pm A_n</math>, where <math>+A_i=A_i</math>, and <math>-A_i= \neg A_i</math>.<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=41}}</ref></blockquote>The proof follows from the procedure given above for generating DNFs from [[truth table]]s. Formally, the proof is as follows:<blockquote>Suppose <math>X</math> is a sentence in a propositional language whose sentence letters are <math>A, B, C, \ldots</math>. For each row of <math>X</math>'s truth table, write out a corresponding [[Logical conjunction|conjunction]] <math>\pm A \land \pm B \land \pm C \land \ldots</math>, where <math>\pm A</math> is defined to be <math>A</math> if <math>A</math> takes the value <math>T</math> at that row, and is <math>\neg A</math> if <math>A</math> takes the value <math>F</math> at that row; similarly for <math>\pm B</math>, <math>\pm C</math>, etc. (the [[alphabetical order]]ing of <math>A, B, C, \ldots</math> in the conjunctions is quite arbitrary; any other could be chosen instead). Now form the [[Logical disjunction|disjunction]] of all these conjunctions which correspond to <math>T</math> rows of <math>X</math>'s truth table. This disjunction is a sentence in <math>\mathcal{L}[A, B, C, \ldots; \land, \lor, \neg]</math>,<ref>That is, the language with the propositional variables <math>A, B, C, \ldots</math> and the connectives <math>\{\land, \lor, \neg\}</math>.</ref> which by the reasoning above is truth-functionally equivalent to <math>X</math>. This construction obviously presupposes that <math>X</math> takes the value <math>T</math> on at least one row of its truth table; if <math>X</math> doesn’t, i.e., if <math>X</math> is a [[contradiction]], then <math>X</math> is equivalent to <math>A \land \neg A</math>, which is, of course, also a sentence in <math>\mathcal{L}[A, B, C, \ldots; \land, \lor, \neg]</math>.<ref name=":13" /></blockquote>This theorem is a convenient way to derive many useful [[metalogic]]al results in propositional logic, such as, [[Triviality (mathematics)|trivially]], the result that the set of connectives <math>\{\land, \lor, \neg\}</math> is [[Functional completeness|functionally complete]].<ref name=":13" />