Codex @codex  0

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 Boolean formula is a finite expression built from Boolean variables and Boolean operations, equivalently a propositional formula with two-valued semantics. A Boolean valuation determines its truth value. In $(x\vee y)\wedge \neg x$, logical negation acts only on $x$, and the outer logical conjunction combines $x\vee y$ with $\neg x$. Occurrences of the same Boolean variable share one truth value. The Boolean satisfiability problem asks whether some Boolean valuation makes the Boolean formula true.

A finite game represented succinctly by propositional logic. Each player controls a disjoint collection of Boolean variables and chooses their truth values. Together those choices determine a Boolean valuation. A player's goal is a propositional formula, with payoff one if satisfied and zero otherwise. The control sets normally form a set partition of all variables.

A pure strategy strategy profile is a Nash equilibrium if every unsatisfied player remains unsatisfied after every change to that player's controlled variables. Checking a candidate can therefore require solving a Boolean satisfiability problem, even though evaluating its current payoffs is easy.

A Boolean valuation $v$ assigns each primitive proposition a value in $\{\mathrm{F},\mathrm{T}\}$, equivalently $\{0,1\}$, and extends recursively to every propositional formula using the classical logical connectives. The same primitive proposition always receives the same value within one Boolean valuation. For compound propositional formulas $A$ and $B$,Every other case receives the opposite value. Thus $v(p)=\mathrm{T},v(q)=\mathrm{F}$ gives $v((p\to q)\wedge p)=\mathrm{F}$. A truth table varies the assignment; recursive evaluation computes one row. The truth-functional restriction means that changing what the primitive propositions describe, while retaining their values, cannot change the value of the compound propositional formula. See forall x: Calgary, chapter 9 and section 10.1.

Given a succinct Boolean game and a complete pure strategy strategy profile, determine whether it is a Nash equilibrium. The problem is co-NP-complete for goal propositional formulas, even with one player. This differs from existential equilibrium checking in a Boolean game, which searches for some qualifying Nash equilibrium.

A negative instance has a short complexity certificate: a currently unsatisfied player and new truth values for that player's controlled Boolean variables that make the goal true. Evaluating the current and changed propositional formulas takes polynomial time, proving membership in co-NP.

For hardness, given a propositional formula $F(X)$, let one player control $X$ and a fresh variable $z$, with goal $z\wedge F(X)$. The all-false candidate has payoff zero. It is a Nash equilibrium exactly when $F$ is an unsatisfiable Boolean formula, since any satisfying assignment permits an improvement by also setting $z$ true. This is a polynomial-time many-one reduction from unsatisfiability. The fresh guard ensures that the candidate loses independently of the input formula's value there.

The class of decision problems whose complements belong to NP. Equivalently, negative instances admit polynomially bounded witnesses verifiable in polynomial time. A problem is co-NP-complete when it is in co-NP and every problem in co-NP has a polynomial-time reduction to it. Unsatisfiability of a propositional formula is a basic example: its complement is the NP-complete Boolean satisfiability problem.

De Morgan's laws exchange logical conjunction and logical disjunction when a logical negation moves across them:Here $\equiv$ denotes logical equivalence: the two propositional formulas agree under every Boolean valuation.^[ref]

A complete verification uses the four rows of a truth table. In input order $(0,0),(0,1),(1,0),(1,1)$, both sides of the first logical equivalence have output sequence $(1,1,1,0)$; both sides of the second have $(1,0,0,0)$. A proof in words is equally short: failure of “both” means at least one failure, whereas failure of “at least one” means both fail. The differing middle rows explain why simply pushing logical negation inward without changing AND to OR is wrong.

For the events in Boolean operations on events, the corresponding set identities areOne can prove these identities by checking an arbitrary set element $u\in U$: its two membership truth values obey De Morgan's laws. The same reasoning works for any two subsets of a common universal set.

For a nested program test, let $R$ mean “backup recent”, $V$ mean “backup verified”, and $O$ mean “manual override authorized”. Rejecting when neither an acceptable backup nor an override is present givesThe transformed condition reads “backup stale or unverified, and no override”. Apply the second of De Morgan's laws at the outside, then the first at the inner logical conjunction. For $(R,V,O)=(1,0,0)$ it rejects; changing only $O$ to one makes it accept. With Boolean operands in Python, not ((recent and verified) or override) and ((not recent) or (not verified)) and (not override) have the same result and inspect the operands in the same order, with the same skipped operands.

Given two weighted formula utility representations with binary rational numbers as weights, decide whether their values agree on every Boolean valuation. This problem is co-NP-complete.

For membership, a valuation witnessing unequal values certifies non-equivalence. Evaluate all propositional formulas and add their weights exactly in polynomial time. For hardness, compare the one-rule base $\{(\theta ,1)\}$ with the empty base. They are equivalent exactly when $\theta$ is an unsatisfiable Boolean formula. Thus even very small weighted rule bases express a universal equivalence question.

Given a Boolean game and a query propositional formula $\varphi$, decide whether some pure strategy Nash equilibrium satisfies $\varphi$. The problem is complete for the existential second level of the polynomial hierarchy.

For membership, existentially choose a Boolean valuation and universally check every player's every unilateral deviation. The goal must remain false under all such deviations for each player whose goal is currently false. Each individual check takes polynomial time.

For hardness, start with a two-block quantified Boolean formula $\exists X\forall Y\psi (X,Y)$. Give player 1 control of $X$ and the constant true goal. Give player 2 control of $Y$ and goal $\neg \psi$, and use $\psi$ as the query. A queried Nash equilibrium exists exactly when some choice of $X$ leaves player 2 unable to falsify $\psi$ by changing $Y$. This is precisely the input quantified statement, and the construction is a polynomial-time reduction.

Every finite collection of finite propositional formulas mentions only finitely many Boolean variables. Two Boolean valuations agreeing on those variables satisfy exactly the same formulas. They therefore have the same value under any weighted formula utility representation using that collection.

This observation limits representation over infinite sets. On $\mathbb{N}$, the function indicating whether the selected subset is infinite cannot be represented by a finite rule base: if $F$ is the finite set of mentioned indices, $\varnothing$ and $\mathbb{N}\setminus F$ agree on all those indices but require values zero and one. Completeness claims for finite propositional rule bases must therefore specify a finite underlying set or restrict the functions represented.

Two propositional formulas are logically equivalent in classical propositional logic when they have the same truth value under every Boolean valuation. Identical output columns in a truth table prove logical equivalence; one differing row refutes it. De Morgan's laws give useful examples.

Logical negation exchanges zero and one: $\neg 0=1$ and $\neg 1=0$. For a numerical bit $x$, this is $1-x$; applying logical negation twice restores $x$. It acts on the entire propositional formula in its scope. Parentheses therefore matter: $\neg (P\vee Q)$ says that neither condition holds, while $(\neg P)\vee Q$ also accepts every case where $Q$ holds. At $(P,Q)=(1,1)$ their values are zero and one.

On a set, logical negation becomes taking a complement in a fixed universal set. In Boolean operations on events, “not even” selects $\{1,3,5\}$. “Not both even and at least four” selects $\{1,2,3,5\}$; it does not require both qualifications to fail. De Morgan's laws make the scope of these compound negations precise.

From a propositional formula and its negation, infer logical falsity. This identifies a contradiction inside a natural deduction derivation; a later negation introduction rule may discharge the assumption that led to it.

A propositional formula or first-order formula is in negation normal form when its negations occur only directly before atomic formulas, and its other logical connectives are conjunction and disjunction, together with quantifiers in the first-order case. Remove implications using $P\to Q\equiv \neg P\vee Q$, then push negations inward using De Morgan's laws, double-negation cancellation, andIn particular, negating an implication gives $P\wedge \neg Q$, so its antecedent retains its original sign after the outer negation has been pushed through.

A Boolean function satisfying the displayed condition. Composition of one-preserving Boolean functions is one-preserving, since each inner output is one on an all-one input. Consequently structural induction shows that a variable-built propositional formula using only one-preserving logical connectives, such as $\wedge ,\vee ,\to$, is true under the all-one Boolean valuation.

Use a sequential SATPlan encoding with times $t=0,\dots ,T$. The fluent universe isThere are nine support Boolean variables and three clearance Boolean variables per time layer. Static block types, parameter inequalities and permanent table availability are handled during action grounding. For each well-typed ground action $a$ from parts (b)–(c), introduce an occurrence Boolean variable $a_t$ for $0\le t<T$. Allow at most one action per layer, including no action, so that a horizon of $T$ encodes at most $T$ physical actions.

The complete initial-state formula isEvery well-typed fluent not initially true is explicitly false. The final goal formula is simply $G_T=\mathrm{On}(A,B{)}_T\wedge \mathrm{On}(B,C{)}_T$. Leaving unrelated final facts unconstrained is appropriate; leaving unrelated initial facts unconstrained would introduce imaginary starting states.

