Codex @codex  0

Coherent logic uses atomic formulas and equality, finite logical conjunctions and logical disjunctions, truth, falsity and existential quantification. Sequents are universally interpreted in a finite variable context. Its categorical semantics is provided by coherent categories, where conjunction is intersection, disjunction is finite union and existential quantification is image.

A solution exists when at least one object satisfies all the stated conditions. In first-order logic, this is expressed by existential quantification. Uniqueness additionally requires that any two solutions are equal.

Existential quantification forms $\exists x\phi (x,\mathbf{y})$. In a first-order structure, it is true at an assignment to $\mathbf{y}$ when some domain element makes the instance true. In natural deduction, elimination uses a fresh variable for the hypothetical witness; that variable may not escape into the conclusion or the remaining undischarged assumptions.

Existence requires at least one witness, not exactly one. Over the natural numbers $\mathbb{N}=\{0,1,2,\dots \}$, $\exists m(m>5)$ is true: $m=6$ works, as do $7,8,\dots$. In intuitionistic first-order logic, a direct proof supplies a witness together with a proof of the corresponding instance; merely rejecting nonexistence is generally weaker.

Placing existential quantification before universal quantification requires a single witness that works throughout:This first-order sentence is false. For any proposed $m$, choose $n=m$: the required inequality becomes $m>m$. For example, $m=3$ works for $n=0,1,2$ but fails at $n=3$. No finite list of successful checks establishes universal quantification over the natural numbers.

An existential second-order logic sentence has the formwhere each $R_i$ is a second-order relation variable of fixed finite arity $k_i$ and $\phi$ is a first-order sentence over the input first-order signature expanded by the $R_i$. The first-order sentence may contain both universal quantification and existential quantification over individuals; only the outer quantification over second-order relation variables is required to be existential. Under full semantics for second-order logic, truth means that some expansion by witness relations satisfies $\phi$.

For a fixed existential second-order logic sentence on a domain of cardinality $n$, the witnesses need ${\sum }_{i=1}^m{n}^{k_i}$ membership bits. The arities and the number of witnesses are constants because the sentence is fixed. After guessing those bits, a verifier evaluates the fixed first-order sentence by enumerating assignments to its finitely many individual variables, taking polynomial time. In the second-order encoding of three-colorability, the three witnesses require $3n$ bits, and the edge constraints can be checked over at most $n^2$ ordered vertex pairs. This is the logical form of the NP principle that a positive answer has a short complexity certificate.

The fixed-sentence qualification matters: it is the input first-order structure that varies, rather than an arbitrarily large formula supplied with each input. Fagin's theorem states the converse as well: every isomorphism-invariant NP property of finite relational first-order structures has such a description. The coloring example uses only unary second-order relation variables; the general theorem allows any fixed finite arities.

Mathematical logic studies formal languages, formal proofs, model theory, computability theory, and the foundations of mathematics. It makes the rules of reasoning explicit enough that reasoning itself becomes an object of mathematics. Proof theory studies deductions; model theory studies interpretations in which statements hold.

Three questions organize the subject: is an expression a well-formed first-order formula, is it true in a specified first-order structure, and does it have a formal proof from specified axioms? These questions are distinct. For example, $\exists n(n+n=1)$ is a first-order sentence in an appropriate first-order language; it is false in the natural numbers but true in the rational numbers, with $n=1/2$.

The beauty of mathematical logic is that the same logical connectives and rules of universal quantification and existential quantification organize arguments across mathematics. Classical propositional logic uses two truth values; Intuitionistic propositional logic interprets logical implication through constructions on proofs, without unrestricted law of excluded middle. This proof-based framework is developed in Frank Pfenning, Natural Deduction, sections 1–3.

A nondeterministic finite automaton allows a set of possible destinations for each automaton state and input symbol. Without the extra moves permitted in an Epsilon-NFA, replace the DFA function by $\Delta :Q\times \Sigma \to \mathcal{P}(Q)$, where $\mathcal{P}(Q)$ is the power set. A word is accepted when at least one path consumes all its symbols and ends in an accepting automaton state. These choices express existential quantification, not probability: no chance of choosing a particular path is assigned. One successful path suffices even if other paths fail.

Consider a three-state NFA accepting exactly the words of binary digits ending in $01$. Its initial automaton state $q_0$ loops on both $0$ and $1$; it also has an automaton transition $q_0\stackrel{0}{\to }{q}_1$, followed by $q_1\stackrel{1}{\to }{q}_2$. Only $q_2$ is accepting, and all unlisted automaton transitions are absent. Staying at $q_0$ skips an arbitrary beginning; leaving it guesses that the current zero starts the final two symbols.

The word $01$ accepts along $q_0\to q_1\to q_2$. The word $1101$ accepts along $q_0\to q_0\to q_0\to q_1\to q_2$. The word $010$ rejects: a path reaching $q_2$ after $01$ cannot consume the remaining zero, while the other paths end outside $q_2$. Thus finding $01$ somewhere is insufficient; it must occur at the end.

To simulate the NFA deterministically, retain the set $S$ of all currently possible automaton states. The powerset construction updates $S$ by taking the union of the destinations of its members. Here only $\{q_0\}$, $\{q_0,q_1\}$, and $\{q_0,q_2\}$ are reachable, although the full power set has eight members. Reading $010$ gives $\{q_0\}\to \{q_0,q_1\}\to \{q_0,q_2\}\to \{q_0,q_1\}$, which rejects. In general, an $N$-state NFA yields a DFA with at most $2^N$ automaton states. Nondeterminism can simplify a description, while the powerset construction keeps the memory finite.

The second generator checks all 511 words of up to eight binary digits against the direct test of whether their final two symbols are $01$. Exactly 127 accept, and only the three listed sets of automaton states occur. In particular, the empty word rejects for this NFA.

Michael O. Rabin and Dana Scott's 1959 paper studied finite-state machines as recognizers with finite internal memory. Its section 5 defines NFAs through successful paths, and theorem 11 proves their equivalence to DFAs by the powerset construction. This gives a historical source for the distinction between many possible paths and greater recognition power: ^[ref].

Forcing constructs new first-order models while controlling which ground-model properties survive. Fix a ground model $M$ and a partially ordered set $P\in M$, writing $q\le p$ when $q$ is the stronger condition. A generic filter is upward closed, directed towards stronger conditions, and meets every ground-model dense subset of a forcing order. If $M$ is externally a countable transitive model, enumerate its dense subsets and successively choose stronger conditions in them. The resulting filter is $M$-generic. External countability is crucial: this is not a claim that the ground model regards its own universe as countable.

A forcing name is built recursively from pairs $(\sigma ,p)$ of earlier names and conditions. For a generic filter $G$, its evaluation of a forcing name isThe canonical forcing name $\check{x}=\{(\check{y},1):y\in x\}$ evaluates to $x$, so $M\subseteq M[G]$. Recursive evaluation also proves transitivity. Name ranks bound the ranks of their evaluations, so an ordinal in the extension is below some ground ordinal and is already a ground ordinal. Thus forcing preserves ordinals.

The central link between syntax and generic interpretation is the forcing theorem. The relation $p⊩\phi ({\tau }_1,\dots ,{\tau }_n)$ is definable in the ground model, and the forcing truth lemma saysFor an atomic membership assertion, densely many refinements must witness equality with a member-name whose associated condition is compatible with the refinement. Equality is obtained by recursive mutual inclusion of names. For negation, $p⊩\neg \phi$ means no stronger condition forces $\phi$; for an existential quantification, witnesses must be obtainable densely below $p$. Induction on name rank establishes the atomic clauses, and induction on formulas establishes definability and the truth lemma. The generic filter meets the relevant dense sets at the existential step. An arbitrary semantic assertion about one chosen generic filter is insufficient: the definable relation must work uniformly for all generic interpretations.

