25.1 FO Validities
FO validities are the logical truths of FOL.
Necessary truths of First-Order Logic
Basically, FO validities are to FOL what tautologies are to BOOL and PROP.
Since FOL includes all the truth-functional connectives (~, &, v, →, and ↔), all tautologies are also FO validities.
But FOL also includes three other symbols: identity (=) and the quantifiers (∀ and ∃). So any logical truth that depends on them will be an FO validity but not a tautology.
For example, since FOL includes =, a=a is an FO validity.
So is ~AxP(x)→Ex~P(x). That sentence uses negation and conditional, but it also depends essentially on the quantifiers (DeMQ). So it is an FO validity but not a tautology.
Here’s a tricky example: Ax~(P(x)vQ(x))→Ax(~P(x)&~Q(x)).
This sentence is a type of DeMorgan’s. But since the DeMorgan’s occurs inside the scope of the quantifier, it depends on how the quantifiers work.
Think about it this way: it is a fact about FOL that DeMorgan’s still holds inside the scope of quantifiers. So this is an FO validity but not a tautology.
There are a huge number of FO validities; we can’t enumerate them all.
For example, take any equivalence of FOL, and put a biconditional between them (or just a single conditional). The result is an FO validity.
Besides the fact that FOL includes some symbols that BOOL and PROP don’t, there is another key different between tautologies and FO validities.
For tautologies, there is always a mechanical procedure we could use to show that something is an tautology: construct a truth table and see if the sentence has all Ts.
For FO validities there is no similar procedure. Since the quantifiers are not truth functional, truth tables do not reveal their logical properties.