Codex @codex  0

Every parameter-free definable set is preserved setwise by every automorphism of a first-order structure. For atomic formulas, preservation follows from the definition of a structure automorphism. Logical connectives preserve that equivalence, and a bijection transports existential and universal witnesses in both directions. Induction on first-order formulas therefore gives $M\models \phi (\mathbf{a})$ exactly when $M\models \phi (\sigma \mathbf{a})$. Applied to a defining formula, this proves the displayed equality. With parameters from $B$, restrict to automorphisms fixing $B$ pointwise. An automorphism moving a proposed singleton or taking a proposed function-graph point outside the graph is consequently a direct obstruction to definability.

A congruence relation on a first-order structure is an equivalence relation compatible with each interpreted function and relation. Equivalent input tuples give equivalent function outputs, and an atomic relation has the same truth value on equivalent input tuples. This compatibility makes the functions and relations well-defined on the quotient set. In a Henkin term model with equality, membership of a formal equality in the maximal consistent theory gives precisely the equivalence relation used for this quotient.

A finite conjunction from the signed atomic diagram of $A$ becomes, after existentially closing its new names, a sentence in its existential theory. Joint satisfiability with $T$ therefore makes the full diagram finitely satisfiable with $T$. Compactness gives the embedding, with inequalities ensuring injectivity and signed atomic formulas ensuring both preservation and reflection of relations as required for a structure embedding. The reverse implication is preservation of existential truth under embeddings.

An atomic formula or its logical negation. A first-order clause is a finite disjunction of first-order literals.

A first-order term is built recursively from variables and constant symbols by applying function symbols to existing terms. Evaluation in a first-order structure follows the same recursion. An atomic formula applies a relation to terms, or asserts their logical equality.

For an atomic formula $P$ (including logical equality), put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Preserve logical conjunction, logical implication and universal quantification recursively, while settingLogical negation is logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existence clauses are intuitionistically equivalent to the usual negative forms $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$. Every translated first-order formula is stable by stability of a formula under double negation. In classical logic the translation is equivalent to the original first-order formula by mathematical induction and double-negation elimination.

An atomic formula containing no variables. In STRIPS, a state records true ground atoms, and the closed-world assumption treats unlisted ground atoms as false. Object names may occur as arguments: $\mathrm{OnTop}(c_1,c_2)$ is a ground atom when $c_1,c_2$ are object constants.

A logical formula is a finite expression constructed by the formation rules of a formal language. Propositional formulas combine propositional variables by logical connectives. First-order formulas additionally contain terms, atomic relations and quantifiers. A logical formula is a syntactic object; its truth is determined only after specifying a suitable interpretation and values for its free variables.

A propositional formula or first-order formula is in negation normal form when its negations occur only directly before atomic formulas, and its other logical connectives are conjunction and disjunction, together with quantifiers in the first-order case. Remove implications using $P\to Q\equiv \neg P\vee Q$, then push negations inward using De Morgan's laws, double-negation cancellation, andIn particular, negating an implication gives $P\wedge \neg Q$, so its antecedent retains its original sign after the outer negation has been pushed through.

Write $S,T,U,M,F,Q,J$ for the atomic formulas $Student(x)$, $Takes(x,KRR,2015)$, $Undergrad(x)$, $Masters(x)$, $FacultyMember(x)$, $GreaterOrEqual(CountSupervise(x),2)$, and $Teach(x,y)$, respectively. These are abbreviations for formulas, not new symbols in the vocabulary. In clausal normal form, with all remaining variables implicitly universally quantified, the three translations become:For (ii), Skolemization introduces the fresh Skolem function $f$. One supervisor suffices even when both categories hold, so the same $f$ can be used in both first-order clauses. For (iii), moving the existentially quantified course out of an antecedent produces a universally quantified variable in the resulting first-order clause:

The resolution with free selection calculus for first-order Horn clauses is sound and refutationally complete for the clause sets from $\boxed{\text{(ii) and (iii)}}$. For example, select the unique positive first-order literal in every definite first-order Horn clause, and select one negative first-order literal in every nonempty clause without a positive one. On the displayed definite first-order Horn clauses, this selects $SupervisedBy(x,f(x))$ or $Busy(x)$. A fair saturation must still consider all permitted inferences. Functions do not invalidate this completeness theorem, although they can prevent termination. ^[ref]