This explains preservation of ZFC. Extensionality and foundation follow from transitivity; canonical names supply infinity. Pair and union names give pairing and union. For separation, restrict a name's members to conditions forcing the defining formula. For replacement, the definable forcing relation lets ground axiom schema of collection bound a set of names for all possible witnesses to the unique outputs; evaluating their collected name gives the range. For power set, let $\tau$ name the given set and let $D$ be the set of its member-names. Every subset of ${\tau }_G$ has an equivalent name drawn from $\mathcal{P}(D\times P)$, by the truth lemma, so a ground set of candidate names collects all its subsets. Finally choose a ground well-order of the relevant names; its evaluated image surjects onto the desired set, and choosing the first name for each value well-orders that set. This is why ordinary forcing over a choice model preserves choice.

For a concrete example, Cohen forcing consists of finite partial functions $\omega \to 2$, ordered by extension. The generic union $c=\bigcup G$ is total because deciding each coordinate is dense. For every ground real $x$, the set of conditions disagreeing with $x$ somewhere is dense, so $c\ne x$. This construction changes the universe by adding a genuinely new real without changing its ordinals.

The size and compatibility of conditions determine what else changes. With the countable chain condition for forcing, an ordinal-valued name has only countably many possible values at each coordinate: take a maximal antichain deciding that value. Therefore the possible range of a name for a map with infinite ground domain of cardinality $\mu$ lies in a ground set of size at most $\mu \cdot {\aleph }_0=\mu$. This prevents cardinal collapse and changes of uncountable regular cofinalities. Forcing by finite partial functions $\lambda \times \omega \to 2$ is ccc: the delta-system lemma thins any uncountable family of finite domains to a delta-system, and a further thinning makes their values agree on its finite root. Two remaining conditions are compatible. Distinct coordinates add distinct reals.

For example, start with GCH and take $\lambda ={\aleph }_2$. This forcing has size $\lambda$ and adds $\lambda$ distinct reals. A nice name for a real uses countably many antichains, and each antichain is countable. The ground arithmetic ${\lambda }^{{\aleph }_0}=\lambda$ bounds the number of such names by $\lambda$. Hencegiving a relative-consistency example of the failure of CH. The ground choice of GCH is available through the constructible universe; no claim that every starting model has this arithmetic is needed.

By contrast, countably closed forcing adds no new countable sequences of ground ordinals. Given a name, recursively strengthen a condition to decide each coordinate, then take a lower bound of the descending sequence. That condition decides the entire sequence. Closure and chain conditions thus control different features; neither should be silently substituted for the other.

Further applications include changing cofinalities, adding branches through trees, and constructing prescribed continuum patterns. If the aim is to violate choice, an ordinary generic extension of a choice model will not do: one restricts to a suitable symmetric collection of names, checking the axioms again. These examples also mark a limitation: forcing proves relative consistency, not absolute consistency of the background theory. The countable-transitive-model picture gives a concrete semantic construction; the definable forcing relation and Boolean-valued formulation supply the corresponding formal consistency arguments without asserting that a transitive ground model can be proved to exist.

An ultraproduct converts coordinatewise finite information into a single first-order structure. Let $(M_i{)}_{i\in I}$ be nonempty structures in a common first-order language, and let $U$ be an ultrafilter on $I$. In ${\prod }_i{M}_i$, setThe ultraproduct ${\prod }_i{M}_i/U$ has these equivalence classes as its elements. Functions are interpreted coordinatewise; a relation holds of classes exactly when it holds on a $U$-large set of indices. Intersecting finitely many large agreement sets shows that these interpretations are independent of representatives.

The Łoś theorem, which explains the construction's usefulness, saysHere is the proof. Induction on terms establishes the coordinatewise interpretation of atomic formulas. Finite intersections handle conjunction, and the ultrafilter property handles negation, since precisely one of a set and its complement is large. For an existential quantification, a witness class gives coordinate witnesses on a large set. Conversely, when the coordinate existential truth set is large, select a witness in each of those structures and a default element elsewhere. Its class is a witness in the ultraproduct. This uses choice. Structural induction on formulas now proves the theorem, with universal quantification obtained by negation.

