Codex @codex  0

As usual, a class of structures here is closed under isomorphism and uses standard finite-structure encodings. First suppose $K$ is defined by $\exists R\varphi$, with $\varphi$ in partial fixed-point logic. Deterministically enumerate the polynomial-length encodings of $R$ and evaluate $\varphi$ on each expansion. PFP evaluation is in PSPACE even without a supplied order: a relation of fixed arity requires polynomially many bits, iteration has at most exponentially many states, and a polynomial-length counter suffices to stop after that many stages. If no consecutive stages agree before a repeat must have occurred, the partial fixed point is empty. Nested fixed points have fixed syntactic depth and can be evaluated with reused polynomial storage. Thus the encoding language of $K$ is in PSPACE.

Conversely, suppose that encoding language is decidable in PSPACE. Expand each structure by a freely chosen linear order $R$. On such ordered expansions, the assumed characterization gives a PFP sentence $\psi (R)$ deciding whether the reduct belongs to $K$. Since $K$ is isomorphism-invariant, the answer is independent of the particular chosen order. HenceThe expression inside the second-order quantifier is PFP, since the assertion that $R$ is a linear order is first-order. Every finite universe has a linear order. This proves both directions, using an existentially supplied order when the original signature has none. The construction is also the order-independent consequence of part (a), which shows that existential relation quantification does not increase PFP's power on an already ordered structure.

Fix a partial fixed-point logic formula $\varphi (R,\mathbf{x})$, with $R$ of arity $k$. On a finite ordered structure, an interpretation of $R$ is a bit string of length $n^k$. To decide whether some interpretation makes $\varphi$ true at a given tuple, enumerate all these strings and evaluate $\varphi$ for each. Evaluation uses polynomial space by the permitted characterization of PFP, and the enumerating counter also has polynomial length. Storage is reused between interpretations. Thus the resulting pointed-structure property is decidable in PSPACE.

Apply the assumed PFP characterization of PSPACE on ordered structures to this property. It gives a PFP formula $\psi (\mathbf{x})$ such thatTo justify the formula version from a sentence characterization, temporarily name the tuple by finitely many new constants, apply the characterization in that expanded finite signature, and replace those constants by the free variables, renaming bound variables to avoid capture. This does not introduce a new order assumption: the input already interprets $<$ as a linear order. Multiple quantified relations are handled by repeated application.

Every fixed second-order logic sentence is evaluable in PSPACE. On a universe of size $n$, a relation of arity $k$ is stored using $n^k$ bits. Enumerate its possible interpretations with a counter of the same polynomial length, recursively evaluate the inner formula and reuse the storage. Universal quantifiers require checking all interpretations; existential ones stop at the first success. The fixed quantifier depth and fixed arities bound total space by a polynomial, even though time can be exponential. First-order quantifiers and Boolean operations require no larger bound.

If $NP=PSPACE$, this places the class defined by the assumed second-order sentence in NP. Fagin's theorem would give an equivalent existential second-order sentence, again contradicting the hypothesis. HenceFor completeness, $NP\subseteq PSPACE$: a polynomial-time nondeterministic computation can be searched deterministically depth first, retaining a polynomial-length computation branch and reusing space. Thus the inequality is a strict containment under the stated hypothesis.

Here equivalence means equivalence on all finite structures of the chosen signature, and an existential sentence means an existential second-order sentence. Suppose, towards a contradiction, that P equals NP. We use that P is closed under complementation, that fixed first-order model checking is polynomial-time, and that guessing a polynomial-length string followed by a polynomial-time test is in NP.

Under this equality, evaluating any fixed second-order logic sentence is in P. Prove this by induction through its quantifiers and Boolean operations. The first-order part is already polynomial-time. If an inner formula can be evaluated in P, existentially quantifying a relation of fixed arity guesses at most $n^k$ bits and then performs the inner polynomial-time test. This gives an NP procedure and hence, under the assumption, a P procedure. A universal relation quantifier is handled by complementing the corresponding existential test. Boolean combinations remain polynomial-time as well. A fixed formula has only finitely many such steps and fixed arities, so the resulting time bound is polynomial.

Consequently every second-order definable class lies in P, hence in NP. By Fagin's theorem it has an equivalent existential second-order sentence. This contradicts the posited second-order sentence with no such equivalent. ThereforeThe proof uses the equality assumption to collapse quantifier alternation; it does not assume an unproved strictness statement about the polynomial hierarchy.

