Propositional formula

A propositional formula is built from atomic propositions using logical connectives. Unlike a first-order formula, it has no quantifiers over individuals. A Boolean valuation interprets its atoms as truth values and evaluates its connectives recursively.

A subformula is a constituent propositional formula in a formula's recursive construction, including the whole formula itself. For an atomic variable the only subformula is itself; for $\neg A$, add $\neg A$ to the subformulas of $A$; for a binary connective, add the combined formula to the union of the two operands' subformulas. The set of distinct subformulas can have smaller cardinality than the number of occurrences in the abstract syntax tree when the same expression appears more than once.

Every propositional formula generated by a parenthesized grammar has equally many opening and closing parentheses. By structural induction, atomic formulas begin with equal zero counts; negation preserves them; and a parenthesized binary logical connective adds its two subformula counts and one parenthesis of each kind. An optional paired-parenthesis construction also adds one to both counts. This necessary syntactic invariant is useful for checking generated expressions, though equal counts alone do not guarantee correctly nested syntax.

A propositional substitution maps each atomic propositional variable to a propositional formula and extends recursively through every logical connective. Replacements are simultaneous: a variable appearing inside a replacement formula is not replaced again in the same substitution step. Since propositional logic has no variable-binding quantifiers, this operation has no variable-capture problem.

A conjunction containing each of a specified finite collection of Boolean variables exactly once, either positively or negated. It is satisfied by exactly one Boolean valuation of those variables. The minterms for all valuations are mutually exclusive and collectively exhaustive, so they can encode an arbitrary finite table of values.

The displayed identity follows by testing the two possible truth values of $p$. Existentially forgetting $p$ gives $A[p:=\top ]\vee A[p:=\perp ]$. Repeating this operation produces a propositional formula on a specified remaining vocabulary. Logical truth constants are needed if that vocabulary is empty.

If $A⊢B$, eliminate the letters private to $A$ byEvery assignment satisfying $A$ satisfies one disjunct of $C$. If an assignment satisfies $C$, change only the eliminated letters to its witnessing assignment. The modified assignment satisfies $A$ and hence $B$, whose letters were unchanged. Thus $A\models C\models B$, and the propositional completeness theorem gives the two derivations. The interpolant uses only common letters; an empty common vocabulary is handled by logical truth constants.