Theorem: Definition:Constructed Semantics/Instance 4/Factor Principle

The Factor Principle:
{{:Factor Principles/Disjunction on Left/Formulation 2}}
:$\paren {p \implies q} \implies \paren {\paren {r \lor p} \implies \paren {r \lor q} }$
is a tautology in Instance 4 of constructed semantics.

Proof:
{{handwaving}}
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Factor Principle can be written as:
:$\neg \paren {\neg p \lor q} \lor \paren {\neg \paren {r \lor p} \lor \paren {r \lor q} }$
This evaluates as follows:
:$\begin{array}{|ccccc|c|cccccccc|} \hline
\neg & (\neg & p & \lor & q) & \lor & (\neg & (r & \lor & p) & \lor & (r & \lor & q)) \\
\hline
1 & 1 & 0 & 0 & 0 & 0 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 \\
1 & 0 & 1 & 0 & 0 & 0 & 1 & 0 & 0 & 1 & 0 & 0 & 0 & 0 \\
1 & 0 & 2 & 0 & 0 & 0 & 1 & 0 & 0 & 2 & 0 & 0 & 0 & 0 \\
1 & 2 & 3 & 0 & 0 & 0 & 1 & 0 & 0 & 3 & 0 & 0 & 0 & 0 \\
1 & 1 & 0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 & 0 & 1 & 0 & 0 \\
1 & 0 & 1 & 0 & 0 & 0 & 0 & 1 & 1 & 1 & 0 & 1 & 0 & 0 \\
1 & 0 & 2 & 0 & 0 & 0 & 0 & 1 & 2 & 2 & 0 & 1 & 0 & 0 \\
1 & 2 & 3 & 0 & 0 & 0 & 2 & 1 & 3 & 3 & 0 & 1 & 0 & 0 \\
1 & 1 & 0 & 0 & 0 & 0 & 1 & 2 & 0 & 0 & 0 & 2 & 0 & 0 \\
1 & 0 & 1 & 0 & 0 & 0 & 0 & 2 & 2 & 1 & 0 & 2 & 0 & 0 \\
1 & 0 & 2 & 0 & 0 & 0 & 0 & 2 & 2 & 2 & 0 & 2 & 0 & 0 \\
1 & 2 & 3 & 0 & 0 & 0 & 1 & 2 & 0 & 3 & 0 & 2 & 0 & 0 \\
1 & 1 & 0 & 0 & 0 & 0 & 1 & 3 & 0 & 0 & 0 & 3 & 0 & 0 \\
1 & 0 & 1 & 0 & 0 & 0 & 2 & 3 & 3 & 1 & 0 & 3 & 0 & 0 \\
1 & 0 & 2 & 0 & 0 & 0 & 2 & 3 & 3 & 2 & 0 & 3 & 0 & 0 \\
1 & 2 & 3 & 0 & 0 & 0 & 2 & 3 & 3 & 3 & 0 & 3 & 0 & 0 \\
0 & 1 & 0 & 1 & 1 & 0 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 1 \\
1 & 0 & 1 & 0 & 1 & 0 & 1 & 0 & 0 & 1 & 0 & 0 & 0 & 1 \\
1 & 0 & 2 & 0 & 1 & 0 & 1 & 0 & 0 & 2 & 0 & 0 & 0 & 1 \\
0 & 2 & 3 & 2 & 1 & 0 & 1 & 0 & 0 & 3 & 0 & 0 & 0 & 1 \\
0 & 1 & 0 & 1 & 1 & 0 & 1 & 1 & 0 & 0 & 1 & 1 & 1 & 1 \\
1 & 0 & 1 & 0 & 1 & 0 & 0 & 1 & 1 & 1 & 0 & 1 & 1 & 1 \\
1 & 0 & 2 & 0 & 1 & 0 & 0 & 1 & 2 & 2 & 0 & 1 & 1 & 1 \\
0 & 2 & 3 & 2 & 1 & 0 & 2 & 1 & 3 & 3 & 2 & 1 & 1 & 1 \\
0 & 1 & 0 & 1 & 1 & 0 & 1 & 2 & 0 & 0 & 1 & 2 & 2 & 1 \\
1 & 0 & 1 & 0 & 1 & 0 & 0 & 2 & 2 & 1 & 0 & 2 & 2 & 1 \\
1 & 0 & 2 & 0 & 1 & 0 & 0 & 2 & 2 & 2 & 0 & 2 & 2 & 1 \\
0 & 2 & 3 & 2 & 1 & 0 & 1 & 2 & 0 & 3 & 1 & 2 & 2 & 1 \\
0 & 1 & 0 & 1 & 1 & 0 & 1 & 3 & 0 & 0 & 3 & 3 & 3 & 1 \\
1 & 0 & 1 & 0 & 1 & 0 & 0 & 3 & 1 & 1 & 0 & 3 & 3 & 1 \\
1 & 0 & 2 & 0 & 1 & 0 & 2 & 3 & 3 & 2 & 0 & 3 & 3 & 1 \\
0 & 2 & 3 & 2 & 1 & 0 & 2 & 3 & 3 & 3 & 0 & 3 & 3 & 1 \\
0 & 1 & 0 & 2 & 2 & 0 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 2 \\
1 & 0 & 1 & 0 & 2 & 0 & 1 & 0 & 0 & 1 & 0 & 0 & 0 & 2 \\
1 & 0 & 2 & 0 & 2 & 0 & 1 & 0 & 0 & 2 & 0 & 0 & 0 & 2 \\
0 & 2 & 3 & 2 & 2 & 0 & 1 & 0 & 0 & 3 & 0 & 0 & 0 & 2 \\
0 & 1 & 0 & 2 & 2 & 0 & 1 & 1 & 0 & 0 & 2 & 1 & 2 & 2 \\
1 & 0 & 1 & 0 & 2 & 0 & 0 & 1 & 1 & 1 & 0 & 1 & 2 & 2 \\
1 & 0 & 2 & 0 & 2 & 0 & 0 & 1 & 2 & 2 & 0 & 1 & 2 & 2 \\
0 & 2 & 3 & 2 & 2 & 0 & 2 & 1 & 3 & 3 & 2 & 1 & 2 & 2 \\
0 & 1 & 0 & 2 & 2 & 0 & 1 & 2 & 0 & 0 & 2 & 2 & 2 & 2 \\
1 & 0 & 1 & 0 & 2 & 0 & 0 & 2 & 2 & 1 & 0 & 2 & 2 & 2 \\
1 & 0 & 2 & 0 & 2 & 0 & 0 & 2 & 2 & 2 & 0 & 2 & 2 & 2 \\
0 & 2 & 3 & 2 & 2 & 0 & 1 & 2 & 0 & 3 & 2 & 2 & 2 & 2 \\
0 & 1 & 0 & 2 & 2 & 0 & 1 & 3 & 0 & 0 & 3 & 3 & 3 & 2 \\
1 & 0 & 1 & 0 & 2 & 0 & 2 & 3 & 3 & 1 & 0 & 3 & 3 & 2 \\
1 & 0 & 2 & 0 & 2 & 0 & 2 & 3 & 3 & 2 & 0 & 3 & 3 & 2 \\
0 & 2 & 3 & 2 & 2 & 0 & 2 & 3 & 3 & 3 & 0 & 3 & 3 & 2 \\
2 & 1 & 0 & 3 & 3 & 0 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 3 \\
1 & 0 & 1 & 0 & 3 & 0 & 1 & 0 & 0 & 1 & 0 & 0 & 0 & 3 \\
1 & 0 & 2 & 0 & 3 & 0 & 1 & 0 & 0 & 2 & 0 & 0 & 0 & 3 \\
1 & 2 & 3 & 0 & 3 & 0 & 1 & 0 & 0 & 3 & 0 & 0 & 0 & 3 \\
2 & 1 & 0 & 3 & 3 & 0 & 1 & 1 & 0 & 0 & 3 & 1 & 3 & 3 \\
1 & 0 & 1 & 0 & 3 & 0 & 0 & 1 & 1 & 1 & 0 & 1 & 3 & 3 \\
1 & 0 & 2 & 0 & 3 & 0 & 0 & 1 & 2 & 2 & 0 & 1 & 3 & 3 \\
1 & 2 & 3 & 0 & 3 & 0 & 2 & 1 & 3 & 3 & 0 & 1 & 3 & 3 \\
2 & 1 & 0 & 3 & 3 & 0 & 1 & 2 & 0 & 0 & 0 & 2 & 0 & 3 \\
1 & 0 & 1 & 0 & 3 & 0 & 0 & 2 & 2 & 1 & 0 & 2 & 0 & 3 \\
1 & 0 & 2 & 0 & 3 & 0 & 0 & 2 & 2 & 2 & 0 & 2 & 0 & 3 \\
1 & 2 & 3 & 0 & 3 & 0 & 1 & 2 & 0 & 3 & 0 & 2 & 0 & 3 \\
2 & 1 & 0 & 3 & 3 & 0 & 1 & 3 & 0 & 0 & 3 & 3 & 3 & 3 \\
1 & 0 & 1 & 0 & 3 & 0 & 2 & 3 & 3 & 1 & 0 & 3 & 3 & 3 \\
1 & 0 & 2 & 0 & 3 & 0 & 2 & 3 & 3 & 2 & 0 & 3 & 3 & 3 \\
1 & 2 & 3 & 0 & 3 & 0 & 2 & 3 & 3 & 3 & 0 & 3 & 3 & 3 \\
\hline
\end{array}$
{{qed}}
{{proofread}}
Category:Formal Semantics
32tklfxkcd1r531ranwvte2j2xp73pw