We previously showed that zero-order logic was complete. What about first-order logic?
Gödel’s’ completeness theorem says that for first order logic, a theory can include all tautologies, the first category.
If the completeness theorem is true and a formula is not in the theory, then the formula is either refutable or satisfiable under some, but not all interpretations.
That is, either the theory will contain \(\theta\), \(\neg \theta\), or \(\theta\) will be satisfiable in some but not all interpretations, and neither will be in the in theory.
To prove this we look for a proof that every formula is either refutable or true under some structure. So for an arbitrary formula \(\theta\) we want to show it is either refutable or satisfiable under some interpretation.
Remove free variables, functions
Note that if this is true, all valid formulae of the form below are provable:
\(\neg \theta\)
This means that there is no interpretation where the following is true:
\(\theta\)
Conversely if \(\neg \theta\) is not in the theory, then \(\theta\) must be true under some interpretation.
That is, if all valid formulae are provable, then all
Reformulating the question:
This is the most basic form of the completeness theorem. We immediately restate it in a form more convenient for our purposes:
Theorem 2. Every formula \(\theta\) is either refutable or satisfiable in some structure.
"\(\theta\)is refutable" means by definition "\(\neg \theta\) is provable".
Given a formula, can we find out if can be derived from the axioms? We can follow a process for doing so which would inform us if the formula was or was not a theorem. Alternative, the process could carry on forever.
If the process never carries on forever the system is decidable: there is a finite process to determine whether the formula is in or out. If the process halts for true formulas, but can carry on forever for false formulas, the system is semi-decidable. If the process takes a long time, we do not know if it is looping infinitely, or approaching its halt point.
Intuitively, use of axioms can make an existing formula shorter or longer, so finding all short formulas can require going forwards and backwards an infinite number of times.