1
$\begingroup$

i need to prove the following and i have no idea how to without using soundness and completeness

$ \neg \forall x A \rightarrow \exists x \neg A $

using the following axioms:

I1. $ A \rightarrow (B \rightarrow A) $

I2. $ (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) $

N1. $(A \rightarrow B) \rightarrow ((A \rightarrow \neg B) \rightarrow \neg A)$

N2. $ \neg \neg A \rightarrow A $

C1. $ A \wedge B \rightarrow A $

C2. $ A \wedge B \rightarrow B $

C3. $ A \rightarrow (B \rightarrow A \wedge B) $

D1. $ A \rightarrow A \vee B $

D2. $ B \rightarrow A \vee B $

D3. $ (A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow (A \vee B \rightarrow C)) $

the next two axioms are for the case when $ x \notin FV(A) $

3.i. $ \forall x (B \rightarrow A) \rightarrow (\exists x B \rightarrow A) $

3.ii. $ \forall x (A \rightarrow B) \rightarrow (A \rightarrow \forall x B) $

the next two are axioms for the case when substituting t instead of x in A wont cause any free variable in t to become bounded by quantifier

$ \forall x A \rightarrow A\{t/x\} $

$ A\{t/x\} \rightarrow \exists x A $ (A{t/x} means substitute t in place of x in A)

and the following inference rules:

$ A,A \rightarrow B $ infer $ B $ (MP)

$ A $ infer $ \forall x A $ (Gen)

1 Answers 1

0

A good idea is to work with the contrapositive. That is show that $\lnot\exists x\lnot A\to\forall x A$. Then show that $A\to\lnot\lnot A$ and $(\lnot A\to\lnot B)\to (B\to A)$. My guess is that some of these steps you are aware of how to do, or you have seen them.

To show that $\lnot\exists x\lnot A\to\forall xA$, use the deduction theorem. Assume that $\lnot\exists x\lnot A$, use axiom $\lnot A\{t/x\}\to\exists x\lnot A$, as well as the fact that $\lnot A\{t/x\}\to\lnot\exists x\lnot A$ (this follows from the assumption that $\lnot\exists x\lnot A$ is true and the first axiom). Now use axiom N1 to deduce $\lnot\lnot A\{t/x\}$. Then use axiom N2 and the generalisation rule to deduce $\forall x A$.