I am usually quite good with these but i just can't wrap my head around this once for some reason. I have to make a Fitch-style proof for the expression:

$(s \rightarrow p) \lor (t \rightarrow q) \vdash(s \rightarrow q) \lor (t \rightarrow p)$

It is easy to see that this is correct because the only time the left hand side is false is when

$(s \land \lnot p) \land (t \land \lnot q)$

Which also holds true for the right hand side since it's just switching around p and q. But how do i go about making a Fitch-style proof?


Whoever set the exercise wasn't being very kind; but tackling this is in fact quite a useful reality check in getting you to think through proof-strategy.

You have a disjunctive premiss, of the form $A \lor B$, and target conclusion $C$. It's a pound to a penny that you are going to have to use disjunction elimination. So the shape of the argument is surely going to be

$\quad A \lor B\\ \quad\quad\mid\quad A\\ \quad\quad\mid\quad \vdots\\ \quad\quad\mid\quad C\\ \quad\quad--\\ \quad\quad\mid\quad B\\ \quad\quad\mid\quad \vdots\\ \quad\quad\mid\quad C\\ \quad C$

So that reduces the problem, to finding two proofs, from $A$ to $C$ and $B$ to $C$. We'll look at the first, the other being similar.

So you now want to fill in the dots

$\quad s \to p\\ \quad \vdots\\ \quad (s \to q) \lor (t \to p)$

Nasty to do from first principles. But it perhaps looks a bit more manageable if you carve things into two stages like this

$\quad s \to p\\ \quad \vdots\\ \quad \neg s \lor p\\ \quad \vdots\\ \quad (s \to q) \lor (t \to p)$

(I didn't pull that out of a hat: think why that is the obvious path to take!) And you are going to need another disjunction elimination for the second part which should pretty obviously go

$\quad s \to p\\ \quad \vdots\\ \quad \neg s \lor p\\ \quad\quad \mid \neg s\\ \quad\quad \mid \vdots\\ \quad\quad \mid (s \to q)\\ \quad\quad \mid (s \to q) \lor (t \to p)\\ \quad\quad --\\ \quad\quad \mid p\\ \quad\quad \mid \vdots\\ \quad\quad \mid (t \to p)\\ \quad\quad \mid (s \to q) \lor (t \to p)\\ \quad (s \to q) \lor (t \to p)$

So we have at least reduced the problem to that of filling in the three gaps. But each of those should be a standard familiar task which you can already do in a Fitch proof. So I'll leave those further details filling in the $A$-to-$C$ proof to you; and the $B$-to-$C$ proof works similarly!

| cite | improve this answer | |
  • 1
    $\begingroup$ This saved my ass. Thank you very much! $\endgroup$ – VictorVH Sep 18 '15 at 13:07

One attempt to solve this problem is to assume the negation of the goal, $(s → q) ∨ (t → p)$, and then attempt to derive a contradiction. The negation with De Morgan rule would turn the disjunction into a conjunction which should simplify things, but it also puts a negation in front of two conditionals. The Fitch-style proof checker that I use does not have a rule that allows me to derive $¬s ∨ p$ from $s → p$ and so I will need to find a way around that.

One thing I could do is instead of negating the goal directly, negate something equivalent to the goal. For example, I could negate this: $(¬s ∨ q) ∨ (¬t ∨ p)$. It might be easier to work with that form of the goal because if converts the conditionals to disjunctions. True, if I do reach a contradiction, I will still have work to do: I will have to derive the original goal from that statement that I know is equivalent to it. Hopefully it will be easier to do that.

Here is a proof using the proof checker associated with the forallx text. I had to capitalize the sentence variables to input the argument into this proof checker:

enter image description here

Note how on line 2 I am negating a different, but equivalent statement to the actual goal I want to achieve. This allows me to derive a contradiction on line 20. With that contradiction I can now use the unnegated statement on line 21 and derive the actual goal on line 38.

This may be an alternate way to approach goals with conditionals in Fitch-style proof checkers if more direct methods are not working.

For the proof checker and a description of the inference rules see the links below.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf

| cite | improve this answer | |

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.