2
$\begingroup$

I'm stuck on proving the following: $$ \forall x(\phi \lor \psi) \vdash \forall x\phi \lor \psi $$ Here, $x$ is not free in $\psi$ but can be free in $\phi$. My proof starts like the following:

  1. $\forall x(\phi \lor \psi)$ (premise)
  2. $x_0$
  3. $\phi[x_0/x] \lor \psi$
  4. $\psi$ (assumption)
  5. $\forall x\phi \lor \psi$ (or-introduction)
  6. $\phi[x_0/x]$ (assumption)
  7. ...

And then I'm stuck. In the proof it is like the or-context is in conflict with the $x_0$-context.

Brams28's answer looks correct. But I don't understand why there can't be a simpler proof. The analoguous sequent in propositional logic is just $(p_1 \lor q) \land (p_2 \lor q) \vdash (p_1 \land p_2) \lor q$ which is easily solvable without contradictions.

$\endgroup$
1
  • $\begingroup$ The problem is that if the disjunction you have is inside a universal quantifier, so to get to the disjunction you need to instantiate it, but as soon as you do that, you lose the generality of the universal .. at least in the particular proof system I used here. $\endgroup$
    – Bram28
    Apr 1, 2018 at 18:38

1 Answer 1

Reset to default
2
$\begingroup$

I don't know exactly what rules you have for the system that you are using, but here is a proof in Fitch, which I'm sure you can convert to your system easily enough. The key is to do a proof by contradiction:

enter image description here

$\endgroup$
3
  • $\begingroup$ It might seem that this proof goes unnecessarily indirectly. For a nice explanation of why the proof needs to be like this, see Richmond Thomason's Symbolic Logic, pp. 203-204. $\endgroup$
    – Peter Smith
    Apr 1, 2018 at 12:44
  • $\begingroup$ @PeterSmith I don't own that book! Brams28 did you figure out the proof yourself? If so how? Or did the computer program solve it for you? $\endgroup$
    – Björn Lindqvist
    Apr 1, 2018 at 18:29
  • 1
    $\begingroup$ @BjörnLindqvist I was me, not the software ... Once you get familiar with formal proofs, you'll start to develop certain 'proof strategies'. And of them is that if you want to prove a disjunction, and there is no immediate to do that, then try a proof by contradiction. The nice thing about that strategy is that you can then effectively do a DeMorgan on the negated disjunction to get the negation of each of the disjuncts, and then it is a matter of deriving a contradiction from that. $\endgroup$
    – Bram28
    Apr 1, 2018 at 18:35

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .