Can you introduce a tautology directly into a proof

logic

For the sake of simplicity, let us restrict the context of this question to classical propositional logic. When formally evaluating the validity of an argument, is it permitted to immediately introduce a proposition that is a tautology? For example, given the premises

$p \rightarrow q$

$\neg p \rightarrow s$

am I permitted to introduce a new premise such as

$p \vee \neg p$

and immediately conclude

$q \vee s$

via disjunction elimination/constructive dilemma? If so, is there a formal rule or law for such a technique?

I understand that one can derive a statement such as $p \vee \neg p$ via the conditional proof. But again, my question is regarding whether we are permitted to bypass those steps altogether and simply introduce the premise $p \vee \neg p$ with the understanding that it is a tautology via negation law. After all, why should we be prohibited from immediately introducing a statement that is always true?

If we are not permitted to do so, why not? Is it simply a matter of convention, or is there some logical error associated with doing so?

This question has been in the back of mind ever since I started learning about logic. I've never seen the technique used and never understood why.

It may look something like this…

  1. $p \rightarrow q$ premise

  2. $\neg p \rightarrow s$ premise

  3. $T$ tautological introduction

  4. $p \vee \neg p$ negation law, 3

  5. $q \vee s$ disjunction elimination, 1,2,4

Best Answer

If so, is there a rule or law for this technique?

Tautological Consequence (TautCon) is the rule by which you can introduce a previously established tautology.   If it has been proven, or otherwise accepted, to be a tautology in the logic system being used, then you may use it.

In this case you are using Law of Excluded Middle, which is accepted in classical logic, but not in constructive logic.

EG: The Law of Excluded Middle is provable in a classical logic natural deduction system with the rule of Double Negation Elimination.$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{}{\fitch{\neg(\phi\vee\neg\phi)}{\fitch{\phi}{\phi\vee\neg\phi\quad\vee\mathsf I\\\bot\hspace{8ex}\neg\mathsf E}\\\neg\phi\hspace{10.5ex}\neg\mathsf I\\\phi\vee\neg\phi\hspace{6ex}\vee\mathsf I\\\bot\hspace{12ex}\neg\mathsf E}\\\neg\neg(\phi\vee\neg\phi)\hspace{5ex}\neg\mathsf I\\\phi\vee\neg\phi\hspace{10ex}\neg\neg\mathsf E}$$

Related Question