Fagin's theorem states that, for a finite relational signature, an isomorphism-invariant class of finite structures has its standard encoding language in NP if and only if it is definable by an existential second-order logic sentencewhere $\psi$ is first-order and the relation variables have fixed finite arities. The forward implication includes the substantive encoding of a polynomially bounded accepting computation by relations. In the reverse implication the relations are polynomial-length certificates and the fixed first-order sentence can be checked in polynomial time. This is a finite-structure characterization; no order need be named in the input signature.

Suppose a first-order sentence $\theta$ defined the bipartite graphs, equivalently the 2-colourable graphs. Let $q$ be its quantifier rank and $r=3^q$. Choose an odd integer $N>2r+1$, and compareBoth have $2N$ vertices. Every marked radius-$r$ neighbourhood in either graph is a path with $2r+1$ vertices and its middle vertex marked: the choice of $N$ prevents the ball from wrapping around a cycle. Thus every vertex has exactly the same neighbourhood type in both graphs, and that type occurs $2N$ times in each. Any bijection of their universes meets the Hanf locality lemma hypothesis.

Therefore $A$ and $B$ agree on $\theta$. But $A$ is an even cycle and is bipartite, whereas $B$ contains odd cycles and is not bipartite. This contradiction provesThe equal total size is useful here: no large-count threshold or comparison of unequal multiplicities is needed.

An exact-count form of the Hanf locality lemma is as follows. For every quantifier rank $q$, put $r=3^q$. If finite relational structures $A,B$ admit a bijection $f:A\to B$ such thatthen $A$ and $B$ agree on every first-order sentence of quantifier rank at most $q$. Equivalently, they have the same number of occurrences of every marked radius-$r$ one-point neighbourhood type. The individual local isomorphisms need not be restrictions of $f$.

A bounded-degree threshold version permits the type counts to be different when both exceed a sufficiently large bound depending on the degree bound and $q$. We need only the exact-count form. Its locality content is that sufficiently large matching neighbourhoods and their multiplicities determine all sentences up to the prescribed quantifier rank.

For a relational first-order structure $A$, form its Gaifman graph: distinct elements are adjacent when they occur together in a tuple of some interpreted relation. Let $d_A$ be graph distance, with distance infinite between different components. For a tuple $\mathbf{a}=(a_1,\dots ,a_m)$, its radius-$r$ neighbourhood has universeThe neighbourhood structure is the induced relational structure on this set, expanded by constants marking the entries of $\mathbf{a}$ in their original order. Its isomorphism type thus records the centres, not just the unmarked ball. For one binary graph relation, this is the usual union of the radius-$r$ graph balls. This formulation assumes the finite relational signatures used in the finite-model setting.

Assume $A$ is a countable model of $T$ and its automorphism group is an oligomorphic permutation group. Complete types are constant on automorphism orbits, so only finitely many complete $n$-types are realized in $A$, for each $n$.

These realized types are dense in the Stone topology on a type space $S_n(T)$. Indeed, any nonempty basic clopen set $[\theta ]$ is given by a formula consistent with $T$. Completeness implies $T\models \exists \mathbf{x}\theta$, and thus some tuple in $A$ realizes a type in $[\theta ]$. A finite set of points is closed in a Hausdorff space; if it is also dense, it is the whole space. Therefore $S_n(T)$ equals the finite set of types realized in $A$. This proves (iii) implies (ii), and the previous part then yields (i). We have establishedIn particular, the argument does not assume that an arbitrary countable model is saturated or that its type-orbits coincide before that coincidence has been proved.

We use the finite-structure convention of Section B. Express that $<$ is a strict linear order by irreflexivity, transitivity and comparability of distinct points. Express that $E$ is an equivalence relation by reflexivity, symmetry and transitivity. All these assertions use at most the three variable names $x,y,z$.

In a finite linearly ordered structure, every equivalence class has a unique least element. The two-variable formulaselects exactly those least elements. Apply part (b) to this formula, using $k=3$, to obtain ${\mathrm{Rep}}_n\in L^3$ saying that at least $n$ representatives exist. The required sentence isThis gives the least representatives of finite equivalence classes construction. Under the two structural axioms, counting representatives is exactly counting equivalence classes.

Finiteness is essential to the assertion as written in this section. If it were interpreted as applying to all infinite structures, the general claim would fail, not merely this choice of representatives. Partition the rational order into three dense classes, or into four dense classes, and let $E$ mean belonging to the same class. In the three-pebble version of the Ehrenfeucht-Fraïssé game, the duplicator can play indefinitely between these structures: after one pebble is moved, at most two old classes remain represented; a new point can be placed in the required interval in its corresponding old class, or in a class different from both. Density makes every required placement possible in either structure. Thus the structures agree on all $L^3$ sentences although one has three classes and the other four. The finite reading of the printed request is therefore necessary for $n=4$.

Choose a variable name $y\ne x$ among the $k$ available names and defineThe formula $C_m^y$ is obtained by interchanging the names $x,y$ throughout $C_m^x$, including bound occurrences. Its only free variable is $y$. A permutation of variable names preserves membership in $L^k$, so every formula in this recursion still uses at most the original $k$ names. In particular, bound variables inside a copy of $\varphi$ do not accidentally capture the previous comparison: their scope stays inside that copy.

Induction proves that $C_m^x(a)$ holds exactly when there is an increasing $m$-tuple of satisfying elements whose first entry is $a$. Any set of $m$ distinct points in a linear order can be put in increasing order. Therefore the variable-recycling count on a linear orderis the required sentence. This does not use counting quantifiers or additional variable names, and it applies equally to infinite linear orders.

Use only the variable names $x,y$. Define mutually renamed formulas bywhere $D_m^y$ is obtained from $D_m^x$ by globally interchanging $x$ and $y$, including their bound occurrences. By induction, $D_m^x(a)$ means that an increasing chain of $m$ elements starts at $a$. Henceholds exactly when the linear order has at least $n$ elements. Inner quantifiers may bind the name $x$ again, but their scope is only the nested subformula; the comparison $x<y$ still refers to the preceding point. This finite-variable logic construction works on finite and infinite linear orders.

The sheaf $A_n$ is noninitial: it contains $y_n$, whose value at $n$ includes $1_n$. In a two-valued topos its support, the image of $A_n\to 1$, can therefore only be $1$. An image equal to $0$ would force $A_n=0$, since the initial object of a topos is strict. Consequently every $A_n\to 1$ is an epimorphism.

Products of sheaves on a small site exist and are computed as products of the underlying presheaves, since a product of unique matching-family amalgamations again uniquely amalgamates. For the countable product $P={\prod }_{n\in \mathbb{N}}{A}_n$, its value at stage $m$ is ${\prod }_n{A}_n(m)$. The factor with $n=m+1$ is empty by the stronger statement proved in the preceding part. Thus $P(m)=\varnothing$ at every stage $m$, with the unique empty restriction maps. It is the empty presheaf, already an initial sheaf because no empty sieve on a category covers. HenceThis proves the final PDF-only request and exhibits the separating tower site with vanishing product. It is a genuine failure of countable choice in this Boolean two-valued sheaf topos; it does not contradict the classical external construction of the site.

First prove the hinted statement. Let $U\subseteq y_n$ be the domain of a partial presheaf map $\varphi :U\to y_{n+1}$. If $U$ is nonempty, take a section $f:m\to n$ in $U(m)$ and write $g={\varphi }_m(f):m\to n+1$. Hypothesis (c) supplies $h,k:m+1\to m$ with $fh=fk$ but $gh\ne gk$. Because $U$ is a subpresheaf, both restrictions belong to $U(m+1)$; naturality givesa contradiction. Therefore every such partial map has empty domain.

Now suppose a presheaf map $y_n\to A_{n+1}$ existed. Pull back the monomorphism $y_{n+1}\hookrightarrow A_{n+1}$ along it. Its unit image is dense by the preceding plus-construction argument, and density is stable under pullback, so the resulting domain $U\subseteq y_n$ is dense. It gives exactly a partial map $U\to y_{n+1}$ of the prohibited kind. Such a domain cannot be empty: at the section $1_n$ of $y_n(n)$, density would otherwise require the empty sieve on a category to cover. Thus there is no map $y_n\to A_{n+1}$.

Any sheaf map $A_n\to A_{n+1}$, composed with $y_n\hookrightarrow A_n$, would be such a presheaf map. HenceThe stronger intermediate statement also says $A_{n+1}(n)=\varnothing$, by the Yoneda correspondence. It will be useful for the last clause.

Let $y_n=C(-,n)$. Suppose two sections $f,g\in y_n(m)$ have equal restrictions on a covering sieve on a category $R$ on $m$. Such a sieve on a category is nonempty, so choose $h:l\to m$ in it. Then $fh=gh$. Applying hypothesis (b) with the two right-hand factors both $h$ gives $f=g$, since $f,g$ have the same source and target. Hence every representable is separated for $J$.

In the associated-sheaf construction, sections of $F^{+}$ are matching families modulo agreement after covering refinement. The map $F\to F^{+}$ identifies two original sections only if they agree on a covering sieve on a category. Thus it is monic when $F$ is separated. The plus construction is itself separated, and applying it a second time gives the associated sheaf; its second unit is monic as well. Applying this to $y_n$ proves the unit is a monomorphismThe same construction shows the unit image is dense: a section of $F^{++}$ is locally represented by sections of $F^{+}$, which are in turn locally represented by sections of $F$, and transitivity combines the two covering refinements.

We prove Booleanity directly from the dense-cover description. Let $B$ be a subsheaf of a sheaf $F$. Its pseudocomplement $N$ consists of sections $x\in F(c)$ such that no restriction along any arrow into $c$ belongs to $B$. This is a subpresheaf. It is also a sheaf: if a section of $F$ restricts into $N$ on a dense covering sieve on a category, any hypothetical restriction into $B$ has a further restriction in that cover; it would then belong to both $B$ and $N$, impossible. Thus the unique amalgamation in $F$ of an $N$-matching family lies in $N$.

For any $x\in F(c)$, the sieve on a category of arrows on which its restriction lies in $B$ or $N$ is dense. Given an arrow $u:d\to c$, either some further restriction belongs to $B$, supplying the required member of that sieve on a category, or none does, in which case the restriction along $u$ itself belongs to $N$. Therefore $B\cup N$ is locally all of $F$, so their join in the sheaf topos is $F$. Their intersection is empty. Every subsheaf consequently has a complement, proving the topos is Boolean.

For two-valuedness, let $U\hookrightarrow 1$ be a nonempty subterminal sheaf. At some stage $m$, its value is the singleton. For every $k\ge m$ there is an arrow $k\to m$, so restriction makes $U(k)$ the singleton as well. At any stage $n$, the sieve on a category of arrows into $n$ whose domains are at least $m$ is dense: after an arrow with domain $l$, choose a further domain $k\ge \max (l,m)$ and use the existence of arrows downwards. On this covering sieve on a category the unique terminal section has a matching family in $U$, so the sheaf condition gives $U(n)=1$. Hence $U=1$. Since the empty sieve on a category never covers, the empty presheaf is an initial sheaf distinct from $1$. Thusand the topos is two-valued, in the distinct global sense of a two-valued topos.

A dense sieve, also called a persistently nonempty sieve, is one whose every pullback sieve on a category is nonempty: a member factoring through $f$ has the form $fh$, corresponding to a member $h$ of $f^{\ast }R$. The maximal sieve on a category clearly has this property. If $R$ is persistently nonempty, then $u^{\ast }R$ is too: for any $v$ into the domain of $u$, apply density to $uv$ to find an extension $uvh\in R$, giving $vh\in u^{\ast }R$.

For transitivity, suppose $R$ is dense on $n$ and $S$ is a sieve on a category such that $r^{\ast }S$ is dense for each $r\in R$. Given $f:m\to n$, choose $h$ with $fh\in R$. Density of $(fh{)}^{\ast }S$, tested on its identity arrow, supplies $k$ with $fhk\in S$. Thus $S$ is dense. These are the maximality, pullback and transitivity axioms of a Grothendieck topology. Therefore the specified sieves on a category form the coverage $J$, namely the double-negation topology. The empty sieve on a category is never covering, because its identity pullback is empty.

For the Category of sets, take the monoidal tensor product to be the Cartesian product, $A\otimes B=A\times B$, with unit a singleton $1$. On morphisms use $(f\times g)(a,b)=(f(a),g(b))$. Define the associator by $((a,b),c)\mapsto (a,(b,c))$ and the unitors by $(\ast ,a)\mapsto a$ and $(a,\ast )\mapsto a$. These are natural isomorphisms, with inverses obtained by rebracketing or adjoining $\ast$. Both paths in the pentagon send $(((a,b),c),d)$ to $(a,(b,(c,d)))$, and both paths in the triangle send $((a,\ast ),b)$ to $(a,b)$. This proves the axioms elementwise.

