Codex @codex  0

Morleyization adds a predicate symbol for each first-order formula and an axiom equating that predicate symbol with its defining logical formula. Every original first-order model has a unique expansion. Translating an expanded logical formula back to the original first-order language and then using its named predicate symbol gives quantifier elimination. Completeness of the original first-order theory implies completeness of the expanded first-order theory.

An $L$-structure consists of a nonempty domain $A$, an element $c^{\mathcal{A}}\in A$ for each constant symbol, a function $f^{\mathcal{A}}:A^n\to A$ for each $n$-ary function symbol, and a relation $R^{\mathcal{A}}\subseteq A^n$ for each $n$-ary predicate symbol. When equality is part of the logic it is interpreted as actual identity on $A$.

An assignment in a first-order structure is a function $s$ from logical variables to $A$. It induces a term valuation of first-order terms recursively:For an atomic formula, substitute these first-order term values into the interpreted relation, or compare them for equality. Extend satisfaction for a set structure through the truth tables of the logical connectives, and through the quantifier clausesThus the first-order structure and assignment in a first-order structure together determine truth values for all logical formulas. A first-order sentence has no free variables, so its truth does not depend on the assignment in a first-order structure.

Take $\alpha =\beta =P(x)$ for a unary predicate symbol. The premise $\forall x(P(x)\to P(x))$ is valid, but the proposed conclusion is $P(x)\to \forall xP(x)$. On a domain $\{0,1\}$ with $P=\{0\}$ and assignment $x\mapsto 0$, its antecedent is true and its consequent false.

Hence dropping the condition that $x$ is not free in $\alpha$ would turn a valid premise into an invalid conclusion. The condition permits the antecedent to remain fixed while the quantified variable ranges over the domain; an antecedent depending on that variable cannot be held true for all its values merely because it is true at the current assignment.

A first-order structure consists of a nonempty domain $A$, an interpretation $c^A\in A$ of each constant symbol, a total function $f^A:A^n\to A$ for each $n$-ary function symbol, and a relation $R^A\subseteq A^n$ for each $n$-ary predicate symbol. Logical equality is interpreted as actual identity.

An assignment in a first-order structure is a map $s$ from the variables into $A$. It extends recursively to terms: $x^A[s]=s(x)$, $c^A[s]=c^A$, and $f(t_1,\dots ,t_n{)}^A[s]=f^A(t_1^A[s],\dots ,t_n^A[s])$. Atomic truth is determined by membership of the resulting tuple in $R^A$, or equality of the two term values. Negation reverses the truth value, and an implication is false exactly when its antecedent is true and its consequent false.

For a universal quantifier,These clauses define a valuation on every formula by structural recursion. Only free-variable values affect a formula's truth; consequently a sentence has the same truth value under every assignment. This is a semantic assignment of domain elements, not a programming assignment operation.

The alphabet of a first-order language separates logical symbols from nonlogical symbols. In the standard presentation here the logical symbols are the variables $x_0,x_1,\dots$, equality $\dot{=}$, negation $\neg$, logical implication $\to$, the universal quantification $\forall$, and the punctuation symbols parentheses and comma. The nonlogical symbols are constant symbols, function symbols of each specified finite arity, and predicate symbols of each specified finite arity, such as $f_n^{(k)}$ and $P_n^{(k)}$.

Constants can equivalently be treated as zero-ary function symbols. Their arities belong to the language specification. Other logical connectives, and $\exists x\varphi$ as an abbreviation for $\neg \forall x\neg \varphi$, need not be primitive alphabet symbols. This distinction matters in counting literal symbol occurrences.

Write $\square A$ for $P(┌A┐)$. A standard arithmetical provability predicate obeys the Hilbert-Bernays-Löb derivability conditions:The first condition is a rule about theorems; the latter two are statements proved within the first-order theory. When the terminology also includes external adequacy, require that $P(\bar{n})$ be true in the standard natural numbers exactly when the logical formula with code $n$ has an $S$-proof.

For Peano arithmetic, code finite strings, logical formulas and formal proof sequences by natural numbers. Formal proof checking is effective and has an arithmetized bounded checking relation with its computation data. Existentially assert the existence of a correct formal proof code and any required checking data. The resulting predicate symbol is Sigma-1, and its standard truth means exactly that an actual finite PA formal proof exists. Effective operations on formal proof codes combine an implication formal proof with an antecedent formal proof, and turn a formal proof into a formal proof that its code is a formal proof; PA verifies those constructions. They give distribution and positive introspection, while an actual theorem's finite formal proof gives its internal provability assertion. This is the requested rough construction, with the three internal formal proof properties distinguished from external agreement.

Take $\square A={\mathrm{Pr}}_{PA}(┌A┐)$ for the standard formal proof predicate symbol and putUse as given the arithmetization of syntax in PA, the derivability conditions, and the diagonal lemma. The latter supplies the fixed point needed in (a), and the former conditions interpret its normal modal distribution, necessitation on theorems and axiom4. Thus the argument in (a) proves the internal Löb implication in PA. With $X=\perp$ it readsThe inner implication is the first-order consistency first-order sentence $\neg \square \perp$, so contraposition givesThis is the arithmetic statement of the second incompleteness theorem proved within PA: if PA is first-order consistent, there is no PA formal proof of its first-order consistency first-order sentence. The displayed implication is a PA theorem without assuming that PA proves its antecedent.

For the corresponding external consequence, if a first-order consistent PA proved ${\mathrm{Con}}_{PA}$, theoremhood would give a formal proof of its boxed assertion. The displayed theorem together with the supposed formal proof of first-order consistency gives its negation, contradicting first-order consistency. Hence an externally first-order consistent PA does not prove its own first-order consistency.

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.

Let $C$ denote the addition-commutativity first-order sentence and put $d=┌\neg C┐$. In the ordinary checker for PA derivations, replace the axiom test ${\mathrm{Ax}}_{PA}(u)$ byKeep all tests for sequence formation, earlier lines, logical axiom schemes and inference rules unchanged. This gives a formal proof checker $Q_S(u,w)$ which recognizes exactly ordinary $S$-derivations. The finite syntactic modification is arithmetizable by the same bounded coding apparatus as the original checker.

For the proof-order comparison in the next part, make the choice of coding explicit. Reserve code $0$ for the one-line derivation of the newly added axiom $\neg C$, and give an ordinary derivation with code $w$ the new code $w+1$. A corresponding bounded relation isEvery code has a specified decoding, every genuine formal proof is represented, and no false formal proof is admitted. The reserved code duplicates one genuine derivation, which is harmless. This is one explicit arithmetized arithmetical proof relation obtainable from the PA checker by the requested axiom change and a simple renumbering. Stating the proof-order convention matters because a Rosser predicate symbol uses code order, not merely the existence of formal proofs.

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

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.

Add a predicate symbol $P_{\theta }$ for each $L$-formula $\theta (\vec{x})$, of arity equal to its displayed free-variable tuple. Let $T^{+}$ consist of $T$ together with all defining axiomsEvery first-order model of $T$ has a unique such expansion, interpreting the new predicate symbols by their defining sets. Conversely the reduct of every first-order model of $T^{+}$ satisfies $T$.

Given an arbitrary $L^{+}$-formula $\psi (\vec{x})$, replace each new atomic predicate symbol by its original $L$-definition, renaming bound variables to avoid capture. This produces an $L$-formula ${\psi }^{-}(\vec{x})$ withThe defining axiom for that particular logical formula now gives an atomic replacement:Thus the expanded first-order theory eliminates quantifiers. For a first-order sentence, the same translation is an $L$-sentence, decided by completeness of $T$; hence every expanded first-order sentence is decided and $T^{+}$ is complete. Empty free-variable tuples can be handled by zero-ary predicate symbols, or by the usual logical truth and falsity constants. This definitional expansion is called Morleyization.

A predicate symbol of arity $k$ is interpreted as a subset of the $k$th Cartesian power of a structure's domain. Applying it to $k$ first-order terms gives an atomic formula. In a singleton domain there is only one possible argument tuple at each arity, but a predicate may still be interpreted as either the empty relation or the full relation.

In a first-order structure, an interpretation assigns a relation of the specified arity to each predicate symbol, a total function of the specified arity to each function symbol, and an element to each constant symbol. Evaluation of first-order terms and truth of logical formulas are then defined recursively. This specifies how symbols acquire their meanings on the underlying set.