Deduction, Soundness, Completeness, and Compactness: Examples and Counterexamples

The annotated derivation is: line $0$: $A$ (assumption); line $1$: $A\to (P(x)\to Q(x))$ (universal instantiation); line $2$: $P(x)\to Q(x)$ (MP on $0,1$); line $3$: $B$ (assumption); line $4$: $B\to P(x)$ (universal instantiation); line $5$: $P(x)$ (MP on $3,4$); line $6$: $Q(x)$ (MP on $5,2$); line $7$: $\mathrm{\forall }xQ(x)=C$ (generalization). Both substitutions are $x\mathrm{/}x$, which is free-for, and both assumptions are sentences, so generalization has no free-assumption obstruction.

Apply F1 to that eight-line proof to obtain $\{A\}⊢B\to C$ and, discharging $A$ instead, $\{B\}⊢A\to C$. Discharge the remaining sentence in the first proof to obtain $⊢A\to (B\to C)$. Thus the example displays a derivation and its actual discharged conclusions.

Let the carrier be $M=\{0,1\}$ with $0\mathrm{\ne }1$, and interpret $P$ by $\{0\}$. Set the assignment $s(v)=0$ for every variable $v$. Then $\mathcal{M},s\models P(x)$. But $s[x:=1]$ does not satisfy $P(x)$, so it does satisfy $\mathrm{\neg }P(x)$. Consequently $\mathcal{M},s\models \mathrm{\exists }x\mathrm{\neg }P(x)$ and $\mathcal{M},s\models ̸\mathrm{\forall }xP(x)$ by F1. The implication $P(x)\to \mathrm{\forall }xP(x)$ has true antecedent and false consequent at $s$, so its expanded negated conjunction is false.

The purported unrestricted inference is explicit: start with the open assumption $P(x)$; generalize the very variable $x$ to obtain $\mathrm{\forall }xP(x)$; discharge that assumption to obtain $P(x)\to \mathrm{\forall }xP(x)$. Step 1.1 refutes this final formula in a nonempty set structure. Thus a deduction theorem used after generalization must retain the restriction on free variables of discharged assumptions; replacing the open assumption by a sentence removes this particular offending free variable. This counterexample establishes invalidity directly and does not assume any completeness theorem.

With no constants or functions, the term constructors give only variables, so none is closed. In the expanded signature each closed term is exactly one of the constants $c_n$, because there are still no function symbols. Let $A$ have carrier $\{0\}$ and interpret every $c_n$ by $0$. Put $H=\mathrm{Th}(A)$, the set of all expanded sentences true in this structure. Negation's truth clause makes exactly one of $\sigma ,\mathrm{\neg }\sigma$ belong to $H$. F2 makes $H$ consistent; it also makes $H$ deductively closed, since any sentence proved from $H$ is true in $A$.

For any existential sentence $\mathrm{\exists }x\varphi$, if it is true in $A$, its only possible witness is $0=c_0^A$, so $\varphi [c_0\mathrm{/}x]$ is true. If it is false, the implication $\mathrm{\exists }x\varphi \to \varphi [c_0\mathrm{/}x]$ is true by the Boolean implication clause. Thus every such witness axiom belongs to $H$, and $H$ is Henkin with seed $c_0$. For all $m,n$ the equation $c_m=c_n$ is true since $0=0$, so all and only the closed terms are in the one class $[c_0]=\{c_n:n<\omega \}$. The quotient of F1 is exactly $\{[c_0]\}$. Its reduct is a singleton model of the original empty theory. This computation concerns this particular $H$, not every Henkin completion of the empty theory.

The positive tail is nonempty since $1\in A$, and restricting $<$ to $A^2$ makes it a substructure: there are no constant or function symbols requiring further closure. Define $f:\omega \to A$ by $f(n)=n+1$. Each positive natural is uniquely a successor, so $g:A\to \omega$ defined by $g(n+1)=n$ satisfies $g(f(n))=n$ and $f(g(m))=m$. Also $n<k$ iff $n+1<k+1$: adding one preserves strict natural-number order, and if $n\ge k$ then $n+1\ge k+1$. Hence $f$ is a bijection preserving and reflecting the sole relation and is an isomorphism. In particular $f(0)=1$; it is different from inclusion.

At the parameter $1\in A$, the formula $\mathrm{\exists }y(y<x)$ holds in $\mathcal{M}$ because $0<1$. It fails in $\mathcal{A}$: every $y\in A$ is a positive natural, so $1\le y$ and $y<1$ is false. Thus inclusion fails to preserve and reflect this formula's truth and is not elementary, despite the isomorphism constructed in step 1.1.

For the fragment $\bar{0}<c,\bar{1}<c,\dots ,\bar{m}<c$ use the standard expansion with $c=m+1$. Its inequalities evaluate to $0<m+1,1<m+1,\dots ,m<m+1$, all true. For example the first three are $0<3$, $1<3$, $2<3$ with $c=3$. With no inequalities use $c=0$. Any accompanying finitely many sentences of $\mathrm{Th}(\mathcal{N})$ remain true because the old structure has not changed.

A putative standard interpretation $c=k$ fails the inequality $\bar{k}<c$, since its evaluation is $k<k$, which is false. Yet F1 supplies a new countable model and an element $b$ satisfying every inequality. Its numeral $\bar{k}$ still denotes the $k$-fold successor of zero; $b$ equals none of these values, because equality would turn the corresponding true inequality into $b<b$, forbidden by the theory's irreflexivity sentence.

Under the stated consistency antecedent, F1 and F3 supply $M\models T_{\mathrm{Z}\mathrm{F}}$ with carrier injecting into $\omega$. F2 makes this carrier infinite. An infinite subset of $\omega$ can be enumerated in increasing order: after finitely many entries it has a least unused member, and each member is eventually reached since only finitely many natural numbers precede it. Composing this enumeration with the injection's inverse on its range gives a bijection $\omega \to M$. Thus $\mathrm{\mid }M\mathrm{\mid }={\mathrm{\aleph }}_0$.

Under A1 apply F4 with $\kappa ={\mathrm{\aleph }}_1$: $M$ is infinite, its size is ${\mathrm{\aleph }}_0\le {\mathrm{\aleph }}_1$, and the membership signature is finite. It gives $N⪰M$ of size ${\mathrm{\aleph }}_1$, which satisfies every sentence of $T_{\mathrm{Z}\mathrm{F}}$ by elementarity. An isomorphism $M\to N$ would be a bijection, contradicting ${\mathrm{\aleph }}_0\mathrm{\ne }{\mathrm{\aleph }}_1$. These are the promised two witnesses under the antecedent. Neither the use of F2 nor the extension argument identifies either internal membership relation with external membership or asserts well-foundedness.