Deduction, Soundness, Completeness, and Compactness

Assign to an assumption line its singleton support, to an axiom the empty support, to an MP line the union of its two preceding supports, and to either quantifier-rule line the support of its one preceding premise. Induction on line number shows each support is finite and that the prefix derives the line from that support: no rule gains assumptions, and all side conditions are unchanged. In particular the last line has finite support.

Enlarging a sentence theory retains every assumption and line annotation. To concatenate proofs, add the length of the first list to every reference in the second. To replace proved sentence assumptions, insert their finite proofs before their uses and redirect each later reference to the new index of its premise. Induction on the old list gives a valid new list. Only finitely many proofs are inserted; a finite family of existing proofs can be selected by finite induction in ZF. Quantifier parameters and their free-variable restrictions are unchanged, and the new base assumptions are sentences.

For a nonempty inclusion-chain, every finite subset of its union lies in one member: choose a member containing each of its finitely many sentences, and repeatedly retain the larger of two comparable members; for the empty finite subset use any one member. A proof of $\mathrm{\perp }$ from the union would thus, by its finite support and weakening, be a proof from a consistent member, which is impossible.

For the empty chain define a syntactic Boolean valuation $V$: every atom has value $1$, negation and conjunction have their Boolean values, and $V(\mathrm{\exists }x\varphi )=V(\varphi )$. Induction on formula construction shows $V(\varphi [t\mathrm{/}x])=V(\varphi )$, since every atomic value is unchanged and substitution commutes with the Boolean constructors and either retains or traverses a quantifier. Consequently $V(\mathrm{\forall }x\varphi )=V(\varphi )$. All six axiom schemes have value $1$: the substitution axioms reduce to $a\to a$, distribution to $(a\to b)\to (a\to b)$, reflexivity to $1$, equality substitution to $1\to (a\to a)$, and Boolean tautologies to true Boolean instances. MP preserves $1$, generalization does not change the value, and existential elimination leaves its premise's value unchanged. But $V(\mathrm{\perp })=0$. Induction on proof length therefore rules out an empty-theory proof of $\mathrm{\perp }$, proving consistency also for the empty union.

The formulas $A\to A$, $A\to \mathrm{\neg }\mathrm{\neg }A$, $\mathrm{\neg }\mathrm{\neg }A\to A$, $(A\to B)\to (\mathrm{\neg }B\to \mathrm{\neg }A)$, $A\to (B\to A\wedge B)$, $A\wedge B\to A$, $A\wedge B\to B$, and $A\to (\mathrm{\neg }A\to B)$ are Boolean tautologies, hence axioms. Applying MP to the displayed antecedents gives the asserted rules. Reflexivity gives $v_0=v_0$; generalization gives $\mathrm{\forall }{v}_0(v_0=v_0)$, which is literally $\mathrm{\neg }\mathrm{\perp }$ for $\mathrm{\perp }=\mathrm{\exists }{v}_0\mathrm{\neg }(v_0=v_0)$. From $\mathrm{\perp }$ and this theorem, the last tautology yields any formula. Conversely contradictory formulas yield $\mathrm{\perp }$ by the same tautology with $B=\mathrm{\perp }$.

Suppose $y$ occurs nowhere in $\varphi$. Instantiation gives $\mathrm{\forall }x\varphi \to \varphi [y\mathrm{/}x]$. Generalize $y$ and use restricted distribution, with $y$ absent from $\mathrm{\forall }x\varphi$, to obtain $\mathrm{\forall }x\varphi \to \mathrm{\forall }y\varphi [y\mathrm{/}x]$. Conversely instantiate $\mathrm{\forall }y\varphi [y\mathrm{/}x]$ at $x$. The substitution is free-for and returns $\varphi$: each new free $y$ is at an originally free $x$ position, hence below no $x$ binder. Generalizing $x$ and distributing gives the converse implication, since $x$ is not free in $\mathrm{\forall }y\varphi [y\mathrm{/}x]$.

Choose a variable $z$ absent from the displayed terms. Apply equality substitution to the formula $z=s$: $s=t\to (s=s\to t=s)$. Reflexivity and Boolean commutation of antecedents give $s=t\to t=s$. For transitivity use the formula $s=z$: $t=u\to (s=t\to s=u)$. MP gives $s=u$ from $s=t,t=u$. More generally the stated free-for formula substitution is already an axiom, and two MP applications give its inference; symmetry gives the reverse inference.

The axiom $\varphi [t\mathrm{/}x]\to \mathrm{\exists }x\varphi$ followed by MP proves existential introduction whenever $t$ is free for $x$. Given a proved $\varphi \to \psi$, combine it with the instance $\psi \to \mathrm{\exists }x\psi$ (substitution $x\mathrm{/}x$) using the Boolean composition tautology. This gives $\varphi \to \mathrm{\exists }x\psi$. Existential elimination now gives $\mathrm{\exists }x\varphi \to \mathrm{\exists }x\psi$, since $x$ is not free in its consequent. Apply this to each of $\mathrm{\neg }\mathrm{\neg }\varphi \to \varphi$ and $\varphi \to \mathrm{\neg }\mathrm{\neg }\varphi$ from step 1.1. The resulting two implications prove $\mathrm{\exists }x\mathrm{\neg }\mathrm{\neg }\varphi \leftrightarrow \mathrm{\exists }x\varphi$.

For existential renaming, introduction gives $\varphi [y\mathrm{/}x]\to \mathrm{\exists }x\varphi$; eliminate $y$, which is absent from the consequent. For the reverse direction introduction at $x$ gives $\varphi \to \mathrm{\exists }y\varphi [y\mathrm{/}x]$ by the same inverse-substitution calculation as step 1.2; eliminate $x$, which is absent from this consequent. Thus both renaming implications are theorems, including vacuous binders. No semantic equivalence has been substituted for a syntactic rule.

For each old line $\eta$ we construct a proof from $T$ of $\sigma \to \eta$, by induction along the finite list. If $\eta =\sigma$, use identity. If $\eta$ is an axiom or belongs to $T$, retain its one-line proof and apply the tautology $\eta \to (\sigma \to \eta )$ by MP. These include every possible first line.

If $\eta$ comes by MP from $\alpha$ and $\alpha \to \eta$, the already transformed premises and the tautology $(\sigma \to \alpha )\to ((\sigma \to (\alpha \to \eta ))\to (\sigma \to \eta ))$ give the new line by two MP applications.

If $\eta =\mathrm{\forall }x\alpha$ comes by generalization, generalize the transformed $\sigma \to \alpha$ to $\mathrm{\forall }x(\sigma \to \alpha )$, then use distribution to obtain $\sigma \to \mathrm{\forall }x\alpha$. Its restriction holds because $x$ is not free in $\sigma$.

If $\eta =(\mathrm{\exists }x\alpha \to \beta )$ comes from $\alpha \to \beta$, the transformed premise is $\sigma \to (\alpha \to \beta )$. Boolean commutation gives $\alpha \to (\sigma \to \beta )$. Eliminate $x$ to get $\mathrm{\exists }x\alpha \to (\sigma \to \beta )$, since $x$ is free in neither $\sigma$ nor $\beta$. Commute back to $\sigma \to (\mathrm{\exists }x\alpha \to \beta )$.

The three rule cases exhaust the list. Concatenating each finite derived block gives a finite proof of $\sigma \to \theta$ from $T$. For a sentence $\sigma$ both variable restrictions hold automatically. Conversely, weaken a proof of $\sigma \to \theta$ to $T\cup \{\sigma \}$, append its assumption $\sigma$ and apply MP to obtain $\theta$.

Assumptions in $T$ are true at every assignment by the hypothesis and coincidence. Boolean tautologies are true under the Boolean values of their constituent formulas. Reflexivity is true because a term's value equals itself. For equality substitution, if $s_0=t_0$ is true, their denotations agree; updating $x$ with either value gives the same assignment, so F2 gives equal truth values for the two substituted formulas. Thus its implication is true.

Universal instantiation is true: the universal truth clause includes the particular value $\mathrm{⟦}t{\mathrm{⟧}}_s$, and F2 identifies the instance. Existential introduction is true: a true instance supplies precisely that value as a witness by F2. For distribution, if $\mathrm{\forall }x(\alpha \to \beta )$ and $\alpha$ are true at $s$, then $\alpha$ stays true at every $s[x:=a]$ because $x$ is not free in it. The universal premise gives $\beta$ at each such assignment, hence $\mathrm{\forall }x\beta$ at $s$.

Induct on proof lines with the invariant “true under every assignment in $M$.” MP preserves this invariant by the implication truth table. For generalization, the invariant for its premise holds at each $s[x:=a]$, so its universal conclusion holds at $s$.

For existential elimination, suppose $M,s\models \mathrm{\exists }x\alpha$. Take one witness $a$. The invariant for the earlier implication $\alpha \to \beta$ applies at $s[x:=a]$, giving $\beta$ there. Since the rule requires $x$ absent from $\mathrm{FV}(\beta )$, F3 gives $\beta$ at $s$. If the existential antecedent is false the conclusion is true by its Boolean clause. This verifies the third rule and finishes the induction.

Thus the last line is true at every assignment in every model of $T$, exactly F4. No such model satisfies $\mathrm{\perp }=\mathrm{\exists }{v}_0\mathrm{\neg }(v_0=v_0)$, because every candidate witness equals itself. A proof of $\mathrm{\perp }$ would contradict the established invariant, so any theory with a model is consistent. Only one witness was used for one implication in step 3.1; no family of witnesses or AC is required.

The finite proof and its finitely many finite annotations mention only finitely many variables. Choose the least-index variable $z$ not mentioned. Replace every token $c$ in formulas and substitution data by $z$, leaving binders unchanged. No binder is $z$, so every inserted $z$ remains free. Assumption lines are unchanged since $c$ is absent from $T$.

A Boolean axiom remains the same tautology pattern with transformed substituted formulas; reflexivity remains reflexivity. For either quantifier substitution axiom and the equality substitution axiom, token replacement commutes with the indicated free-variable substitution. Its new term can gain only the free variable $z$, and no binder in the transformed matrix is $z$, so every former free-for condition still holds. Universal distribution's restricted variable is an old variable: replacing $c$ by $z$ creates no free occurrence of that old variable in its antecedent. Thus every transformed axiom is an axiom of the smaller signature.

MP retains the identical implication/premise matching. A generalization in an old variable still generalizes that variable after replacement. For existential elimination the eliminated variable is old and distinct from $z$; the consequent gains no occurrence of it, so its restriction persists. Therefore induction along the unchanged reference indices gives a valid transformed derivation. Generalization in $z$ may be appended because the base assumptions are sentences.

If the conclusion omits $c$, it is unchanged by this operation; we obtain the asserted smaller-language proof. A proof in an expansion by any set of fresh constants mentions only finitely many of them. Remove them one at a time by the operation above, each time taking a new variable outside the finite current proof. The final proof uses only the original signature. Conversely every original proof is still a proof in the expansion. Hence the expansion is conservative.

If $T\cup \{\mathrm{\neg }\sigma \}⊢\mathrm{\perp }$, deduction gives $T⊢\mathrm{\neg }\sigma \to \mathrm{\perp }$. Combining with the theorem $\mathrm{\neg }\mathrm{\perp }$ gives $T⊢\mathrm{\neg }\mathrm{\neg }\sigma$ by Boolean contraposition, and hence $T⊢\sigma$. Conversely a proof of $\sigma$ remains valid after adjoining $\mathrm{\neg }\sigma$; explosion then proves $\mathrm{\perp }$. This proves both directions for arbitrary $T$.

If $T\cup \{\sigma \}$ is inconsistent, deduction and $\mathrm{\neg }\mathrm{\perp }$ similarly give $T⊢\mathrm{\neg }\sigma$. If also $T\cup \{\mathrm{\neg }\sigma \}$ were inconsistent, step 1.1 would give $T⊢\sigma$; the two conclusions would prove $\mathrm{\perp }$ in $T$. For consistent $T$ this is impossible. Thus if the positive extension is inconsistent the negative extension is consistent; otherwise the positive extension itself is consistent.

Write $E=\mathrm{\exists }x\varphi$ and $h=(E\to \varphi [c\mathrm{/}x])$, a sentence by the free-variable restriction in F1. If $T\cup \{h\}⊢\mathrm{\perp }$, deduction and $\mathrm{\neg }\mathrm{\perp }$ give $T⊢\mathrm{\neg }h$. The Boolean implications $\mathrm{\neg }(A\to B)\to A$ and $\mathrm{\neg }(A\to B)\to \mathrm{\neg }B$ then yield proofs from $T$ of $E$ and $\mathrm{\neg }\varphi [c\mathrm{/}x]$.

Apply fresh-constant replacement to the latter finite proof, choosing $z$ absent also from $\varphi$, $x$ and $\mathrm{\perp }$. The result is $T⊢\mathrm{\neg }\varphi [z\mathrm{/}x]$. This substitution identity follows because $c$ was absent from $\varphi$ and $z$ is unbound there. Boolean explosion gives $T⊢\varphi [z\mathrm{/}x]\to \mathrm{\perp }$. Eliminate $z$ to obtain $T⊢\mathrm{\exists }z\varphi [z\mathrm{/}x]\to \mathrm{\perp }$; $\mathrm{\perp }$ is a sentence, so the rule's restriction holds.

Fresh-variable existential renaming gives $T⊢E\to \mathrm{\exists }z\varphi [z\mathrm{/}x]$. Together with the proof of $E$ and step 2.1, MP yields $T⊢\mathrm{\perp }$ in the pure constant expansion. Conservativity removes that expansion, contradicting the given consistency of $T$. Therefore the witness extension is consistent. The same conservativity statement, without adding any sentence axiom, proves the seed-constant assertion.

Assign each original symbol a code $p(0,q(s))$, each variable $v_i$ the code $p(1,i)$, each of the finitely many distinct logical or punctuation tokens a distinct code $p(2,j)$, and the seed constant code $p(3,0)$. Reserve $p(4,p(n,k))$ for the possible witness constant $c_{n,k}$ introduced at stage $n$ for formula code $k$. Injectivity of $p$ and $q$ separates every tag and every entry within a tag. Thus even the set of all possible such constants, before selecting those actually used, has a fixed joint alphabet injection.

For a finite list of natural numbers define $r(\mathrm{\varnothing })=0$ and $r(a_0,\dots ,a_n)=p(r(a_0,\dots ,a_{n-1}),a_n)$. Use recursion for each finite list, or the corresponding recursion on finite sequences. Encode a list $\bar{a}$ of length $n$ by $p(n,r(\bar{a}))$. Equal codes imply equal lengths by F3. Inducting on that common length, equality of the last paired values gives equality of the last entries and of the prefix values; the induction hypothesis recovers the prefixes. For length zero both lists are empty. Hence this is an explicit injection on all finite lists. Composing with the alphabet code of step 1.1 gives an injection on all words and thus on terms and formulas by F2.

Starting with the original symbols and seed, at stage $n$ assign the fresh constant $c_{n,k}$ to each existential sentence of the current language whose word code is $k$. These are distinct because the word code is injective, and no such constant occurred earlier because its stage tag is fresh. The successor operation is definable on the set of subsets of the possible tagged alphabet together with the natural stage, so F4 gives all finite stages. Each embeds into the same alphabet of step 1.1, as does their union. A finite expression in the union uses finitely many symbols and therefore lies in some stage. A finite list of formulas is coded by applying step 2.1 again to their word codes. For annotated proofs, first encode the finitely many annotation types by distinct natural tags. All their fields are natural line indices, variables, terms, formulas, or finite lists of these, including the finite Boolean templates and substitution lists for axiom instances. Tag each field by its type and apply the list injection of step 2.1 to its component codes; applying the same construction to each line record and then the finite list of line records gives an injection on annotated proofs. The tags and list lengths recover the record structure, and injectivity at each field recovers every annotation as well as every formula. Restrict this injection to any specified proof set; no test deciding validity or membership is needed.

The sentence ${\sigma }_{\ast }:=\mathrm{\exists }{v}_0(v_0=v_0)$ is available in every one of these languages, even with no nonlogical symbols. For a fixed stage or the union, let $e$ be its sentence-code injection. Define ${\sigma }_n$ to be the unique sentence of code $n$ when one exists, and ${\sigma }_{\ast }$ otherwise. Separation and Replacement give this sequence; its definition may test membership in a set and need not be computable. Every sentence $\sigma$ occurs at index $e(\sigma )$. Thus the sequence is exhaustive and uses no choice of enumerations of unspecified countable sets.

Start with $L_0=L\cup \{c_{\ast }\}$ and $T_0=T$, consistent in $L_0$ by F2. For each round $n$, F1 provides a fixed exhaustive sequence $({\sigma }_{n,k}{)}_{k<\omega }$ of $L_n$-sentences. Reserve a distinct constant $c_{n,k}$ for each index $k$, disjoint from $L_n$. Let $L_{n+1}$ include all these constants, and regard $T_n$ in this pure expansion; it remains consistent by F6.

In round $n$ put $U_0=T_n$. At index $k$ put $V_k=U_k\cup \{{\sigma }_{n,k}\}$ if this is consistent, and $V_k=U_k\cup \{\mathrm{\neg }{\sigma }_{n,k}\}$ otherwise. F3 makes $V_k$ consistent. If ${\sigma }_{n,k}=\mathrm{\exists }x\varphi$, put $U_{k+1}=V_k\cup \{\mathrm{\exists }x\varphi \to \varphi [c_{n,k}\mathrm{/}x]\}$; otherwise put $U_{k+1}=V_k$. The new constant occurs in neither $V_k$ nor the matrix, since only earlier indices have been used and every enumerated sentence belongs to $L_n$. F2 gives consistency in the one-constant extension, and F6 gives it in the whole $L_{n+1}$. Thus each $U_k$ is consistent.

The test “has no finite proof of bottom” is a set-theoretic predicate, so the successor rule in step 2.1 is a definable function, even when not computable. Encode its state by the index and the current subset of the potential sentence set; define any unused malformed-state transition to a fixed state. F5 then supplies the inner sequence, and F4 makes $T_{n+1}={\bigcup }_k{U}_k$ consistent. The outer round operation is likewise definable on a set of language/theory states, so F5 supplies all rounds. No arbitrary choice of enumerations or of consistent sides is made.

Put $L_{\mathrm{\infty }}={\bigcup }_n{L}_n$ and $U={\bigcup }_n{T}_n$. Each $T_n$ remains consistent in $L_{\mathrm{\infty }}$ by F6, so F4 gives consistency of $U$. Every finite formula in $L_{\mathrm{\infty }}$ lies in some $L_n$ by F1. Round $n$ therefore decides each such sentence and supplies a witness axiom for every such existential sentence. Repeated enumeration entries do no harm: each index has its own fresh constant.

Let $H=\{\sigma \in \mathrm{Sent}(L_{\mathrm{\infty }}):U⊢\sigma \}$. This is a set by Separation. If $H$ proved bottom, finite support would use finitely many members of $H$; replace them by their finite $U$-proofs using F4 to contradict consistency of $U$. The same composition shows that every sentence consequence of $H$ already belongs to $H$. It contains $U$, all decisions and all witness axioms from step 4.1, and the seed is a closed term. F1 injects the union alphabet and syntax into $\omega$. Thus $H$ has every asserted property in ZF.

If both $\sigma$ and $\mathrm{\neg }\sigma$ belonged to $H$, their assumption proofs and explosion would prove bottom, contrary to consistency. If $\sigma \mathrm{\notin }H$, completeness gives a proof of $\sigma$ or $\mathrm{\neg }\sigma$; the first would put $\sigma$ in $H$ by deductive closure, so the second puts $\mathrm{\neg }\sigma$ in $H$. Conversely $\mathrm{\neg }\sigma \in H$ excludes $\sigma \in H$ by the first argument.

If $\sigma \wedge \tau \in H$, conjunction elimination and closure put both conjuncts in $H$. If both conjuncts belong, the conjunction introduction tautology and two MP applications give their conjunction in $H$. Thus both conjunction directions hold.

If $\mathrm{\exists }x\varphi \in H$, take the single witness constant in F1; MP and closure yield $\varphi [c\mathrm{/}x]\in H$, with $c$ a closed term. Conversely a closed term $t$ has no free variables and is free for $x$ in $\varphi$; applying existential introduction to $\varphi [t\mathrm{/}x]\in H$ and closing gives $\mathrm{\exists }x\varphi \in H$. This proves the existential equivalence even for vacuous $x$. No simultaneous selection of witnesses and no rewriting inside a quantifier is used.

Reflexivity proves $s=s$, so closure puts it in $H$. If $s=t$ belongs to $H$, symmetry proves $t=s$, which belongs to $H$. If $s=t,t=u$ belong, transitivity proves $s=u$, which belongs to $H$. These give precisely reflexivity, symmetry and transitivity of $\sim$.

If $s\sim t$ and $\alpha$ is a formula, the terms $s,t$ are free for any variable $x$ because they have no free variables. Equality substitution and MP give $H⊢\alpha [s\mathrm{/}x]\to \alpha [t\mathrm{/}x]$; symmetry gives the reverse implication. When the instances are sentences, closure and MP show their memberships in $H$ agree. If they retain other free variables, the same implication proofs remain valid without claiming that open formulas are members of $H$.

Let $s_i\sim t_i$ for $1\le i\le n$. Replace the tuple entries in order, applying step 2.1 at one placeholder variable absent from all the other displayed terms and formulas. Closed substituted terms cannot introduce or capture a variable. At every replacement the two closed instances have the same membership; transitivity of logical equivalence proves this for the full tuple. This applies to $R(s_1,\dots ,s_n)$ and to arbitrary closed formula instances. For $n=0$ no replacement is performed and the formula is identical.

For a function $f$, begin with the reflexive equation $f(\bar{s})=f(\bar{s})\in H$. Replace the entries in the right-hand occurrence alone in decreasing order $i=n,n-1,\dots ,1$, using the formula $f(\bar{s})=f(s_1,\dots ,s_{i-1},z,t_{i+1},\dots ,t_n)$. At this stage the entries to its right have already been replaced and the entries to its left have not. Step 2.1 gives each successive equality, ending with $f(\bar{s})=f(\bar{t})\in H$. Thus the function outputs are equivalent. A constant is its own fixed class; if there are no function or relation symbols, the equivalence relation proof still applies.

By term induction, the denotation of a term $u$ whose variables lie in the tuple is $[u[\bar{t}\mathrm{/}\bar{x}]]$. At a variable this is the given value, at a constant it is F1, and at $f(u_1,\dots ,u_r)$ the induction hypotheses and F1 give $[f(u_1[\bar{t}\mathrm{/}\bar{x}],\dots ,u_r[\bar{t}\mathrm{/}\bar{x}])]$, the required substituted term. Closed insertions do not acquire free variables; sequential substitution at distinct variables agrees here with simultaneous substitution, since inserted terms contain no free variables.

For equality atoms step 1.1 gives equality of classes iff the two closed terms are equivalent, which is exactly membership of their equality in $H$. For a relation atom, step 1.1 and its definition in F1 identify truth with membership of the substituted atom. F5 ensures the result is unchanged if any representative is replaced by an equivalent term.

