# How to prove math theorems in formal logic or at least in the style of natural deduction?

I have become rather interested lately in proofs in mathematics, and I discovered at first to my surprise that they are written in paragraph form using natural language. Although this seemed out of character for the mathematics I have always known, upon reflection I embraced that change of pace: since my primary interest is in philosophy, it is absolutely imperative that I learn to write rigorous "informal" arguments anyway. I was curious though, is there any system for deriving mathematical theorems that is similar to natural deduction? I would like to have the best of both worlds--to be able to express myself informally yet with rigor, but also to be able to fall upon iron-clad symbols if need be. To give an idea of what I am looking for, this is an improvised example (without using symbols from formal logic though):

1. 2x + 7 = 11

Ergo* x = 2

1. 2x + 7 - 7 = 11 - 7 ..... 1, SI (Subtraction Introduction)
2. 2x + 0 = 11 - 7 ..... 2, SE (Subtraction Elimination)
3. 2x + 0 = 4 ..... 3, SE (Subtraction Elimination)
4. 2x = 4 ..... AE (Addition Elimination)
5. 2x/2 = 4/2 ….. DI (Division Introduction)
6. x = 4/2 ….. DE (Division Elimination)
7. x = 2 ….. DE (Division Elimination)

QED

Those abbreviations and names for those rules of algebra I made up on the spot, but hopefully you all get the idea. I am most used to natural deduction as it is presented in Patrick Hurley’s book (with names like Simplification and Disjunctive Syllogism instead of “_ introduction” and “_ elimination” where the given symbol that is manipulated is placed in the _). I hope that this question is not too broad for the forum—if it is, suggesting a book would help too.

*I used "Ergo" since I lack the ability to type the triangle-dot symbol which means "therefore" in logic.

• If you get to the point of using MathJax, the triangle dot symbol is \therefore. It ends up looking like $\therefore$. Commented Sep 15, 2014 at 0:21
• There's no system that I know of (that's why they are "informal" proofs), but you may want to check out Patrick Suppes's Introduction to Logic, chapter 7, which tries to ease the transition from a natural deduction system to a more informal setting. I think David Velleman's How to Prove It also focus on this informal setting. Commented Sep 15, 2014 at 1:04

Some further remarks: you'll find that deriving mathematical theorems is strikingly similar to doing natural deduction (not by chance: Gentzen was inspired by actual mathematical reasoning in setting up his system). So, if you really want to, you can try to convert an informal proof into a natural deduction one. For instance, let's analyze your little deduction a bit more closely. Step 2, which you called "Subtraction Introduction", is actually an instantiation of a general logic rule, which can be formally states as:

$$\forall x \forall y \forall z (y = z \rightarrow f(x, y) = f (x, z))$$

(The above rule is given as an "equality axiom" in Shoenfield's *Mathematical Logic", for instance; cf. p. 21).

So, in your above proof, you could introduce this axiom as a premiss in your preferred natural deduction system, signaling the dependence of what comes next on this line (that's generally not a problem, as your derivations will typically depend on the axioms of whatever theory you're working with plus the logical axioms).

Now, going to step three, there are actually two steps there: you are instantiating a field axiom to $$7$$ (specifically, the existence of an inverse axiom: $$\forall x \exists y (x + y = 0)$$) and then using term substitution (I think Shoenfield calls it the "equality theorem" in his book; cf. p. 35) to replace $$+(7, -7)$$ by $$0$$; similarly, in step 4, you're substituting $$+(11, -7)$$ by $$4$$. On step 5, you're using another field axiom, namely the existence of an identity element ($$\exists x \forall y (x + y = y)$$), and again substitution, to obtain $$2x$$ from $$+(2x, 0)$$. On step 6., you're using the existence of an inverse to multiplication and the logical rule referred above to introduce division. Finally, both step 7 and 8 use substitution. Let's try to put this into a natural deduction system (I'll just sketch a more or less Fitch style deduction here).

So, in order to codify this more neatly into a natural deduction, I'll take the above equality axiom (let's call it EA) also substitution (let's call it SUB) as rules of inference. I'll also use the following axioms, listed above (let's assume that the underlying theory is the field of reals; for simplicity, let's also assume that the language has constants to denote all the real numbers; I'll not use all of the field axioms, just the relevant ones).

A1. $$\forall x \forall y \forall z ((x + y) + z = x + (y + z))$$;

A2. $$\forall y (0 + y = y)$$;

A3. $$\forall x \exists y (x + y = 0)$$;

A4. $$\forall x (x \not = 0 \rightarrow (\exists y (x \cdot y = 1)))$$

Now, from the above axioms and the rules of inference it's possible to show that the $$y$$ in both A3. and A4. is unique for each real number, so we can introduce constants to denote them. It's also possible to show that subtraction and division are possible by carefully choosing our substitution instances (e.g. the possibility of subtraction can be said to consist in the fact that the following sentence holds in the structure: $$\forall x \forall y \exists z (x + z = y)$$; we can show that this holds by choosing $$z = (-x + y)$$). Here, I'll just assume that this can be all be "read off" from those axioms.

So we would have something like:

1. $$\exists x (2x + 7 = 11)$$ Assumption; 2.$$2a + 7 = 11$$ 1, Existential Elimination;
2. $$(2a + 7) + (-7) = 11 + (-7)$$ 2, EA;
3. $$2a + (7 + (-7)) = 11 + (-7)$$ 3, A1;
4. $$7 + (-7) = 0$$ A3 (by definition, (-7) denotes the inverse of 7);
5. $$2a + 0 = 11 + (-7)$$ 4, 5, SUB;
6. $$2a = 11 + (-7)$$ 6, A2
7. $$11 + (-7) = 4$$ A2, A3 (by the theorem which states the possibility of subtraction, mentioned above);
8. $$2a = 4$$ 7, 8, SUB;
9. $$2a/2 = 4/2$$ 9, EA;
10. $$2a/2 = a$$ A4 (by the possibility of division, actually);
11. $$4/2 = 2$$ A4 (same as above)
12. $$a = 4/2$$ 10, 11, SUB;
13. $$a = 2$$ 12, 13, SUB;

Anyway, that was a bit rough, but it should give you some idea about how to do it. As I said, I strongly recommend reading chapter 7 of Suppes's book, which provides a nice transition from natural deduction proofs (which are dealt with in a more relaxed manner in his book) to informal mathematical proofs.

• @goblin - Thanks for the correction! I've changed it already. Commented Apr 6, 2016 at 0:56
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 31, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "https://math.stackexchange.com/questions/931681/how-to-prove-math-theorems-in-formal-logic-or-at-least-in-the-style-of-natural-d", "fetch_time": 1723047136000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2024-33/segments/1722640694594.35/warc/CC-MAIN-20240807143134-20240807173134-00696.warc.gz", "warc_record_offset": 311349130, "warc_record_length": 39809, "token_count": 1841, "char_count": 6650, "score": 3.90625, "int_score": 4, "crawl": "CC-MAIN-2024-33", "snapshot_type": "latest", "language": "en", "language_score": 0.9455605149269104, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00050-of-00064.parquet"}