Editing Propositional calculus (section)

== 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"/><ref name=":31"/><ref name=":32"/>

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

{| class="wikitable" style="margin:1em auto; text-align:center;"
|-
! ''p''
! ''q''
! ''r''
! {{math|''q'' ∨ ''r''}}
! {{math|''r'' → ¬''p''}}
! {{math|''q'' ∨ ''r'' → (''r'' → ¬''p'')}}
! {{math|''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 name="ms60"/><ref name="ms61"/>