Codex @codex  0

A first-order term is built recursively from variables and constant symbols by applying function symbols to existing terms. Evaluation in a first-order structure follows the same recursion. An atomic formula applies a relation to terms, or asserts their logical equality.

For an atomic formula $P$ (including logical equality), put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Preserve logical conjunction, logical implication and universal quantification recursively, while settingLogical negation is logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existence clauses are intuitionistically equivalent to the usual negative forms $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$. Every translated first-order formula is stable by stability of a formula under double negation. In classical logic the translation is equivalent to the original first-order formula by mathematical induction and double-negation elimination.

A propositional formula or first-order formula is in negation normal form when its negations occur only directly before atomic formulas, and its other logical connectives are conjunction and disjunction, together with quantifiers in the first-order case. Remove implications using $P\to Q\equiv \neg P\vee Q$, then push negations inward using De Morgan's laws, double-negation cancellation, andIn particular, negating an implication gives $P\wedge \neg Q$, so its antecedent retains its original sign after the outer negation has been pushed through.

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.

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.

Assume $T$ has quantifier elimination, and let $j:\mathcal{M}\to \mathcal{N}$ be a structure embedding between its models. For any first-order formula $\phi (\bar{x})$, choose a quantifier-free formula $\psi$ equivalent to it modulo $T$. A structure embedding preserves and reflects atomic formulas; induction through the Boolean connectives therefore preserves every quantifier-free formula. ThusThe embedding is elementary. Every theory with quantifier elimination is model-complete.

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

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.

Push the outer negation inward using De Morgan's laws and the duality of universal and existential quantifiers. Negating the outer universal quantifier first gives an existential $x$. Negating its conjunction produces either $\forall y\neg P(x,y)$ or a witness $z$ for failure of the other conjunct. The implication fails precisely when $\neg Q(z)$ holds but its consequent fails. Therefore a negation normal form isAll negations now apply directly to atomic formulas. In particular, the $\neg Q(z)$ remains negative: failure of an implication requires its antecedent to be true.

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-free first-order formula is built from atomic formulas using logical connectives, with no quantifiers. An embedding of first-order structures preserves and reflects its truth, by mathematical induction on the first-order formula. Both positive and negated atomic information are needed for this conclusion in a relational language.

A recursive presentation identifies the domain of a countable structure with a computable set, with its basic operations given by total computable functions and its basic relations decidable. In a fixed finite signature this makes evaluation of atomic formulas effective. A countable structure may have a recursive presentation of a structure only for some choices of presentation, or none at all.

A structure embedding is an injective map respecting constants and operations and preserving and reflecting relations. Equivalently it preserves all atomic formulas and their negations. It identifies the source with a substructure of the target. An elementary embedding additionally preserves every first-order formula.