2
$\begingroup$

I have a problem to solve this question. I thought I should eliminate the existential first but it seems not work..Not sure how to use the existential condition to prove the later one.

Here's the rule for existential elimination,
1: Ev.p(v) // use E for ∃
2: Av.(p(v) => q) //use A for ∀
EE 1,2: q

And the Fitch system provides new method also, it calls equalization introduction and equalization elimination..But I don't know how to use it..Since the lecture doesn't have any information about that..If someone know, could you tell me??

Thanks for your help!!

$\endgroup$
  • $\begingroup$ Let $y_0$ be the value of $y$ such that $\forall x. p(x,y)$, whose existence is guaranteed by the assumption. Then, $\forall x. p(x,y_0)$, so $\forall x. \exists y. p(x,y)$. $\endgroup$ – DHMO Apr 13 '17 at 0:14
  • $\begingroup$ @DHMO Unfortunately that isn't natural deduction. Most formal proof systems don't have the concept of "constant" in them (notable exception being peano arithmetic). $\endgroup$ – DanielV Apr 13 '17 at 17:32
  • $\begingroup$ @DanielV Looks like I need to really study logic... $\endgroup$ – DHMO Apr 13 '17 at 17:37
  • $\begingroup$ If you know proof by cases, it might help understand existential elimination. $$\frac {C_1 \lor C_2,~ C_1 \Rightarrow Q,~ C_2 \Rightarrow Q}{Q}$$ generalizes to $$\frac {C_1 \lor \dots \lor C_N,~ C_1 \Rightarrow Q,~\dots,~C_N \Rightarrow Q}{Q}$$ which then generalizes to $$\frac {\exists k~ C_k,~ C_k \Rightarrow Q}{Q}$$ $\endgroup$ – DanielV Apr 13 '17 at 17:44
  • $\begingroup$ @DHMO To be able to reason and to be able to convey your reasoning in a formal language are 2 different things. You don't really need to learn "logic" (putting reasoning into a formal language) unless you have some reason to want to convey that reasoning in painstaking formality (such as software design, or investigations of what is and isn't possible to deduce). $\endgroup$ – DanielV Apr 13 '17 at 17:46
2
$\begingroup$

Ugh, I hate how they defined that Existential Elimination rule!

Anyway, here is how you do that one:

  1. $\exists y \forall x \: p(x,y)$ Premise

  2. $\quad \forall x \: p(x,y)$ Assumption

  3. $\quad p(x,y)$ $\forall $ Elim 2

  4. $\quad \exists y \: p(x,y)$ $\exists$ Intro 3

  5. $\forall x \: p(x,y) \rightarrow \exists y \: p(x,y)$ $\rightarrow$ Intro 2-4

  6. $\forall y (\forall x \: p(x,y) \rightarrow \exists y \: p(x,y))$ $\forall$ Intro 5

  7. $\exists y \: p(x,y)$ $\exists$ Elim 1,6

  8. $\forall x \exists y \: p(x,y)$ $\forall $ Intro 7

$\endgroup$
  • $\begingroup$ WOW, I guess I need to study harder and harder...I am kind of relying on this website. and thanks a lot~!!! You are impressive!!! $\endgroup$ – tang aqua Apr 13 '17 at 3:02
  • $\begingroup$ @tangaqua Well, don't feel bad about this one .. That Existential elimination rule is real tricky! $\endgroup$ – Bram28 Apr 13 '17 at 3:04
  • $\begingroup$ I'm pretty sure that $$\frac {\exists x ~P(x), P(x) \Rightarrow Q}{Q}$$ is the standard rule? What do you prefer? $\endgroup$ – DanielV Apr 13 '17 at 4:14
  • $\begingroup$ @DanielV I prefer either $\exists x P(x) \vdash P(a)$ (with $a$ a new constant) or $\exists x P(x), P(a) \vdash Q \vdash Q$ (again with $a$ a new constant) or $\exists P(x) \vdash P(x)$ (with appropriate constraints as well); in all cases I can just drop the quantifier. But with this rule, I am required to first generate a Universal Conditional, which I find very unintutive. For example, to infer $\exists x (P(x) \land Q(x))$ from $\exists x(Q(x) \land P(x))$ I would first need to prove something like $\forall x ((Q(x) \land P(x)) \rightarrow (P(x) \land Q(x)))$ which seems overly complicated. $\endgroup$ – Bram28 Apr 13 '17 at 12:12
  • $\begingroup$ @Bram28 I see, thank you. It tentatively seems to me that the "required subproof" of the no-constants-version is equivalent to the parts of the constants-version which assume that y0 is a constant. That is, if you explicitly annotated that y0 is a constant wherever it appears, the annotated parts are equivalent to the $P(x) \Rightarrow Q$ subproof. $\endgroup$ – DanielV Apr 13 '17 at 15:16

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.