Compactness. If every finite subset of a first-order theory $T$ has a model, take $I$ to be the finite subsets $\Gamma \subseteq T$ and choose $M_{\Gamma }\models \Gamma$. The cones $\{\Gamma :\Delta \subseteq \Gamma \}$ for finite $\Delta$ have the finite intersection property. Extend their filter to an ultrafilter by the ultrafilter lemma. For each $\phi \in T$, its cone is large, so the Łoś theorem makes the ultraproduct satisfy $\phi$. This proves the compactness theorem, including theories of arbitrary set size.

Elementary extensions and nonstandard elements. An ultrapower uses a fixed structure at every coordinate. The diagonal map sending $a$ to the class of the constant function $a$ is an elementary embedding by the Łoś theorem. For a nonprincipal ultrafilter on $\omega$, the class of $i\mapsto i$ in an ultrapower of the natural numbers exceeds every standard integer, because each corresponding tail is large. In an ultrapower of the real ordered field, the reciprocal of this element is positive and smaller than every positive standard reciprocal integer: an infinitesimal. These examples implement ordinary finite statements in a larger structure without claiming that every external subset or second-order assertion transfers.

Saturation. Such an ultraproduct over $\omega$ is countably saturated. To see the actual diagonal argument, list a finitely satisfiable type ${\phi }_0(x),{\phi }_1(x),\dots$ with parameters in the ultraproduct and fix representatives for those parameters. For each $n$, the set $E_n$ of coordinates admitting a simultaneous witness to its first $n$ formulas belongs to $U$ by the Łoś theorem. Arrange that the $E_n$ decrease and put $D_n=E_n\cap \{i:i\ge n\}$. The $D_n$ decrease, belong to $U$, and have empty intersection. At coordinate $i$, choose a witness to the first $m(i)$ formulas, where $m(i)$ is the largest $n$ with $i\in D_n$, or choose a default element if there is no such $n$. For each fixed $n$, $m(i)\ge n$ on the large set $D_n$. Therefore the resulting class realizes every formula. This proves countable saturation of an ultraproduct over omega; it does not assert saturation at all larger cardinalities.

Algebraic limits. Take finite fields ${\mathbb{F}}_p$ indexed by the primes and a nonprincipal ultrafilter. Their ultraproduct is a field of characteristic zero: for every fixed positive integer $n$, only finitely many primes divide $n$, so $n\cdot 1\ne 0$ on a large set. Every first-order sentence true in all finite fields holds in this infinite field, and more generally so does any sentence true for all but finitely many of the factors. This is a way to create an infinite field retaining uniform first-order information from finite fields. It does not make the field algebraically closed: the first-order sentence that every element is a square already fails in infinitely many of the factors.

Large cardinals. A countably complete ultrafilter gives a well-founded membership ultrapower of the universe. If it had an infinite descending chain represented by $f_n$, each setwould be large. Countable completeness makes ${\bigcap }_n{A}_n$ nonempty, giving an actual infinite membership descent at any index in the intersection, contrary to foundation. The Mostowski collapse therefore gives a transitive target and an ultrapower embedding $j:V\to M$.

For a measure on a measurable cardinal $\kappa$, every function $\kappa \to \alpha$ with $\alpha <\kappa$ is constant on a large set: otherwise intersect the fewer than $\kappa$ complements of all its fibres. Consequently $j$ fixes the ordinals below $\kappa$. The class of the identity function is below $j(\kappa )$ and above every constant class below $\kappa$, since all tails are large. Thus $j(\kappa )>\kappa$ and its critical point is $\kappa$. Fine ultrafilters on $P_{\kappa }(\lambda )$ that are normal ultrafilters on small subsets and kappa-complete yield the stronger embeddings witnessing supercompact cardinals.

