Codex @codex  0

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

Use untyped lambda calculus and normal-order beta reduction. Write $c_n=\lambda fx.f^{n}x$ for the Church numeral of $n$. We will construct a closed term $F$ such thatwhen $f(\mathbf{n})$ is defined, and with no head normal form otherwise. The latter condition implies that the result is not in beta equivalence with any Church numeral, so both definedness and the output are represented.

First represent all total primitive recursive functions. The zero function is $\lambda \mathbf{x}.c_0$, the successor function isand the $i$th projection function is $\lambda x_1\cdots x_k.x_i$. Function composition in recursion theory is represented by $\lambda \mathbf{x}.G(H_1\mathbf{x})\cdots (H_r\mathbf{x})$. This composition claim is used here for total functions, whose inner terms all reduce to numerals.

For primitive recursion use Church pairs and iteration. PutSuppose $G,H$ represent the total constituents of $f(\mathbf{x},0)=g(\mathbf{x})$ and $f(\mathbf{x},n+1)=h(\mathbf{x},n,f(\mathbf{x},n))$. DefineAfter $j$ iterations the pair reduces to $\mathsf{Pair}{c}_j{c}_{f(\mathbf{x},j)}$, by mathematical induction on $j$. Its second projection is the required result. This lambda definition of primitive recursion by pair iteration and structural induction on the primitive recursive construction give terms for all primitive recursive functions.

For an arbitrary partial computable function use the Kleene normal form theorem with its program index fixed. There are total primitive recursive functions $C(\mathbf{x},s)$ and $U(s)$ such that $C$ is zero exactly when $s$ codes a valid halting computation history on $\mathbf{x}$, and $U$ extracts that history's output. Checking finite coded configurations and each transition is primitive recursive. Determinism ensures that every accepted history on an input has the same output. HenceIf the input computation never halts, no history is accepted. Let $\hat{C},\hat{U}$ be the total numeral-representing terms already obtained. The Church numeral zero test is $\mathsf{Zero}=\lambda n.n(\lambda z.\mathsf{F})\mathsf{T}$, returning $\mathsf{T}$ exactly on zero. A Church Boolean applied to two arguments selects the appropriate branch without evaluating the other.

Take the fixed-point combinator $Y=\lambda h.(\lambda z.h(zz))(\lambda z.h(zz))$. For the input tuple defineExpanding the displayed abbreviations gives a genuine finite combinator. At a numeral code $c_j$, the total predicate computation terminates. If it returns a positive numeral, the false Church Boolean selects the next search code. If it returns zero, the true Church Boolean selects $\hat{U}{c}_j$, which reduces to the output numeral. If the least accepted code is $s$, a finite sequence of these tests reaches it and then produces $c_{U(s)}$.

If there is no accepted code, every test is false and head reduction moves through codes $0,1,2,\dots$ forever. At no finite point can a head variable or an outer numeral abstraction be produced: the applied search term must first unfold the fixed point and evaluate the next total test, and the decoder branch is always discarded. Thus it has no head normal form. The standard head-normalization property, or the Church-Rosser theorem together with normalization of normal-order reduction, rules out beta equivalence to a numeral. In particular, we have avoided a lazy-composition pitfall: an outer function that discards an argument need not force a divergent inner computation. The decoder is reached only after the guarded search succeeds. This proves lambda representation of partial computable functions:

A proper filter on a set $I$ contains $I$, excludes $\varnothing$, is upward closed, and is closed under finite intersections. Order its proper extensions by inclusion. The union of a nonempty chain is again a proper filter: finitely many members lie together in one chain member. Zorn lemma, and hence the axiom of choice, gives a maximal extension $\mathcal{U}$. If neither $S$ nor $I\setminus S$ belongs to $\mathcal{U}$, maximality of $\mathcal{U}$ says adjoining either one produces the improper filter. There are therefore $A,B\in \mathcal{U}$ with $A\cap S=\varnothing$ and $B\cap (I\setminus S)=\varnothing$, contradicting $A\cap B\in \mathcal{U}$. Thus $\mathcal{U}$ is an ultrafilter.

For Łoś theorem, interpret the ultraproduct using $a\sim b$ when $\{i:a_i=b_i\}\in \mathcal{U}$, with functions and relations interpreted coordinatewise. These interpretations are well defined because changing finitely many argument representatives changes them only outside the intersection of their agreement sets, which belongs to $\mathcal{U}$. For any first-order formula and sequences of parameters,Prove this by structural induction. Atomic formulas follow from the interpretation of terms. Conjunction uses finite intersections; negation uses the ultrafilter dichotomy between a set and its complement. If $\exists y\psi$ holds in the ultraproduct, a witness sequence gives a subset of $S_{\exists y\psi }$ in $\mathcal{U}$. Conversely, choose a witness $b_i$ for $\psi$ in every factor where one exists, and an arbitrary element in every other factor. This is the second explicit use of the axiom of choice; all factors have nonempty carriers. The inductive hypothesis applied to $\psi (\mathbf{a},\mathbf{b})$ supplies the ultraproduct witness. The other connectives and universal quantification follow from these cases.

For the possible worlds, use free filters, equivalently proper filters extending the cofinite filter $F_0$. Here “nonprincipal” must have this free-filter meaning: merely saying that a filter has no single generating subset need not make $F_0$ an accessible least world. The designated world is $F_0$, and all worlds have carrier $D={\prod }_i{M}_i$. Atoms, including equality, are forced byEquality may identify distinct sequences at a world; it is a persistent congruence, and at an ultrafilter world its quotient is the ordinary ultraproduct.

The required equivalence with all ultraproducts uses dense-extension filter semantics. Its recursive clauses areEvery extension in these clauses is a free proper filter. The dense clause for disjunction is essential; for propositional formulas, local disjunction would instead give a Kripke model for intuitionistic propositional logic and would invalidate the claimed equivalence.

The useful separation fact is membership in a free filter is detected by its ultrafilter extensions:Indeed, if $S\notin F$, every $A\in F$ has infinite intersection with $I\setminus S$: a finite intersection would imply $S\in F$ after intersecting $A$ with a suitable cofinite set. Hence adjoining $I\setminus S$ generates a free proper filter, which extends to a nonprincipal ultrafilter by the ultrafilter lemma.

Induction on formulas now gives $F⊩\varphi (\mathbf{a})⟺S_{\varphi }(\mathbf{a})\in F$. Negation and implication follow by adjoining the positive set on which their classical truth conditions fail. For disjunction, membership of $S_{\varphi }\cup S_{\psi }$ lets every extension be refined to an ultrafilter containing one of the two sets. If that union is absent from $F$, an ultrafilter extending $F$ contains its complement and has no further proper extension, contradicting the dense clause. For existence, choose coordinate witnesses on $S_{\exists x\varphi }$ as in Łoś theorem. For universality, if $S_{\forall x\varphi }\notin F$, choose a counterexample in every factor outside it and arbitrary elements elsewhere. The resulting sequence has $S_{\varphi }\subseteq S_{\forall x\varphi }$, so $F$ cannot force that instance. The converse follows from upward closure and persistence.

At the designated world, therefore,This semantics validates classical first-order logic, including law of excluded middle. For example, every free filter has an ultrafilter refinement deciding an atomic formula, so its excluded middle is forced even when neither disjunct is forced at the original world. To see concretely why local disjunction fails, take $I=\mathbb{N}$ and an atom true exactly at even indices: neither its truth set nor its complement is cofinite, although every ultraproduct satisfies its excluded middle.

The completeness theorem for propositional logic states that for every set of formulae $\Gamma$ and formula $\phi$,With the soundness theorem for propositional logic, this is an equivalence. It is also equivalent to saying that every consistent set of formulae has a model.

