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

first-order-logiclogicpredicate-logic

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!

Best Answer

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.

Related Question