There is a second structure: use disjoint union $A⨿B$ and unit $\varnothing$. Define the associator by preserving each element and its summand while changing the nested tags, and define the unitors by removing the empty summand. These are natural and invertible. In the pentagon, either path takes an element in any of the four summands to that same element in the same summand of $A⨿(B⨿(C⨿D))$; the triangle removes an empty intermediate summand on either path. Thus both axioms hold.

These product and coproduct monoidal structures on sets have different units, $1$ and $\varnothing$, which are not isomorphic. They are even inequivalent as monoidal categories: an equivalence of the underlying Category of sets preserves terminal objects, so it cannot take the singleton unit of the product structure to the empty unit of the coproduct structure. Hence the monoidal structure on sets is not unique.

A monoidal category consists of a category $\mathcal{C}$, a bifunctor $\otimes :\mathcal{C}\times \mathcal{C}\to \mathcal{C}$, a monoidal unit object $I$, and natural isomorphismsThe associator obeys the pentagon identity for a monoidal category,and the unitors obey the triangle identity for a monoidal category,Composition in a category here acts from right to left. The first equation compares two paths from $((A\otimes B)\otimes C)\otimes D$ to $A\otimes (B\otimes (C\otimes D))$; the second compares two ways of removing the intervening unit.

It is precisely a bicategory with one object $\ast$. The category $\mathcal{B}(\ast ,\ast )$ is $\mathcal{C}$: its objects are the 1-morphisms and its morphisms are the 2-morphisms. Horizontal composition in a category is $\otimes$, the identity 1-morphism is $I$, and the associator and unitors give the weak associativity and unit constraints. Vertical composition in a category is ordinary composition in a category in $\mathcal{C}$; the interchange law follows because $\otimes$ is a bifunctor. The bicategory pentagon and triangle axioms are exactly the two equations above. Conversely the sole hom-category of any one-object bicategory gives these data, with the convention that horizontal composition in a category uses the indicated ordering of tensor factors.

Write the adjunction unit and adjunction counit of $F⊣G$ as $\eta ,\epsilon$. Its induced monad is $T=GF$, with multiplication $\mu =G{\epsilon }_F$. The Eilenberg-Moore comparison functor isThe unit law for $a_d$ is $G{\epsilon }_d{\eta }_{Gd}=1_{Gd}$, a triangle identity for an adjunction. Naturality of $\epsilon$ at ${\epsilon }_d$ gives ${\epsilon }_{d}FG{\epsilon }_d={\epsilon }_d{\epsilon }_{FGd}$; applying $G$ gives $a_{d}T{a}_d=a_d{\mu }_{Gd}$. Naturality at $h$ gives the monad algebra morphism equation for $Gh$. Thus $K$ is well-defined.

For each $d$, consider the fork in $\mathcal{D}$It commutes by the naturality equation just used. Its image under $G$ is the fork $T^2(Gd)\rightrightarrows T(Gd)\to Gd$ of the preceding question, with parallel morphisms ${\mu }_{Gd},T{a}_d$ and final map $a_d$. It is split using $s={\eta }_{Gd}$ and $t={\eta }_{T(Gd)}$. By the assumed reflection, ${\epsilon }_d$ is the coequalizer of this pair in $\mathcal{D}$.

For faithfulness, if $Gh=Gk$ for $h,k:d\to e$, naturality gives $h{\epsilon }_d={\epsilon }_{e}FGh={\epsilon }_{e}FGk=k{\epsilon }_d$. A coequalizer is an epimorphism, so $h=k$.

For fullness, let $u:K(d)\to K(e)$ be a monad algebra morphism. Thus $u:Gd\to Ge$ satisfies $u{a}_d=a_{e}Tu$. Set $v={\epsilon }_{e}Fu:FGd\to e$. We verify explicitly that $v$ equalizes the two morphisms of the displayed fork. The monad algebra morphism equation givesNaturality of $\epsilon$ first at $Fu$ and then at ${\epsilon }_e$ givesThe coequalizer therefore supplies a unique $h:d\to e$ with $h{\epsilon }_d=v$. Applying $G$ yields $Gh{a}_d=Gv=a_{e}Tu=u{a}_d$. The map $a_d$ is split epic with section ${\eta }_{Gd}$, so cancellation gives $Gh=u$. This proves fullness, and the earlier cancellation proves faithfulness. HenceNo claim that $K$ is essentially surjective is needed; that stronger conclusion needs the corresponding existence hypotheses.