Fitch-style proof propositional logic

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!


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