Codex @codex  0

In the language of first-order logic, defineThus a least element lies below every element, whereas a minimal element merely has no distinct element below it. The latter definition allows multiple incomparable minimal elements.

Here is a formal natural deduction proof, with the antisymmetry axiom available as a premise. Assume $\mathrm{Bottom}(b)$ and take a fresh arbitrary variable $t$. Assume $R(t,b)$. By universal elimination applied to $\mathrm{Bottom}(b)$, obtain $R(b,t)$. By conjunction introduction, obtain $R(t,b)\wedge R(b,t)$. Instantiate antisymmetry at $t,b$, and use modus ponens rule to obtain $t=b$. Discharge the assumption $R(t,b)$ by implication introduction, obtaining $R(t,b)\Rightarrow t=b$. Since $t$ was arbitrary and is free in no undischarged assumption, universal introduction gives $\mathrm{Minimal}(b)$. Discharge the initial assumption and universally quantify $b$ to concludeOnly antisymmetry was needed for this implication; reflexivity and transitivity are part of the ambient partial order axioms.

In first-order logic with equality, the three first-order sentences areA reflexive relation relates each element to itself. An antisymmetric relation forbids distinct elements from relating in both directions. A transitive relation contains every composite of two successive related pairs. Together these axioms define a partially ordered set.

The dot after $\forall x$ gives it scope over the following implication: read the premise as $H=\forall x(P(x)\to Q(x))$. Choose a fresh arbitrary eigenvariable $u$. A natural deduction proof isAt line 6, $u$ is free in no undischarged assumption, so the universal quantifier introduction rule is valid.

The proposed variant is not derivable in a sound first-order logic. For a countermodel, use the two-element domain $\{0,1\}$, interpret both predicates $P,Q$ as $\{0\}$, and assign the free variable $x$ the value 0. Then $\forall x(P(x)\to Q(x))$ is true, as is $P(x)$ under the assignment, but $\forall xQ(x)$ is false at element 1. The premise's bound $x$ and the conclusion's free $x$ have different scopes.Attempting to generalize from $Q(x)$ in the variant would violate the eigenvariable condition, because $x$ remains free in the undischarged assumption $P(x)$.

Using first-order logic with equality, one suitable sentence isThe distinct witnesses give at least two solutions, and the universal clause excludes every third solution. All variables are bound, and the same equation variable $e$ is used in every solution predicate. This is an instance of a first-order definition of exactly finitely many witnesses.

Describe a branching vertex by the first-order logic sentenceand the existence of a sink by $\delta =\exists x\forall y\neg E(x,y)$. The directed path has sinks but no branching vertex; the directed cycle has neither sinks nor branching vertices; the directed arborescence has a branching vertex. Thus the following three sentences distinguish the named structures in order:Here $\beta ,\delta$ are abbreviations for the displayed formulas; replacing them gives sentences in the single-relation first-order signature $\{E\}$. Explicitly, ${\phi }_1$ says that some vertex has no successor and that no vertex has two distinct successors. The truth table across the three structures is:

The conditions distinguish these three finite structures; they are not claimed to characterize all directed paths, cycles or trees among arbitrary directed graphs. Only local out-degrees and the presence of a sink are needed, without quantifying over paths of unbounded length.

Solutions to all eight questions of the Oxford Preliminary Examination held on 15 June 2023. Source release: released examination archive, member 2022/T/a10101w1.pdf. The cover identifies Trinity Term 2023. The three section headings and all question labels below follow this historical paper; its grouping is independent of subsequent course changes. Although candidates were asked to attempt at most five questions, every marked subpart is solved here.

In 8(b), the source's parenthetical definition describes a dominating set, while its name suggests a vertex cover. Both readings are treated explicitly. In 8(c)–(d), we make the scopes of the printed quantifiers explicit; in particular, the opening universal quantifiers in 8(c) govern both irreflexivity and transitivity. As usual in first-order logic, domains are nonempty, and graphs are finite simple graphs unless an infinite domain is specified.

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.

An unintended change of binding caused by moving or substituting a term beneath a binder. In first-order logic, substituting $y$ for the free $x$ in $\forall yS(x,y)$ without renaming would yield $\forall yS(y,y)$, incorrectly binding the substituted occurrence. First rename the bound $y$ to a fresh $z$, obtaining $\forall zS(x,z)$, and then substitute to get $\forall zS(y,z)$. The paper's condition that a term be free for a variable excludes such capture.