I thought that any FOT is a subset of FOL, but that does not seem to be the case, because FOL is complete (every formula is either valid or invalid), while some FOT (like linear integer arithmetic) is not complete.

So, is FOL more expressive than any of FOT? Or incomparable?

Also, the statement "there are statements that are valid in LIA but cannot be proved using axioms of LIA" is weird. How can the statement be valid if we cannot prove its validity? I always thought that if you cannot prove the validity of the statement, then you cannot claim it is valid.

  • $\begingroup$ I think that the statement "there are statements that are valid in LIA but cannot be proved using axioms of LIA" is false. The completeness theorem of godel makes sure that a valid statement can eventually be proved in a finite quantity of time. I think that you are confusing logical validity with logical truth. Those are two different things. The meaning of completeness that is used in the completeness theorem of godel and the one used in the incompleteness theorem is not the same. $\endgroup$
    – rotia
    Apr 26, 2016 at 18:23

3 Answers 3


First-order logic is a mathematical subject which defines many different concepts, such as first-order formula, first-order structure, first-order theory, and many more. One of these concepts is first-order theory: it is a set of first-order formulas. Often we consider the first-order theory generated by a finite number of axioms and axiom schemes. Such a theory is closed with respect to logical derivations, and we usually only consider theories satisfying this condition.

A first-order theory is complete if for every statement $\sigma$, it contains either $\sigma$ or its negation. Not every theory is complete. Indeed, Gödel's incompleteness theorem highlights the fact that many interesting first-order theories are necessarily incomplete.

A model of a first-order theory is a valid interpretation of the theory (we leave the exact definition for textbooks). For example, the first-order theory of groups consists of all statements that follow from the group axioms. Every group is a model of the first-order theory of groups.

For every given model, very given sentence is either true or false. Gödel's completeness theorem states that if a first-order sentence is true in all models of a first-order theory, then it is provable from a finite number of sentences in the theory. For example, every first-order statement in the language of groups which holds for all groups is provable from the group axioms.

LIA is (presumably) a first-order theory which is interesting enough to be incomplete due to Gödel's incompleteness theorem. However, in the standard model – the "true" integers – every sentence is either true or false. In particular, if $\sigma$ is a statement such that neither $\sigma$ nor $\lnot \sigma$ belong to LIA, then either $\sigma$ or $\lnot \sigma$ holds for the true integers, but this fact isn't provable in LIA.

  • $\begingroup$ what is special about 'complete' theories? why are they interesting? 'of course', many theories are incomplete, because the def of completeness asks if a sentence is true for all models. On incompleteness: in "standard integers model", we don't care about all models that satisfy the axioms, we have only one, "standard integers model". Doesn't the incompleteness theorem hints that the way we define validity (especially, our consideration of all models that satisfy the axioms) is inappropriate? $\endgroup$
    – Ayrat
    Apr 26, 2016 at 14:44
  • 2
    $\begingroup$ Complete theories are special since they give a definite truth value for every statement. This is something you would like to have. The rest of your questions belong to the realm of philosophy. That said, Gödel's completeness theorem equates validity in all models with provability. $\endgroup$ Apr 26, 2016 at 15:04
  • $\begingroup$ still don't see the usefulness -- consider FOL, which is complete: suppose you want to check if F is valid or not: 'completeness' does not help much if F is invalid, because validity of FOL is semi-decidable. Do I miss something? $\endgroup$
    – Ayrat
    Apr 26, 2016 at 15:35
  • $\begingroup$ The statement "first-order logic is complete" is either meaningless or false. $\endgroup$ Apr 26, 2016 at 15:38
  • 2
    $\begingroup$ It is not true that a first-order theory is a consistent set of first-order sentences. The correct thing to say is: a first-order theory is a set of first-order formulas which is closed under deduction. I can perfectly well formulate an inconsistent theory. It may take years before we find out that it is inconsistent. And a theory may contain formulas, not just sentences (which are closed formulas). $\endgroup$ Apr 26, 2016 at 18:25

The phrase "first-order logic" has two meanings:

  1. It is a chapter of mathematical logic in which we study certain kinds of formal systems and everything related to them.

  2. It is a special kind of first-order theory, namely the one generated by an empty signature and an empty set of axioms.

