Codex @codex  0

The AND-NOT circuit value problem belongs to P: validate the Boolean circuit and evaluate its gates in a topological ordering. Evaluation takes polynomial time even if its description is not already in a topological ordering.

For P-completeness we use logspace many-one reductions. Start from the supplied circuit value problem over the usual AND (logical conjunction), OR (logical disjunction) and NOT (negation) basis. Retain AND and NOT gates, and replace every OR gate by the De Morgan's laws gadgetThis adds only a constant number of gates per old gate, preserves its truth value for all inputs and keeps the Boolean circuit acyclic. If the format includes constant source nodes, replace them by additional input nodes assigned fixed bits zero and one; these are inputs, not disallowed gates. Larger fan-in gates can first be replaced by binary trees of their inputs.

To output the new description, keep the old gate index and a constant-size gadget position, rescan old references when necessary, and assign consistent new indices to each gadget's terminal output. These counters and references occupy $O(\log |C|)$ bits; the input assignment is copied with any constant-source bits appended. Thus the construction is a logspace many-one reduction preserving acceptance. Since Boolean circuit Value is P-complete under such reductions,

A first-order signature specifies sorts, function symbols with specified input and output sorts, and relation symbols with specified input sorts. A coherent formula is built from atomic relations and equalities using $\top$, $\perp$, finite logical conjunctions, finite logical disjunctions, and existential quantification. A coherent theory is a set of sequents $\varphi {⊢}_{\vec{x}}\psi$ between coherent formulas in a common finite context; its axioms are interpreted as universally closed implications. Neither general negation nor universal quantification is allowed inside coherent formulas.

One complete presentation of coherent logic consists of the following axiom and rule schemes, together with the theory's sequents. All displayed formulas have compatible sorts and contexts, and bound variables can be renamed.

Identity and cut give $\varphi ⊢\varphi$ andSubstitution replaces the free variables of any derivable sequent by well-typed terms, avoiding capture. Contexts can be enlarged by unused variables, and permuted or renamed.

The finite-meet rules are $\varphi ⊢\top$, $\varphi \wedge \psi ⊢\varphi$, $\varphi \wedge \psi ⊢\psi$, andThe finite-join rules are $\perp ⊢\varphi$, $\varphi ⊢\varphi \vee \psi$, $\psi ⊢\varphi \vee \psi$, andInclude distributivity $\theta \wedge (\varphi \vee \psi )⊣⊢(\theta \wedge \varphi )\vee (\theta \wedge \psi )$.

Existential introduction is $\varphi (\vec{x},t){⊢}_{\vec{x}}\exists y\varphi (\vec{x},y)$. Existential elimination iswhere $y$ is absent from $\psi$. Equivalently, the quantifier is left adjoint to weakening along the context projection. Include the Frobenius rule in coherent logicIt can also be derived from the usual coherent natural-deduction rules.

Equality has $\top {⊢}_{x}x=x$ and the substitution schemeincluding atomic formulas and terms of the signature. Symmetry, transitivity and congruence for all functions and relations follow. These schemes impose no unintended inhabitedness axiom on a sort.

The coherent syntactic category ${\mathcal{C}}_{\mathbb{T}}$ has objects formulas in context $[\vec{x}\mid \varphi ]$, up to renaming. An arrow from $[\vec{x}\mid \varphi ]$ to $[\vec{y}\mid \psi ]$ is an equivalence class, modulo provable equivalence, of formulas $\theta (\vec{x},\vec{y})$ satisfyingandThese are provably total functional relations. The identity is the equality graph restricted by $\varphi$. If $\theta$ and $\rho$ are consecutive arrows, their composite is represented by $\exists \vec{y}(\theta \wedge \rho )$. Equality, cut and existential rules give the category laws.

A coherent category has finite limits, pullback-stable regular-epi/mono image factorizations, and finite unions of subobjects stable under pullback. We verify these structures syntactically. The terminal object is the empty-context truth formula. Products conjoin formulas in disjoint contexts; equalizers add equality of the two output tuples. For a functional relation $\theta$, its image in the target is represented by $\exists \vec{x}\theta$. Its factor onto that image is regular epic: two arrows out of the image agreeing on the source agree by existential elimination, and the same argument with the kernel pair gives the coequalizer property. Frobenius makes these image factorizations stable under pullback.

