Formal languages, structures, and satisfaction

A first-order signature declares constant, function, and relation symbols with fixed finite arities. Terms are built recursively from variables, constants, and function application. Atomic formulas assert relations between terms or their equality; connectives and quantifiers build larger formulas. A structure supplies a nonempty domain, an element for each constant, a total operation for each function symbol, and a relation for each relation symbol. Equality is interpreted as actual equality in the domain.

An assignment maps variables into the domain. Term evaluation follows the term's recursive construction, so a variable's current assigned value is different from its printed name. A sentence has no free variables, and its truth is independent of the assignment. Open formulas usually depend on assignments. Renaming a bound variable preserves meaning, but substituting a term requires avoiding variable capture: inserting a free variable beneath an unrelated quantifier can change its intended dependency.

Existential satisfaction permits choosing one domain element, while universal satisfaction requires every domain element. In a universally quantified existential assertion, the existential witness may depend on the universal input. Reversing the order requires one witness that works simultaneously for all inputs. This distinction survives even in tiny finite structures, where checking a table is possible. It should be understood as a dependency statement rather than merely a rule for rearranging printed symbols.

For a domain of six residues, interpret f as addition of two modulo six and P as the three even residues. The operation is a permutation, so every element has a preimage, including the odd elements. Starting at zero and repeatedly applying f visits only the even residues. Reachability from a designated constant is therefore different from quantification over the whole domain. A single displayed orbit cannot by itself establish a claim about all domain elements.

Satisfaction says that a structure meets specified sentences. Semantic consequence means every model of a theory satisfies a conclusion, and validity is consequence from no assumptions. Syntactic derivability instead asserts the existence of a finite proof in a fixed calculus. Syntactic consistency means no contradiction is derivable; satisfiability means some structure exists. Their equivalence for classical first-order logic needs the soundness and completeness theorems, rather than belonging to the definitions.

Even when a finite structure satisfies every sentence of a theory, those sentences need not describe the intended natural numbers or any other intended object uniquely. Conversely, an expression being false in the residue structure says nothing by itself about its derivability from unrelated arithmetic axioms. Explicitly name the language, premises, calculus, and model class whenever moving between these judgments. Later undecidability statements will additionally require an effective presentation of syntax, which an arbitrary signature need not possess.