2
$\begingroup$

In a current exam-prep exercise, we were tasked to prove the following formula using natural deduction of first-order logic:

$(\exists x. P \lor Q) \rightarrow P \lor (\exists x.Q)$ for arbitrary $P,Q$ where $P$ does not have free occurences of variable x.

I managed to do the prove, until I arrived at the following:

$\frac{}{\exists x.P\lor Q, P \lor Q \ \vdash \ (\exists x. P) \lor (\exists x.Q)}$

Unfortunately, applying $\lor-elimination$ only strengthens what I need to prove, so applying that doesn't work. In general, whichever rule I try to apply, I cannot get far. I also cannot apply $\exists-elimination$, as the $Q$ in $P\lor Q$ is not guaranteed to have only bound occurenes of x.

Actually, $\frac{}{\exists x.P\lor Q, P \lor Q \ \vdash \ (\exists x. P) \lor (\exists x.Q)}$ is just a rewritten form of distributivity of existential quantification: $\frac{}{\vdash \ \exists x.P\lor Q \rightarrow (\exists x. P) \lor (\exists x.Q)}$.

How shall I proceed in the prove?

Improve this question
$\endgroup$
1
  • $\begingroup$ Informally, $\exists x.(P\lor Q(x))\to P\lor Q(x)\to P\lor(\exists x:Q(x))$. $\endgroup$
    – user16034
    Mar 24 at 8:46

1 Answer 1

Reset to default
0
$\begingroup$

You didn't say exactly what you tried, but it looks like you're trying to get there by applying elimination rules. That's not the simplest approach, and it might not work directly without case analysis on $P$ and $Q$ (I haven't tried). There's a very powerful theorem about natural deduction and most other basic logical framework: if there's a way to derive a proposition, there's a way to derive it without using elimination rules. This is called normalization. In the Curry-Howard correspondence, normalization of derivations corresponds to evaluation of programs and an introduction-only proof is a value (program with only constructors).

To prove that $(\exists x. P \lor Q) \rightarrow P \lor (\exists x.Q)$, let's use $\rightarrow_I$: we need to prove that if there's a derivation of $\exists x. P \lor Q$ then there's a derivation of $P \lor (\exists x.Q)$.

If there's a derivation of $\exists x. P \lor Q$, then there is a normal derivation of it, and in particular there is a derivation ending in $\exists_I$. The premise of this derivation is $[t/x](P \lor Q) = ([t/x]P) \lor ([t/x]Q)$ for some term $t$. This proposition itself has a derivation ending in one of the introduction rules for disjunction: either $_I\lor$ with the premise $[t/x]P$ or $\lor_I$ with the premise $[t/x]Q$. In the first case, we have a derivation of $[t/x]P = P$. In the second case, we can apply $\exists_I$ to derive $\exists x. Q$. In the first case, we can then derive $P \lor (\exists x. Q)$ with $_I\lor$. In the second case, we can derive the same proposition $P \lor (\exists x. Q)$ with $\lor_I$. We've shown that if there's a derivation of $\exists x. P \lor Q$ then there's a derivation of $P \lor (\exists x. Q)$, QED.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Your claim about normal forms is incorrect. For example, you cannot prove $P \lor Q \to Q \lor P$ without elimination of disjunction. I believe you may have confused things a bit: the theorem you refer to works when there are no schematic letters (but we have $P$ and $Q$). Also, you are using elimination rules for existentials and disjunction in your third paragraph. You are dressing it up by talking about normal-form derivations, but it's really just elimination rules. If you think otherwise, please provide an explicit derivation or proof term that does not use any eliminations. $\endgroup$
    – Andrej Bauer
    Mar 9, 2020 at 19:28
  • $\begingroup$ The theorem you're looking for is that every derivation tree can be normalized so that all applications of elimination rules are pushed upward, above the introduction rules. $\endgroup$
    – Andrej Bauer
    Mar 9, 2020 at 19:32
  • $\begingroup$ @AndrejBauer You're right. A value has applications under $\lambda$… I only use the fact that it's a head normal form, so the gist of my proof is correct, isn't it? Are elimination rules for disjunction and exists complete, or does the proof need to reason about normal forms? I present a proof that a derivation exists, not an opaque construction of a derivation: I show that the rule is admissible, not that it's derivable. Is it derivable? $\endgroup$
    – Gilles 'SO- stop being evil'
    Mar 10, 2020 at 8:55
  • $\begingroup$ I think it's a lot easier to just give the proof than to muddle waters with normal forms. We're talking to a struggling student here, so just tell them they should use intro rules at first (I call this "follow your nose") until they get stuck, at which point they'll have to use one of the assumptions (an elimination rule), or something else that's been previously known (cut rule). $\endgroup$
    – Andrej Bauer
    Mar 10, 2020 at 22:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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