The phrase "first-order logic" has two meanings:
It is a chapter of mathematical logic in which we study certain kinds of formal systems and everything related to them.
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:
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.
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.
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
- $T$ is contained in $P$ (in fact $T$ is contained in every theory),
- $T$ is complete,
- $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:
- You did not know that "first-order logic" may refer to the theory with empty signature generated by the empty axioms.
- A complete theory may become incomplete when we extend it.
- 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.
