Codex @codex  0

Finite strict total orders and increasing injections, including the empty order, give a presheaf classifier for strict total orders. Trichotomy locally merges two finite sorted tuples, identifying equal entries. A strict map from a chain is injective, so parallel maps admitting the same realization are already equal. Reflexification gives a geometric morphism to the classifying topos of linear orders; pulling back weak totality gives exactly strict trichotomy.

Choose a strict total order $v_1<\cdots <v_n$ of the vertices of a finite simple graph. Direct every edge $v_i{v}_j$ from $v_i$ to $v_j$ when $i<j$. Along every directed path, the index strictly increases. Returning to the starting vertex would require an impossible strict increase back to the initial index, so this is an acyclic orientation. The displayed $D_1$ comes from $A<B<C$.

The chosen strict total order is a topological order of the resulting Directed acyclic graph. Conversely, every acyclic orientation of a finite simple graph has a topological order, and orienting its edges from earlier to later in that order recovers it. Different topological orders can induce the same acyclic orientation, since vertices with no edge between them need not impose a choice of arrow.^[ref]

An order respects reachability but does not create it: $u<v$ in a chosen topological order does not imply a directed path from $u$ to $v$. For example, orient the two edges of the graph path $A,B,C$ using $A<C<B$. The arrows are $A\to B$ and $C\to B$; there is no directed path from $A$ to $C$, despite $A<C$. In $D_1$, however, $A$ reaches $C$ both directly and via $B$. Following outgoing directed edges with graph search decides this directional reachability.^[ref]

Let $\mathbf{FinPos}$ be a small skeleton of finite partially ordered sets with all weak order-preserving functions, and let $\mathbf{FinSPos}$ consist of finite strict partial orders with all strict order-preserving functions. Include the empty structure, because no inhabitation axiom has been imposed. The two classifiers areThese are covariant functor categories, or presheaves on the opposite finite-model categories; reversing this variance would give the wrong generic models. In each case the generic carrier sends a finite model to its underlying set, with the generic relation given by its order at that stage. These are the classifying topos of partial orders and the classifying topos of strict partial orders.

We justify the finite-model presentations internally, so an identification of set-based model categories alone is not being mistaken for a classifying property. A finite weak-order presentation takes a finite graph of required inequalities, closes it transitively and reflexively, and identifies vertices in mutually reachable cycles; this produces a finite poset representing that positive diagram. For the strict theory, a transitive cycle makes the presentation contradictory by irreflexivity; otherwise transitive closure produces a finite strict poset. Homomorphisms from these presentations into any model are exactly the tuples satisfying the specified finite relations.

More explicitly, an internal model $M$ gives $F_M(P)=\mathrm{Hom}(P,M)$ on the opposite finite-model category. Its finite realizations form an internally filtered system. It is nonempty through the empty presentation. Two realizations combine through a disjoint-union presentation. To equalize parallel presentation maps whose composites in $M$ agree, quotient their target by the finitely many required identifications and close the relation transitively. In the weak case, collapse the resulting mutually comparable blocks; antisymmetry in $M$ guarantees that the realization factors through this quotient. In the strict case, either the quotient is a finite strict poset and gives the required factorization, or it has a cycle, making the supposed realization impossible. These constructions prove the flatness conditions without deciding equality of arbitrary elements of $M$.

Conversely a flat functor gives an internal filtered colimit of finite models with the indicated carrier and relation. Each finite axiom remains true under that filtered presentation. One-point presentations recover every element; two-point comparison presentations recover every relation; and finite identifications recover equality. These constructions are inverse: a realization of any finite diagram in the colimit factors locally through a finite stage, and two such realizations agreeing in the colimit agree after a further stage. Thus internal models in every Grothendieck topos correspond to flat functors on the opposite finite-model category. The presheaf case of the Diaconescu equivalence for geometric morphisms gives the displayed classifiers. This direct finite-presentation argument is the relevant safeguard in identifying presheaf classifiers; agreement of set-model categories by itself would not suffice, as emphasized in Research on theories of presheaf type.

The reflexification of a strict partial order interprets the weak theory byReflexivity is supplied by the equality disjunct. For transitivity, distribute over the two disjunctions: a pair of strict comparisons composes by strict transitivity, and any equality substitutes into the other comparison. For antisymmetry, the case of two opposed strict comparisons implies $x<x$ and hence falsity; every remaining case supplies equality. All these are coherent deductions, so the interpretation works in an arbitrary topos rather than only in classical sets.

It gives a functor $V:\mathbf{FinSPos}\to \mathbf{FinPos}$ and hence a geometric morphismThis applies Question 5 to $V^{\mathrm{op}}$ on the presheaf indexing categories. Every finite weak poset is the reflexification of its classical strict part, so every target indexing object is in the image. Question 5(ii) therefore makes $g$ surjective. But $V$ is not full: the constant map from a two-element chain to a singleton is weak-order-preserving and not strict-order-preserving. Question 5(iii) consequently proves the morphism is a surjection, not an injection. The strict part of a weak order would require an inequality predicate, so the classical equivalence of weak and strict orders on sets does not supply an inverse geometric interpretation.

For the extended theories, interpret the printed final symbols ${\mathcal{F}}_1,{\mathcal{F}}_2$ as the classifiers of ${\mathbb{L}}_1,{\mathbb{L}}_2$, respectively; the repeated ${\mathbb{P}}_i$ names in that sentence are a source slip. Let $\mathbf{FinLin}$ contain finite totally ordered sets and all weak monotone maps, and let $\mathbf{FinSLin}$ contain finite strict total orders and increasing injections. Again include the empty order. Then both linear-order classifiers are presheaf toposes:For the weak-total model, two finite nondecreasing realized tuples can locally be merged into a single nondecreasing tuple: compare their first remaining entries using totality, take an entry known to be no larger than the other, and continue. This finite procedure uses only finite totality disjunctions and permits duplicate values; it does not require decidable equality. To equalize maps between finite chains, collapse the convex intervals forced equal by their realization; antisymmetry guarantees that all values in such intervals agree. These give the flatness conditions for $\mathrm{Hom}(P,M)$, and finite tuples recover the model exactly as above.

For a strict-total model, trichotomy merges two finite increasing tuples, identifying entries when the equality alternative holds. Every strict map out of a finite chain is injective: if two indices differ, their images are strictly comparable and cannot be equal. Consequently parallel increasing injections with the same realized tuple are already equal, supplying the equalization condition. The same reconstruction proves the classifying topos of strict linear orders claim; in the weak case it proves the classifying topos of linear orders claim. In particular the latter proof has not silently replaced weak totality by decidable strict trichotomy.

Finally, reflexification sends a strict-total model to a weak-total one. Indeed pulling back weak totality under the interpretation givesexactly the strict trichotomy axiom. Thus the original morphism restricts to the corresponding subtoposes, giving the commutative squareThe vertical embeddings are induced by the full inclusions of finite chains among finite partial orders, and their images classify precisely the added axioms. On presheaves $g_{\mathrm{lin}}^{\ast }$ is restriction along $V_{\mathrm{lin}}:\mathbf{FinSLin}\to \mathbf{FinLin}$. The same object-surjectivity and two-element-collapse argument show that the restricted morphism is also surjective and not an embedding. The exact pullback of the added totality axiom further identifies the square as the corresponding base change of subtoposes.

Let $A$ be a finite set of alternatives with $|A|\ge 3$, and let each agent report a strict total order on $A$. A profile is the tuple of these orders. The domain is unrestricted: every tuple of orders is allowed. A deterministic social choice function $f$ selects one alternative from each profile. It is onto if every alternative is selected at some profile. It is strategyproof if no agent, holding all other reports fixed, can obtain an outcome strictly preferred according to its true order by reporting another order. A dictatorship in social choice means that one fixed agent's highest-ranked alternative is always selected, regardless of all other reports.

The Gibbard-Satterthwaite theorem says that every onto, deterministic strategyproof social choice function on this unrestricted domain is a dictatorship in social choice. Equivalently, with at least three possible alternatives an onto nondictatorial rule must permit manipulation. Both the number of alternatives and the unrestricted preference domain are essential hypotheses.

For the requested top-bottom decisiveness lemma, suppose $f(R,S)=a$, with $a$ top in $R$ and bottom in $S$. Fix any $R^{\prime }$ with $a$ top. If $f(R^{\prime },S)\ne a$, agent $1$ with true order $R^{\prime }$ could report $R$ and obtain its best outcome $a$, contrary to strategyproofness. Hence $f(R^{\prime },S)=a$. Now fix any $S^{\prime }$. If $f(R^{\prime },S^{\prime })=b\ne a$, agent $2$ with true order $S$ could report $S^{\prime }$ and obtain $b$, which is better than its bottom alternative $a$. ThereforeCall this agent $1$ being decisive for $a$. The same argument with agents interchanged applies to agent $2$.

Here is a complete proof of the two-agent theorem. First, onto plus strategyproofness gives unanimity. If $a$ occurs at some profile, change agent $1$ to any order with $a$ top: a different outcome would allow that agent to obtain $a$ by returning to its old report. Then change agent $2$ to any order with $a$ top in the same way. Thus every profile with both agents ranking $a$ top selects $a$.

We also need Pareto efficiency. A useful rank-raising monotonicity lemma follows from strategyproofness: if the current outcome is $b$, and one agent changes its order without placing above $b$ any alternative previously below $b$, the outcome remains $b$. Otherwise an outcome $c\ne b$ would satisfy $b\succ c$ in the old order, since a profitable deviation is forbidden there, but $c{\succ }^{\prime }b$ in the new order, since reporting the old order is forbidden there. Those comparisons contradict the allowed change. If both agents prefer $a$ to a selected $b$, change their orders one at a time to put $a$ first and $b$ second. These changes only raise $b$ relative to other alternatives, so the outcome remains $b$, contradicting unanimity for $a$. Therefore an alternative unanimously dominated by another cannot be selected.

Choose distinct $a,b$. Give agent $1$ order $b\succ a\succ \text{the rest}$ and agent $2$ order $a\succ b\succ \text{the rest}$. Pareto efficiency forces the outcome to be $a$ or $b$. If it is $b$, move $b$ to the bottom of agent $2$'s order while keeping $a$ top. A switch to $a$ would be a profitable deviation for its old true order. Every other alternative is unanimously dominated by $a$. Hence the outcome stays $b$, and the top-bottom decisiveness lemma makes agent $1$ decisive for $b$. If the outcome is $a$, the symmetric argument makes agent $2$ decisive for $a$. Consequently some agent is decisive for some alternative. Rename that agent $1$ and that alternative $a$.

Both agents cannot be decisive for this same $a$. To see this, choose $b,c\ne a$ distinct, with every remaining alternative below these three, and considerAt $(R,S^{\prime })$, agent $1$ can obtain $a$ by placing it top, so strategyproofness restricts the outcome to $a$ or $b$. Both agents prefer $b$ to $a$, so Pareto efficiency forces $b$. At $(R^{\prime },S^{\prime })$, agent $1$ still ranks $b$ top and can obtain it by reporting $R$, so the outcome must again be $b$. On the other hand, at $(R^{\prime },S)$, decisiveness of agent $2$ for $a$ restricts the outcome to $a$ or $c$. Both agents prefer $c$ to $a$, so it must be $c$. Since $c$ is top in $S^{\prime }$, agent $2$ can obtain it at $(R^{\prime },S^{\prime })$ by reporting $S$, forcing outcome $c$ there. This contradiction proves that agent $2$ is not decisive for $a$.

Now fix $b\ne a$ and any agent-$1$ order $R$ with $b$ first and $a$ second. At every $(R,S)$, agent $1$ can force $a$ by placing it top, so the outcome must lie in $\{a,b\}$. If $a$ occurs for even one report $S$, changing agent $2$ to an order with $a$ first and $b$ second preserves $a$, because it can return to $S$ to obtain its top choice. Lower $a$ to the bottom of agent $1$'s order, keeping $b$ top. A switch to $b$ would be a profitable deviation under its old order, and any other outcome is unanimously dominated by $b$. Thus $a$ remains selected at a profile where agent $2$ ranks it top and agent $1$ ranks it bottom. The top-bottom decisiveness lemma would make agent $2$ decisive for $a$, a contradiction.

Therefore every $(R,S)$ with agent $1$ ranking $b$ first and $a$ second selects $b$. Choose $S$ with $b$ bottom and apply the top-bottom decisiveness lemma once more: agent $1$ is decisive for $b$ in every order placing $b$ top. This holds for each $b\ne a$, and it already holds for $a$. Agent $1$ is a dictator in social choice, proving the two-agent theorem.

With three agents and only two alternatives, the two-alternative majority rule is onto and strategyproof and has no dictator in social choice. An agent whose vote is not pivotal cannot change the outcome. A pivotal agent obtains its preferred alternative by voting truthfully and its less preferred alternative by reversing its vote. No one is a dictator in social choice, since the other two agents can both oppose its preference. There is no tie with three agents. This does not contradict the theorem because its hypothesis $|A|\ge 3$ fails.

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

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

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

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

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

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

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

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

A strict order-preserving function preserves strict comparisons. Between strict partial orders it may identify incomparable elements. Between strict total orders it is necessarily injective, and in a finite chain it is exactly an increasing injection. It need not reflect comparisons between incomparable elements of general partial orders.