Soundness and Gödel completeness

Fix a standard classical first-order calculus with equality, including its side conditions. Soundness asserts that every derivation from premises preserves semantic consequence. Its proof proceeds through the finite derivation: assumptions hold in any model of the premises, logical axioms are valid, and each inference transfers truth from its inputs to its conclusion. Quantifier rules require particular care because a variable used as an arbitrary representative cannot secretly depend on an undischarged assumption.

For existential elimination, a fresh parameter names a temporary witness. The desired conclusion and other open assumptions must not contain that parameter. Otherwise a proof could infer a claim about a specially chosen object as if it concerned all objects. Side conditions are mathematical hypotheses of the soundness theorem. A proof checker that verifies only the visible connective pattern while ignoring freshness has not checked the stated calculus.

Strong completeness says that if every model of any set T of first-order sentences satisfies a sentence, then a finite T-proof exists. Equivalently, every syntactically consistent T has a model. For a countable language, a Henkin construction adjoins witness constants, extends consistently to decide each sentence, and forms a term model. Equality requires quotienting terms by provable equality. The truth lemma then connects membership in the completed theory with truth in that model.

This is an outline of the general construction, not a replacement for its consistency and truth-lemma proofs. For arbitrary set-sized languages the usual classical metatheory uses corresponding transfinite or choice-based constructions. Completeness of the calculus is distinct from completeness of a theory, which would mean deciding each sentence or its negation. An arithmetic theory may be incomplete even though its underlying first-order proof calculus is complete for semantic consequence.

In a computably presented language, finite proofs can be effectively generated. If the extra axioms are computably enumerable, enumeration-stage certificates can be attached to axiom uses, making finite certificate checking decidable. Searching those certified proofs eventually finds any actual consequence. When no proof exists, that search may continue forever. Completeness guarantees eventual success on semantically entailed conclusions, not a stopping rule for nonconsequences.

Finite truth tables decide propositional validity because only finitely many valuations matter for a fixed finite list of atoms. Arbitrary first-order structures have no comparable uniform finite bound. Finding a countermodel is a semantic method, but enumerating only finite models misses formulas with exclusively infinite countermodels. The distinction between sound inference, complete inference, and a total decision procedure will become central when we formalize computation.