Fitch-style proof propositional logic 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? 
 A: 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!
A: 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:

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
