Codex @codex  0

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.

Under any Boolean valuation there are two possibilities. If $\neg (\psi \to \chi )$ is false, the outer logical implication is true by vacuous truth. If it is true, then $\psi \to \chi$ is false, which forces $\psi$ true and $\chi$ false. In that case $\neg \chi$ is true, so the outer logical implication is again true. These possibilities exhaust the truth values of its antecedent; therefore

For a standard classical propositional calculus, strong completeness statesTogether with soundness, this identifies semantic consequence with formal derivability. One proves the contrapositive by the maximal consistent set in propositional logic construction. If $\Gamma ⊬\varphi$, the set $\Gamma \cup \{\neg \varphi \}$ is propositionally consistent, by the deduction theorem for propositional logic and classical propositional reasoning. Extend it to a maximal consistent set in propositional logic $M$, deciding each logical formula in turn. At each stage at least one selection of $\theta$ or $\neg \theta$ preserves propositional consistency; a contradiction in the union would use only finitely many assumptions and hence already occur at a stage.

Define a Boolean valuation by $v(p_i)=1$ exactly when $p_i\in M$. Maximal consistency in propositional logic gives $\neg \theta \in M$ exactly when $\theta \notin M$, and $(\theta \to \eta )\in M$ exactly when either $\theta \notin M$ or $\eta \in M$. Structural induction on logical formulas therefore proves the maximal consistent set truth lemma $v(\theta )=1⟺\theta \in M$. Thus $v$ satisfies $\Gamma$ but falsifies $\varphi$, contradicting semantic entailment. The countable language here permits an enumeration of logical formulas; the corresponding general-language argument uses a well-ordering or a principle of maximality in a partially ordered set.

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:

A propositional type is a set $\Sigma$ of propositional formulas; a Boolean valuation realizes it if every member is true, and omits it if at least one member is false. A consistent propositional theory $T$ locally omits $\Sigma$ if every formula $\theta$ which implies all members of $\Sigma$ modulo $T$ is refutable modulo $T$. Equivalently, whenever $T\cup \{\theta \}$ is consistent, there is a $\sigma \in \Sigma$ for which $T\cup \{\theta ,\neg \sigma \}$ is consistent. For a consistent propositional type, this says that it is a nonprincipal propositional type.

The extended omitting types theorem for propositional logic says that if a consistent $T$ locally omits each of a countable family ${\Sigma }_0,{\Sigma }_1,\dots$, there is one Boolean valuation satisfying $T$ and omitting them all. It also works inside any prescribed finite condition consistent with $T$.

To prove it, start with such a condition ${\theta }_0$, taking $\top$ when none is prescribed. At stage $i$, choose ${\sigma }_i\in {\Sigma }_i$ such thatSuch a choice exists by local omission. More explicitly, failure would imply $T⊢{\theta }_i\to \sigma$ for every $\sigma \in {\Sigma }_i$, hence $T⊢\neg {\theta }_i$, contradicting the stage invariant. Every finite subset of $T\cup \{{\theta }_0\}\cup \{\neg {\sigma }_i:i\in \mathbb{N}\}$ lies inside a consistent stage. By the propositional compactness theorem and the completeness theorem for propositional logic, it has a Boolean valuation. That Boolean valuation satisfies $T$ and makes the selected member ${\sigma }_i$ of every type false. All types are therefore omitted simultaneously. No effective test for consistency is assumed, and the argument does not require the ambient propositional language to be countable. Only the family of omission requirements is countable.

Use the specified construction as a polynomial-time many-one reduction from 3-SAT. There are $2n+3m$ vertices and $n+6m$ edges: one edge per variable pair, three edges per clause triangle in a graph, and three occurrence edges per clause. Any vertex cover must take at least one vertex from every variable pair and at least two from every clause triangle. Therefore every cover has at least $n+2m$ vertices.

Given a satisfying Boolean valuation, include the vertex corresponding to the true Boolean literal in each variable pair. In each clause choose a true occurrence and omit its clause vertex, including the other two. Every variable edge and triangle edge is covered. An occurrence edge with an included clause endpoint is covered automatically; the only omitted occurrence vertex is joined to the included true-literal vertex. This is a vertex cover with exactly $n+2m$ vertices.

Conversely, a cover of that size must use exactly one vertex in each variable pair and exactly two in each triangle. Declare a variable true precisely when its positive-literal vertex is included. Each clause has one omitted vertex. Its occurrence edge forces the corresponding literal vertex into the cover, so that literal is true. Every clause is therefore satisfied. ThusThe construction and target size are polynomial in the input length. Since 3-SAT is NP-complete, the decision problem is NP-hard. The usual “at most $k$” version has the same equivalence here because $n+2m$ is an unavoidable lower bound. More generally, a cover with fewer than $k\le |V|$ vertices can be padded to exactly $k$. Verifying a proposed cover is polynomial, so the usual vertex-cover decision problem is also in NP and hence NP-complete.

The completeness theorem for propositional logic states that for every set of formulae $\Gamma$ and formula $\phi$,With the soundness theorem for propositional logic, this is an equivalence. It is also equivalent to saying that every consistent set of formulae has a model.

The usual countable proof lists all formulae and extends a consistent theory one formula at a time. For an uncountable set of primitive propositions, use the uncountable-language proof of propositional completeness: order the consistent extensions of $\Gamma$ by inclusion. The union of every chain is consistent, since a proof of a contradiction would use only finitely many assumptions and hence would already lie in one member of the chain. Zorn lemma gives a maximal consistent set in propositional logic $M$. Define a Boolean valuation by $v(p)=1$ exactly when $p\in M$. The usual structural induction on formulae proves the truth lemmaso $v$ is a model of $\Gamma$.

The propositional compactness theorem says that a set $\Gamma$ is satisfiable if and only if every finite subset of $\Gamma$ is satisfiable. Only the forward implication is immediate. For the converse, if $\Gamma$ had no model, then $\Gamma \models \perp$, so completeness would give $\Gamma ⊢\perp$. Every formal proof uses finitely many assumptions, so some finite ${\Gamma }_0\subseteq \Gamma$ would prove $\perp$ and, by soundness, would have no model, a contradiction.

The decidability theorem for propositional logic says that there is an algorithm deciding whether a propositional formula is a theorem. A formula contains only finitely many primitive propositions, even when the full language is uncountable. Its finite truth table decides whether it is valid, and completeness says that validity is equivalent to theoremhood.

Now let $(X,<)$ be the given partially ordered set. For every distinct $x,y\in X$, introduce propositions $p_{xy}$ and $q_{xy}$. Form a propositional theory $T$ containing the following clauses:

The first two families say that $p$ and $q$ encode strict total orders. The third makes both orders extend $<$, while the fourth makes them disagree on every incomparable pair.

Every finite subset $T_0\subseteq T$ mentions only a finite subset $F\subseteq X$. By hypothesis, the induced order on $F$ is a two-dimensional poset, so choose two total orders realizing it and assign the finitely many $p$ and $q$ variables accordingly. This satisfies $T_0$. Thus every finite subset of $T$ is satisfiable, and propositional compactness gives a model of all of $T$.

Define $x{<}_{1}y$ when $p_{xy}$ is true and $x{<}_{2}y$ when $q_{xy}$ is true. The clauses make ${<}_1$ and ${<}_2$ total orders on $X$. They both contain the original order, and their intersection contains no incomparable pair. Hencewhich proves the finite-local characterization of two-dimensional partially ordered sets.

The succinct input is the players' variable-control sets, their goal propositional formulas, and a complete candidate Boolean valuation; an exponentially expanded payoff matrix is not part of the input. This representation is essential to candidate equilibrium checking in a Boolean game.

For membership in co-NP, consider the complement: the candidate is not a Nash equilibrium. A complexity certificate consists of a player $i$ and an alternative Boolean valuation of that player's controlled Boolean variables. Evaluate the current goal and the goal after this unilateral deviation, keeping every other player's variables fixed. A profitable unilateral deviation exists precisely when the current goal is false and the new goal is true. The certificate has at most the number of input variables plus the player index, and both propositional formula evaluations take polynomial time. Thus the complement belongs to NP, and the original decision problem belongs to co-NP.

