Codex @codex  0

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 propositional formula with two blocks of quantified Boolean variables. Determining the truth of an existential-then-universal instance is a canonical complete problem for the existential second level of the polynomial hierarchy, ${\Sigma }_2^{\mathrm{P}}$. For completeness one may restrict the matrix $\psi$ to a disjunction of terms with at most three literals. The order of the quantifiers matters: the assignment to $X$ must work for every assignment to $Y$.

A finite rule base pairs propositional formulas with weights and sums the weights of the formulas satisfied by a Boolean valuation. Over a finite set $S$, associate one Boolean variable to membership of each element. Any utility function $u:2^S\to \mathbb{R}$ is represented by giving each subset's minterm weight $u(T)$. Exactly one rule fires at each valuation, so at most $2^{|S|}$ rules suffice. This bound counts rules, not the symbols required to write all formulas.

For computational questions, the weight encoding matters. Binary rational numbers permit exact addition and comparison in polynomial time; unrestricted real constants do not specify an ordinary finite input encoding.