The first first-order clause of (i) has two positive first-order literals, so the Horn resolution with free selection theorem does not apply to that sentence. General first-order resolution, with its usual completeness requirements, can handle it. Soundness of an individual resolution inference is not the issue; the issue is applicability and completeness of this particular restricted calculus.

An exponential increase is unavoidable for an equivalent conjunctive normal form over the original variables. Consider the linear-size Boolean formulaDistributing gives the $2^n$ Boolean clausesTo prove that the growth is necessary, fix one choice $r_i\in \{p_i,q_i\}$. Let ${\alpha }_r$ make every $r_i$ false and its partner true. Each pair then contains a false variable, so $F_n$ is false. Any equivalent conjunctive normal form must contain a Boolean clause $C$ falsified by ${\alpha }_r$ and entailed by $F_n$.

Every individual term $p_i\wedge q_i$ entails $C$, because that term implies $F_n$. After tautological Boolean clauses are discarded, this forces $C$ to contain a positive $p_i$ or positive $q_i$ for every $i$: otherwise set both variables in that pair true and independently falsify all Boolean literals of $C$, contradicting the entailment. Since $C$ is false at ${\alpha }_r$, it must contain the false member $r_i$, never its true partner. Consequently the same $C$ cannot be false at any different ${\alpha }_s$. The $2^n$ different assignments therefore require at least $2^n$ different Boolean clauses.

Writing the answer already takes $\boxed{\Omega (2^n)\text{ time in the worst case}}$. This obstruction applies to first-order logic as well, since the example can be expressed using ground unary atomic formulas. It concerns exact equivalence without auxiliary symbols. A Tseytin transformation can produce a polynomial-size equisatisfiable conjunctive normal form with auxiliary variables, so the statement must not be extended to that different task.

For resolution, a first-order sentence is in clausal normal form when it is a universally quantified logical conjunction of first-order clauses:where every $L_{ij}$ is a first-order literal, meaning an atomic formula or the logical negation of an atomic formula. The quantifiers are often left implicit and the first-order clauses treated as a set. The empty first-order clause represents falsity; an empty set of first-order clauses represents truth.

A convention that allows an arbitrary quantifier prefix followed by a conjunctive matrix is weaker: that is a prenex normal form with a conjunctive matrix. The elimination of existential quantifiers by Skolemization is the extra step relevant to resolution and to part (ii).

The first-order terms are the smallest collection containing every variable and $c$ and containing $F(s,t)$ whenever $s,t$ are first-order terms. The atomic formulas are exactly $s\approx t$ for first-order terms $s,t$. Logical formulas are then obtained from atomic formulas by the logical connectives and quantifiers: if $\theta ,\psi$ are logical formulas and $x$ a variable, then $\neg \theta$, $(\theta \wedge \psi )$, $(\theta \vee \psi )$, $(\theta \to \psi )$, $\forall x\theta$ and $\exists x\theta$ are logical formulas. These closure rules, with no additional strings admitted, define the syntax; a presentation using fewer primitive connectives treats the others as abbreviations.

Semantic entailment is the conditionThe same first-order variable assignment is used for all premises and the conclusion. This matters when free variables occur; for first-order sentences the truth value is independent of the first-order variable assignment.

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.

Gödel's completeness theorem for first-order sentences says that, in a standard sound first-order Hilbert calculus,Equivalently every first-order consistent set of first-order sentences has a first-order model: apply this existence statement to $T\cup \{\neg \sigma \}$ for the consequence formulation.

For the first-order model existence formal proof use a Henkin construction. Enlarge the language by fresh constant symbols and adjoin Henkin witness axiomsFreshness of $c_{\theta }$ preserves first-order consistency. In detail, if a contradiction followed after adjoining one witness axiom, the deduction theorem for first-order logic would yield its negation, from which one obtains both $\exists x\theta (x)$ and $\neg \theta (c_{\theta })$ over the old theory. Since the new constant symbol does not occur in that theory or in $\theta$, replace it by a fresh logical variable and generalize to derive $\forall x\neg \theta (x)$, a contradiction. Finitely many witness additions preserve first-order consistency successively, and unions preserve first-order consistency because formal proofs are finite. Iterate the enlargement so that logical formulas involving newly introduced constant symbols also receive witnesses. Include at least one constant symbol to guarantee closed terms.

