Compact Truth Table

Definition

Compact Truth Table

A compact truth table is a truth table method that tests a single target combination of truth values instead of enumerating all $2^n$ rows for $n$ atoms.

The target combination is the one the property rules out: all premises true and the conclusion false to test validity, the formula false to test whether it is a tautology. The method assigns the target values and propagates the values the connectives force, so only the atoms needed for that combination receive values.

Mechanism

Forcing and forking

The method alternates two moves:

1. Force. Wherever a connective’s truth table admits only one way to realise an already assigned value, record the forced values. Making $A\to B$ false, for instance, forces $A$ true and $B$ false.
2. Fork. If nothing is forced and unassigned atoms remain, choose one and try both values; a branch that contradicts itself is dead, a branch that finishes consistently is a witness.

The search therefore ends either with a contradiction on every branch — the target combination does not exist, so the property holds — or with one consistent assignment that realises it.

Order Independence

When forking, the choice of which unassigned atom to try first changes the size of the table but never the verdict: an assignment either exists or it does not, independently of the order in which it is found.

Example

Testing satisfiability

Test the satisfiability of

$$\neg ((p\to q)\wedge (p\wedge q\to r)\to (p\to r))$$

by trying to make it true. Writing $X$ for the inner implication:

1. $\neg X$ true forces $X$ false.
2. $X$ false forces its antecedent $(p\to q)\wedge (p\wedge q\to r)$ true and its consequent $(p\to r)$ false.
3. $(p\to r)$ false forces $p$ true and $r$ false.
4. $(p\wedge q\to r)$ true with $r$ false forces $p\wedge q$ false, hence $q$ false.
5. $(p\to q)$ true with $p$ true forces $q$ true — a contradiction.

The assumption of a satisfying assignment leads to a contradiction, so the formula is unsatisfiable. Only the atoms needed to force the contradiction received values; the full table’s $2^3=8$ rows were never written.