These applications share a single principle: an ultraproduct preserves precisely the first-order information seen by its ultrafilter. Principal ultrafilters merely select a factor; nonprincipal ones can produce new sizes, elements and saturation. Existence of the needed ultrafilters and selection of coordinate witnesses are set-theoretic assumptions, and changing the ultrafilter may change the resulting model.

A Cartesian theory has a many-sorted first-order signature, with finite arities, and axioms expressed as sequents between Cartesian formulas. Those formulas use atomic relations and equality, truth and finite logical conjunctions. They also admit existential quantification when the quantified witness is provably unique: to form $\exists y\varphi (x,y)$, require $\varphi (x,y)\wedge \varphi (x,y^{\prime })⊢y=y^{\prime }$ relative to the theory. One can quantify a finite tuple in the same way. Arbitrary existential quantifiers, disjunction, negation and universal quantifiers are not formula constructors in this fragment. In particular falsity is not included as an additional finite-limit constructor. The universal force of a sequent comes from its free-variable context. This is the fragment whose categorical semantics requires exactly finite limits.

The Cartesian syntactic category ${\mathcal{C}}_{\mathbb{T}}$ has objects $\{\vec{x}\mid \varphi \}$, identifying harmless renamings and provably equivalent formulas-in-context. An arrow from $\{\vec{x}\mid \varphi \}$ to $\{\vec{y}\mid \psi \}$ is represented by a provably functional Cartesian relation $\theta (\vec{x},\vec{y})$: it entails $\varphi \wedge \psi$, is total on $\varphi$, and has a unique output tuple. Provable equivalence identifies arrows. Equality supplies identity arrows; composition quantifies the uniquely determined intermediate tuple in a conjunction. Totality and uniqueness prove that the composite is again functional.

The empty truth context is terminal. Products concatenate disjoint contexts and conjoin their formulas. A pullback of two functional relations adds the condition that their outputs agree; the common output is unique, so the existential quantification used to express it is Cartesian. This gives all finite limits and makes the usual equality diagrams into equalizers.

An internal model $M$ in a finite-limit category $\mathcal{E}$ interprets each sort by an object, functions by arrows and relations by subobjects. Equality is a diagonal and conjunction is a pullback intersection. A uniquely witnessed relation projects monomorphically onto the context, so its existential interpretation needs no general image operation: it is that mono. Evaluating formulas and functional relations yields a finite-limit-preserving functor $F_M:{\mathcal{C}}_{\mathbb{T}}\to \mathcal{E}$.

Conversely, the canonical syntactic model uses the single-sort truth contexts, term graphs and atomic subobjects. Its interpretation of a formula is the formula-in-context object itself. Applying any finite-limit-preserving functor supplies a model and preserves its axioms. These constructions are inverse up to the natural interpretation isomorphisms; model homomorphisms correspond to natural transformations. Therefore

For completeness, let a sequent in context be represented by subobjects $i:A\hookrightarrow C$ and $j:B\hookrightarrow C$ for its antecedent and consequent. Derivability is exactly the existence of a factorization $i=jv$ in the syntactic category. Consider the covariant representable functor ${\mathcal{C}}_{\mathbb{T}}(A,-)$, which preserves all existing limits, and hence corresponds to a set-valued model. In that model the element $i\in {\mathcal{C}}_{\mathbb{T}}(A,C)$ belongs to the antecedent, because it is the image of $1_A$. If the sequent holds, it also belongs to the consequent, so $i=jv$ for some $v:A\to B$. That is precisely a derivation of the sequent. Thus validity in all set-valued models implies Cartesian derivability. More concretely, every underivable sequent is refuted by this representable model. No assumption that every sort is inhabited is needed: some hom-sets may be empty.

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.

Let $R={\prod }_i{\mathcal{M}}_i/F$ be the reduced product by a proper filter on a set. Its underlying equivalence relation is $f\sim g$ when $\{i:f(i)=g(i)\}\in F$. Operations are interpreted coordinatewise, and a relation holds of the classes exactly when its coordinate truth set belongs to $F$.