For hardness, start with a propositional formula $F(X)$ and introduce a fresh Boolean variable $z$. Construct a one-player Boolean game in which that player controls $X\cup \{z\}$ and has goalChoose the candidate pure strategy assigning every variable false. Its payoff is zero because $z$ is false, regardless of $F$. If $F$ has a satisfying assignment, changing $X$ to that assignment and $z$ to true is a profitable unilateral deviation. If $F$ is an unsatisfiable Boolean formula, no unilateral deviation can satisfy the goal. ThereforeThe construction increases the formula length by only a constant and writes a candidate of linear length, so it is a polynomial-time many-one reduction. Unsatisfiability is co-NP-complete; combining hardness and membership proves that candidate Nash equilibrium checking for Boolean games is co-NP-complete. If a convention requires at least two players, add a player controlling a fresh unused variable and having the always-true goal; this changes neither direction of the proof.

For the intended finite representation, put $m=|S|<\infty$. For each $T\subseteq S$, form the mintermA Boolean valuation satisfies ${\chi }_T$ exactly when its selected subset is $T$. Therefore the weighted formula utility representationrepresents $u$ exactly: at the Boolean valuation for $T$, only that minterm contributes, with weight $u(T)$. This proves completeness and the bound of $2^{|S|}$ rules simultaneously. Zero-weight rules may be omitted. The bound counts rules; writing each minterm also requires $O(m)$ symbols in Big O notation.

For the computational question, assume rule weights are rational numbers encoded in binary. This makes exact equality of sums a finite computational task. With this conventional encoding, equivalence of weighted formula utility representations is co-NP-complete.

For membership, the complement has a short witness: a Boolean valuation on the variables occurring in either rule base. Evaluate each propositional formula, sum the weights of satisfied rules, and accept the witness if the sums differ. Propositional formula evaluation takes polynomial time. Exact sums of binary rational numbers also have polynomially bounded bit lengths: the product of their denominators has bit length at most the sum of the input denominator lengths. Thus non-equivalence lies in NP, and equivalence lies in co-NP.

For hardness, take a Boolean satisfiability problem instance $\theta$ and constructThe first utility function is one at satisfying Boolean valuations and zero elsewhere, while the second is always zero. ConsequentlyThe unsatisfiable Boolean formula problem is co-NP-complete, as the complement of the NP-complete Boolean satisfiability problem. The construction is a polynomial-time reduction, proving hardness even with the single weight $1$.

Two qualifications matter in the literal wording. First, unrestricted real weights have no specified finite encoding, so a standard bit-complexity classification needs the encoding assumption above. Second, the problem says only that $S$ is nonempty. If infinite $S$ is allowed while rule bases remain finite, its completeness claim is false. For $S=\mathbb{N}$, take $u(T)=1$ when $T$ is infinite and $u(T)=0$ when $T$ is finite. A finite rule base mentions only a finite subset $F$ of the variables. The Boolean valuations for $\varnothing$ and $\mathbb{N}\setminus F$ agree on all those variables but have different required values. No such rule base represents this $u$. Thus the construction answers the intended finite-set question and identifies the missing hypothesis in the unrestricted statement.

The definition in this part uses a single Boolean valuation, so the relevant Nash equilibria are pure strategy equilibria of a Boolean game. Use its standard convention that the players' control sets form a set partition of the variables.

Membership follows from an existential choice of a strategy profile and a universal check of all unilateral deviations. Assign payoff one to satisfying a player's goal and zero otherwise. A strategy profile $\sigma$ is a Nash equilibrium precisely when, for every player $i$ and every alternative Boolean valuation ${\tau }_i$ of that player's variables,is true: either the goal is already satisfied or no deviation can satisfy it. Thus the requested property isThe strings encoding $\sigma$, $i$ and ${\tau }_i$ have polynomial length, and evaluating the bracketed propositional formulas takes polynomial time. Invalid encodings of a player index can simply be ignored by the test. This is the existential second level of the polynomial hierarchy, ${\Sigma }_2^{\mathrm{P}}$.

