Completeness

A deductive system is complete when every statement true in all models of its premises is provable within the system. It connects semantic consequence with formal derivability.

Semantic consequence: A sentence is a semantic consequence of premises when every model satisfying the premises also satisfies that sentence. Completeness asks whether every semantic consequence can also be derived.
Gödel's completeness theorem: The theorem that first-order logic proves every sentence true in all models of its premises. It establishes completeness for classical first-order logic.
Henkin construction: A method that expands a formal theory with witness constants to build a model of a consistent theory. It turns syntactic consistency into a model, the key step in a standard completeness proof.
Semantic completeness: The property that every semantic consequence in a specified logic is derivable in its proof system. This is the model-theoretic-to-proof-theoretic property defined by the concept.
Syntactic consequence: A sentence is a syntactic consequence of premises when a formal proof derives it from those premises. It is the proof-theoretic side completeness requires to capture semantic consequence.
Propositional logic: A formal logic whose formulas combine proposition letters using truth-functional connectives. Its standard proof systems are complete for truth-table validity.
Maximal consistent set: A consistent set of sentences that cannot be enlarged without becoming inconsistent. Such sets provide the sentences used to define truth in a canonical model.
Syntactic completeness: A theory is syntactically complete when it decides every sentence in its language, proving it or its negation. It concerns a theory's ability to decide sentences, not a calculus capturing all semantic consequences.
Model theory: The mathematical study of formal languages through their interpretations and models. Models supply the interpretations used to define semantic consequence.
First-order logic: A formal logic with variables, predicates, quantifiers, and domains of objects. Gödel's completeness theorem concerns its semantic consequence relation.

Linked from 20 pages