# Can you introduce a tautology directly into a proof?

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

• I think this happens alot (maybe even indirectly), when there is a prove by contradiction. Especially when you need to show that two things are true, but one premise negates one while validating another – CoffeeArabica Sep 30 '19 at 4:37
• If you allow excluded middle then through natural deduction you can introduce "truth T" anywhere and derive excluded middle from it – qwr Sep 30 '19 at 4:38
• Excluded middle is NOT a tautology in intuitionist logic. – qwr Sep 30 '19 at 4:39
• @qwr - From what I understand the law of the excluded middle is more of a underlying principle in classical logic and not a rule of inference used in natural deduction. If I'm wrong, however, please correct me, and perhaps show me some examples that exist in texts? I'm specifically wondering if there are established rules that permit the immediate introduction of a tautology like the one I've described. – RyRy the Fly Guy Sep 30 '19 at 4:45
• @CoffeeArabica - I absolutely agree that this sort of approach occurs often in an INDIRECT way. I'm wondering whether a direct approach is permitted, and if not, why not? – RyRy the Fly Guy Sep 30 '19 at 4:48

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}$$

• Thanks for the response. I'll look into this and get back to you. This is the first time I've heard of tautological consequences. – RyRy the Fly Guy Sep 30 '19 at 13:11

I think your reasoning is a bit circular. In a proof tree of a propositional calculus, the only premises you are allowed to have are (a) your assumptions, and (b) premises that are 'cancelled' by use of an inference rule (see, eg, the exercise cited here). But this still allows you to do what you want to do (in a sense). A tautology, by definition, is a statement that can be derived from no premises: it is always true. The particular example you give isn't quite appropriate, because that's the law of the excluded middle, which is an inference rule of classical logic and not a tautology (especially because it is not true in intuitionistic logic). The tautology I'm thinking of is $$p \rightarrow p$$, which can be introduced into your proof by adding $$p$$ as a premise and using an implication-introduction to derive $$p \rightarrow p$$ and cancel the premise-$$p$$.

So, yes, you can introduce tautologies wherever you want, because they require no premises to prove. You seem to understand this with your line about "introducing it via the conditional proof", but I do not see a difference between proving it from nothing and inserting it without proof, except that the latter is less formal.

• You said my example in which I introduce $p \vee \neg p$ is not appropriate because it is the law of the excluded middle and not a tautology. You then go on to illustrate your own example in which you derive $p \rightarrow p$, which is identical to what I did! Note that $p \rightarrow p$ in your example is logically equivalent to $p \vee \neg p$ via impl and comm laws, and the method you described for deriving $p \rightarrow p$, that is, the conditional proof, is the very method I acknowledged one could use to derive a statement such as $p \vee \neg p$ with no help from other premises. – RyRy the Fly Guy Sep 30 '19 at 12:30
• Despite misconstruing my example, you seem to understand the essence of my question, which is why don't we introduce a tautology such as $p \vee \neg p \Leftrightarrow p \rightarrow p$ directly among our premises "without proof" vs. going through the process of deriving a tautology (apart from any premises, of course, because as you pointed out we don't need premises to derive a tautology). You said you see no difference between the two approaches except that the former is less formal. The former is much briefer as well. – RyRy the Fly Guy Sep 30 '19 at 12:49
• If your criticism is that the former approach, that is, introducing a tautology directly among our premises "without proof," is less formal, then I suppose I would like to know why you think so. If a statement is simply true in the context of the logical system that you're using, then I don't understand why it is inappropriate to introduce it directly among the premises. – RyRy the Fly Guy Sep 30 '19 at 12:55
• Here is a criticism that comes to mind as I am discussing this with you: the example I give is a very simple example in which the tautology I'm introducing is extremely obvious. In that case, then yes, my argument to simply introduce the statement directly among the premises "without proof" feels reasonable and less like a transgression against any respectable proof. However, one could what if one wants to introduce a tautology in the form of a much longer and more complex statement? – RyRy the Fly Guy Sep 30 '19 at 13:03
• In that case, simply introducing a tautology "without proof" is not as acceptable, and it would be desirable and certainly more rigorous to go through the steps and derive the entire statement from scratch. So maybe in the end your final criticism against introducing tautologies "without proof" is legit. It is indeed less formal. It doesn't seem that way when one is introducing simple tautologies into an argument, but it becomes more apparent when one introduces more complex tautologies. – RyRy the Fly Guy Sep 30 '19 at 13:05

Perhaps you are also interested in a bit more practical, theorem prover-oriented side.

Let's assume we know $$1 + 1 = 2$$ and use that to prove $$(1 + 1) + 1 = 2 + 1$$. Clearly, we can just use the first equality to replace $$(1 + 1)$$ by $$2$$ yielding our goal.

This toy example looks as follows in the theorem prover Coq:

(* vvv Just some imports *)
From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* Actually we don't assume 1 + 1 = 2, but in fact prove it *)
Theorem thm: 1 + 1 = 2.
Proof.
(* albeit by a powerful command which can prove it on its own without human
intervention *)
by auto.
Qed.

Theorem thm': (1 + 1) + 1 = 2 + 1.
Proof.
(* Here we deduce 1 + 1 = 2 in an ad-hoc manner by just referencing
the previous thm *)
have U: (1 + 1 = 2) by apply: thm.

(* Then we rewrite as explained in the answer text above *)
by rewrite U.
Qed.


Hence, yes, similar to how a mathematician can pull a theorem out of thin air to insert it in their script, we can do so in Coq.

Note that a theorem is nothing else than a tautology. So you have cascade of interdependent theorems with axioms at the very top. But axioms behave very much the same way as theorems in Coq, so can also by used in have commands.

• Thanks for responding. It's true that mathematicians simply insert necessary theorems into proofs as needed, as your program is illustrating. And I suppose that, in the context of propositional logic, tautologies could be conceived as logical consequences or "theorems" descending from a larger set of axioms underlying the logical system. For example, $p \vee \neg p$ is only a tautology under the assumption that propositions are either true or not true. However, even when we introduce such tautologies in the conventional manner, we don't start with such axioms. – RyRy the Fly Guy Sep 30 '19 at 14:47
• So, yes, to an extent I suppose we already do the very thing I am talking about... to an extent. The answer to my question is starting to become more clear. – RyRy the Fly Guy Sep 30 '19 at 14:49
• @RyRytheFlyGuy Exactly, tautologies are just theorems. And yes, usually you just want to say "import theorem/tautology xyz, please" instead of replaying all of the proof. Sure, theoretically, replaying suffices, but eventually, we want to get to usable systems for formalizing maths, don't we? – ComFreek Sep 30 '19 at 14:52

Whether you can add in a tautology or not would depend on the proof assistant/checker you are using and the inference rules that tool permits. If you are doing it manually it depends on what the audience watching or reading your proof will permit you to use.

Here is a proof of the example using a Fitch-style proof checker:

I could add the premise $$P \lor \lnot P$$, but since I already have an LEM (law of the excluded middle) inference rule, it does not save me any work and it adds to the set of premises. However, after the list of premises, I could not add this as a line in the proof because this particular tool has no inference rule permitting that.

Also, although this tool has a disjunction elimination rule, I would need two subproofs in additional to the line containing the disjunction to use the rule as justification. This would be similar to what I provided above to reference LEM.

The advantage of using such tools is they make sure one is always using a well-formed formula and one is following the inference rules exactly. If one does that one can get a confirmation that the proof is correct. The disadvantage is that one has to follow those syntax and inference rules exactly.

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