Suppose the equivalence has been proved for immediate subformulas, with arbitrary finite representative tuples. At $\mathrm{\neg }\psi$, its semantic truth means failure of $\psi$; the induction hypothesis and F2 translate that to membership of the closed negation. At $\psi \wedge \theta$, truth means truth of both subformulas, which the hypotheses and F2 identify with membership of the closed conjunction. Both calculations are equivalences.

For $\varphi =\mathrm{\exists }y\psi$, substitute the supplied closed terms for the free variables other than $y$ in $\psi$, obtaining a matrix $\rho$ with free variables at most $y$. The closed instance of $\varphi$ is literally $\mathrm{\exists }y\rho$. If ${\mathcal{M}}_H,a\models \mathrm{\exists }y\psi$, take its one witness class $b$ and one closed term $u$ with $b=[u]$. The induction hypothesis for $\psi$ with the updated finite tuple gives $\rho [u\mathrm{/}y]\in H$. F2 gives $\mathrm{\exists }y\rho \in H$. Free-for composition here is legitimate because all inserted terms are closed: binders cannot capture them, and insertions in distinct free positions do not interfere; equivalently their semantic updates agree by F3.

Conversely if $\mathrm{\exists }y\rho \in H$, F2 supplies a closed term $u$ with $\rho [u\mathrm{/}y]\in H$. The induction hypothesis for $\psi$ gives ${\mathcal{M}}_H,a[y:=[u]]\models \psi$, hence the existential formula is true. If $y$ is vacuous, the same argument uses the nonempty quotient and the unchanged instance. These two directions establish the constructor case.

The atom, Boolean and existential cases exhaust the primitive syntax, so F4 proves the equivalence for every formula. For a sentence the tuple is empty and the closed instance is the sentence itself; each member of $H$ is therefore true in the quotient. At any induction step only finitely many representative classes and at most one additional witness are involved; finite existential selections are available in ZF and no global representative function is constructed.

If $T$ is consistent, use F1 and F2 to form a quotient model $M_H\models H\supseteq T$. Its reduct to the original language satisfies $T$ by F6 and has the same nonempty carrier.

Let $q$ be the closed-term injection from F5. For each quotient class $b$, define $j(b)=\min \{q(t):[t]=b\}$. The set minimized is nonempty because $b$ is a class of a closed term. Equal values of $j$ name the same term by injectivity of $q$, hence the same class. Thus $j$ injects the carrier into $\omega$, with no choice of a family of representatives.

If $T\models \sigma$ but $T⊬\sigma$, F3 makes $T\cup \{\mathrm{\neg }\sigma \}$ consistent. Steps 1.1–2.1 supply a model of this theory, which satisfies $T$ and falsifies $\sigma$, a contradiction. Thus semantic consequence implies provability. Conversely F4 gives $T⊢\sigma \Rightarrow T\models \sigma$, even if $T$ has no model.

If $M\models T$, the same $M$ satisfies every subset, in particular every finite subset. Conversely suppose each finite subset of $T$ has a model. Any proof of bottom from $T$ would have finite support $T_0$ by F2; its model would contradict F3. Thus $T$ is consistent and F1 supplies an at most countable nonempty model. This also handles $T=\mathrm{\varnothing }$: the finite-subset hypothesis then concerns that empty theory itself.

If $T\models \sigma$, F1 gives a finite proof $T⊢\sigma$. F2 supplies its finite assumption set $T_0\subseteq T$, with $T_0⊢\sigma$. F3 then gives $T_0\models \sigma$. The support can be empty when $\sigma$ is logically provable. No selection of models for all finite subsets was needed in step 1.1: a single alleged proof would call for only one model.

