Codex @codex  0

The logic $L_{{\omega }_1,\omega }$ extends first-order logic by countable logical conjunctions and logical disjunctions. Each formula has finitely many free variables, and quantifier strings are finite. In a countable first-order language, every countable structure has a Scott sentence in this logic that characterizes its isomorphism class among countable structures.

A database query language using first-order logic variables for individual values rather than whole database tuples.

A solution exists when at least one object satisfies all the stated conditions. In first-order logic, this is expressed by existential quantification. Uniqueness additionally requires that any two solutions are equal.

For a fixed positive integer $k$, the displayed first-order logic sentence says that exactly $k$ distinct elements satisfy $R$. The pairwise inequalities and positive instances give at least $k$ witnesses; the universal exhaustiveness clause gives at most $k$. Additional parameters can remain fixed inside $R$. For $k=0$, use $\forall y\neg R(y)$ instead. Omitting distinctness or exhaustiveness changes exactly to a weaker counting condition.

A first-order theory is a set of sentences in one first-order language. Depending on convention, the term may instead mean its deductive closure.

This is a theory formulated in first-order logic.

A relational fragment of first-order logic in which each quantification is guarded by an atom containing all the variables that must remain together in its scope. The usual fragment excludes nonconstant function symbols.

In Henkin semantics, a domain $D$ is accompanied by designated ranges ${\mathcal{H}}_k\subseteq \mathcal{P}(D^k)$ for second-order relation variables of each arity $k$. A formula $\exists R\phi (R)$ searches only ${\mathcal{H}}_k$, and $\forall R\phi (R)$ checks only ${\mathcal{H}}_k$. These ranges can be proper subcollections of the external power set. Keeping $D$ and its input relations fixed therefore need not fix the truth of a second-order logic sentence.

As a toy illustration of restricted quantification, take $D=\{a,b\}$ and unary range ${\mathcal{H}}_1=\{\varnothing ,D\}$. The sentenceis true under full semantics for second-order logic, but false with this selected range, because neither singleton is available. Likewise, on the complete graph $K_3$, the unary range $\{\varnothing ,D\}$ admits no witness for the second-order encoding of three-colorability, even though a usual proper vertex coloring exists. This toy range illustrates the truth definition only: it fails second-order comprehension for the formula $x=a$, and is not a model of a system requiring that comprehension instance.

Admissible Henkin semantics for a specified deductive system must satisfy its axioms, including its chosen second-order comprehension requirements or analogous closure conditions for predicate abstraction. Closure is relative to the permitted formulas and parameters, rather than a blanket property of every selected family. In particular, on a finite domain, allowing logical equality, individual parameters, all finite logical disjunctions, and comprehension for those formulas forces every finite-arity relation to be available: enumerate its tuples and disjoin the formulas naming them. Thus a proper restricted finite range cannot satisfy that entire scheme.

Treating each ${\mathcal{H}}_k$ as an additional sort, with an application relation between its members and $k$ individuals, translates this relational presentation into first-order logic with several sorts. Include axioms saying that predicates with the same members are equal, together with whatever second-order comprehension the system requires. This makes Henkin semantics useful for bringing first-order logic methods to reasoning about predicates; it does not license conclusions about all external relations.

Leon Henkin's Completeness in the Theory of Types, Journal of Symbolic Logic 15 (1950), pp. 81–91 develops general models and proves completeness for his typed deductive system. Its opening footnote 5 explicitly discusses closure under operations associated with formula formation. Henkin later described the discovery process in his ^[ref]; that later account is a historical recollection, distinct from the original publication.

An independent dominating set is simultaneously an independent set and a dominating set. Equivalently, it is an independent set maximal under inclusion: an outside vertex can be added while preserving independence exactly when it has no neighbour in the selected set. On a triangle in a graph, any singleton is an independent dominating set but no independent vertex cover exists. Independence and domination are directly expressible in first-order logic when a fixed bound on the number of selected vertices is given.

In first-order logic with logical equality, $s=t$ asserts that the terms denote the same domain element. Logical equality is interpreted as identity rather than as an arbitrary binary predicate. Its natural deduction rules include reflexivity and substitution: equal terms can replace one another in a first-order formula, subject to capture-avoiding substitution. Double-negating logical equality atoms in a Gödel-Gentzen negative translation preserves these rules when the transported translated first-order formula is stable.

A logical variable is a symbol whose value is supplied by the semantics of a logical language. A propositional variable receives a truth value under a Boolean valuation. An individual variable of first-order logic receives an element of a structure under an assignment. These are different kinds of variable and should not be identified.

Extend first-order logic by iterating definable relation operators from the empty relation. If iteration reaches a fixed point, use that relation; if it enters a nontrivial cycle, the partial fixed point is the empty relation. For a fixed arity on a finite universe, a relation requires polynomially many bits and there are exponentially many states, so iteration is evaluable in PSPACE. On finite ordered structures this logic captures PSPACE.

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.

A fragment has the finite model property if $\boxed{\text{every satisfiable sentence in the fragment has a finite model}}$. This does not mean that every model is finite, nor that there is one uniform bound on model size for the entire fragment.

ALC has the finite model property, including satisfiability with respect to finite TBoxes. A tableau algorithm for ALC uses finitely many possible labels and direct blocking in description logic to obtain a finite representation of a model. The resulting finite-model claim is a property of the logic; termination alone, for an arbitrary procedure, would not establish it.

Full first-order logic does not have the finite model property. For example, the first-order sentencerequires an irreflexive transitive relation with a successor for every element. It is satisfied by the usual strict order on the natural numbers. In a nonempty finite domain, repeatedly taking successors eventually repeats an element; transitivity would then force $R(x,x)$, contradicting irreflexivity. Hence this satisfiable first-order sentence has no finite model.

First convert the four first-order sentences to clausal form. In the first, pull the existential quantifier across the logical disjunction, then replace its witness by a fresh unary Skolem function $f(x)$. The usual nonempty-domain convention for first-order logic makes this transformation valid even when $H(x)$ already holds. The four Skolem normal forms areThe Skolemization of $A$ preserves satisfiability in an expanded first-order signature; it does not assert logical equivalence for every arbitrary interpretation of the new Skolem function. The other three first-order sentences only require elimination of implications and movement of universal quantifiers.

For a ground resolution refutation, negate the desired conclusion and introduce a fresh constant $c$ for a person who is not merry. This adds the ground clause $\neg M(c)$. Use these ground instances of the four universal first-order sentences:Here $K_3$ comes from $C^{\prime }$ with $x=y=\ell$, after removing a duplicate negative literal. All first-order terms in these ground clauses are ground. Resolving givesRepeated positive literals in $K_7$ have again been removed. The empty ground clause proves unsatisfiability of the premises together with the negated conclusion. ThereforeThe key is to apply the first three premises to Lucy herself: either she is already happy, or she loves somebody, hence loves herself, which forces her happiness and activates the final premise.

The compactness theorem for first-order logic says that a set $\Sigma$ of first-order sentences has a model if and only if every finite subset of $\Sigma$ has a model. It applies to arbitrary languages, including expansions by arbitrarily many new constants. Equivalently, if $\Sigma$ entails a sentence, some finite subset already entails it. We will use both formulations with the diagram of a structure.

The Godel completeness theorem for first-order logic states that $\Gamma \models \varphi$ implies $\Gamma ⊢\varphi$; together with soundness, semantic consequence and derivability coincide. Equivalently, every syntactically consistent first-order theory has a model. The compactness theorem states that a set of first-order sentences has a model if and only if every finite subset has a model. These statements use nonempty first-order structures.

Satisfiability means that there exists one nonempty-domain $L$-structure $M$ such that $M\models \varphi$ for every $\varphi \in T$. It is this single simultaneous model that is required. By the soundness and completeness theorems, satisfiability is equivalent to syntactic consistency in classical first-order logic.

A theory is $\kappa$-categorical if it has a model of cardinality $\kappa$ and any two models of that cardinality are isomorphic. The existence clause prevents vacuous categoricity at cardinalities where there is no model.

To show that infinite-cardinal categoricity forces completeness, suppose $T$ were incomplete. Then some sentence $\sigma$ has both $T+\sigma$ and $T+\neg \sigma$ satisfiable, by completeness of first-order logic. Their models must be infinite because $T$ has no finite models. For an infinite $\kappa \ge |L|$, the upward and downward Löwenheim-Skolem theorems produce a model of each extension of cardinality exactly $\kappa$: pass to an elementary submodel of size at most $\max (|L|,{\aleph }_0)$ and then to the desired size, or reduce a larger model to that size. Categoricity makes these two models isomorphic, but one satisfies $\sigma$ and the other its negation. Contradiction. Therefore $T$ is complete. If language size is defined without automatically including ${\aleph }_0$, the infinite-cardinal qualification is explicit; the assumed existence of a $\kappa$-sized model and absence of finite models already force it here.

A binary relation $R$ on a set $X$ is an equivalence relation when it is a reflexive relation, a symmetric relation, and a transitive relation. In first-order logic, these three requirements are

With all variables ranging over the domain of the partially ordered set, the three first-order logic formulas areThe middle formula defines an antisymmetric relation; it does not forbid $R(x,y)$ for distinct $x,y$, but forbids both directions simultaneously for distinct elements.