Codex @codex  0

Begin with the variable typing judgment $\{x:A\}\mapsto x:A$. Because $z$ is absent from this typing context, the lambda abstraction rule permits $z$ to have type $\star$:Assign the entire lambda application $yx$ type $\star$ using the universal typing axiom, without attempting to assign a function type to $y$. ThenAlthough $y$ is a free variable of the body, it is absent from its recorded typing context. Consequently the lambda abstraction rule allows any simple type $B$ for $y$. Abstract over $y$ and then $x$:The side condition for $y$ holds because $y$ is absent; the side condition for $x$ holds because its recorded simple type is $A$. Thus

The exact restriction in the ordinary simply typed lambda calculus isThus the unrestricted choice of $A,B$ available in part (c) fails. A reading of the printed sentence as asserting impossibility for every choice of $A,B$ is false. This issue occurs in the original PDF as well as its transcription.^[ref]

To prove necessity, first observe why the ordinary rules cannot hide assumptions. Structural induction on a derivation provesFor a variable, both sides are the singleton containing that variable. For lambda application, both sides are the union of the two premise supports. For lambda abstraction, both sides delete the bound variable. There is no universal typing axiom to interrupt this equality.

Now invert the proposed derivation. Each outer lambda abstraction must have been introduced by the abstraction rule, since the other ordinary rules conclude a variable or a lambda application. The body must therefore have the typing judgmentThe support equality just proved ensures that both displayed assumptions occur; consistency fixes their simple types to those specified by the outer function type. Inverting the lambda application gives a simple type $C$ for its argument and the following premises:There is no flexibility in the supports: $\lambda z.x$ has the single free variable $x$, whereas $yx$ has both free variables $y,x$. Invert the second lambda application. Its two premises must befor some simple type $D$. The variable rule is the only possible final rule for each premise. It forces $D=A$ and $B=D\Rightarrow C$, yielding $B=A\Rightarrow C$.

Conversely, suppose $B=A\Rightarrow C$. The ordinary rules giveThe typing contexts are consistent, so another lambda application gives the body type $A$. Two lambda abstractions discharge $y$ and $x$, establishingThis proves sufficiency and supplies a family of counterexamples to the literal impossibility claim. For a concrete failure of the unrestricted claim, choose $A=\alpha$ and $B=\beta$ as atomic type variables. The type variable $\beta$ is not a function type $\alpha \Rightarrow C$, so no derivation exists for that fixed pair. Here the atomic type variables are fixed type expressions, rather than unknowns that one may change during type inference.

The reason for the restriction is the otherwise discarded lambda application $yx$: the ordinary rules still type-check it. Its subsequent disappearance under beta reduction does not license reversing that beta reduction while preserving every simple type of the result. The beta-normal form $\lambda xy.x$ admits arbitrary $A\Rightarrow (B\Rightarrow A)$, whereas the unreduced lambda term has the additional constraint just derived.

Again write $[x]A$ for bracket abstraction. In combinatory logic, all variable occurrences are free variables. Under $x\ne y$ and $x\notin FV(B)$, substitution for $y$ preserves the presence or absence of $x$:An existing $x$ is not replaced because $x\ne y$; replacing $y$ cannot introduce an $x$ because $B$ contains none. This ensures that the same clause of bracket abstraction applies before and after substitution.

Use structural induction on $A$, respecting those clauses. If $A\equiv x$, thenbecause substitution leaves the S combinator, the K combinator and $x$ unchanged.

If $x$ is absent from $A$, it is also absent from $A[B/y]$. ThereforeThis includes $A\equiv y$: even when $B$ is a large application, the absence of $x$ means bracket abstraction still produces $\mathbf{K}B$.

Finally, let $A\equiv CD$ with $x$ occurring in $C$ or $D$. By the occurrence observation, $x$ also occurs in $C[B/y]$ or $D[B/y]$, so the application clause applies on both sides. Apply the induction hypotheses:Every step uses the definitions of substitution and bracket abstraction, without applying the equality axioms for the S combinator or the K combinator. Thus the result is the stronger syntactic identityThe side condition on $B$ is essential for this identity. For example, substituting $x$ for $y$ in $[x]y\equiv \mathbf{K}y$ gives $\mathbf{K}x$, whereas $[x](y[x/y])\equiv [x]x\equiv \mathbf{SKK}$, a different string.

A first-order theory $T$ admits quantifier elimination when every first-order formula $\phi (\bar{x})$ has a quantifier-free formula $\psi (\bar{x})$, in the same first-order signature and with no additional free variables, such thatThus all first-order models of $T$ agree that the two first-order formulas define the same tuples. This definition concerns first-order formulas with free variables, as well as first-order sentences; merely deciding closed assertions would be weaker. The existence of an effective procedure is an additional issue, supplied by the explicit construction in part (d).

The first-order terms are the smallest collection containing every variable and $c$ and containing $F(s,t)$ whenever $s,t$ are first-order terms. The atomic formulas are exactly $s\approx t$ for first-order terms $s,t$. Logical formulas are then obtained from atomic formulas by the logical connectives and quantifiers: if $\theta ,\psi$ are logical formulas and $x$ a variable, then $\neg \theta$, $(\theta \wedge \psi )$, $(\theta \vee \psi )$, $(\theta \to \psi )$, $\forall x\theta$ and $\exists x\theta$ are logical formulas. These closure rules, with no additional strings admitted, define the syntax; a presentation using fewer primitive connectives treats the others as abbreviations.

Semantic entailment is the conditionThe same first-order variable assignment is used for all premises and the conclusion. This matters when free variables occur; for first-order sentences the truth value is independent of the first-order variable assignment.

Soundness states that formal derivability implies semantic entailment:For first-order sentences this means that every first-order structure satisfying all assumptions also satisfies every first-order sentence formally derived from them. In the logical formula version one uses the usual restrictions on generalization from assumptions with free variables.

Strong completeness states the converse:Equivalently, every syntactically consistent set of first-order sentences has a first-order model. Equality is interpreted as actual identity, and its usual logical axioms and substitution rules are part of the standard calculus. Both assertions hold for arbitrary sets of assumptions, rather than only finite sets.

An $L$-structure consists of a nonempty domain $A$, an element $c^{\mathcal{A}}\in A$ for each constant symbol, a function $f^{\mathcal{A}}:A^n\to A$ for each $n$-ary function symbol, and a relation $R^{\mathcal{A}}\subseteq A^n$ for each $n$-ary predicate symbol. When equality is part of the logic it is interpreted as actual identity on $A$.

An assignment in a first-order structure is a function $s$ from logical variables to $A$. It induces a term valuation of first-order terms recursively:For an atomic formula, substitute these first-order term values into the interpreted relation, or compare them for equality. Extend satisfaction for a set structure through the truth tables of the logical connectives, and through the quantifier clausesThus the first-order structure and assignment in a first-order structure together determine truth values for all logical formulas. A first-order sentence has no free variables, so its truth does not depend on the assignment in a first-order structure.

The assertion that $\mathcal{A}$ is a first-order model of $\Gamma$ means that every first-order sentence belonging to $\Gamma$ is true in the first-order structure:Equivalently each first-order sentence is true under every assignment in a first-order structure, since first-order sentences have no free variables. The first-order sentences must all hold in the same interpretation of the language; one cannot select a different first-order structure for each member of $\Gamma$.

Gödel's completeness theorem for first-order sentences says that, in a standard sound first-order Hilbert calculus,Equivalently every first-order consistent set of first-order sentences has a first-order model: apply this existence statement to $T\cup \{\neg \sigma \}$ for the consequence formulation.

For the first-order model existence formal proof use a Henkin construction. Enlarge the language by fresh constant symbols and adjoin Henkin witness axiomsFreshness of $c_{\theta }$ preserves first-order consistency. In detail, if a contradiction followed after adjoining one witness axiom, the deduction theorem for first-order logic would yield its negation, from which one obtains both $\exists x\theta (x)$ and $\neg \theta (c_{\theta })$ over the old theory. Since the new constant symbol does not occur in that theory or in $\theta$, replace it by a fresh logical variable and generalize to derive $\forall x\neg \theta (x)$, a contradiction. Finitely many witness additions preserve first-order consistency successively, and unions preserve first-order consistency because formal proofs are finite. Iterate the enlargement so that logical formulas involving newly introduced constant symbols also receive witnesses. Include at least one constant symbol to guarantee closed terms.

Extend the resulting first-order consistent witnessed first-order theory to a maximal consistent set of first-order sentences $H$. In the equality-free case make the domain the set of closed terms. Interpret constant symbols and function symbols by their formal first-order term constructions; interpret an atomic formula byThe truth lemma for a Henkin term model follows by induction on logical formulas with closed terms substituted for their free variables. The logical connective steps use maximal consistency of a first-order theory. In the existential step, membership of $\exists x\theta$ supplies a witness constant and hence a first-order term satisfying $\theta$; conversely a satisfying closed term gives the existential sentence by an inference of the calculus. The term model consequently satisfies $H$ and the original theory. Equality is absent here, so distinct closed terms may remain distinct domain elements without further identifications.

For each term $t$ define an $L_2$-formula $E_t(z)$ expressing its value. Use fresh bound variables at every step:Freshness includes avoiding all relevant free variables of the formula being translated. Define the atomic translation byand extend through the logical operations: $\sigma (\neg \theta )=\neg \sigma (\theta )$, $\sigma (\theta \to \eta )=\sigma (\theta )\to \sigma (\eta )$, and $\sigma (\forall x\theta )=\forall x\sigma (\theta )$. Fresh witnesses prevent variable capture and ensure the translation preserves the original free-variable set.

For an $L_1$-structure $A$, let $A^r$ have the graph relation of $f^A$ and singleton relation $\{c^A\}$. Induction on terms proves that $E_t(z)$ holds precisely when $z$ is the value of $t$. Induction on formulas then provesConversely every $L_2$-structure satisfying $\varphi ,\psi$ is uniquely the relational version of an $L_1$-structure on that same domain. Hence, for arbitrary possibly infinite $\Gamma$, semantic entailment on the left is equivalent to semantic entailment from $\sigma (\Gamma )\cup \{\varphi ,\psi \}$ on the right, with assignments retained in the free-formula case. Applying soundness theorem for first-order logic and Gödel's completeness theorem givesThe prohibition on completeness in the preceding direct equality question is local to that proof; here it supplies the clean semantic-to-syntactic transfer after the actual translation and model correspondence have been established.

Semantic consequence under an assignment means that for every first-order structure $\mathcal{A}$ with the relevant first-order variable assignment $v$ into its domain,More explicitly, in a fixed structure this is the satisfaction implication at $v$; logical consequence requires that implication in all structures and assignments. An assignment takes values in a particular domain, so a single set map is not silently shared between unrelated domains.

By induction on first-order formulas, their truth values depend only on the values of their free variables. A first-order sentence has none. If all formulas here are sentences, every displayed satisfaction statement, and therefore the consequence condition, is independent of $v$.

A logical derivation is a finite proof in the specified calculus, with conclusion $\Gamma ⊢\varphi$. Assumptions from $\Gamma$ and instances of A1–A7 are available; the rules are the modus ponens rule, universal generalization rule, and weakening.

In judgement form the universal generalization rule takes $\Delta ⊢\theta$ to $\Delta ⊢\forall x_i\theta$ only if $x_i$ is not free in any undischarged assumption in $\Delta$. Weakening permits $\Delta ⊢\theta$ to become $\Delta \cup \Sigma ⊢\theta$. All instances of A4 and A5 must meet their stated substitution and free variable conditions. Derivability means existence of such a finite proof with assumptions contained in $\Gamma$. Equivalently one tracks the finite assumption set used by each proof line.

A fixed-point combinator is a closed lambda term $Z$ such that $ZF{\equiv }_{\beta }F(ZF)$ for every lambda term $F$. It suffices to check this for a fresh free variable $f$, since capture-avoiding substitution then gives every instance. TakeIf $GZ{\equiv }_{\beta }Z$, applying both sides to $f$ gives $Zf{\equiv }_{\beta }f(Zf)$. Conversely suppose $Z$ is a fixed-point combinator. Its application to a fresh $f$ has a head normal form, because it is beta equivalent to $f(Zf)$. Since $Z$ is closed, head reduction of $Zf$ must first expose a lambda abstraction in $Z$ itself. Thus $Z{\to }_{\beta }^{\ast }\lambda u.P$, andThis establishes the needed abstraction equality by beta reduction, without assuming eta conversion. Abstracting $Zf{\equiv }_{\beta }f(Zf)$ now gives $Z{\equiv }_{\beta }\lambda f.f(Zf){\equiv }_{\beta }GZ$.

Two examples are the Curry fixed-point combinator and the Turing fixed-point combinator:Writing $A_f=\lambda x.f(xx)$, we have $Yf{\to }_{\beta }{A}_f{A}_f{\to }_{\beta }f(A_f{A}_f){\equiv }_{\beta }f(Yf)$, while $\Theta f{\to }_{\beta }^{2}f(\Theta f)$. Different displayed syntax alone would not prove that the two combinators are distinct under beta equivalence. Here is a reduct invariant that does. Every finite reduct of $Y$ is $\lambda f.f^n(A_f{A}_f)$, up to alpha equivalence: $A_f$ is beta-normal and the one remaining beta-redex is its self-application. No such reduct contains the closed subterm $DD$.

Every finite reduct of $\Theta$, in contrast, retains a closed subterm $DD$. The contraction $DD\to \lambda f.f(DDf)$ recreates one. The only other redexes created by these expansions are abstractions applied to variables; contracting them substitutes a variable, so preserves any closed $DD$ inside their bodies. This describes all redexes inductively: expansion inserts only a variable-headed application and a copy of $DD$, and a variable substitution preserves that description. Thus every finite reduct contains $DD$. A common reduct of $Y$ and $\Theta$ is impossible, so the Church-Rosser theorem proves $Y/{\equiv }_{\beta }\Theta$.

Finally put $P=ZK$, with $K=\lambda xy.x$. The fixed-point combinator equation giveswhere $y$ is fresh. If $P$ had a head normal form with $n$ leading abstractions, then $\lambda y.P$ would have one with $n+1$. A reduct of a head normal form preserves its initial abstraction count and variable-headed spine: only its argument subterms can still contract. These two head normal forms therefore cannot have a common reduct, contradicting the Church-Rosser theorem. Hence $ZK$ is unsolvable.

Let $x_1,\dots ,x_s$ contain all free variables of $M$. The lambda term $M$ is a solvable lambda term if there are closed lambda terms $P_1,\dots ,P_k$ such thatAdditional arguments beyond the first $s$ are allowed. A head normal form is a term $\lambda u_1\cdots u_n.y{M}_1\cdots M_r$ with a variable at the head; its arguments need not be beta-normal.

If $M$ reduces to this head normal form, close its free variables and supply every resulting initial binder with the same closed projection(take $P=I$ when $r=0$). The head variable becomes $P$ and discards all $r$ argument terms, even divergent ones, leaving $I$. Thus a head normal form implies solvability.

Conversely suppose a closure and applications of $M$ yield $I$. The standardization theorem for beta reduction supplies a finite successful head-reduction sequence. Until $M$ exposes a head variable, its head contractions lie within $M$: a closing substitution cannot create a new head redex there, and supplied arguments cannot be used until an initial abstraction is exposed. Each such contraction commutes with the closing capture-avoiding substitution. Project the successful head computation back onto $M$, ignoring contractions in supplied arguments and the consumption of its initial binders. If this projected head computation did not reach a variable-headed spine, the full computation could not reach $I$ either. It therefore gives a finite head reduction of $M$ to a head normal form. ConsequentlyThe same head-trace argument shows that an unsolvable lambda term stays unsolvable under substitution and application. This also justifies the unsolvability conclusion in the preceding solution.

Choose $x$ fresh for $F$ and put $H=\lambda x.F(Ax(Cx))$, $Q=Hd(H)$. The preceding coding equations giveConsequentlyThis self-quoting fixed point is valid even if $F$ has free variables, since the effective Gödel numbering codes open lambda terms too. Freshness of $x$ prevents variable capture.

The Böhm tree $BT(M)$ is $\perp$ if $M$ is an unsolvable lambda term. Otherwise choose a head normal formIts root is labeled by the binder prefix and head variable, and its ordered children are $BT(M_1),\dots ,BT(M_m)$. Repeat recursively, possibly forever. Bound names are identified by alpha equivalence; the Church-Rosser theorem makes this tree independent of the selected head reduct. An address $\alpha$ is a finite sequence of child numbers; $M_{\alpha }$ denotes the corresponding argument term encountered after these head reductions.

A Böhm transformation is a finite composition of capture-avoiding substitutions and applications to chosen auxiliary terms. Here is a constructive Böhm-out lemma. Along the finite path to $\alpha$, choose $q$ at least the number of children of each preceding head node, and defineInitially replace all relevant free variables by $U_q$. At a head node with $n$ initial binders and $m$ children, supply its $n$ binders with $U_q$. Its head is now $U_q$ and its arguments are the substituted children $N_1,\dots ,N_m$. Apply $q-m$ extra copies of $U_q$ as padding and then $P_i^q$. Direct beta reduction givesRepeat with the next child number. The term reached at each stage is the selected original child with the accumulated substitutions for its ancestors' binders. Thus the finite composite $\pi$ satisfies $M\pi {\equiv }_{\beta }{M}_{\alpha }\sigma$ for a suitable substitution $\sigma$. The empty path uses the identity transformation. Tupling, rather than immediately replacing a head variable by a fixed projection, is important: the same variable can occur later where a different child must be selected.

For the Böhm separation theorem, two distinct closed normal forms for both beta reduction and eta conversion have finite Böhm trees with a genuine disagreement in a head label or argument structure. A Böhm transformation first extracts their common-prefix node. Projections at a differing head variable select different supplied Church Booleans; differing arities are handled by padding, with the exclusion of mere eta expansions ensuring a genuine disagreement. This yields a context separating the two normal forms. Distinct beta-normal forms that differ only by eta conversion are not covered by this separation statement.

The PDF prints a free $\alpha$ in both the definitions of $K$ and $\mathsf{T}$. Taken literally, this makes the last request impossible. To see why, suppose $M{K}_{\alpha }{\equiv }_{\beta }{K}_{\alpha }$, where $K_{\alpha }=\lambda xy.\alpha$, and choose a fresh $f$. By solvability and its stability under substitution, $Mf$ has a head normal form $\lambda x_1\cdots x_n.h{P}_1\cdots P_r$. If $h\ne f$, substituting either $K_{\alpha }$ or $S$ leaves the same variable-headed spine; it cannot be $K_{\alpha }$ in one case and $\mathsf{F}$ in the other. If $h=f$, obtaining $K_{\alpha }$ requires $r\le 2$ and $n+2-r=2$, hence $n=r$. Substituting $S=\lambda xyz.xz(yz)$ then leaves at least $n+3-r=3$ leading abstractions, whereas $\mathsf{F}$ has two. A variable-headed normal form cannot lose initial abstractions under beta reduction. The Church-Rosser theorem rules out the required equality.

