tautologies in predicate logic
Let FO$(\mathrm{\Sigma})$ be a first order language over signature^{} $\mathrm{\Sigma}$. Recall that the axioms for FO$(\mathrm{\Sigma})$ are (universal^{}) generalizations^{} of wff’s belonging to one of the following six schemas:

1.
$A\to (B\to A)$

2.
$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

3.
$\mathrm{\neg}\mathrm{\neg}A\to A$

4.
$\forall x(A\to B)\to (\forall xA\to \forall xB)$, where $x\in V$

5.
$A\to \forall xA$, where $x\in V$ is not free in $A$

6.
$\forall xA\to A[a/x]$, where $x\in V$, $a\in V(\mathrm{\Sigma})$, and $a$ is free for $x$ in $A$
where $V$ is the set of variables and $V(\mathrm{\Sigma})$ is the set of variables and constants, with modus ponens^{} as its rule of inference^{}: from $A$ and $A\to B$ we may infer $B$.
The first three axiom schemas^{} and the modus ponens tell us that predicate logic is an extension^{} of the propositional logic^{}. On the other hand, we can also view predicate logic as a part of propositional logic if we treat all quantified formulas as atoms. This can be done precisely as follows:
Call a wff of FO$(\mathrm{\Sigma})$ quasiatom if it is either atomic, or of the form $\forall xA$, where $A$ is a wff of FO$(\mathrm{\Sigma})$. Let $\mathrm{\Gamma}$ be the set of all quasiatoms of FO$(\mathrm{\Sigma})$.
Proposition 1.
Every wff of FO$\mathrm{(}\mathrm{\Sigma}\mathrm{)}$ can be uniquely built up from $\mathrm{\Gamma}$ using only logical connectives $\mathrm{\to}$ and $\mathrm{\neg}$.
Proof.
Induction^{} on the complexity of wff. For any wff $A$ of FO$(\mathrm{\Sigma})$, it has one of the following forms: $B\to C$, $\mathrm{\neg}B$, or $\forall xB$, where $B,C$ are wff’s. If $A$ were $B\to C$ or $\mathrm{\neg}B$, by induction, since $B$ and $C$ were in $\mathrm{\Gamma}$, $A$ is in $\mathrm{\Gamma}$ as a result. If $A$ were $\forall xB$, then $A$ is quasiatomic, and therefore in $\mathrm{\Gamma}$ by the definition of $\mathrm{\Gamma}$. Unique readability follows from the unique readability of wff’s of propositional logic. ∎
Since no quantifiers^{} are involved in the builtup process, the language^{} based on $\mathrm{\Gamma}$ as the set of atoms can be considered as the language of propositional logic. Call this logic PL$(\mathrm{\Gamma})$. So the atoms of PL$(\mathrm{\Gamma})$ are precisely the quasiatoms of FO$(\mathrm{\Sigma})$.
Definition. We call a wff of FO$(\mathrm{\Sigma})$ a tautology^{} if it is a tautology of PL$(\mathrm{\Gamma})$ (via truth tables^{}).
Proposition 2.
In FO$\mathrm{(}\mathrm{\Sigma}\mathrm{)}$, every tautology is a theorem^{}, but not conversely.
Proof.
Suppose wff $A$ is a tautology in FO$(\mathrm{\Sigma})$. Then it is a tautology in PL$(\mathrm{\Gamma})$ by definition, and therefore a theorem in PL$(\mathrm{\Gamma})$ since propositional logic is complete^{} with respect to truthvalue semantics. If ${A}_{1},\text{ldot},{A}_{n}$ is a deduction^{} of $A$ (with ${A}_{n}=A$), then each ${A}_{i}$ is either an axiom, or is obtained by an application of modus ponens. If ${A}_{i}$ is an axiom (of PL$(\mathrm{\Gamma})$), it is an instance of one of the first three axiom schemas of FO$(\mathrm{\Sigma})$ above, which means that ${A}_{i}$ is an axiom of FO$(\mathrm{\Sigma})$. Furthermore, since modus ponens is a rule of inference for FO$(\mathrm{\Sigma})$, ${A}_{1},\mathrm{\dots},{A}_{n}$ is a deduction of $A$ in FO$(\mathrm{\Sigma})$, which means that $A$ is a theorem of FO$(\mathrm{\Sigma})$.
On the other hand, any wff that is an instance of one of the last two axiom schemas of FO$(\mathrm{\Sigma})$ is a theorem that is not a tautology. For example, $\forall x(x=y)\to (z=y)$ is an instance of the fourth axiom schema, which takes the form $C\to D$, where $C$ is a quasiatom, and $D$ an atom, both of which are atoms of PL$(\mathrm{\Gamma})$. Any truthvaluation that takes $C$ to $1$ and $D$ to $0$, takes $C\to D$ to $0$. Therefore, $\forall x(x=y)\to (z=y)$ is not a tautology. ∎
Title  tautologies in predicate logic 

Canonical name  TautologiesInPredicateLogic 
Date of creation  20130322 19:32:25 
Last modified on  20130322 19:32:25 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  15 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03B10 