0

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!

KarmaPeasant
  • 838
  • It would be better to show the concrete proof, not only its structure. – Peter Sep 13 '18 at 11:45
  • Actually, if this proof sketch is your own work, it would be simpler just to prove $G\to G$ at the beginning and then combine $F\lor G$, $F\to G$, $G\to G$ like line 7 does. – hmakholm left over Monica Sep 13 '18 at 12:03
  • @Peter "Concrete proof" of what? I just literally took an exercise out of my textbook and proved conclusion differently than in solution. – KarmaPeasant Sep 13 '18 at 12:19
  • @HenningMakholm Why do you call it "proof sketch"? In my textbook such constructions are called "proofs", not "proof sketches". – KarmaPeasant Sep 13 '18 at 12:28

2 Answers2

1

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.

hmakholm left over Monica
  • 286,031
  • I'm the author of the "construction". And by the way, I don't understand why you don't count it as a proof. I literally took exercise out of my textbook and proved conclusion differently than in solution. – KarmaPeasant Sep 13 '18 at 12:18
  • @user161005: Your textbook is doing exactly what I describe here -- it's explaining how to piece together a proof from parts you already have. This is generally completely unproblematic. I'm not mentioning it as a criticism of the textbook or your proofs -- only pointing it out because you seemed to doubt that doing so is legit. – hmakholm left over Monica Sep 13 '18 at 12:40
0

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

Francisco José Letterio
  • 2,146