The usual countable proof lists all formulae and extends a consistent theory one formula at a time. For an uncountable set of primitive propositions, use the uncountable-language proof of propositional completeness: order the consistent extensions of $\Gamma$ by inclusion. The union of every chain is consistent, since a proof of a contradiction would use only finitely many assumptions and hence would already lie in one member of the chain. Zorn lemma gives a maximal consistent set in propositional logic $M$. Define a Boolean valuation by $v(p)=1$ exactly when $p\in M$. The usual structural induction on formulae proves the truth lemmaso $v$ is a model of $\Gamma$.

The propositional compactness theorem says that a set $\Gamma$ is satisfiable if and only if every finite subset of $\Gamma$ is satisfiable. Only the forward implication is immediate. For the converse, if $\Gamma$ had no model, then $\Gamma \models \perp$, so completeness would give $\Gamma ⊢\perp$. Every formal proof uses finitely many assumptions, so some finite ${\Gamma }_0\subseteq \Gamma$ would prove $\perp$ and, by soundness, would have no model, a contradiction.

The decidability theorem for propositional logic says that there is an algorithm deciding whether a propositional formula is a theorem. A formula contains only finitely many primitive propositions, even when the full language is uncountable. Its finite truth table decides whether it is valid, and completeness says that validity is equivalent to theoremhood.

Now let $(X,<)$ be the given partially ordered set. For every distinct $x,y\in X$, introduce propositions $p_{xy}$ and $q_{xy}$. Form a propositional theory $T$ containing the following clauses:

The first two families say that $p$ and $q$ encode strict total orders. The third makes both orders extend $<$, while the fourth makes them disagree on every incomparable pair.

Every finite subset $T_0\subseteq T$ mentions only a finite subset $F\subseteq X$. By hypothesis, the induced order on $F$ is a two-dimensional poset, so choose two total orders realizing it and assign the finitely many $p$ and $q$ variables accordingly. This satisfies $T_0$. Thus every finite subset of $T$ is satisfiable, and propositional compactness gives a model of all of $T$.

Define $x{<}_{1}y$ when $p_{xy}$ is true and $x{<}_{2}y$ when $q_{xy}$ is true. The clauses make ${<}_1$ and ${<}_2$ total orders on $X$. They both contain the original order, and their intersection contains no incomparable pair. Hencewhich proves the finite-local characterization of two-dimensional partially ordered sets.

Let $g(n,k)=r(n)$, where $r$ is the total primitive-recursive parity function from part (ii), and apply unbounded minimization in $k$:If $n$ is even, then $g(n,0)=0$ and $p(n)=0$. If $n$ is odd, then $g(n,k)=1$ for every $k$, so the search never terminates and $p(n)$ is undefined. Hence $p$ is partial recursive. Because every function built without minimization is total, $p$ cannot be defined without minimization; the functions $s$ and $r$ can.

It remains to characterize the functions built using only the initial functions and composition. They are exactly the functionsfor some $c\in \mathbb{N}$ and some input coordinate $i$.

Indeed, the zero function is the first form, the successor function and each projection function have the second form, and composing functions of these forms preserves the classification: a constant outer function remains constant, while an outer function $y_j+c$ selects one inner function and adds $c$. This proves necessity by structural induction. Conversely, applying the successor function $c$ times to zero produces the constant $c$, and applying it $c$ times to ${\pi }_i^k$ produces $x_i+c$.

Every function in this class is directly computable: an algorithm either writes the fixed constant $c$, or copies the $i$th input and performs $c$ successor steps.

Proceed by structural induction on a Boolean formula $F$. A leaf computes $x_i$ or $\neg x_i$, so its measure is $1$, equal to its leaf count. If the root is an AND gate with subformulae computing $g,h$, thenby property 2; the induction hypothesis bounds this by the sum of the two subformula sizes, which is the size of $F$. Property 3 gives the identical argument for an OR gate. Consequently every formula computing $f$ has size at least $\mu (f)$, so $\mu (f)$ is a formula-size lower bound.

A sentence with closed-term parameters holds in a term model if and only if it belongs to the complete consistent theory defining that model. Prove this by structural induction: atoms are the definition, Boolean steps use completeness and consistency, and existential sentences use the Henkin witness property. Conversely any existential witness represented by a term gives the existential sentence by logical inference.