For hardness, reduce the canonical complete problem of deciding a two-block quantified Boolean formulaMake a two-player Boolean game: player 1 controls $X$ and has goal ${\gamma }_1=\top$; player 2 controls $Y$ and has goal ${\gamma }_2=\neg \psi$. Set the query formula to $\varphi =\psi$. The construction has size linear in the input formula.

If an assignment $x$ satisfies $\forall Y\psi (x,Y)$, combine it with any assignment $y$. Player 1 already satisfies its goal, and player 2 cannot satisfy $\neg \psi$ by any unilateral deviation. Thus $(x,y)$ is a Nash equilibrium satisfying the query.

Conversely, let $(x,y)$ be a Nash equilibrium satisfying $\psi$. Player 2 currently has payoff zero. If some alternative $y^{\prime }$ made $\psi (x,y^{\prime })$ false, that deviation would satisfy player 2's goal and increase its payoff to one. The Nash equilibrium condition therefore implies $\forall Y\psi (x,Y)$. This proves the required equivalence and the polynomial-time reduction.

Together, membership and hardness prove ${\Sigma }_2^{\mathrm{P}}$-completeness of existential equilibrium checking in a Boolean game. The reduction works with only two players and one constant goal.

The given logical implication is false exactly when $A=B$ and $C\ne D$. For every literal on $A,B,C,D$, there is such a false Boolean valuation making that literal true. For a prescribed value of $A$ or $B$, give the other the same value and choose $C\ne D$. For a prescribed value of $C$ or $D$, give the other the opposite value and choose $A=B$.

Consequently no literal implies the whole propositional formula: there is no one-literal implicant. If an equivalent disjunctive normal form contained a one-literal conjunction term $\ell$, then every Boolean valuation satisfying $\ell$ would satisfy that disjunctive normal form, contradicting its equivalence to the given propositional formula. This proves the claim. Even if auxiliary Boolean variables are allowed in the equivalent expression, a one-literal term on one of them fails too: fix any false Boolean valuation of the original four and set the auxiliary literal true. The word “conjunct” here refers to a conjunction term in the disjunctive normal form, not a factor in a conjunctive normal form.

Use structural induction on the propositional formula. The induction claim is that its truth value under the all-one Boolean valuation is one. A variable has this truth value by definition. For the induction step, suppose the immediate subformulas $\alpha ,\beta$ each have truth value one. ThenThese are all permitted construction cases. Thus every such propositional formula evaluates to one. Equivalently, the three logical connectives define one-preserving Boolean functions, and composition preserves this property. The variable-only base grammar matters: admitting a constant false formula would invalidate the claim.

Repeated use of $U\to V\equiv \neg U\vee V$ yieldsThis logical disjunction is false exactly when $A_2,\dots ,A_n$ are all true and $A_1$ is false. There is precisely one such Boolean valuation out of the $2^n$ assignments to the $n$ independent propositional variables. Thus the number of satisfying assignments is $2^n-1$. This is the satisfying-assignment count for nested implications; the implication brackets associate to the right here.

Interpret $x_1,\dots ,x_n$ as the bits of a binary number, with $x_1$ most significant. Construct a propositional formula saying that this number is strictly less than $k$. This gives a quadratic-size formula with prescribed model count.

For $0<k<2^n$, write $k=(b_1\cdots b_n{)}_2$. For each $i$ with $b_i=1$, define the conjunctionThe empty prefix for $i=1$ is omitted. Let ${\phi }_k={\bigvee }_{i:b_i=1}{T}_i$. A Boolean valuation satisfies $T_i$ exactly when its first difference from the binary representation of $k$ is at position $i$, changing a one of $k$ to a zero. All later bits are unrestricted. Hence these cases are disjoint and cover exactly the numbers $0,\dots ,k-1$.

Alternatively, counting the disjoint cases directly givesEach $T_i$ has length $O(i)$, including its logical connectives and parentheses; the total length is at most a constant multiple of ${\sum }_{i=1}^{n}i=O(n^2)$. The endpoints are ${\phi }_0=\perp$ and ${\phi }_{2^n}=\top$. If constants are unavailable and $n\ge 1$, use $x_1\wedge \neg x_1$ and $x_1\vee \neg x_1$ instead. Assignments are counted over all $n$ specified variables, including any absent from the formula. For $n=0$, the constants describe the two possible counts, zero and one. Thus the construction covers $0\le k\le 2^n$, including the endpoint zero despite the source's word “positive”.

