# Axioms of Hilbert Proof System Instance 1 for Predicate Logic are Tautologies

## Theorem

Let $\mathscr H$ be Instance 1 of a Hilbert proof system for predicate logic.

Then the axioms of $\mathscr H$ are tautologies.

## Proof

### Axiom 1

This is precisely the statement of Propositional Tautology is Tautology in Predicate Logic.

$\Box$

By Well-Formed Formula is Tautology iff Universal Closure is Tautology, we prove the results for axioms 2 through 11 for the WFFs instead of their universal closures.

Let $\sigma$ be an assignment in a structure $\AA$.

Let $\map { \operatorname{val}_\AA } {\cdot} \sqbrk \sigma$ be the value mapping for $\sigma$ in $\AA$.

### Axiom 2: $\mathbf A \implies \paren{ \forall x: \mathbf A }$

We have that $\map { \operatorname{val}_\AA } {\forall x: \mathbf A} \sqbrk \sigma = T$ if and only if:

$\forall a \in A: \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk { \sigma + \paren{ a / x } } = T$

By assumption, $x$ does not occur freely in $\mathbf A$.

By Value of Formula under Assignment Determined by Free Variables, it follows that:

$\forall a \in A: \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk { \sigma + \paren{ a / x } } = \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk { \sigma }$

and hence:

$\map { \operatorname{val}_\AA } {\forall x: \mathbf A} \sqbrk \sigma = \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk { \sigma }$

Therefore:

 $\ds \map { \operatorname{val}_\AA } {\mathbf A \implies \paren{ \forall x: \mathbf A } } \sqbrk \sigma$ $=$ $\ds \map { f^\to } { \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk \sigma, \map { \operatorname{val}_\AA } {\forall x: \mathbf A} \sqbrk \sigma }$ $\ds$ $=$ $\ds \map { f^\to } { \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk \sigma, \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk \sigma }$ $\ds$ $=$ $\ds T$ Definition of Truth Function of Conditional

Since $\AA$ and $\sigma$ are arbitrary, it follows that $\mathbf A \implies \paren{ \forall x: \mathbf A }$ is a tautology.

$\Box$

### Axiom 3: $\paren{ \forall x: \mathbf A \implies \mathbf B } \implies \paren{ \paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } }$

Aiming for a contradiction, suppose that $\paren{ \forall x: \mathbf A \implies \mathbf B } \implies \paren{ \paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } }$ is not a tautology.

Then there exist $\AA, \sigma$ such that:

$\map { \operatorname{val}_\AA } { \paren{ \forall x: \mathbf A \implies \mathbf B } \implies \paren{ \paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } } } \sqbrk \sigma = F$

By definition of $\operatorname{val}_\AA$, this means:

$\map { f^\to } { \map { \operatorname{val}_\AA } {\forall x: \mathbf A \implies \mathbf B} \sqbrk \sigma, \map { \operatorname{val}_\AA } {\paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } } \sqbrk \sigma } = F$

By definition of the truth function $f^\to$, this happens if and only if:

$\map { \operatorname{val}_\AA } {\forall x: \mathbf A \implies \mathbf B} \sqbrk \sigma = T$
$\map { \operatorname{val}_\AA } {\paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } } \sqbrk \sigma = F$

and, applying the same argument on the second statement, we get:

$\map { \operatorname{val}_\AA } {\forall x: \mathbf A \implies \mathbf B} \sqbrk \sigma = T$
$\map { \operatorname{val}_\AA } {\forall x: \mathbf A } \sqbrk \sigma = T$
$\map { \operatorname{val}_\AA } {\forall x: \mathbf B } \sqbrk \sigma = F$

By definition of $\operatorname{val}_\AA$, the last of these statements means that for some $a \in A$:

$\map { \operatorname{val}_\AA } {\mathbf B } \sqbrk { \sigma + \paren{x / a} } = F$

where $\sigma + \paren{x / a}$ is the extension of $\sigma$ by mapping $x$ to $a$.

Similarly, from the first two statements it follows that:

$\map { \operatorname{val}_\AA } {\mathbf A } \sqbrk { \sigma + \paren{x / a} } = T$
$\map { \operatorname{val}_\AA } {\mathbf A \implies \mathbf B} \sqbrk { \sigma + \paren{ x / a} } = T$

However, by definition of $\operatorname{val}_\AA$:

 $\ds \map { \operatorname{val}_\AA } {\mathbf A \implies \mathbf B} \sqbrk { \sigma + \paren{ x / a} }$ $=$ $\ds \map { f^\to } {\map { \operatorname{val}_\AA } {\mathbf A} \sqbrk { \sigma + \paren{ x / a} }, \map { \operatorname{val}_\AA } {\mathbf B} \sqbrk { \sigma + \paren{ x / a} } }$ $\ds$ $=$ $\ds \map { f^\to } { T , F }$ from above $\ds$ $=$ $\ds F$ Definition of Truth Function of Conditional

Thus, by Proof by Contradiction, $\paren{ \forall x: \mathbf A \implies \mathbf B } \implies \paren{ \paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } }$ is a tautology.

$\Box$