Is proving a theorem the same as showing that a logical expression is a tautology? The question I am trying to answer is this: 
Prove that
$$((\neg r \lor \neg f) \to (s \land l)) \land (s \to t) \land (\neg t) \to r $$ is a theorem using a deductive proof method. 
Can someone help me with this? Do I have to show that this is a tautology in order to prove that it is a theorem? If that is the case, I only know how to do that using truth tables and I do not think that is what I am supposed to do.
This is what I have done so far:
$$(\neg (r \land \neg f) \to (s \land l)) \land  (\neg s \lor t) \land (\neg t) \to r $$
$$(\neg (r \land \neg f) \to (s \land l)) \land  (\neg s \lor \neg t) \land (t \lor \neg t) \to r $$
$$(\neg (r \land \neg f) \to (s \land l)) \land  (\neg s \lor \neg t) \land T \to r $$
$$((r \land \neg f) \lor (s \land l)) \land  (\neg s \lor \neg t) \land T \to r $$ 
Could someone please help? Thanks.
 A: Recall that the material condition ($A \to B$) is equivalent to $(\neg A \lor B)$. We can now use this to simplify the statement using DeMorgan's laws and the distributive property: $A \land(B \lor C) \iff (A \land B) \lor (A \land C)$
$\begin{align} 
((\neg r \lor \neg f) \to (s \land l)) \land(s \to t) \land (\neg t) &\to r \\
(\neg(r \land f) \to (s \land l)) \land (\neg s \lor t) \land (\neg t) &\to r\\
((r \land f) \lor (s \land l)) \land ((\neg s \land \neg t) \lor(t \land \neg t)) &\to r  
\end{align}$
Recall that $A \lor (\neg B \land B )$ is equivalent to $A$(since $\neg B \land B$ is always false).
$\begin{align}
((r \land f) \lor (s \land l)) \land ((\neg s \land \neg t)) &\to r  \\
((r \land f) \land (\neg s \land \neg t)) \lor ((s \land l) \land (\neg s \land t)) &\to r
\end{align}$
Recall that the logical and($\land$) is associative.
$\begin{align}
((r \land f) \land (\neg s \land \neg t)) \lor (s \land \neg s \land t \land l) &\to r\\
(r \land f) \land \neg(s \lor t) &\to r\\
\neg((r \land f) \land \neg(s \lor t)) &\lor r\\
\neg(r \land f) \lor (s \lor t) &\lor r\\
\neg r \lor \neg f \lor s \lor t &\lor r\\
\end{align}$
Now recall that the logical or($\lor$) is associative and commutative. Also remember that $a \lor \neg a$ is always true(let $T$ represent truth). This yields
$\begin{align}
\neg r \lor r \lor s \lor \neg f &\lor t\\
T \lor s \lor \neg f &\lor t\\
T \lor \neg f &\lor t\\
T &\lor t\\
T
\end{align}$
Therefore the statement is always true, which means its a tautology. All we have to do to show that this is a theorem is to show that its a tautology, which we have just done. Therefore the logical statement is a theorem.
A: It is helpful to have a definition of tautology at hand. Here is Wikipedia's definition:

In logic, a tautology (from the Greek word ταυτολογία) is a formula or assertion that is true in every possible interpretation.

For truth-functional logic we can list all of the possible interpretations in a truth table. For this formula we could generate a truth table like the following:

Note the red column. That conditional is the top-level connective. For every true-false interpretation of the five atomic propositions, the formula is true. Therefore it is a tautology.
There are various ways one can derive $r$ from the three premises, $(\neg r \lor \neg f) \to (s \land l)$, $(s\to t)$, and $\neg t$. If the proof system we use is sound, then whatever we derive will also be a tautology which can be shown in a truth table. If the proof system is complete, then anything that can be shown to be a tautology by a truth table, can also be derived in that proof system.
In Chapter 20 the authors of forallx note that the Fitch-style natural deduction method of derivations they present is both sound and complete. They come to the following conclusion: (page 163)

Now that we know that the truth table method is interchangeable with the method of derivations, you can chose which method you want to use for any given problem.

Because of that the following proof in the proof checker associated with that text would also show that the sentence viewed as a set of premises and conclusion is also a tautology:


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
Michael Rieppel. Truth Table Generator. https://mrieppel.net/prog/truthtable.html
Wikipedia contributors. (2019, August 16). Tautology (logic). In Wikipedia, The Free Encyclopedia. Retrieved 12:55, August 28, 2019, from https://en.wikipedia.org/w/index.php?title=Tautology_(logic)&oldid=911151624
