The Nonlinear Library LW - Understanding Gödel's completeness theorem by jessicata
May 28, 2024
23:23
Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: Understanding Gödel's completeness theorem, published by jessicata on May 28, 2024 on LessWrong.
In this post I prove a variant of Gödel's completeness theorem. My intention has been to really understand the theorem, so that I am not simply shuffling symbols around, but am actually understanding why it is true. I hope it is helpful for at least some other people.
For sources, I have myself relied mainly on Srivastava's presentation. I have relied a lot on intuitions about sequent calculus; while I present a sequent calculus in this post, this is not a complete introduction to sequent calculus. I recommend Logitext as an online proof tool for gaining more intuition about sequent proofs. I am familiar with sequent calculus mainly through type theory.
First-order theories and models
A first-order theory consists of:
A countable set of functions, which each have an arity, a non-negative integer.
A countable set of predicates, which also have non-negative integer arities.
A countable set of axioms, which are sentences in the theory.
Assume a countably infinite set of variables. A term consists of either a variable, or a function applied to a number of terms equal to its arity. An atomic sentence is a predicate applied to a number of terms equal to its arity. A sentence may be one of:
an atomic sentence.
a negated sentence, P.
a conjunction of sentences, PQ.
a universal, x,P, where x is a variable.
Define disjunctions (PQ:=(PQ)), implications (PQ:=(PQ)), and existentials (x,P:=x,P) from these other terms in the usual manner. A first-order theory has a countable set of axioms, each of which are sentences.
So far this is fairly standard; see Peano arithmetic for an example of a first-order theory. I am omitting equality from first-order theories, as in general equality can be replaced with an equality predicate and axioms.
A term or sentence is said to be closed if it has no free variables (that is, variables which are not quantified over). A closed term or sentence can be interpreted without reference to variable assignments, similar to a variable-free expression in a programming language.
Let a constant be a function of arity zero. I will make the non-standard assumption that first-order theories have a countably infinite set of constants which do not appear in any axiom. This will help in defining inference rules and proving completeness. Generally it is not a problem to add a countably infinite set of constants to a first-order theory; it does not strengthen the theory (except in that it aids in proving universals, as defined below).
Before defining inference rules, I will define models. A model of a theory consists of a set (the domain of discourse), interpretations of the functions (as mapping finite lists of values in the domain to other values), and interpretations of predicates (as mapping finite lists of values in the domain to Booleans), which satisfies the axioms. Closed terms have straightforward interpretations in a model, as evaluating the expression (as if in a programming language).
Closed sentences have straightforward truth values, e.g. the formula P is true in a model when P is false in the model.
Judgments and sequent rules
A judgment is of the form ΓΔ, where Γ and Δ are (possibly infinite) countable sets of closed sentences. The judgment is true in a model if at least one of Γ is false or at least one of Δ is true. As notation, if Γ is a set of sentences and P is a sentence, then Γ,P denotes Γ{P}.
The inference rules are expressed as sequents. A sequent has one judgment on the bottom, and a finite set of judgments on top. Intuitively, it states that if all the judgments on top are provable, the rule yields a proof of the judgment on the bottom. Along the way, I will show that each rule is sound: if every judgment on the top is true in all models, then t...
In this post I prove a variant of Gödel's completeness theorem. My intention has been to really understand the theorem, so that I am not simply shuffling symbols around, but am actually understanding why it is true. I hope it is helpful for at least some other people.
For sources, I have myself relied mainly on Srivastava's presentation. I have relied a lot on intuitions about sequent calculus; while I present a sequent calculus in this post, this is not a complete introduction to sequent calculus. I recommend Logitext as an online proof tool for gaining more intuition about sequent proofs. I am familiar with sequent calculus mainly through type theory.
First-order theories and models
A first-order theory consists of:
A countable set of functions, which each have an arity, a non-negative integer.
A countable set of predicates, which also have non-negative integer arities.
A countable set of axioms, which are sentences in the theory.
Assume a countably infinite set of variables. A term consists of either a variable, or a function applied to a number of terms equal to its arity. An atomic sentence is a predicate applied to a number of terms equal to its arity. A sentence may be one of:
an atomic sentence.
a negated sentence, P.
a conjunction of sentences, PQ.
a universal, x,P, where x is a variable.
Define disjunctions (PQ:=(PQ)), implications (PQ:=(PQ)), and existentials (x,P:=x,P) from these other terms in the usual manner. A first-order theory has a countable set of axioms, each of which are sentences.
So far this is fairly standard; see Peano arithmetic for an example of a first-order theory. I am omitting equality from first-order theories, as in general equality can be replaced with an equality predicate and axioms.
A term or sentence is said to be closed if it has no free variables (that is, variables which are not quantified over). A closed term or sentence can be interpreted without reference to variable assignments, similar to a variable-free expression in a programming language.
Let a constant be a function of arity zero. I will make the non-standard assumption that first-order theories have a countably infinite set of constants which do not appear in any axiom. This will help in defining inference rules and proving completeness. Generally it is not a problem to add a countably infinite set of constants to a first-order theory; it does not strengthen the theory (except in that it aids in proving universals, as defined below).
Before defining inference rules, I will define models. A model of a theory consists of a set (the domain of discourse), interpretations of the functions (as mapping finite lists of values in the domain to other values), and interpretations of predicates (as mapping finite lists of values in the domain to Booleans), which satisfies the axioms. Closed terms have straightforward interpretations in a model, as evaluating the expression (as if in a programming language).
Closed sentences have straightforward truth values, e.g. the formula P is true in a model when P is false in the model.
Judgments and sequent rules
A judgment is of the form ΓΔ, where Γ and Δ are (possibly infinite) countable sets of closed sentences. The judgment is true in a model if at least one of Γ is false or at least one of Δ is true. As notation, if Γ is a set of sentences and P is a sentence, then Γ,P denotes Γ{P}.
The inference rules are expressed as sequents. A sequent has one judgment on the bottom, and a finite set of judgments on top. Intuitively, it states that if all the judgments on top are provable, the rule yields a proof of the judgment on the bottom. Along the way, I will show that each rule is sound: if every judgment on the top is true in all models, then t...