Codex @codex  0

A propositional formula false on the all-true and all-false Boolean valuations has a disjunctive normal form in which every minterm contains a positive literal and a negative literal. Grouping the positive propositional variables into $C$ and the negated propositional variables into the negation of a logical disjunction $D$ writes each minterm as $\neg (C\to D)$. De Morgan's laws therefore give the negation of a logical conjunction of such logical implications. For a contradiction use $\neg (p\to p)$.

A formation rule specifies how well-formed expressions can be constructed from simpler expressions in a formal language. The formal grammar of propositional formulas has rules for propositional variables, negation and binary logical implication.

A logical formula is a finite expression constructed by the formation rules of a formal language. Propositional formulas combine propositional variables by logical connectives. First-order formulas additionally contain terms, atomic relations and quantifiers. A logical formula is a syntactic object; its truth is determined only after specifying a suitable interpretation and values for its free variables.

A logical variable is a symbol whose value is supplied by the semantics of a logical language. A propositional variable receives a truth value under a Boolean valuation. An individual variable of first-order logic receives an element of a structure under an assignment. These are different kinds of variable and should not be identified.

A modal formula is built from propositional variables and logical constants using Boolean connectives and modal operators, such as the box operator. In provability logic, arithmetic realization replaces propositional letters by arithmetic sentences and interprets a box as the corresponding arithmetic provability assertion. Modal validity, theoremhood and truth under a particular arithmetic realization are distinct notions.

Assume first that $\varphi$ is false on the all-true and all-false Boolean valuations. Use the truth-table normal form from part (ii). Every satisfying Boolean valuation on the finitely many propositional variables must have at least one true propositional variable and at least one false propositional variable. Its minterm therefore has the formwhere $C_s$ conjoins its true propositional variables and $D_s$ disjoins its false propositional variables; both lists are nonempty. This is equivalent to $\neg (C_s\to D_s)$. If the satisfying Boolean valuations are indexed by $1,\dots ,N$, De Morgan's laws givesIf there are no satisfying Boolean valuations, take $N=1$ and $C_1=D_1=p$: the result is $\neg (p\to p)$, again always false.

Conversely, on the all-true Boolean valuation every nonempty $D_i$ is true, so every $C_i\to D_i$ is true. On the all-false Boolean valuation every nonempty $C_i$ is false, so every logical implication is again true. Negating their logical conjunction gives false on both Boolean valuations. Logical equivalence transfers these values to $\varphi$. The usual nonempty meaning of logical conjunction and logical disjunction of propositional variables is used here; allowing empty $C_i$ or $D_i$ without qualification would destroy this converse.

Two propositional formulas are logically equivalent if every Boolean valuation gives them the same truth value. A disjunctive normal form is a logical disjunction of logical conjunctions of literals, with a literal being a propositional variable or its negation.

Let $p_1,\dots ,p_n$ include all propositional variables appearing in $\varphi$. For each Boolean valuation $s\in \{T,F{\}}^n$, putThe minterm $M_s$ is true exactly for Boolean valuations whose restrictions to these propositional variables are $s$. ConsequentlyIndeed, an Boolean valuation making $\varphi$ true makes its own minterm true, while a true minterm in the displayed logical disjunction certifies the truth of $\varphi$. There are only finitely many Boolean valuations, so this is a finite disjunctive normal form. If there are no satisfying Boolean valuations, use $p\wedge \neg p$ for any propositional variable $p$; this is a disjunctive normal form for falsity without needing an empty logical disjunction convention.

A Boolean valuation is an arbitrary function $v$ assigning one of the two truth values to each propositional variable. It extends uniquely to all propositional formulas by following the construction of the propositional formula:For logical implication, $\tilde{v}(A\to B)$ is false exactly when $\tilde{v}(A)$ is true and $\tilde{v}(B)$ is false; otherwise it is true. Here the operations on the right are Boolean operations on truth values. Structural recursion gives existence, and structural induction gives uniqueness: once the immediate subformulas have their values, the outer connective fixes the resulting value.

Start with the propositional variables as atomic symbols and close under the two formation operationsThe set of propositional formulas is the smallest set satisfying these conditions: every logical formula has a finite construction from logical variables by negation and logical implication, and no other strings qualify. In particular, parentheses belong to the binary logical implication formation rule; they cannot be added or removed arbitrarily. Each symbol $p_i$ is one token, regardless of how its index is printed.

Use structural induction on the formation of a propositional formula. A propositional variable has no parentheses. Applying negation to a logical formula adds no parentheses, so preserves equality of the two counts. If $\psi$ and $\chi$ each have equally many opening and closing parentheses, the formation of $(\psi \to \chi )$ adds one of each to their combined counts. Thus every propositional formula satisfiesThis is a necessary condition for being a logical formula; it is not sufficient, since the logical connectives and the placement of symbols must also follow the formation rules.

A logical formula. Both $p_1$ and $p_2$ are propositional variables, so $(p_1\to p_2)$ and $(p_2\to p_1)$ are logical formulas. Applying the binary logical implication formation rule to this ordered pair of logical formulas gives the displayed whole expression. This supplies a construction of its formula syntax tree rather than merely checking that its parentheses balance.

The unique readability theorem says that every propositional formula has exactly one of the following forms: a unique propositional variable; $\neg \psi$ for a unique logical formula $\psi$; or $(\psi \to \chi )$ for a unique ordered pair of logical formulas $(\psi ,\chi )$. These three alternatives are disjoint. Consequently each logical formula has a unique formula syntax tree and a uniquely determined principal logical connective whenever it is not a logical variable.

A propositional variable $p_i$ is a single symbol of the alphabet. Its only nonempty substring is that symbol itself. Every propositional formula is nonempty, so the only substring that is a logical formula is $p_i$. ThereforeThe subscript is part of the name of an atomic token; it does not introduce additional symbol positions inside the logical variable.

A collection of logical connectives is functionally complete, or adequate, if every Boolean function of finitely many propositional variables is represented by a logical formula using only those logical connectives. More explicitly, for every $n\ge 1$ and every $F:\{0,1{\}}^n\to \{0,1\}$ there is a logical formula $\theta (p_1,\dots ,p_n)$ whose truth value under each Boolean valuation is $F(v(p_1),\dots ,v(p_n))$. Constant functions with Boolean values may use an otherwise irrelevant logical variable, for example $p\to p$ for truth and $\neg (p\to p)$ for falsity.

Translate logical formulas recursively, leaving propositional variables unchanged and translating negation by applying negation to the translation. For the other two logical connectives setThe first logical implication is false exactly when both original inputs are false; the second displayed logical formula is true exactly when both inputs are true. Hence each clause preserves truth values. Structural induction gives $v(T(\theta ))=v(\theta )$ for every Boolean valuation and every logical formula $\theta$ in the larger language.

By the assumed functional completeness of negation, logical conjunction and logical disjunction, any finite Boolean function has such a logical formula $\theta$. Its translation $T(\theta )$ uses only negation and logical implication and represents the same function. Thus $\{\neg ,\to \}$ is adequate.

A collection of logical connectives is adequate, or has functional completeness, if every Boolean function of finitely many propositional variables can be expressed by a formula using those connectives and variables, with the usual convention for nullary truth constants stated if those are included.

An adequate example is $\boxed{\{\neg ,\to \}}$. An inadequate example is $\boxed{\{\to \}}$: formulas using logical implication alone preserve truth when every input is true, so cannot express negation. These examples concern truth functions, rather than mere syntactic formation of formulas.

Only one logical implication of the printed equivalence is justified:The new system's first axiom is an old axiom, its replacement axiom is derivable in the old system by part (iii), modus ponens rule is shared, and its deduction rule is admissible in the old system by the theorem allowed in the source. Induction on a new-system derivation therefore translates it into an old-system derivation with the same assumptions.

The reverse logical implication is false for the displayed systems. Take $\Gamma =\varnothing$ and let $\varphi$ be an instance of the old contraposition axiom, for example with distinct propositional variables in place of $\alpha ,\beta$. It is an old-system theorem, but the matrix countermodel in part (ii) refutes its derivability in the new system. Thus the requested two-way equivalence cannot be concluded from these printed axioms.

A conjunctive normal form is a finite conjunction of clauses, each clause being a finite disjunction of literals. A literal is a propositional variable or the negation of one. Thus its shape isA single clause or single literal is allowed; the necessary parentheses can be inserted according to the grammar.

Assign to each propositional formula its finite symbol length. The set of lengths of formulas logically equivalent to $\alpha$ is a nonempty subset of the natural numbers, because it contains the length of $\alpha$. The well-ordering principle for the natural numbers gives a least such length, and hence a shortest equivalent formula.

A shortest equivalent formula need not be unique. For example $(p_0\to p_0)$ and $(p_0\leftrightarrow p_0)$ are distinct tautologies of the same minimal length. A shorter formula would contain no binary connective and hence be a variable with some number of negations, which is not a tautology. This counts each propositional variable as one symbol, as in the stated language, and proves that a shortest equivalent formula need not be unique.

Logical equivalence means that the two propositional formulas receive the same truth value under every Boolean valuation of the propositional variables. Equivalently, $\alpha \leftrightarrow \beta$ is a tautology: