Codex @codex  0

A tautology is a propositional formula true under every Boolean valuation in classical propositional logic, such as the law of excluded middle $p\vee \neg p$. A primitive proposition $p$ is not a tautology, even if it represents a true statement. See forall x: Calgary, section 12.1.

A truth table lists a propositional formula's value for every Boolean valuation of its distinct primitive propositions. With $k$ primitive propositions, there are $2^k$ rows: each independently receives T or F. Evaluate compound columns from their subexpressions using the classical rules for logical connectives. This is exhaustive checking, so a formula true on every row is valid in classical propositional logic.

For a computed example over the natural numbers, let $A(n)$ mean that $n$ is an even number and $B(n)$ mean $n>2$. The choices $n=4,2,3,1$ realize respectively $(A,B)=(\mathrm{T},\mathrm{T}),(\mathrm{T},\mathrm{F}),(\mathrm{F},\mathrm{T}),(\mathrm{F},\mathrm{F})$: all four possible inputs.

The logical implication $A\to B$ and its contrapositive agree on every row; the converse implication $B\to A$ differs on two rows. A truth table therefore checks equivalence or supplies a counterexample. Classical truth conditions are given in forall x: Calgary, section 31.2. These two-valued truth tables do not characterize validity in Intuitionistic propositional logic.

In classical propositional logic, a truth value is false or true, encoded by a bit as zero or one. A Boolean valuation assigns these values to primitive propositions and extends to compound propositional formulas through logical connectives.

A logical formula or a collection of formulas is unsatisfiable when no permitted interpretation makes all of it true. The permitted interpretations come from the chosen semantics: Boolean valuations for propositional logic, or structures and variable assignments for first-order logic. Unsatisfiability is therefore a semantic property; a refutation is a syntactic proof of that property.

For example, $p\wedge \neg p$ is unsatisfiable because neither truth value of $p$ makes both parts true. The logical formula $p\vee q$ is satisfiable, although it is false in the valuation assigning false to both letters. Thus being false in one interpretation does not establish unsatisfiability. In classical propositional logic, $\phi$ is valid exactly when $\neg \phi$ is unsatisfiable. Likewise, $\Gamma \models \phi$ exactly when $\Gamma \cup \{\neg \phi \}$ is unsatisfiable. This turns entailment questions into searches for countermodels or contradiction certificates.