The Downward Lowenheim-Skolem theorem says that for an $L$-structure $M$ and a subset $S\subseteq M$, there is an elementary substructure $N\preccurlyeq M$ containing $S$ withIf an infinite cardinal $\kappa$ satisfies $\max (|L|,{\aleph }_0)\le \kappa \le |M|$, one can in particular obtain size exactly $\kappa$ by starting with a subset of that size.

Choose a default element $a_0\in M$. For every logical formula $\exists x\varphi (x,\vec{y})$ choose a Skolem function $F_{\varphi }$ which returns a witness in $M$ when one exists, and returns $a_0$ otherwise. Begin with $S$, the interpretations of the first-order language's constants, and $a_0$. Successively adjoin the values of all the original functions and these Skolem functions on finite tuples already chosen. Let $N$ be the union of the resulting countable sequence of closure stages.

There are at most $\max (|L|,{\aleph }_0)$ logical formulas, and each function has finite arity. With $\kappa =\max (|S|,|L|,{\aleph }_0)$, each closure stage has size at most $\kappa$, and so does their countable union. Closure under the original functions makes $N$ an $L$-substructure. Whenever $M\models \exists x\varphi (x,\vec{a})$ for parameters in $N$, its chosen Skolem witness belongs to $N$, since the finitely many parameters lie in some common stage. The Tarski–Vaught test therefore gives $N\preccurlyeq M$.

For the exact-cardinality version, choose an initial set of $\kappa$ elements, enlarged to contain any prescribed subset of size at most $\kappa$. The construction gives an upper bound $\kappa$ while containment gives the matching lower bound.

If $\mathcal{A}\subseteq \mathcal{B}$, interpret each new constant $c_a$ in $\mathcal{B}$ as the same element $a$. Atomic logical formulas and their negations then have exactly their truth values in ${\mathcal{A}}_A$, so the expansion satisfies the diagram of a structure. If the inclusion is elementary, every logical formula with those named parameters has the same truth value, so the expansion satisfies the elementary diagram.

Conversely, from any expansion ${\mathcal{B}}^{+}$ satisfying the diagram of a structure defineThe diagram of a structure contains $c_a\ne c_{a^{\prime }}$ whenever $a\ne a^{\prime }$, so $e$ is injective. It contains every true function-value equation, so $e$ commutes with all operations and constants. Positive and negative relation instances ensure both preservation and reflection of the relations. Thus $e$ is an embedding of first-order structures. If the expansion satisfies the elementary diagram, for every logical formula $\varphi$ and tuple $\vec{a}$ it also givesso $e$ is an elementary embedding of first-order structures.

The precise conclusion for an arbitrary expansion is an embedding of first-order structures, rather than a literal inclusion of the original carriers. The source's inclusion notation is correct when one uses the customary identification of $\mathcal{A}$ with its embedded copy, or requires the expansion to interpret $c_a$ as the actual element $a$ of a carrier already containing $A$. With that naming convention, $e$ is the inclusion and the requested two equivalences follow exactly.

Without the convention the literal wording fails, even in the first-order language of logical equality: singleton first-order structures with carriers $\{0\}$ and $\{1\}$ have a diagram-satisfying expansion by sending the first first-order structure's named point to $1$, but the first carrier is not a subset of the second. The embedding of first-order structures formulation proved above states the invariant result and makes the intended inclusion formulation precise.

Let $L_A$ expand $L$ by a constant $c_a$ for each $a\in A$, and let ${\mathcal{A}}_A$ be the canonical expansion interpreting $c_a$ as $a$. Its diagram of a structure is the set of all atomic and negated atomic $L_A$-sentences true in ${\mathcal{A}}_A$. Its elementary diagram is the set of all $L_A$-sentences true there:A substructure inclusion $\mathcal{A}\subseteq \mathcal{B}$ means that $A\subseteq B$, constants have the same interpretations, the operations of $\mathcal{B}$ restrict to those of $\mathcal{A}$, and each relation restricts to the corresponding relation on $A$.

