Editing Propositional calculus (section)

== 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"/> 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" />