For example, $n=4,k=11=(1011{)}_2$ gives the disjoint cases $0\ast \ast \ast$, $100\ast$ and $1010$, with $8+2+1=11$ satisfying assignments.

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.

Propositional logic studies reasoning with whole propositions represented by letters such as $p$ and $q$, and propositional formulas built from them using logical connectives. The classical two-valued, truth-functional presentation below assigns each primitive proposition either true or false: each compound value depends only on its component values. This is classical propositional logic; other systems, including Intuitionistic propositional logic, have different semantics and rules.

Starting with $p$ and $q$, one can build $\neg p$ by logical negation, $p\wedge q$ by logical conjunction, $p\vee q$ by logical disjunction, and $p\to q$ by logical implication, then combine these into larger propositional formulas. Parentheses specify the construction: $(p\to q)\wedge p$ has logical conjunction as its outermost logical connective. Primitive propositions have no internal structure in this language; a first-order formula can additionally describe objects and quantify over them. The formation rules are given in forall x: Calgary, chapter 6.

The following truth table shows the four basic logical connectives. Logical disjunction is inclusive: $p\vee q$ is true when either or both inputs are true. Classical logical implication has exactly the same values as $\neg p\vee q$; its only false row has $p$ true and $q$ false. These truth conditions are specified in forall x: Calgary, chapter 9.

Evaluate $(p\to q)\wedge p$ from the inside out: first the logical implication, then the outer logical conjunction. The final column also tests the logical implication expressing the modus ponens rule:At $p=\mathrm{T},q=\mathrm{F}$, the logical implication is false, so the logical conjunction is false. The abstract syntax tree below separates the construction of the propositional formula from the values propagated through it. Both occurrences of $p$ receive the same value from the Boolean valuation. With the opposite assignment $p=\mathrm{F},q=\mathrm{T}$, the logical implication is true but the logical conjunction is still false because its second input $p$ is false. Recursive evaluation and exhaustive truth tables are explained in forall x: Calgary, chapter 11.

The last column is always true: $((p\to q)\wedge p)\to q$ is a tautology. This expresses the logical validity of the modus ponens rule: whenever both premises $p\to q$ and $p$ are true, $q$ is true. It does not say the premises are true under every Boolean valuation; their logical conjunction is true only on the first row. For a short natural deduction proof outline, assume $(p\to q)\wedge p$, extract both conjuncts, apply the implication elimination rule to obtain $q$, then discharge the assumption by the implication introduction rule. See forall x: Calgary, sections 17.3–17.5.

Three tests answer different questions: Boolean satisfiability requires at least one true row, a tautology requires every row true, and a contradiction has every row false. Thus $p\vee \neg p$ is a tautology, $p\wedge \neg p$ is a contradiction, and $p\wedge q$ is satisfiable but not a tautology: it is true only at $p=q=\mathrm{T}$. See forall x: Calgary, sections 12.1–12.4.

Propositional logic is useful because an inference pattern can be checked once and reused for many choices of propositions. Its beauty is that a finite truth table completely settles classical truth-functional questions about a fixed propositional formula. But logical validity does not verify real atomic claims. If $p$ means “the switch is closed” and $q$ means “the lamp is lit”, a valid use of the modus ponens rule still requires establishing its premises about the apparatus; the truth table supplies neither an observation nor a causal explanation. See forall x: Calgary, chapter 2 and chapter 10.

A propositional theory is a set of propositional formulas, sometimes identified with its deductive closure. It is a consistent set of formulae when contradiction is not derivable from it. The completeness theorem for propositional logic identifies consistency with existence of a satisfying Boolean valuation.

A propositional type is a collection of propositional formulas to be jointly realized by a Boolean valuation. A valuation realizes it when every member is true and omits it when some member is false. For propositional omission arguments, the collection need not itself be consistent.

A propositional variable is an atomic symbol assigned a truth value by a Boolean valuation. A propositional formula is built from these symbols by logical connectives. The variables carry no quantifiers over individuals; their values may be chosen independently.