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.
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$ :
:$\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:
Since $\AA$ and $\sigma$ are arbitrary, it follows that $\mathbf A \implies \paren{ \forall x: \mathbf A }$ is a tautology.
=== Axiom 3: $\paren{ \forall x: \mathbf A \implies \mathbf B } \implies \paren{ \paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } }$ ===
 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 :
:$\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$:
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.
=== Axiom 4-11 ===
== Sources ==
* : $\text{II}.10$ Formal Proofs: Exercise $\text{II}.10.2$
Category:Proof Systems
Category:Predicate Logic