1
$\begingroup$

I need to prove the following formula $$(\exists x A(x) \to B) \to \forall y (A(y) \to B)$$ Where $y\notin \mbox{free}(A)$ and $y\notin \mbox{free}(B)$

Axioms that I use.

1. $A \to (B \to A)$

2. $(A \to B) \to ( (A \to (B \to C)) \to (A \to C))$

3. $(\lnot B \to A) \to ((\lnot B \to \lnot A) \to B)$

4. $\forall x_i A(x_i) \to A(t)$ where $A$ is wf and $t$ is free for $x_i$ in $A$

5. $\forall (x_i) (A \to B) \to (A \to \forall x_i B)$ where $x_i$ is not bounded in $B$

Rules of inferences are Gen and Modus Ponens.

Here's my try.

$1. \vdash \lnot \forall x \lnot A(x)$ (premise)

$2. \vdash \lnot \forall x \lnot A(x) \to B $ (premise)

$3. \vdash B$ (1 and 2 m.p.)

Lemma 0: $ \lnot \forall x \lnot A(x) \vdash A(t)$

Suppose that

$1. \lnot \forall x \lnot A(x), \lnot A(t) \vdash \lnot A(t)$ (premise)

$2. \vdash \forall x \lnot A(x)$ (Gen 1.)

$3. \vdash \lnot \forall x \lnot A(x)$ (premise)

Contradiction. So

$4. \lnot \forall x \lnot A(x) \vdash A(t)$

End of Lemma 0

$5. \vdash A(t)$ (1. and Lemma 0)

$6. \vdash (B \to (A(t) \to B))$ (A1)

$7. \vdash A(t) \to B$ (3 and 6 m.p.)

$8. \vdash \forall y (A(y) \to B$) (Gen 7.)

$9. \vdash (\lnot \forall x \lnot A(x) \to B) \to \forall y (A(y) \to B$) (Deduction theorem)

But I think I left an error in the step 7. Everything below that is true, only if $\lnot \forall x \lnot A(x)$ is true.

Maybe there's an easier way?

P.S: $\exists$ is an abbreviation for: $\lnot \forall \lnot$ (Thanks to @MauroALLEGRANZA)

$\endgroup$
  • $\begingroup$ It seems correct to me: the application of DT is right, because in the derivation Gen is used on the var $x$ that is not free in the premises. $\endgroup$ – Mauro ALLEGRANZA Dec 17 '17 at 13:57
  • $\begingroup$ @MauroALLEGRANZA, thanks for the feedback. I think my mistake is in the step 7, but not after it. Sorry about that. $\endgroup$ – shcolf Dec 17 '17 at 15:58
  • $\begingroup$ Your proof system is that of Elliott Mendelson, Introduction to Mathematical Logic, CRC Press (6th ed 2015); see page 72 for the Deduction Th. $\endgroup$ – Mauro ALLEGRANZA Dec 17 '17 at 16:05
0
$\begingroup$

Lines 8 and 9 are fine ... but your Lemma is not. What you need to show is $A(t) \vdash \neg \forall x \neg A(x)$, so that together with $\neg \forall x \neg A(x) \rightarrow B$ you can get $A(t) \rightarrow B$ and then apply 8 and 9.

Also, while I don't know the exact notation of your system, I find the way you introduce premises suspect. For example, you write:

$1. \vdash \lnot \forall x \lnot A(x)$ (premise)

Given the $\vdash$, that looks like a theorem, not a premise. I would suspect that something like:

$1. \lnot \forall x \lnot A(x) \vdash \lnot \forall x \lnot A(x)$ (premise)

or simply

$1. \lnot \forall x \lnot A(x) $ (premise)

would be called for.

$\endgroup$
  • $\begingroup$ Yeah, you are correct. Maybe I messed the syntax. I should have put premises in left hand side. So it will be obvious. Let me try your suggestion. $\endgroup$ – shcolf Dec 17 '17 at 17:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.