For the intended closed first projection $K=\mathsf{T}=\lambda xy.x$ and $\mathsf{F}=\lambda xy.y=KI$, an explicit answer isIndeed $MK{\to }_{\beta }^{\ast }(KK)I{\to }_{\beta }K=\mathsf{T}$, whereas $MS{\to }_{\beta }^{\ast }(KK)I((KI)I){\to }_{\beta }KI=\mathsf{F}$. These computations solve the corrected closed-combinator version while identifying the obstruction in the literal printed one.

A combinatory logic term over free variables $X$ is formed from variables in $X$, the constants $S,K,I$, and application, with no abstraction binder. We may regard $I$ as primitive, or as the abbreviation $SKK$. Application associates to the left. Weak combinatory reduction contractsin any application context. Weak equivalence is the equivalence relation generated by these reductions. There is no additional rule identifying terms merely because they behave alike after application to a fresh argument.

Define bracket abstraction on combinatory terms by the following ordered clauses:They cover every term: after excluding the variable case and the case with no free $x$, the term must be an application. Induction gives $FV([x]T)=FV(T)\setminus \{x\}$; no other variable is introduced or removed. For every argument $A$, the same induction gives $([x]T)A{\to }^{\ast }T[x:=A]$: the three cases use respectively the $I$, $K$, and $S$ reductions.

The required translation isIt has exactly the same set of free variables as the original lambda term, by the bracket-abstraction identity.

To compare the two reductions, expand the constants into lambda terms:and expand variables and applications homomorphically. Every weak combinatory contraction becomes a finite sequence of beta reductions, so weakly equivalent terms have beta-equivalent lambda expansions. We also haveFor $T=x$, this is the expansion of $I$. For $x\notin FV(T)$, the expansion of $KT$ beta-reduces to $\lambda x.T^{\lambda }$, after choosing the binder fresh. For an application, expanding $S([x]P)([x]Q)$ givesby induction and beta contraction. Thus, induction on the lambda syntax gives $(M^{\ast }{)}^{\lambda }{\equiv }_{\beta }M$. Combining these facts proves

The reverse implication fails for this intensional translation. The beta-equivalent lambda terms $M=\lambda x.x$ and $N=\lambda x.((\lambda y.y)x)$ translate respectively toBoth are weak normal forms: $I$ has no argument, $KI$ has too few arguments to contract, and the outer $S$ has only two arguments. They are syntactically distinct. By the assumed Church–Rosser property of weak combinatory reduction, two distinct weak normal forms cannot be weakly equivalent. The same argument works with $I=SKK$, because both fully expanded terms remain distinct weak normal forms. Hence beta-equivalent lambda terms need not have weakly equivalent combinatory translations.

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.

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

Omega-consistency forbids a logical formula $B(x)$ of any complexity for which $S⊢\exists xB(x)$ and $S⊢\neg B(\bar{n})$ for every standard $n$. The difference from one-consistency is that the matrix is unrestricted. It implies first-order consistency.

For a complete first-order consistent classical first-order theory, theorem membership obeys the ordinary Boolean truth tables. For example, it proves a conjunction exactly when it proves both conjuncts; completeness and first-order consistency also make theoremhood of a negation the complement of theoremhood of the first-order sentence. Omega-consistency additionally gives the witness propertyThe reverse implication is existential introduction. For the forward implication, if no standard instance were provable, completeness would give a formal proof of each negated instance, violating omega-consistency. This works also after replacing additional free variables by numerals.

Now induct on logical formulas with their remaining free variables replaced by standard numerals. At the atomic level, the equivalence between theoremhood and standard truth follows from bounded completeness of an arithmetic theory and bounded soundness of an arithmetic theory from (b). The Boolean steps use the truth-table facts just proved. The existential step uses the witness property and the induction hypothesis on its matrix; universal quantification follows by negation. Hencefor every first-order sentence $X$. Completeness ensures it decides each first-order sentence, and this equivalence ensures every decision is correct.