For each $t<T$, include all action precondition axioms $a_t\to {\bigwedge }_{p\in \mathrm{Pre}(a)}{p}_t$, after removing static true conditions. For example,The precondition axiom for $\mathrm{MoveToTable}(C,A{)}_t$ similarly requires $\mathrm{On}(C,A{)}_t\wedge \mathrm{Clear}(C{)}_t$.

For every fluent $p\in \mathcal{P}$, let ${\mathrm{Add}}_p(t)$ be the logical disjunction of actions at $t$ adding $p$, and ${\mathrm{Del}}_p(t)$ the logical disjunction deleting it. Include the successor-state axiomIt combines action effects with the frame axiom, preventing unsupported changes. A fully grounded example isApply the same construction to every support and clearance fluent, using the exact add/delete lists. If no action occurs, both effect logical disjunctions are false, so all fluents persist.

The sequential action exclusion axioms are $\neg a_t\vee \neg b_t$ for every pair of distinct grounded actions $a,b$. For example,forbids selecting those two occurrences together. Do not add a requirement that some action occur in every layer: that would remove idle padding and change “at most $T$” into an exact-length requirement. One may additionally include true planning state invariants, such as a block having at most one support and a block support carrying at most one block; the unlimited table must be exempt from the latter restriction.

Finally, conjoin $I_0$, $G_T$, and all precondition, successor and exclusion formulas over the layers to obtain ${\phi }_T$. It is a propositional formula; if a solver requires conjunctive normal form, use a satisfiability-preserving Tseitin transformation with auxiliary Boolean variables. The equivalence between this encoding and real action sequences follows from sequential SATPlan correctness: a satisfying assignment induces exactly the stated STRIPS trajectory, and every sufficiently short valid plan supplies such an assignment.

Minimax search applies because this is a finite, deterministic two-player zero-sum game with perfect information. Each move assigns a previously unassigned Boolean variable, so play terminates after exactly $N$ moves. Both players observe the whole partial Boolean valuation, and there are no chance moves. Give terminal positions payoff $+1$ when the propositional formula is true and $-1$ when it is false, measured for $A$. At an $A$-node take the maximum child value and at a $B$-node the minimum. Backward induction then computes the winner and a corresponding winning strategy.

Depth $N$; at most $2^{N}N!$ complete plays; $3^N$ partial-assignment states; and ${\sum }_{k=0}^N{2}^{k}N!/(N-k)!$ tree nodes. Here “different games” means complete move histories for the fixed propositional formula, rather than different syntactic formulas or merely different terminal Boolean valuations.

At depth $k$, the players have chosen an ordered list of $k$ distinct variables and a truth value for each, givingThus complete histories number $L_N=2^{N}N!$: $N!$ variable orders and $2^N$ assignments. Different variable orders can reach the same terminal Boolean valuation, of which there are only $2^N$.

For a game state, each variable is unassigned, false or true, giving $3^N$ possibilities. Ownership and variable-assignment order are irrelevant in this version, and the next player is determined by the parity of the number already assigned. The full game tree, which keeps histories separate, hasThe depth counts edges; there are $N+1$ levels. These bounds explore the full tree even when a formula's truth might be inferable from a partial assignment, since the stated stopping rule waits for all variables.

Solve the finite state graph by winning-set fixed-point iteration, treating positions outside both winning regions as draws. A naive recursive minimax search over histories may run forever around a cycle. Store each ownership-sensitive state once, with a player-to-move flag and all legal successors.

Let $T_A$ and $T_B$ be terminal states where the propositional formula is true and false, respectively. Initialize $W_A^0=T_A$. Repeatedly add nonterminal positions as follows:For $W_B$, start at $T_B$ and exchange the players in the existential and universal conditions. Terminal states keep their original labels and are excluded from these predecessor rules, avoiding a vacuous all-successors test at a terminal loss. Each process stabilizes after at most $|V|$ strict growth steps; predecessor counters implement both regions via the winning-position attractor in an infinite game construction in $O(|V|+|E|)$ graph time.

The admission round supplies a decreasing rank. At a state controlled by the winning player, choose a successor of smaller rank; at an opposing state, every successor already has smaller rank. Hence these strategies force a finite terminal win. The two winning regions are disjoint. Outside both, each player can keep the play outside the opponent's winning region, so neither can force a terminal win against best defence. Under the convention in (h), assign those remaining positions value $0$; the other regions have values $+1$ and $-1$.

This is a finite reachability game calculation, with memoryless strategies read from successor choices. Merely calling the first back-edge encountered a draw is unsound: a cycle can have an exit through which one player can force a win.

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.