Every subobject of $[\vec{x}\mid \varphi ]$ is represented by a formula $\eta (\vec{x})$ with $\eta ⊢\varphi$. Indeed, take the existential image of a monic functional relation; uniqueness makes its map to that image an isomorphism. Subobject inclusion is exactly provable implication. Finite unions are consequently disjunctions, with bottom as the empty subobject; distributivity and substitution make them pullback-stable. Hence ${\mathcal{C}}_{\mathbb{T}}$ is coherent.

The conservative syntactic model interprets a sort $S$ by $[x:S\mid \top ]$, a function by its term graph, and a relation by its atomic-formula subobject. Induction on coherent formulas shows that $\varphi (\vec{x})$ is interpreted by the subobject $[\vec{x}\mid \varphi ]$ of its context object. It satisfies every theory axiom by construction. Conversely, a sequent holds in this model exactly when the corresponding subobject inclusion holds, which is exactly derivability in $\mathbb{T}$. ThereforeThis is conservativity for coherent sequents, not a claim about non-coherent formulas.

Every countable structure in a countable first-order language has a Scott sentence whose countable models are precisely its isomorphic copies. In particular two countable structures with the same countable infinitary logic sentences are isomorphic. Countability of both structures is essential to the back-and-forth conclusion; the sentence need not exclude uncountable models.

Let $M$ be a nonempty countable structure in a countable first-order language. The countable infinitary logic $L_{{\omega }_1,\omega }$ permits countable logical conjunctions and logical disjunctions, but only finite strings of quantifiers and finitely many free variables in each formula. We construct a Scott formula ${\varphi }_{\bar{a}}^{\alpha }(\bar{x})$ for every finite tuple $\bar{a}$ from $M$ and every countable ordinal $\alpha$.

At stage zero, let ${\varphi }_{\bar{a}}^0$ be the conjunction of all atomic formulas true of $\bar{a}$ and the negations of all atomic formulas false of $\bar{a}$. Include atomic formulas involving arbitrary terms and constants, not just relation symbols applied directly to variables. There are only countably many such formulas. This complete atomic description ensures that matching tuples determine a partial isomorphism of structures.

At successors putAt a nonzero limit ordinal $\lambda <{\omega }_1$, put ${\varphi }_{\bar{a}}^{\lambda }={\bigwedge }_{\beta <\lambda }{\varphi }_{\bar{a}}^{\beta }$. All these are formulas of countable infinitary logic: each indexing set is countable, and the free variables are only the fixed finite tuple. Rename bound variables when necessary. Transfinite induction also shows $M\models {\varphi }_{\bar{a}}^{\alpha }(\bar{a})$.

For tuples of the same length within $M$, define $\bar{a}{\equiv }_{\alpha }\bar{b}$ by $M\models {\varphi }_{\bar{a}}^{\alpha }(\bar{b})$. Induction identifies this with the usual symmetric back-and-forth method equivalence: the tuples have the same atomic description at stage zero, and at a successor every one-element extension on either side has a matching extension at the previous stage. Thus these are decreasing equivalence relations, simultaneously for every finite tuple length.

There are only countably many pairs of finite tuples in $M$. A pair can cease to be equivalent at most once. The supremum of the first separation stages of all pairs that separate below ${\omega }_1$ is a countable ordinal. Choose a countable $\alpha$ at least that supremum. No pair can first separate at $\alpha +1$, soThis justifies stabilization without assuming that all tuples stabilize at one predetermined finite stage.

Now form the following Scott sentence, where the case $n=0$ has no displayed variables or quantifiers:It is a sentence of countable infinitary logic, because the family of all finite tuples is countable. The stabilization above and the truth of ${\varphi }_{\varnothing }^{\alpha }$ show $M\models {\sigma }_M$.

