Propositional logic: Proving contingency without truthtable
How can one proof that a proposition is a contingency? With a truth table it is easy (show that there is at least 1 true and 1 false outcome).
But with rewriting propositions using logical equivalence laws this becomes a lot more difficult. Normally the tautology and the contradiction are easy since you have a simple final state. But with a contingency you could end up with a complex expression and in theory you could apply an infinite set of transformation steps and not making any progress.
So how can one detect that no further transformations should be applied?
$\endgroup$ 23 Answers
$\begingroup$The general theory of sequent calculus gives a way to prove directly that certain statements are not tautologies. To illustrate the method, I will present a variant of sequent calculus due to Roy Dyckhoff known as LJT.
In this system, the propositions are built up from a set of given atoms, truthhood $\top$, and falsity $\bot$ using $\rightarrow$, $\wedge$, $\vee$. Then $\lnot P \overset{def}{=} (P \rightarrow \bot)$ and $(P \leftrightarrow Q) \overset{def}{=} ((P \rightarrow Q) \wedge (Q \rightarrow P))$. In general, it works on provability statements like $p \vee q, p \rightarrow r, q \rightarrow s \vdash r \vee s$ where the elements to the left of $\vdash$ represent hypotheses and the proposition to the right of $\vdash$ represents a conclusion.
The proof formation rules of LJT are (in the following, $\Gamma$ will represent an arbitrary set of hypotheses, and it will be understood that the hypotheses can be arbitrarily reordered; and in each rule, the provability of the statement below the line follows from provability of all statements above the line):
Assumption: \begin{align*} \\ \hline P, \Gamma \vdash P \end{align*}
$\top$-intro: \begin{align*} \\ \hline \Gamma \vdash \top \end{align*}
$\bot$-elim: \begin{align*} \\ \hline \bot, \Gamma \vdash P \end{align*}
$\wedge$-intro: \begin{align*} \Gamma & \vdash P \\ \Gamma & \vdash Q \\ \hline \Gamma & \vdash P \wedge Q \end{align*}
$\wedge$-elim: \begin{align*} P, Q, \Gamma & \vdash R \\ \hline P \wedge Q, \Gamma & \vdash R \end{align*}
$\vee$-intro (L): \begin{align*} \Gamma & \vdash P \\ \hline \Gamma & \vdash P \vee Q \end{align*}
$\vee$-intro (R): \begin{align*} \Gamma & \vdash Q \\ \hline \Gamma & \vdash P \vee Q \end{align*}
$\vee$-elim: \begin{align*} P, \Gamma & \vdash R \\ Q, \Gamma & \vdash R \\ \hline P \vee Q, \Gamma & \vdash R \end{align*}
$\rightarrow$-intro: \begin{align*} P, \Gamma & \vdash Q \\ \hline \Gamma & \vdash P \rightarrow Q \end{align*}
$\top \rightarrow$-red: \begin{align*} P, \Gamma & \vdash Q \\ \hline \top \rightarrow P, \Gamma & \vdash Q \end{align*}
$\wedge \rightarrow$-red: \begin{align*} P \rightarrow (Q \rightarrow R), \Gamma & \vdash S \\ \hline (P \wedge Q) \rightarrow R, \Gamma & \vdash S \end{align*}
$\vee \rightarrow$-red: \begin{align*} P \rightarrow R, Q \rightarrow R, \Gamma & \vdash S \\ \hline (P \vee Q) \rightarrow R, \Gamma & \vdash S \end{align*}
$\rightarrow \rightarrow$-elim: \begin{align*} P, Q \rightarrow R, \Gamma & \vdash Q \\ R, \Gamma & \vdash S \\ \hline (P \rightarrow Q) \rightarrow R, \Gamma & \vdash S \end{align*}
$\rightarrow$-elim: \begin{align*} P, Q, \Gamma & \vdash R \\ \hline P, P \rightarrow Q, \Gamma & \vdash R. \end{align*}
Of these, the only really nontrivial rule is $\rightarrow \rightarrow$-elim. This corresponds to the argument: we want to try to prove $P \rightarrow Q$ to be able to apply the hypothesis $(P \rightarrow Q) \rightarrow R$ to conclude $R$. To do this, we start by $\rightarrow$-intro; but then, if we know that $P$ is true, then $(P \rightarrow Q) \rightarrow R$ is equivalent to $Q \rightarrow R$.
It turns out that LJT is sound and complete for intuitionistic propositional calculus. Moreover, in a search for a proof of any $\vdash$ statement in LJT, a mechanical search through all the possibilities always terminates along all branches of the search. (This is because there is a "measure" of the "complexity" of a $\vdash$ statement which decreases in each step of the search.) Therefore, for example, if the search for $\vdash P$ turns up empty, we know that the original $P$ is not an intuitionistic tautology.
If instead you want to prove some statement is not a classical tautology, then you can use the theorem: $P$ is a classical tautology if and only if $\lnot (\lnot P)$ is an intuitionistic tautology. (Note that this is only true for pure propositional calculus; if you allow quantifiers $\forall, \exists$ then more generally you need to use a Goedel double-negation embedding.) (There is also a variant LJT* which directly applies to classical propositional logic; however, I'm personally not as familiar with that variant.)
So, for example, to show that $p \vee \lnot q$ is not a classical tautology (where $p$ and $q$ are distinct atoms), we show that in LJT, $\vdash \lnot (\lnot (p \vee \lnot q))$ is false. So, suppose we had a proof of $\vdash \lnot (\lnot (p \vee \lnot q))$; then the only possible "outermost step" of the proof derivation tree is $\rightarrow$-intro, so we must have a proof of $$(p \vee \lnot q) \rightarrow \bot \vdash \bot.$$ (Remember that in the proof search, we are matching against the bottom lines of proof rules to find "simpler" $\vdash$ statements above the horizontal lines which will imply what we want.) From here, the only possible next outermost step is $\vee \rightarrow$-red, which means we would have a proof of $$p \rightarrow \bot, (q \rightarrow \bot) \rightarrow \bot \vdash \bot.$$ Then from there, the only possible third outermost step is $\rightarrow\rightarrow$-elim on $(q \rightarrow \bot) \rightarrow \bot$, which means we would have a proof of $$p \rightarrow \bot, q, \bot \rightarrow \bot \vdash \bot$$ as well as a proof of $$p \rightarrow \bot, \bot \vdash \bot.$$ Now in proving the first of these, there is no possible next inner step. Therefore, we conclude that $p \vee \lnot q$ is not a classical tautology.
Similarly, we can show that $\lnot (p \vee \lnot q)$ is not a classical tautology. (This could be abbreviated by using the fact that $\lnot \lnot \lnot P$ is equivalent to $\lnot P$ in intuitionistic propositional calculus.) Therefore, $p \vee \lnot q$ is a contingency in classical propositional calculus.
$\endgroup$ $\begingroup$Unfortunately proving that a Boolean expression is a contingency is NP-complete, so there really isn't a better method than truth tables in general. We can prove that it is NP-complete by a reduction to and from the Boolean satisfiability problem:
Determining if a Boolean expression is satisfiable can be reduced to plugging in arbitrary values into the expression. If it's true, we're done. If it's false, determine if it's a contingency.
The contingency problem can also be reduced to the satisfiability problem because one way of determining that a proposition is a contingency is to simply determine if the proposition and its negation are both satisfiable.
Since the Boolean satisfiability problem is NP-complete and it can be reduced to the contingency problem in polynomial time and vice-versa, the contingency problem is also NP-complete.
$\endgroup$ 6 $\begingroup$Pick a known sound and complete axiom set, let's call this set A, for propositional calculus. That ensures that any formula that gets joined to the system which is not a tautology will enable the derivation of a variable.
Now, contradictions take as axioms will also enable the derivation of a variable.
Thus, to show that a formula C is contingent without a truth-table, first join C to A. Show that a variable can get derived. Then join $\lnot$C to A. Show that a variable can get derived. And then you can concluded that C is contingent (and you can also concluded that $\lnot$C is contingent).
Example, due to Russell and Whitehead, {ANAppp, ANqApq, ANApqAqp, ANApAqrAqApr, ANANqrANApqApr} is a sound and complete axiom set under the rules of uniform substitution and {AN$\alpha$$\beta$, $\alpha$} $\vdash$ $\beta$. Embedding those axioms and those rules into a language appropriate for William McCune's Prover9 program we have:
-P(A(N(x), y)) | -P(x) | P(y).
P(A(N(A(x, x)), x)).
P(A(N(x), A(y, x))).
P(A(N(A(x, y)), A(y, x))).
P(A(N(A(x, A(y, z))), A(y, A(x, z)))).
P(A(N(A(N(x), y)), A(N(A(z, x)), A(z, y)))).
You can think of 'P' as meaning provable.
Thus, to show that ApNq is contingent, we first join ApNq to that axiom set. And very quickly Prover9 produces this:
% -------- Comments from original proof --------
% Proof 1 at 0.00 (+ 0.05) seconds.
% Length of proof is 8.
% Level of proof is 3.
% Maximum clause weight is 9.
% Given clauses 11.
1 P(x) # label(non_clause) # label(goal). [goal].
2 -P(A(N(x),y)) | -P(x) | P(y). [assumption].
5 P(A(N(A(x,y)),A(y,x))). [assumption].
8 P(A(x,N(y))). [assumption].
9 -P(c1). [deny(1)].
27 P(A(N(x),y)). [hyper(2,a,5,a,b,8,a)].
29 P(x). [hyper(2,a,27,a,b,27,a)].
30 $F. [resolve(29,a,9,a)].
Now we just need to do the same for NApNq. And also very quickly, Prover9 shows that a variable can get deduced:
% -------- Comments from original proof --------
% Proof 1 at 0.01 (+ 0.05) seconds.
% Length of proof is 10.
% Level of proof is 4.
% Maximum clause weight is 9.
% Given clauses 27.
1 P(x) # label(non_clause) # label(goal). [goal].
2 -P(A(N(x),y)) | -P(x) | P(y). [assumption].
4 P(A(N(x),A(y,x))). [assumption].
5 P(A(N(A(x,y)),A(y,x))). [assumption].
8 P(N(A(x,N(y)))). [assumption].
9 -P(c1). [deny(1)].
30 P(A(x,N(A(y,N(z))))). [hyper(2,a,4,a,b,8,a)].
113 P(A(N(A(x,N(y))),z)). [hyper(2,a,5,a,b,30,a)].
117 P(x). [hyper(2,a,113,a,b,113,a)].
118 $F. [resolve(117,a,9,a)].
Thus, we have shown that it would be inconsistent to join either ApNq or NApNq to the above axiom set. Consequently, neither NApNq nor ApNq can neither be a contradiction, nor a tautology. Therefore, ApNq is contingent.
$\endgroup$ 4