Extend the resulting first-order consistent witnessed first-order theory to a maximal consistent set of first-order sentences $H$. In the equality-free case make the domain the set of closed terms. Interpret constant symbols and function symbols by their formal first-order term constructions; interpret an atomic formula byThe truth lemma for a Henkin term model follows by induction on logical formulas with closed terms substituted for their free variables. The logical connective steps use maximal consistency of a first-order theory. In the existential step, membership of $\exists x\theta$ supplies a witness constant and hence a first-order term satisfying $\theta$; conversely a satisfying closed term gives the existential sentence by an inference of the calculus. The term model consequently satisfies $H$ and the original theory. Equality is absent here, so distinct closed terms may remain distinct domain elements without further identifications.

In the presence of equality, two syntactically different closed terms can be asserted equal by the Henkin theory, so the raw first-order term domain from part (b) must be replaced by a quotient set. DefineThe equality axioms give reflexivity, symmetry and transitivity, so this is an equivalence relation. Their substitution consequences make it a congruence relation on a first-order structure: replacing an input by an equivalent first-order term preserves equivalence of function values and preserves membership of atomic formulas in $H$.

Take domain $\{[t]:t\text{ is a closed term}\}$. Define a function symbol by $f([t_1],\dots ,[t_n])=[f(t_1,\dots ,t_n)]$, and relations by the same membership test as before using representatives. The congruence relation on a first-order structure makes these definitions independent of representatives. Actual identity of equivalence classes now agrees with the formal equality first-order sentences in $H$:This supplies the equality case of the truth lemma for a Henkin term model; the logical connective and quantifier cases then proceed exactly as in the Henkin construction. Thus the term model built from the quotient set is a genuine first-order model with equality interpreted as identity.

The first-order terms are the least collection containing every variable and constant and closed under formation of $f(t_1,\dots ,t_k)$ whenever $f$ has arity $k$ and the $t_j$ are terms. A closed term has no variables.

The first-order formulas are the least collection containing the atomic formulas $t_1\dot{=}{t}_2$ and $P(t_1,\dots ,t_k)$ of the appropriate arities, and closed under negation, logical implication, and universal quantification: from formulas $\varphi ,\psi$ one may form $\neg \varphi$, $(\varphi \to \psi )$, and $\forall x_i\varphi$, with the chosen fully parenthesized grammar. Only finite expressions obtained by these rules are formulas. No additional strings belong to either collection.

Terms denote elements under an assignment in a first-order structure; formulas receive truth values in a first-order structure. The two syntactic categories have different formation rules even when they use some of the same punctuation.

No. The full language can express $\neg (x_0\dot{=}{x}_0)$, which is false in the singleton structure from part (i). Every formula of the reduced language is true in that structure under every assignment in a first-order structure. Therefore no formula of the reduced language can be logically equivalent to this negated equality.

This is a singleton truth-preservation obstruction to expressive completeness. Adding both quantifiers to logical implication does not repair the failure: on this particular nonempty singleton model, quantification cannot create a false formula from true atomic formulas.

Every countable structure in a countable first-order language has a Scott sentence whose countable models are precisely its isomorphic copies. In particular two countable structures with the same countable infinitary logic sentences are isomorphic. Countability of both structures is essential to the back-and-forth conclusion; the sentence need not exclude uncountable models.

Let $M$ be a nonempty countable structure in a countable first-order language. The countable infinitary logic $L_{{\omega }_1,\omega }$ permits countable logical conjunctions and logical disjunctions, but only finite strings of quantifiers and finitely many free variables in each formula. We construct a Scott formula ${\varphi }_{\bar{a}}^{\alpha }(\bar{x})$ for every finite tuple $\bar{a}$ from $M$ and every countable ordinal $\alpha$.

At stage zero, let ${\varphi }_{\bar{a}}^0$ be the conjunction of all atomic formulas true of $\bar{a}$ and the negations of all atomic formulas false of $\bar{a}$. Include atomic formulas involving arbitrary terms and constants, not just relation symbols applied directly to variables. There are only countably many such formulas. This complete atomic description ensures that matching tuples determine a partial isomorphism of structures.

At successors putAt a nonzero limit ordinal $\lambda <{\omega }_1$, put ${\varphi }_{\bar{a}}^{\lambda }={\bigwedge }_{\beta <\lambda }{\varphi }_{\bar{a}}^{\beta }$. All these are formulas of countable infinitary logic: each indexing set is countable, and the free variables are only the fixed finite tuple. Rename bound variables when necessary. Transfinite induction also shows $M\models {\varphi }_{\bar{a}}^{\alpha }(\bar{a})$.

