Is it OK to insert a tautology in a proof out of thin air?

Question

As far as I understand, normally all lines of a proof follow from some premises (except for the premises themselves, of course) or from lines following from premises, or from lines following from lines following from premises, .... But I have never seen a proof where you pull a tautoloy out of thin air and insert it into middle of your proof in order to make it work. Is this technique legitimate? Or were I just being lucky that it worked in my proof? Sorry if it's naive question, but I just want to be safe and be more-or-less sure that my self-made technique won't get me into trouble.

Consider this example:

Conclusion to prove: G

Proof:

1.F->G /Premise

2.FvG /Premise

3.~~FvG /2 Double negation of F

4.~F->G /3 Rule of replacement for implication

5.~FvF /Tautology inserted out of thin air

6.(F->G)&(~F->G) /1,4 Conjunction

7.GvG /5,6 Conclusion of constructive dilemma

8.G /7 Rule of replacement for tautology

We proved the conlclusion!

Answer 1

We usually work under axiomatic systems when constructing proofs. This means that you start with base identities that we assume to be true for any formulae that we plug in. Then we also define the rule of modus ponens: Knowing that $A \rightarrow B$ is true and $A$ is true, we define $B$ to be true (the modus ponens is itself an axiom).

ALL other axioms (under a complete a axiomatic system) can be deduced via Modus Ponens from our base axioms and another axioms we find along the way. So the $\lnot F \lor F$ statement has its own proof. It would be time consuming to write every proof of every axiom whenever you use one, so we just say it's true because we know it has its own proof

Surprisingly, whenever we do proofs in any other area of mathematics, we're implicitly using axioms. For example, let's say you're trying to prove an algebraic identity, and at one step you need to use the fact $a + b = b + a$. This fact has its own proof, and its proof is at the same time based on axioms (usually the Peano axioms). When we use this identity, it's not like it's spawning out of thin air, we just know it has a proof, and writing a proof for every axiom/fact we want to use would be a lot of wasted effort.

In your case, you're doing the same: the fact that $\lnot F \lor F$ is deductible (that is, can be proved just by axioms) is already known, so you don't have to prove it again to use it in your proof

Answer 2

Strictly speaking what you have there is not a formal proof, but a description of how to construct a formal proof.

The author is basically saying,

You remember that we have already see that $\neg F\lor F$ has a proof, right? Imagine all the steps of that proof being inserted here.

This allows them to focus more clearly on the points that are new in the proof you're looking at.