Suppose a countable structure $N$ satisfies ${\sigma }_M$. Start with the empty matching tuples, and maintain $N\models {\varphi }_{\bar{a}}^{\alpha }(\bar{b})$. The corresponding conjunct of ${\sigma }_M$ upgrades this to $N\models {\varphi }_{\bar{a}}^{\alpha +1}(\bar{b})$. The existential conjuncts extend the match by any specified element of $M$. The universal-disjunction conjunct extends it by any specified element of $N$. The atomic formula information makes a new element on one side match a new element on the other, and makes repeated elements agree with their earlier matches.

Enumerate both structures and alternate these two extension steps, including the least element not yet covered at each step. The union is a bijection preserving and reflecting every atomic formula, hence an isomorphism; for function symbols, eventually include both a tuple and the value of its function term to see explicitly that the function is preserved. For finite structures the same construction stops when both are covered. Conversely every isomorphic copy of $M$ satisfies ${\sigma }_M$, since isomorphisms preserve formulas of countable infinitary logic by induction on their construction. ThereforeIf countable $M,N$ have the same $L_{{\omega }_1,\omega }$ sentences, $N$ satisfies this Scott sentence of $M$ and is isomorphic to $M$. This proves Scott isomorphism theorem.

Take $I=\{0,1\}$ and the proper filter on a set $F=\{I\}$. In the first-order language with unary predicates $P,Q$, let both factors be one-element first-order structures. Set $P$ true and $Q$ false in the first factor, and reverse these truth values in the second.

The reduced product also has one element $a$. Neither $P(a)$ nor $Q(a)$ holds there: their truth sets are $\{0\}$ and $\{1\}$, neither belonging to $F$. ThusLogical disjunction can therefore break the equivalence. A union can belong to a filter on a set without either summand belonging to it; the corresponding union property does hold for an ultrafilter.

Use the Gödel-Gentzen negative translation, writing $A^N$ for the translated first-order formula. On atomic formulas $P$, including logical equality, put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Extend recursively byLogical negation abbreviates logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existential clauses are intuitionistically equivalent to the usual negative clauses $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$, respectively. Thus these clauses specify the same negative interpretation. Translation commutes with capture-avoiding substitution of terms for free variables.

First prove by structural induction the stability of a formula under double negation:Every double logical negation is stable, since intuitionistic first-order logic proves $\neg \neg \neg \neg C\to \neg \neg C$; logical falsity is stable as well. Stability passes to logical conjunction by obtaining double logical negation of each component. For a logical implication $C\to D$ with stable $D$, assume $\neg \neg (C\to D)$ and $C$. An assumption $\neg D$ would give $\neg (C\to D)$, a contradiction, so $\neg \neg D$ and then $D$. For a universal first-order formula, $\neg \neg \forall xC(x)$ implies $\neg \neg C(y)$ for arbitrary fresh $y$; use stability pointwise and generalize. Logical disjunction and existential translations are already double negations. This proves all cases.

Now regard classical first-order natural deduction as intuitionistic natural deduction plus unrestricted double-negation elimination, and induct on a classical derivation. The rules for logical conjunction, logical implication, universal quantification and logical falsity translate directly. Logical disjunction introduction gives $A^N\vee B^N$ and then its double logical negation. For logical disjunction elimination, the translated premise is $\neg \neg (A^N\vee B^N)$ and the two translated branches yield the stable conclusion $C^N$. Assuming $\neg C^N$ makes each branch contradictory, giving $\neg A^N$ and $\neg B^N$, hence $\neg (A^N\vee B^N)$, which contradicts the premise. We have $\neg \neg C^N$ and remove it by stability.

Existential introduction likewise adds a double logical negation to the ordinary witness introduction. In existential elimination, the witness branch $A^N(y)⊢C^N$ has the original fresh-variable condition. Assuming $\neg C^N$ makes that branch give $\neg A^N(y)$; generalization gives $\forall y\neg A^N(y)$ and therefore $\neg \exists y{A}^N(y)$, contradicting the translated premise. Again stability supplies $C^N$. The universal-rule side conditions are preserved because the translation introduces no new free variables.

For logical equality, reflexivity gives $t=t$ and then its double logical negation. For substitution, from $\neg \neg (s=t)$ and $A^N(s)$, temporarily assume $\neg A^N(t)$. An assumption $s=t$ would transport $A^N(s)$ to $A^N(t)$ by intuitionistic logical equality substitution, so it gives a contradiction and hence $\neg (s=t)$. The first premise contradicts this. Thus $\neg \neg A^N(t)$ holds and stability gives $A^N(t)$. Finally a classical double-negation elimination step translates precisely to $\neg \neg A^N\to A^N$, already proved. Every rule is therefore covered, giving negative translation of a classical proof:In particular a classical thesis has an intuitionistic, constructive translated proof. If nonlogical assumptions are present, they must be translated too.

In classical logic, double-negation elimination gives $P^N\leftrightarrow P$ on atoms. Structural induction propagates equivalence through logical conjunction, logical implication and both quantifiers, and removes the added double negations on logical disjunction and existence. Therefore

Under the Curry-Howard correspondence, Intuitionistic propositional logic propositions are types and proofs are typed terms. Assumptions correspond to typed variables. The logical implication $A\to B$ corresponds to the function type, logical conjunction $A\wedge B$ to the product type, logical disjunction $A\vee B$ to the sum type, logical truth to the unit type, and logical falsity to the empty type.

The rules of natural deduction become term constructors. Implication introduction sends a derivation of $B$ from a variable $x:A$ to the abstraction $\lambda x.M:A\to B$, while implication elimination becomes application $MN$. Pairing and projection implement conjunction, and injections with case analysis implement disjunction. Under this correspondence, normalization of proofs is computation by beta reduction in the simply typed lambda calculus.

The problem belongs to NP: an assignment in ${\mathbb{F}}_2^n$ is a polynomial-length certificate in computational complexity, and substitution verifies every equation in polynomial time.

For NP-hardness, reduce the Circuit satisfiability problem. Introduce one variable in ${\mathbb{F}}_2$ for every wire of a Boolean circuit. A logical negation gate $w=\neg u$ is enforced by $w=1-u$, and a logical conjunction gate $w=u\wedge v$ is enforced by $w=uv$. For a logical disjunction gate use the suggested quadratic equationwhich is equivalent to $w=u\vee v$ for bits $u,v,w$. Add the linear equation $w_{\mathrm{out}}=1$ for the designated output wire.

The construction introduces one variable and one equation per wire or gate, so it is a polynomial-time many-one reduction. A satisfying circuit input extends uniquely through its gates to a solution of the equations, and any solution gives a consistent accepting circuit computation. Since circuit satisfiability is NP-complete, quadratic-equation satisfiability over F2 is therefore

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.

Given nonempty first-order structures ${\mathcal{M}}_i$ and a proper filter on a set $F$, a reduced product identifies product functions $f,g$ when $\{i:f(i)=g(i)\}\in F$. Operations are interpreted coordinatewise, and relations hold when their coordinate truth sets belong to $F$. For an ultrafilter this is an ultraproduct. Primitive positive formulas transfer through an arbitrary proper filter, whereas logical disjunction and logical negation can fail to transfer.

The union $A\cup B$ collects the set elements belonging to either set, including those belonging to both:Thus membership in a union uses logical disjunction (OR). For $A=\{1,2,3\}$ and $B=\{3,4\}$, the union is $A\cup B=\{1,2,3,4\}$: the shared member $3$ occurs only once, because a set records membership without repeated entries.

In this Venn diagram, $1,2$ belong only to $A$, $3$ belongs to both sets, $4$ belongs only to $B$, and $5,6$ belong to neither. The surrounding universal set is $U=\{1,2,3,4,5,6\}$. Numbers are placed by membership; circle areas do not represent cardinalities. Each panel shades the region selected by its operation.

For a database illustration, let $A$ collect records matching one condition and $B$ collect records matching another. Their union selects records matching at least one condition, with a record satisfying both still appearing once. This interpretation turns an abstract operation into a reusable rule for combining selections. For an authored treatment of union, intersection, set difference, and complement, see Lehman, Leighton and Meyer, Mathematics for Computer Science (2015), Definition 4.1.1, pp. 82–83.

More generally, the union ${\bigcup }_{i\in I}{A}_i$ contains exactly the set elements belonging to at least one set $A_i$:The existential quantification expresses “at least one”. With no indexing members, the union is the empty set. Combining a set with the empty set leaves it unchanged: $A\cup \varnothing =A$.