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

The Tarski-Vaught test says that $(M,\in )$ is an elementary substructure of $(N,\in )$ if and only if every existential statement true in $N$ with parameters from $M$ has a witness in $M$ that satisfies its matrix in $N$. Explicitly, for every first-order formula $\psi (x,\bar{y})$ and every parameter tuple $\bar{a}\in M^{|\bar{y}|}$, requireThe truth of the matrix in this test is evaluated in the larger structure $N$. Under this criterion, $(M,\in )\prec (N,\in )$ means that all first-order formulas with parameters from $M$ have identical truth values in the two structures.

Use the cardinalhood formula $C$ from part (b), and let a finite flag choose between it and its negation:Here $0,1$ abbreviate their parameter-free definitions as Finite von Neumann ordinals, and both belong to $M$. This is one first-order formula with two free variables.

For $\beta =({\omega }_1{)}^M$, part (b) proved $M\models C(\beta )$ and $N\models \neg C(\beta )$. The shared parameters $(\beta ,0)$ therefore make ${\phi }_3$ true in $M$ and false in $N$, disproving upward set-theoretic absoluteness. The shared parameters $(\beta ,1)$ make it false in $M$ and true in $N$, disproving downward set-theoretic absoluteness. Hence the same formula fails both directions, with explicit witnesses to each failure.

The constructible hierarchy is defined by transfinite recursion using the definable power set. With parameters permitted in the internal definitions, write $\mathrm{Def}(A,1)$ for the definable subsets of $A$. ThenIts class union is the constructible universe $L={\bigcup }_{\alpha \in \mathrm{Ord}}{L}_{\alpha }$. Only subsets definable over $(L_{\alpha },\in )$ using a first-order formula and finitely many parameters from $L_{\alpha }$ enter at a successor stage.

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.

Let $N$ be a well-founded model of set theory of the complete theory $T$, and suppose that a Paris model $M\models T$ were ill-founded. Its internal ordinals would then contain an external descending sequenceFor every $n$, choose a first-order formula ${\phi }_n$ that uniquely defines ${\alpha }_n$ in $M$. The sentences asserting that ${\phi }_n$ uniquely defines an ordinal and that the object defined by ${\phi }_{n+1}$ belongs to the object defined by ${\phi }_n$ are true in $M$. Since $T$ is complete, all its models satisfy the same first-order sentences, so the corresponding uniquely defined ordinals in $N$ form an external descending membership sequence. This contradicts the well-foundedness of $N$. Thus Paris models are well-founded when their complete theory has a well-founded model proves that every Paris model of $T$ is well-founded.

The definable power set $\mathcal{D}(A)$ performs one definability step over the single structure $(A,\in )$, whereas the constructible power set ${\mathcal{P}}^L(A)$ contains subsets of $A$ created at arbitrarily late stages of the constructible hierarchy.

For the concrete case $A=\omega$, there are only countably many first-order formulas and finite tuples of natural-number parameters, so $\mathcal{D}(\omega )$ is a countable set. In contrast, the constructible universe satisfies ZFC, and Cantor theorem makes its full power set ${\mathcal{P}}^L(\omega )$ uncountable inside $L$. Consequentlyso the two notions do not agree in general.

Fix names $\dot{x},{\dot{a}}_1,\dots ,{\dot{a}}_n\in M$ and a first-order formula $\phi$. Using the syntactic forcing relation, form in $M$ the nameThis is a set by the axiom schema of separation in $M$. If $(\tau ,r)\in \dot{y}$ and $r\in G$, then the forcing theorem gives both ${\tau }^G\in {\dot{x}}^G$ and $\phi ({\tau }^G,{\dot{a}}_1^G,\dots ,{\dot{a}}_n^G)$. Conversely, if $z\in {\dot{x}}^G$ satisfies $\phi$, choose $(\tau ,q)\in \dot{x}$ with $q\in G$ and ${\tau }^G=z$. The truth direction of the forcing theorem supplies $s\in G$ forcing $\phi (\tau ,{\dot{a}}_1,\dots ,{\dot{a}}_n)$; directedness of $G$ gives $r\in G$ below both $q$ and $s$, so $(\tau ,r)\in \dot{y}$.

ThusEvery instance has such a witness, so separation in a generic extension proves $M[G]\models$ Separation.

Suppose that a first-order formula $\phi$ described the inaccessible cardinal $\kappa$, so that $\kappa$ were the least ordinal with $V_{\kappa }\models \phi$. Since $\kappa$ is inaccessible, $V_{\kappa }$ is a model of ZFC. Apply the Lévy reflection theorem inside this model to the single formula $\phi$. There is some $\alpha <\kappa$ for whichThe right side holds, so the left side contradicts the asserted minimality of $\kappa$. Hence no first-order formula describes an inaccessible cardinal, as recorded by ordinal described by a first-order formula.

For a first-order theory $T$ in a first-order language $L$, a complete $n$-type is a maximal $T$-consistent set $p(x_1,\dots ,x_n)$ of formulas whose free variables lie among $x_1,\dots ,x_n$. Equivalently, it chooses exactly one of $\phi$ and $\neg \phi$ for every such formula while remaining consistent with $T$.

An isolated type $p$ is isolated by a formula $\theta (\bar{x})$ when $T\cup \{\exists \bar{x}\theta (\bar{x})\}$ is consistent andfor every $\phi \in p$. The type is an omitted type in an $L$-structure $M$ when no tuple $\bar{a}\in M^n$ satisfies every formula in $p$.

The omitting types theorem states that if $T$ is a consistent theory in a countable language and $(p_i{)}_{i\in \mathbb{N}}$ is a countable family of nonisolated finite-arity types, then $T$ has a countable model omitting every $p_i$.

The Lévy reflection theorem says that for every finite collection $\Phi$ of first-order formulas there are arbitrarily large ordinals $\alpha$ such that, for every $\phi \in \Phi$ and every tuple of parameters $a_1,\dots ,a_n\in V_{\alpha }$,Equivalently, the ordinals simultaneously reflecting all formulas in $\Phi$ form a closed unbounded class.

Let $a,p\in M[G]$, and suppose a first-order formula $\psi (x,y,p)$ defines exactly one $y$ for every $x\in a$. Apply the Lévy reflection theorem to the formulas needed to express this assertion, choosing an ordinal $\alpha$ with $a,p\in V_{\alpha }^{M[G]}$ such thatfor every $x\in a$. Therefore every required value lies in the set $V_{\alpha }^{M[G]}$.

The already established axiom schema of separation forms the setFunctionality makes $b$ exactly the range of the definable function on $a$. This proves every instance of the Axiom schema of replacement in the generic extension $M[G]$.

A syntactically ${\Pi }_1$ first-order formula has an unbounded universal quantifier block followed by a bounded formula in set theory. Universal quantification makes it downward absolute between transitive models. A Pi-one formula modulo ZF may have another syntax but has such an equivalent provable in ZF.

A first-order formula is ${\Pi }_1^{\mathrm{ZF}}$ if ZF proves it equivalent, with the same free variables, to a universal unbounded quantifier block followed by a bounded formula in set theory. Bounded quantifiers do not increase its level in the Lévy hierarchy. Such properties are downward absolute between appropriate transitive models of ZF.

A propositional formula is built from atomic propositions using logical connectives. Unlike a first-order formula, it has no quantifiers over individuals. A Boolean valuation interprets its atoms as truth values and evaluates its connectives recursively.

Propositional logic studies reasoning with whole propositions represented by letters such as $p$ and $q$, and propositional formulas built from them using logical connectives. The classical two-valued, truth-functional presentation below assigns each primitive proposition either true or false: each compound value depends only on its component values. This is classical propositional logic; other systems, including Intuitionistic propositional logic, have different semantics and rules.

Starting with $p$ and $q$, one can build $\neg p$ by logical negation, $p\wedge q$ by logical conjunction, $p\vee q$ by logical disjunction, and $p\to q$ by logical implication, then combine these into larger propositional formulas. Parentheses specify the construction: $(p\to q)\wedge p$ has logical conjunction as its outermost logical connective. Primitive propositions have no internal structure in this language; a first-order formula can additionally describe objects and quantify over them. The formation rules are given in forall x: Calgary, chapter 6.

The following truth table shows the four basic logical connectives. Logical disjunction is inclusive: $p\vee q$ is true when either or both inputs are true. Classical logical implication has exactly the same values as $\neg p\vee q$; its only false row has $p$ true and $q$ false. These truth conditions are specified in forall x: Calgary, chapter 9.

Evaluate $(p\to q)\wedge p$ from the inside out: first the logical implication, then the outer logical conjunction. The final column also tests the logical implication expressing the modus ponens rule:At $p=\mathrm{T},q=\mathrm{F}$, the logical implication is false, so the logical conjunction is false. The abstract syntax tree below separates the construction of the propositional formula from the values propagated through it. Both occurrences of $p$ receive the same value from the Boolean valuation. With the opposite assignment $p=\mathrm{F},q=\mathrm{T}$, the logical implication is true but the logical conjunction is still false because its second input $p$ is false. Recursive evaluation and exhaustive truth tables are explained in forall x: Calgary, chapter 11.

The last column is always true: $((p\to q)\wedge p)\to q$ is a tautology. This expresses the logical validity of the modus ponens rule: whenever both premises $p\to q$ and $p$ are true, $q$ is true. It does not say the premises are true under every Boolean valuation; their logical conjunction is true only on the first row. For a short natural deduction proof outline, assume $(p\to q)\wedge p$, extract both conjuncts, apply the implication elimination rule to obtain $q$, then discharge the assumption by the implication introduction rule. See forall x: Calgary, sections 17.3–17.5.

Three tests answer different questions: Boolean satisfiability requires at least one true row, a tautology requires every row true, and a contradiction has every row false. Thus $p\vee \neg p$ is a tautology, $p\wedge \neg p$ is a contradiction, and $p\wedge q$ is satisfiable but not a tautology: it is true only at $p=q=\mathrm{T}$. See forall x: Calgary, sections 12.1–12.4.

Propositional logic is useful because an inference pattern can be checked once and reused for many choices of propositions. Its beauty is that a finite truth table completely settles classical truth-functional questions about a fixed propositional formula. But logical validity does not verify real atomic claims. If $p$ means “the switch is closed” and $q$ means “the lamp is lit”, a valid use of the modus ponens rule still requires establishing its premises about the apparatus; the truth table supplies neither an observation nor a causal explanation. See forall x: Calgary, chapter 2 and chapter 10.

A quantifier binds a free variable in a first-order formula and specifies how its truth depends on elements of a first-order structure: universal quantification $\forall$ requires every element, while existential quantification $\exists$ requires at least one.

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.