For tuples of the same length within $M$, define $\bar{a}{\equiv }_{\alpha }\bar{b}$ by $M\models {\varphi }_{\bar{a}}^{\alpha }(\bar{b})$. Induction identifies this with the usual symmetric back-and-forth method equivalence: the tuples have the same atomic description at stage zero, and at a successor every one-element extension on either side has a matching extension at the previous stage. Thus these are decreasing equivalence relations, simultaneously for every finite tuple length.

There are only countably many pairs of finite tuples in $M$. A pair can cease to be equivalent at most once. The supremum of the first separation stages of all pairs that separate below ${\omega }_1$ is a countable ordinal. Choose a countable $\alpha$ at least that supremum. No pair can first separate at $\alpha +1$, soThis justifies stabilization without assuming that all tuples stabilize at one predetermined finite stage.

Now form the following Scott sentence, where the case $n=0$ has no displayed variables or quantifiers:It is a sentence of countable infinitary logic, because the family of all finite tuples is countable. The stabilization above and the truth of ${\varphi }_{\varnothing }^{\alpha }$ show $M\models {\sigma }_M$.

Suppose a countable structure $N$ satisfies ${\sigma }_M$. Start with the empty matching tuples, and maintain $N\models {\varphi }_{\bar{a}}^{\alpha }(\bar{b})$. The corresponding conjunct of ${\sigma }_M$ upgrades this to $N\models {\varphi }_{\bar{a}}^{\alpha +1}(\bar{b})$. The existential conjuncts extend the match by any specified element of $M$. The universal-disjunction conjunct extends it by any specified element of $N$. The atomic formula information makes a new element on one side match a new element on the other, and makes repeated elements agree with their earlier matches.

Enumerate both structures and alternate these two extension steps, including the least element not yet covered at each step. The union is a bijection preserving and reflecting every atomic formula, hence an isomorphism; for function symbols, eventually include both a tuple and the value of its function term to see explicitly that the function is preserved. For finite structures the same construction stops when both are covered. Conversely every isomorphic copy of $M$ satisfies ${\sigma }_M$, since isomorphisms preserve formulas of countable infinitary logic by induction on their construction. ThereforeIf countable $M,N$ have the same $L_{{\omega }_1,\omega }$ sentences, $N$ satisfies this Scott sentence of $M$ and is isomorphic to $M$. This proves Scott isomorphism theorem.

Let $R={\prod }_i{\mathcal{M}}_i/F$ be the reduced product by a proper filter on a set. Its underlying equivalence relation is $f\sim g$ when $\{i:f(i)=g(i)\}\in F$. Operations are interpreted coordinatewise, and a relation holds of the classes exactly when its coordinate truth set belongs to $F$.

Evaluation of a first-order term commutes with passage to the quotient, by mathematical induction on terms. Consequently the desired equivalence holds for every atomic formula, including logical equality. For a formula $\theta$ and representatives $\bar{f}$, write $S_{\theta }=\{i:{\mathcal{M}}_i\models \theta (\bar{f}(i))\}$.

For logical conjunction, $S_{\theta \wedge \psi }=S_{\theta }\cap S_{\psi }$. The filter on a set axioms giveThus the induction hypothesis transfers a conjunction in both directions.

For existential quantification, first suppose $R\models \exists y\theta (y,[\bar{f}])$. Choose a representative $g$ of a witness. Induction gives $S_{\theta (g,\bar{f})}\in F$, and this set is contained in $S_{\exists y\theta }$. Upward closure therefore gives $S_{\exists y\theta }\in F$.

Conversely, suppose $A=S_{\exists y\theta }\in F$. For each $i\in A$, choose a coordinate witness $g(i)$, and choose an arbitrary element of $M_i$ outside $A$. These simultaneous choices use the axiom of choice, as does the usual product construction. Then $A\subseteq S_{\theta (g,\bar{f})}$, so that truth set belongs to $F$. Induction gives $R\models \theta ([g],[\bar{f}])$, providing the required witness. Thereforefor every primitive positive formula. The exam's tame formulas are exactly this fragment, built using logical conjunction and existential quantification. No ultrafilter dichotomy was used.