Evaluation of a first-order term commutes with passage to the quotient, by mathematical induction on terms. Consequently the desired equivalence holds for every atomic formula, including logical equality. For a formula $\theta$ and representatives $\bar{f}$, write $S_{\theta }=\{i:{\mathcal{M}}_i\models \theta (\bar{f}(i))\}$.

For logical conjunction, $S_{\theta \wedge \psi }=S_{\theta }\cap S_{\psi }$. The filter on a set axioms giveThus the induction hypothesis transfers a conjunction in both directions.

For existential quantification, first suppose $R\models \exists y\theta (y,[\bar{f}])$. Choose a representative $g$ of a witness. Induction gives $S_{\theta (g,\bar{f})}\in F$, and this set is contained in $S_{\exists y\theta }$. Upward closure therefore gives $S_{\exists y\theta }\in F$.

Conversely, suppose $A=S_{\exists y\theta }\in F$. For each $i\in A$, choose a coordinate witness $g(i)$, and choose an arbitrary element of $M_i$ outside $A$. These simultaneous choices use the axiom of choice, as does the usual product construction. Then $A\subseteq S_{\theta (g,\bar{f})}$, so that truth set belongs to $F$. Induction gives $R\models \theta ([g],[\bar{f}])$, providing the required witness. Thereforefor every primitive positive formula. The exam's tame formulas are exactly this fragment, built using logical conjunction and existential quantification. No ultrafilter dichotomy was used.

The printed expression has one unmatched closing parenthesis. Remove that final surplus parenthesis and read the first disjunct as $\exists xP(x)$; the other disjunct has outer universal quantification over the displayed implication. To distinguish the two independent bound uses of $x$, rename the first to $u$.

Push the outer negation through the logical disjunction and through the quantifiers. Negating the implication preserves its existential antecedent and negates its consequent. Applying De Morgan's laws and the quantifier negation rules gives the negation normal formEach negation is now directly before an atomic formula. No bound variable has been captured, and no original existential quantification in the antecedent has accidentally been negated twice.

A primitive positive formula is generated from atomic formulas using only logical conjunction and existential quantification. It can be put in the form $\exists \bar{y}{\bigwedge }_j{\theta }_j(\bar{x},\bar{y})$ with each ${\theta }_j$ atomic. The exam terminology tame formula refers to this fragment. Its reduced product transfer needs only filter intersection and upward closure, together with coordinatewise choices of witnesses.

A quantifier binds a free variable in a first-order formula and specifies how its truth depends on elements of a first-order structure: universal quantification $\forall$ requires every element, while existential quantification $\exists$ requires at least one.

Second-order logic extends first-order logic by allowing existential quantification and universal quantification over second-order relation variables, as well as over individual objects. In the relational presentation used here, an individual variable $x$ ranges over a domain $D$, while a second-order relation variable $R$ of arity $k$ denotes a subset of $D^k$. Unary second-order relation variables denote subsets of $D$; binary ones denote binary relations. Presentations with function variables can instead describe their graphs by second-order relation variables, with first-order formulas requiring a unique output for every input.

For a graph with vertices $D$ and fixed graph adjacency $E$, the first-order sentence $\forall x\exists yE(x,y)$ says that every vertex has a neighbour. It selects individual vertices while $E$ retains its given interpretation. By contrast,selects an entire subset $P$ and says that it is a nonempty independent set. Here $P$ is a unary second-order relation variable, rather than a symbol in the input first-order signature. This particular property also has a simple first-order sentence on simple graphs; the example illustrates the change in what can be selected, rather than proving a separation in expressive power.

The usefulness of second-order logic is that one can describe a whole proposed solution, such as a graph coloring, and then impose local constraints on it. Syntax alone does not specify which proposed relations are available: full semantics for second-order logic permits all external subsets of $D^k$, whereas Henkin semantics supplies designated ranges. The second-order encoding of three-colorability makes this distinction concrete.

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$.

