First Order Logic (FOL) is complete in the sense that: there is a proof procedure for FOL such that just the statements(/wffs) of FOL that are true and remain true under any re-interpretation of their non-logical terms (i.e. apart from "and", "not", "for all" etc.,) are theorems.

Gödel's incompleteness theorem assures us that set theory (say ZFC) is incomplete. Since the only additional term that features is "∊" ZFC would be complete if: There is a proof procedure for ZFC such that just the statements that are true and remain true under any re-interpretation of their non-logical terms apart from "is a member of" (i.e. apart from "∊", "and", "not" "for all " etc.,) that renders the axioms of ZFC true are theorems.

(1) are these two statements of completeness correct?

(2) Given FOL is complete and ZFC isn't, there must be some re-interpretation of "∊" that renders all the axioms of ZFC true, but converts some truth of ZFC into a falsehood. Do we have any examples of such a statement (wff of ZFC) and interpretation, or do we just know that they exist but we cannot construct them?

Or (3) to strip away all formality - how on earth can FOL be complete and ZFC be incomplete?

  • 3
    "Completeness" is used in two different senses there. Semantic completeness of FOL theories means that all and only their theorems are true in all of their models. ZFC is semantically complete. It is syntactically incomplete, i.e. there are statements in it such that neither they nor their negations are theorems. In other words, you cannot correspond its theorems to truths in any single model.
    – Conifold
    Jun 21, 2023 at 6:14
  • 1
    No, Im fairly confident thats not the issue. Putting aside syntactical completeness. ZFC is not semantically complete - Goedels first incompleteness theorem (applied to ZFC) establishes that there is a formula which is true on the standard interpretation (i.e. interpreting of "∊" as member of) that is not a theorem of ZFC. What is different between the "two" notions of completeness is the range of terms up for re-interpretation. In FOL all but logic terms, in ZFC all but logic terms and "∊". You are helping me see Im asking what the other interpretations of "∊" might be.
    – Surprised
    Jun 21, 2023 at 7:31
  • 4
    There is no "standard interpretation" of ZFC, there are multiple "standard models". But even if there was, as for Peano arithmetic, undecidable statements do not disturb semantic completeness. It just means that they are true in some models and false in others. Under Gödel's conditions, the body of theorems cannot cover the body of truths in any one model, "standard" or otherwise. The "standard" designation is rather informal to begin with.
    – Conifold
    Jun 21, 2023 at 8:09

1 Answer 1


First Order Logic is complete in the sense that: there is a proof procedure for FOL such that just the statements(/wffs) of FOL that are true and remain true under any re-interpretation.

Yes; completeness is wrt the "underlying logic", in the sense that the logical axioms+rules can formally prove all valid (i.e. true in every interpretation) formulas.

More generally, the Completeness Theorem asserts that: Γ ⊨ φ iff Γ ⊢ φ, where Γ is a set of formulas and φ is a formula, i.e. a formula φ is a logical consequence of a set Γ of formulas iff it is derivable from Γ.

The incompleteness is relative to a mathematical theory (with some specific requirements) that is built on top of the "underlying logic" with the addition of mathematical symbols and axioms, like e.g. Peano arithmetic.

In this case, Gödel’s Incompleteness Theorems asserts that there is a sentence G such that neither G nor its negation ¬G are derivable from the axioms of the theory. We say that G is undecidable (wrt first-order arithmetic).

Where is the link between the two results? Why there is no inconsistency?

Because neither G nor ¬G are valid formulas: they are formulas in the language of arithmetic, and thus they express a "fact" about numbers; being sentences, one of them must be true (and consequently, its negation is false) but it is not a logical consequence of the axioms of arithmetic.

Thus, your point (2) above is correct: the incompleteness of first-order arithmetic (and ZFC as well) means that there are models of the arithmetical axioms in which the said formula is not true. See Non-standard models of arithmetic.

See also Paris-Harrington theorem for a more "natural" example of a true statement about the integers that could be stated in the language of arithmetic, but not proved in Peano arithmetic.

For more details, see How is First Order Logic complete but not decidable?

The result applies to ZFC simply because we can Deduce PA's axioms in ZFC; see also How to prove that Gödel's Incompleteness Theorems apply to ZFC.

Regarding ZFC, we have many "non esoteric" examples; see List of statements independent of ZFC.

The first one was due (partly) to Gödel again: the Continuum hypothesis or CH is idependent of ZFC.

In 1940 Gödel produced a model of ZFC in which CH is true, showing that CH cannot be disproven in ZFC; Paul Cohen in 1963 invented the method of forcing to exhibit a model of ZFC in which CH fails, showing that CH cannot be proven in ZFC.

Thus, CH is an example of undecidable statement wrt ZFC (like formula G above). See also Solutions to the Continuum Hypothesis.

Another example of statement independent of ZFC is the so-called Axiom of constructibility: usually written as V = L, where V and L denote the von Neumann universe and the constructible universe, respectively.

The axiom, first investigated by Kurt Gödel (again!), is inconsistent with the proposition stronger large cardinal axioms (see list of large cardinal properties). See also Completion of ZFC.

In conclusion, re your question about "non-standard" interpretation of the "is a member of" relation (), if we assume that the von Neumann universe V is the standard interpretation of , we have that the Constructible universe L is a non-standard one.

  • Thx very helpful. Yes neither G or ~G are logical consequences of the axioms of ZFC (i.e. there is some reinterp. of "∊" which renders G false while keeping ZFCs axioms true). Not so happy to call G undecidable. As I use the term it is sets of wffs that are decidable or undecidable (this is the sense used in the question you linked). The set of theorems of FOL is undecidable because there is only a proof procedure (not a decision procedure) for recognising theorems. Link to non-standard m. of arithmetic very helpful. I wonder if anyone has an example of a non-standard interp. of "∊"
    – Surprised
    Jun 21, 2023 at 7:49
  • 2
    Regarding whether to call G undecidable, it is standard terminology in mathematics. But see this wikipedia entry regarding senses of "undecidable" in mathematical use.
    – Lee Mosher
    Jun 21, 2023 at 18:21

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .