Codex @codex  0

The universal consequences $T_{\forall }$ of a first-order theory $T$ are all universal first-order sentences entailed by $T$. Their model class is exactly the class of substructures of models of $T$, up to structure embedding. This characterization follows from the diagram embedding criterion for universal theories.

A universal sentence has the form $\forall \mathbf{x}\psi (\mathbf{x})$ with quantifier-free formula $\psi$, including an empty quantifier block. Its truth passes from a first-order structure to every substructure of a first-order structure: tuples from the smaller domain are also tuples of the larger domain, and quantifier-free truth agrees. Therefore a first-order theory of universal sentences has a first-order model class closed under substructures of a first-order structure.

If $B$ satisfies the universal theory of $A$, every existential sentence true in $B$ is true in $A$, since its falsehood in $A$ would supply a universal negation. Apply the existential-theory embedding criterion to $B$ and the complete theory of $A$ to obtain $A^{\ast }$. Conversely universal truth descends to substructures. The elementarily equivalent model need not be the original structure itself.

Consider extending $S+{\mathrm{Con}}_S$ by a rule sending every ${\mathrm{Con}}_A$ to ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. Put $A=S+\neg {\mathrm{Con}}_S$. The initial consistency axiom proves ${\mathrm{Con}}_A$ by the negated-consistency extension theorem, so the rule proves ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. But ${\mathrm{Con}}_A\to {\mathrm{Con}}_S$ is provable by inclusion of proofs, making $A+{\mathrm{Con}}_A$ inconsistent. Arithmetic verifies its finite contradiction proof. Thus the unrestricted rule proves both that theory's consistency and inconsistency. This differs from an externally justified progression along specified sound theories.

A logical formula weakly defines a total numerical function in a first-order theory when, at every standard input tuple, it proves the graph instance with the correct standard output and refutes graph instances with every incorrect standard output. This is numeralwise representation of the graph; it does not yet assert uniqueness against nonstandard outputs inside a first-order model.