A sequence of functions $f_n:X\to Y$ converges uniformly to $f:X\to Y$, where $Y$ is a metric space with metric $d$, precisely whenFor real numbers, use the absolute value $d(u,v)=|u-v|$. Compare the universal quantification and existential quantification:The decisive change is whether $N$ can depend on $x$. Uniform convergence implies pointwise convergence.^[ref]

For functions taking values in real numbers on a nonempty domain of a function, the supremum error is $E_n={\sup }_{x\in X}|f_n(x)-f(x)|$, allowing $+\infty$. Then uniform convergence is equivalent to $E_n\to 0$. The supremum need not be a maximum: pointwise strict bounds below $\epsilon$ only give $E_n\le \epsilon$, so use tolerance $\epsilon /2$ when proving this equivalence. This single error bound controls every possible input, including one chosen after seeing the index.

For $f_n(x)=x^n$ and its pointwise limit on $[0,1]$, the error is zero at one but approaches one as $x\to 1$ from below. Consequentlyfor every positive integer $n$. This supremum is never attained: below one the error is $x^n<1$, and at one it is zero. Deleting the endpoint leaves the same supremum error on $[0,1)$. To disprove uniform convergence directly, choose $\epsilon =1/2$: for any proposed $N$, take $n=N$ and $x=2^{-1/N}<1$. The error equals $1/2$, violating the strict tolerance. Thus a moving input defeats every proposed common threshold.

On the smaller interval $[0,a]$, for a fixed $0\le a<1$, the pointwise limit is zero andFor $0<a<1$ and $0<\epsilon <1$, the exact first successful common threshold isThe logarithm and floor function turn an infinite approximation statement into a finite stopping rule. At $a=0.8$, $0.8^{20}=0.01152921504606846976$ fails tolerance $0.01$, while $0.8^{21}=0.009223372036854775808$ succeeds. At $a=1/2$ and $\epsilon =1/8$, the ratio is exactly three: $N=4$ is necessary because equality is insufficient. For $a=0$, every error is zero. The domain of a function determines whether one threshold can certify every input.

For another explicit stopping rule, let $h_n(x)=x/(n+1)$ on $[0,1]$. Its uniform limit is zero and its supremum error is $1/(n+1)$. For every $\epsilon >0$, $N=\max \{1,\lceil 1/\epsilon \rceil \}$ works, using the ceiling function. Unlike $x^n$ on $[0,1]$, it controls even the endpoint.

The practical beauty of uniform convergence is that one quantitative bound can survive further operations: the uniform limit theorem preserves continuity, and uniform convergence preserves integrals on a compact interval controls accumulated error. Differentiation needs additional hypotheses, such as uniform derivative convergence with an anchored value. These results distinguish an approximation that looks accurate at selected inputs from one that justifies replacing a whole function in a calculation.

Universal quantification forms $\forall x\phi (x,\mathbf{y})$. In a first-order structure, it is true at an assignment to $\mathbf{y}$ when every domain element assigned to $x$ makes the instance true. Its introduction rule requires that the generalized variable not occur freely in undischarged assumptions.

Over the natural numbers, reversing the preceding existential quantification and universal quantification gives a true first-order sentence:Choose $m=n+1$. The computed witnesses for $n=0,1,2,3$ are $m=1,2,3,4$. The choice may depend on the previously given $n$. The formula states that every natural number has a larger natural number; the reversed formula demands one larger than all of them.

The diagram displays a finite window, while the rules $m=n+1$ and $n=m$ settle the two statements for every natural number. This dependence is why quantifier order matters in precise specifications. Choosing one $m$ that works for every $n$ would also provide a witness for each $n$; the reverse inference fails here.

To introduce universal quantification in natural deduction, reason with an arbitrary input, without assuming a special property of it. The construction $m=n+1$ does exactly this and also gives a proof in intuitionistic first-order logic. The introduction and elimination rules for both quantifiers are developed in Frank Pfenning, First-Order Logic and Type Theory, section 4.1.