Proving the axioms of $HFOL$ are semantic tautologies for $FOL$

Question

We wish to construct an axiomatic system similar to $HPC$ i.e. Hilbert System for Propositional Calculus, for first order languages, denoted as $HFOL$.

We wish to prove the following axioms of $HFOL$ are tautologies in order to show $HFOL$ is sound for $FOL$, that is everything we can prove using $HFOL$ is semantically correct in $FOL$ to my understanding.

The axioms are:$\\\: \\1. \space \phi_1= \forall x(A\rightarrow B)\rightarrow(A\rightarrow\forall xB) \\ 2. \space \phi_2 = \forall x(B\rightarrow A)\rightarrow (\exists xB\rightarrow A)$

We also demand that $x$ is not a free variable in A i.e. $x\notin FV(A).$ Not sure why this demand.

We can also use the generalization rule.

So basically we want to show $\phi_1 ,\phi_2$ are tautologies in $FOL$, more precisely that (to my understanding) we want to show $M,v \models \{ \phi_1, \phi_2\}$ for every possible $M = (D,I)$ structure in $FOL$ and $v: V\rightarrow D$ from the set of variables in $A,B$ to the domain of the structure. How do you show this? Am I right with the quantifiers? Because I was thinking it might be that for every structure there exists a valuation $v$ that satisfies the axioms.

I would appreciate many type of proofs, such as proof trees and natural deduction type proofs. Thanks!

Answer 1

You have to show that the provided axioms are valid, i.e. true for every model $M$ and valuation $v$.

Consider the first one and assume that it is not valid, i.e. that :

$M,v \nvDash ∀x(A → B) → (A → ∀xB)$, for some $M$ and $v$.

This means that : $M,v \vDash ∀x(A → B)$ and $M,v \nvDash (A → ∀xB)$.

Consider the second formula; it means that : $M,v \vDash A$ and $M,v \nvDash ∀xB$.

Now we apply the clause of the semantical specifications related to the universal quantifier, and we have that :

for some $a \in D$ (where $D$ is the domain of the model) : $M, v(x|a) \nvDash B$ [in plain language : if $∀xB$ does not hold in $M$, tehre is some object $a \in D$ such that $B$ does not hold of it].

Consider now $A \to B$.

We have $M,v \vDash A$ and $x \notin \text {FV}(A)$ [here the proviso is crucial]. Thus, also $M,v(x|a) \vDash A$.

But $M,v(x|a) \nvDash B$.

Thus :

$M, v(x|a) \nvDash (A \to B)$,

contradicting the assumption that : $M,v \vDash \forall x (A \to B)$.

---

Same approach for the second axiom.