Suppose $\mathcal{A}\prec \mathcal{M}$ and $\mathcal{M}\models \mathrm{\exists }x\psi [\bar{a}]$. By elementarity $\mathcal{A}\models \mathrm{\exists }x\psi [\bar{a}]$, so some $b\in A$ satisfies $\mathcal{A}\models \psi [\bar{a},x:=b]$. Applying elementarity to the matrix and this enlarged tuple gives $\mathcal{M}\models \psi [\bar{a},x:=b]$. This proves necessity, including existential sentences with no parameters.

Now assume the witness condition. For a term evaluated at a tuple from $A$, variable values and constant values coincide in the two structures. If its argument terms coincide, their values belong to $A$, and the restricted function gives the same output in both structures. Constructor induction therefore gives equality of all term values, with positive arity as required by the signature convention. Literal equality and relation restriction then give identical truth values for atomic formulas, with the positive arities in the signature.

Induct simultaneously over all parameter tuples for each formula. If $\theta$ has identical truth in both structures, $\mathrm{\neg }\theta$ does too, since its truth is the negation of that same value. If $\theta ,\eta$ each have identical truth, $\theta \wedge \eta$ does too, since it is true exactly when both are true. Restrict a given tuple to the required free variables when applying the induction hypothesis.

For $\mathrm{\exists }x\psi$, if it holds in $\mathcal{A}$, choose its witness $b\in A$. The induction hypothesis for $\psi$ transfers its truth to $\mathcal{M}$, where $b$ is also a witness. Conversely, if it holds in $\mathcal{M}$, the assumed condition supplies $b\in A$ for which the matrix is true in $\mathcal{M}$. The induction hypothesis transfers the matrix to $\mathcal{A}$, giving the existential statement there. Updates at $x$ overwrite any earlier value, so the argument also covers a vacuous quantifier.

Steps 1.2–1.4 cover the primitive constructors equality, relations, negation, conjunction and existential quantification. All other connectives are their abbreviations. Thus every formula agrees on every tuple from $A$, which is exactly $\mathcal{A}\prec \mathcal{M}$. Together with step 1.1 this proves the equivalence.

By F5 and A1 fix a well-order of $M$. Its least element is $m_0$; selecting the least satisfying element of each nonempty existential witness set, and $m_0$ otherwise, gives the family of F1. The same remaining argument applies to any already supplied family. This is the use of choice needed to produce witnesses for an arbitrary structure.

The alphabet consisting of the nonlogical symbols, countably many variables and finitely many punctuation/constructor tokens has size at most $\kappa$, by F4. Fix an injection of it into $\kappa$ and a pairing injection ${\kappa }^2\to \kappa$ from F3. Recursively pairing coordinates gives injections ${\kappa }^n\to \kappa$ for each positive finite $n$; the empty word is one additional element. Encoding the length as well gives an injection of all finite words into $\omega \times \kappa$, of size $\kappa$ by F4. Formulas are particular finite words, so there are at most $\kappa$ formulas and at most $\kappa$ pairs $(x,\psi )$. Thus there are at most $\kappa$ closure operations in F1, all of finite arity.

If $\mathrm{\mid }{H}_n\mathrm{\mid }\le \kappa$, the same finite-tuple encoding gives at most $\kappa$ tuples of each arity and at most $\kappa$ operation/tuple pairs in total. Their image has size at most $\kappa$: well-order the pair codes and assign to each image element its least preimage code. Adding $H_n$ and the at most $\kappa$ constants preserves the bound by F4. Also $\mathrm{\mid }{H}_0\mathrm{\mid }=\mathrm{\mid }A\cup \{m_0\}\mathrm{\mid }\le \kappa$. Induction proves $\mathrm{\mid }{H}_n\mathrm{\mid }\le \kappa$ for all $n$. To bound the union, use A1 on the nonempty sets of injections $H_n\to \kappa$, obtaining injections $j_n$ simultaneously. Assign $a\in H$ the pair $(n,j_n(a))$ for its least membership stage $n$. This injects $H$ into $\omega \times \kappa$, giving $\mathrm{\mid }H\mathrm{\mid }\le \kappa$ by F4. This explicitly accounts for the countable choice in this union bound.