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 })$ quasi-atom 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 quasi-atoms 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 quasi-atomic, 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 built-up 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 quasi-atoms 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 truth-value semantics. If $A_1,,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 quasi-atom, and $D$ an atom, both of which are atoms of PL$(\mathrm{\Gamma })$. Any truth-valuation 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	2013-03-22 19:32:25
Last modified on	2013-03-22 19:32:25
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	15
Author	CWoo (3771)
Entry type	Definition
Classification	msc 03B10