Your question refers to the second meaning, but to understand this, we need to build things up:

  1. There is a certain formal language called the language of first-order logic. Speaking informally, it is the stuff you can build from variables, equality, $\land$, $\lor$, $\lnot$, $\Rightarrow$, $\forall$ and $\exists$. This stuff is known as first-order formulas.

  2. There is a certain formal system called first-order logic which tells us what it means that we prove a first-order formula. The system is given as a set of inference rules.

  3. A first-order theory $\mathcal{T}$ is given by:

    • a signature $\Sigma_{\mathcal{T}}$ which consists from a set of constants, function symbols, and relation symbols. Think of these as extensions of the basic language of first-order logic. We call it the language of $\mathcal{T}$.
    • a deductively closed set of first-order formulas written in the language extended by the signature.

A set $S$ of formulas is said to be deductively closed if any application of inference rules of first-order logic to formulas in $S$ gives formulas which are again in $S$. In other words, $S$ contains all of its logical consequences. A common way of creating such a set $S$ is: start with some chosen set of formulas $A$, and add to it all of its logical consequences, and the consequences of those consequences, and so on. This is called the deductive closure of $A$. We often call the formulas in $A$ axioms.

A theory may or may not be complete. It is not important to know what "complete" means here, but it is important to know that the following can happen: we can have two sets of formulas $A$ and $B$, such that $A \subseteq B$, the deductive closure of $A$ is a complete theory, and the deductive closure of $B$ is not a complete theory.

We are now ready to answer your question. Let $T$ be the theory whose signature is empty and whose set of formulas is the deductive closure of the empty set. Let $P$ be the theory whose signature is that of Peano arithmetic (constant $0$, unary operation $S$, binary operations $+$ and $\times$) and the formulas are the deductive closure of Peano axioms. It is a fact that

  1. $T$ is contained in $P$ (in fact $T$ is contained in every theory),
  2. $T$ is complete,
  3. $P$ is not complete.

The theory $T$ is popularly called "first-order logic", but this really is a misnomer. Some people are a bit more precise and call it "the pure theory of first-order logic".

In summary, your question revealed the following:

  1. You did not know that "first-order logic" may refer to the theory with empty signature generated by the empty axioms.
  2. A complete theory may become incomplete when we extend it.
  3. You used the wrong definition of completeness. The correct definition is: a theory is complete if, every sentence or its negation is a theorem of the theory.

NB: a sentence is a closed formula (one that does not contain any free variables).

Lastly, let me address your question about validity:

  • a formula is provable if there is a proof of it
  • a formula is valid if it is true in every model

A basic meta-theorem about first-order logic is that every provable formula is valid. The reverse holds as well and is known as Gödel's completeness theorem.

However, it often happens that in some particular situation one purposely makes a mismatach between validity and provability for a good reason. For instance, if we limit attention to just finite models, then it may easily happen that there would be valid statements which have no proof. Why would one do that? In computer science it could be for algorithmic reasons, or because one is interested in a particular class of models only.

HYou say "the only way to know that a sentence is valid is to prove it". This may be the case at some informal level (I think God would disagree with you), but notice that any such proof of validity happens outside the theory, at the meta-level. Indeed, since establishing validity requires one to talk about all models this is certainly not something we would expect to perform inside the theory.

  • $\begingroup$ You seem to have gotten mixed up about Godel's completeness theorem and Godel's incompleteness theorems. What you call "Godel's incompleteness theorem" seems to be a direct negation of Godel's completeness theorem. Godel's first incompleteness theorem is about sentences that can neither be proved nor disproved, not sentences that are valid but unprovable. $\endgroup$ Apr 26, 2016 at 19:06
  • $\begingroup$ Thanks, I just deleted that bit because it does not add anything to the explanation. $\endgroup$ Apr 26, 2016 at 19:35
  • $\begingroup$ @AndrejBauer could you clarify the following 'paradox' with "1. $T$ is contained in $P$" ? : Since $P$ is incomplete then there exists $s$ such that $s \not\in P$ and $\neg s \not\in P$. Now ask "$s \in T$"? Since $T \subset P$ (deductive closures of their axioms), then there should be either $s \in T$ or $\neg s \in T$, but both violate the assumption of existence of such $s$! $\endgroup$
    – Ayrat
    May 1, 2016 at 11:20
  • $\begingroup$ another question: do you have an example of valid statement which does not have a proof? $\endgroup$
    – Ayrat
    May 1, 2016 at 11:43

A minor clarification:

You may be thinking that the theory with empty signature is an empty theory, i.e contains no closed formulae. That is incorrect. First-order logic allows one to prove - without appeal to axioms - certain closed formulae known as tautologies. These are 'true' due solely to their form; they have no meaningful content as such. Godel's Completeness Theorem then says that the collection of tautologies is complete - i.e, all closed formulae which are valid (i.e 'true in all models') are actually derivable in first-order logic. [The proof is interesting and decidedly nontrivial.]


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.