An elementary substructure additionally preserves the truth of every logical formula with parameters from $A$:Here the right-hand condition includes the substructure requirements by applying it to atomic logical formulas and their negations.

Expand the ring first-order language by a new constant $c$ and considerEvery finite subset is satisfiable in the integer ring itself. Only finitely many divisibility conditions occur; interpret $c$ as a nonzero common multiple of their positive integer indices, using $1$ if none occur. All first-order sentences from $\mathrm{Th}(\mathbb{Z})$ are automatically true there.

Compactness theorem therefore gives a first-order model. Its reduct $R$ to the original ring first-order language satisfies the complete theory of $\mathbb{Z}$, so $R\equiv \mathbb{Z}$. Its element $c^R$ is nonzero and divisible by every positive standard integer. ThusSuch an element cannot be an ordinary nonzero integer, since an integer of absolute value less than $n$ cannot be a nonzero multiple of $n$. The statement concerns each standard integer index separately; it does not assert divisibility by every internally nonzero element of $R$.

The compactness theorem states that a set of first-order sentences has a first-order model if and only if every finite subset has a first-order model.

For the nontrivial direction suppose every finite subset of $\Sigma$ is satisfiable. If $\Sigma$ were inconsistent, a finite formal derivation of a contradiction would use only finitely many premises ${\Sigma }_0\subseteq \Sigma$. Soundness of an arithmetic theory would then exclude a first-order model of ${\Sigma }_0$, contradicting finite satisfiability. Therefore $\Sigma$ is first-order consistent. The completeness theorem, proved by adjoining witnesses and constructing a Henkin term model, supplies a first-order model of $\Sigma$.

The reverse direction is immediate by restriction of the list of required first-order sentences. The key reason compactness theorem follows from syntactic completeness is that every formal proof uses only finitely many premises, even when the whole first-order theory is infinite.

The set $\Sigma$ is satisfiable if there is one $L$-structure $\mathcal{A}$ satisfying every first-order sentence in $\Sigma$ simultaneously. It is finitely satisfiable if each finite subset ${\Sigma }_0\subseteq \Sigma$ has a first-order model; that first-order model is allowed to depend on the chosen finite subset.

Thus the two statements have different quantifier orders:Satisfiability immediately implies finite satisfiability by using the same first-order structure for every finite subset. The converse is the substantive content of compactness theorem.

An $L$-structure has a nonempty underlying set $A$. It assigns to each constant symbol $c_k$ an element $c_k^{\mathcal{A}}\in A$, to each $n$-ary function symbol $f_j$ a function $A^n\to A$, and to each $n$-ary predicate symbol $P_i$ a relation contained in $A^n$. Logical equality, when included as logical equality, is interpreted as actual identity.

The arities belong to the specification of the first-order language. An assignment of logical variables to elements of $A$ then evaluates first-order terms recursively and determines satisfaction of logical formulas through the logical connectives and quantifiers. A first-order sentence has no free variables, so its truth in the first-order structure is independent of the assignment.

Under the arithmetical interpretation $\square A=P_S(┌A┐)$, the Löb axiom says that a formal proof of the local reflection implication for $A$ already entails a formal proof of $A$:It is a formalized constraint on self-verification of a formal proof system. Externally, Löb's theorem says that if the system itself proves its own local reflection implication for $A$, it proves $A$. Distribution reflects closure of formal proofs under implication, necessitation reflects that a theorem has an arithmetically recognizable formal proof, and positive introspection reflects formal proof verification inside arithmetic.

Taking $A$ to be a refutable first-order sentence, especially a contradiction, recovers the obstruction behind the second incompleteness theorem: a first-order consistent sufficiently strong system cannot prove the corresponding claim that no formal proof of that first-order sentence exists. This does not identify provability with truth, nor grant the unrestricted factivity principle $\square A\to A$ as a theorem of the system. The Löb axiom is the characteristic additional scheme of Gödel–Löb provability logic.

Set $Y=\square X\to X$. The Löb axiom at $X$ is $\square Y\to \square X$. Therefore $Y$ and $\square Y$ together imply $X$, provingFor the converse, the tautology $X\to Y$ gives $\square X\to \square Y$ by necessitation and distribution. Consequently $\square Y\to X$ together with $\square X$ gives $X$, sowhose consequent is $Y$. Combining both directions gives an unboxed equivalence as a theorem of GL. Necessitation then yields exactly

Let $C=\square X\wedge X$. The normal distribution axiom and necessitation of $C\to X$ give $\square C\to \square X$. Combining this with propositional reasoning yields the theoremIndeed, $X$ together with $\square C$ supplies both conjuncts of $C$. Necessitate this theorem and apply distribution to obtainThe new Löb axiom at $C$ now gives $\square X\to \square C$. Finally, necessitation and distribution applied to the tautology $C\to \square X$ give $\square C\to \square \square X$. Composition provesNo positive-introspection instance was used in deriving it. The argument shows why that scheme can be dropped when the Löb scheme is added.

The source's system called $K$ already contains positive introspection, so its displayed axioms are those usually called $K4$. PutWe first show that its axioms prove $\square A\to A$, the implication suggested in the hint. From $B$, positive introspection gives $\square B$. Distribution applied to $\square A=\square (B\to \square X)$ and $\square B$ gives $\square \square X$. Distribution applied to $B=\square (\square X\to X)$ and this last result gives $\square X$. Thus the theorem-level implications combine by propositional reasoning intowhich is $K4⊢\square A\to A$.

Since $S$ contains these axioms, it proves that implication. Its assumed Löb inference rule, applied to the first-order sentence $A$, yields $S⊢A$. Unpacking $A$ provesThis uses necessitation only as part of the ordinary modal theorem rules; no inference of a boxed temporary assumption has been made.

Let $j=i+n$ with $n\ge 1$. Positive introspection supplies the theorem $F_k\to F_{k+1}$ for every $k\ge 1$, since $F_k$ itself has the form $P_S(┌F_{k-1}┐)$.

Induction on $n$ consequently givesAt $n=1$ this is the identity implication. To pass from $n$ to $n+1$, compose the induction hypothesis with the positive-introspection implication at $k=i+n$, which is at least one. Composing the result with the assumed $F_j\to F_i$ givesi.e. $S⊢P_S(┌F_i┐)\to F_i$. Löb's rule now yieldsThe index restriction on positive introspection has been respected even when $i=0$: the chain begins at $F_{i+1}$, which already is a provability assertion.

Take a first-order sentence $Y$ refutable in $S$ and suppose, toward contradiction, that a first-order consistent $S$ proved $\neg P_S(┌Y┐)$. Propositional logic would then giveLöb's inference, applied with $X=Y$, would give $S⊢Y$, contradicting the existing formal proof of $\neg Y$. Hence first-order consistency excludes the proposed formal proof of non-provability.

Thus the familiar unprovability of the first-order consistency statement associated with a refutable first-order sentence is a special consequence of the general ruleThe general rule applies to every first-order sentence, not just a chosen false or refutable one.

Put $T=S\cup \{\neg X\}$ and assume $S⊢P_S(┌X┐)\to X$. In $T$, contraposition against its extra axiom gives $\neg P_S(┌X┐)$.

Classical logic proves $(\neg X\to X)\to X$. By the derivability conditions,Compose this with the supplied formalized deduction implication from $P_T(┌X┐)$ to its left-hand side. Then $T$ provesand thereforeThe other supplied assumption says this is impossible if $T$ is first-order consistent. Thus $T$ is inconsistent. By the deduction theorem, inconsistency after adjoining $\neg X$ yields $S⊢\neg \neg X$, henceThis establishes Löb's inference rule using precisely the strengthened unprovability assumption and the formalized deduction property supplied in the question.

Use the Hilbert-Bernays-Löb derivability conditions for an arithmetical provability predicate. Abbreviate $P_S(┌A┐)$ by $PA$. The conditions needed below areThese are the usual theoremhood, distribution and positive-introspection conditions intended by a standard arithmetical provability predicate; arbitrary predicate symbols merely agreeing with provability externally need not satisfy them.

Since $S⊢\neg Y$, it proves $Y\to G$. The first two conditions give $S⊢PY\to PG$. For the converse, the fixed-point equivalence gives $S⊢G\to (PG\to Y)$. Applying theoremhood and distribution givesPositive introspection also gives $PG\to PPG$, and distribution combines these to yield $S⊢PG\to PY$. Thus $S⊢PG\leftrightarrow PY$. Combining with $G\leftrightarrow \neg PG$ provesIf $S$ proved $\neg PY$, it would prove $G$. The theoremhood condition would then give $PG$, while the fixed-point equivalence gives $\neg PG$. Therefore first-order consistency implies

If PA is first-order consistent and already proves $\neg X$, it cannot also prove $X$. By the correctness of the ordinary arithmetized arithmetical proof relation, $\mathbb{N}\models \neg {\mathrm{Pr}}_{PA}(┌X┐)$.

If PA is inconsistent, it proves $X$ by explosion, so an actual formal proof code witnesses ${\mathrm{Pr}}_{PA}(┌X┐)$ in the standard natural numbers. ThusThe hypothesis that $X$ is refutable is essential to this first-order consistency characterization for an arbitrary fixed first-order sentence.

If PA is inconsistent, every desired conclusion is already a theorem, so it suffices to analyze the first-order consistent case. Use $Q(u,v)$ for the bounded arithmetical proof relation and $\mathrm{neg}(u)$ for the code of the negation of the logical formula coded by $u$.

Suppose $PA⊢E_n$ and let $m$ be the code of an actual formal proof. By first-order consistency there is no formal proof of $\neg E_n$, in particular none with code at most $m$. Thusis a true bounded arithmetic sentence. Bounded completeness of an arithmetic theory proves it in PA, and existential introduction gives $PA⊢{\mathrm{Pr}}_{PA}^{\ast }(\bar{n})$.

Conversely suppose $PA⊢\neg E_n$ and choose an actual formal proof code $k$ of that negation. First-order consistency excludes every formal proof of $E_n$, so each of the finitely many statements $\neg Q(\bar{n},\bar{j})$ for $j<k$ is true and provable. The supplied finite-case theorem permits PA to combine them into the assertion that no formal proof code below $k$ proves $E_n$.

PA also proves $Q(\overline{\mathrm{neg}(n)},\bar{k})$. For any candidate formal proof code $v\ge \bar{k}$, this one code already refutes the universal no-earlier-negation condition in the Rosser predicate symbol. For $v<\bar{k}$, the finite verification refutes its positive formal proof condition. The supplied order dichotomy and finite-case expansion cover all $v$. ThereforeThe argument uses bounded verification of a finite initial segment and one fixed counter-witness beyond it; it does not infer that PA proves the absence of all ordinary formal proofs merely from first-order consistency.

Write $\rho ={\mathrm{Pr}}_{PA}^{\ast }(┌R┐)$. The supplied fixed-point equivalence gives $PA⊢R\leftrightarrow \neg \rho$.

If PA proved $R$, the first assumed property would give $PA⊢\rho$, while the equivalence would give $PA⊢\neg \rho$. This contradicts first-order consistency. If PA proved $\neg R$, the second assumed property would give $PA⊢\neg \rho$, and the reverse implication of the equivalence would give $PA⊢R$, again a contradiction. HenceThis is the Rosser improvement: its comparison of formal proof codes permits ordinary first-order consistency to exclude both alternatives, without assuming one-consistency.