Practical Way Of Writing Natural Deduction Proofs

Question

Natural deduction has "natural" rules of deduction but has very "unnatural" and inpractical way of writing proofs as a trees. Is there some decently formalized way of writing natural deduction proofs that is useful in structuring everyday mathematical proofs?

Answer 1

I find the Fitch notation that has very explicit subproof structures, and that have to be strictly nested inside each other to be most like 'natural' deduction. It certainly looks very different from the Wikipedia page on Natural Deduction, which is probably what you are looking at. The Wikipedia page does refer to several different sequential representations rather than trees, and one of those is the Fitch notation. But please note that there are also sequential notations, such as the Lemmon System (System L), where assumptions can be discharged in any order ... which in my eyes is less 'natural' than the Fitch notation: when we do a mathematical proof, for example, we tend to discharge assumptions in the reverse order in which we introduce them, and that is exactly what the Fitch notation does. So again, in my eyes that is a much more 'natural' deductive system, even as there are many systems of 'natural deduction'.

Finally, I should mention that Fitch systems are characterized by having exactly one Introduction and one Elimination rule for each operator which, while mathematically elegant, does not always make for the most user-friendly system in terms of elementary inferences. For example, you won't find handy inference principles like Modus Tollens, Disjunctive Syllogism in a typical Fitch system. Also, Fitch systems typically don't have equivalence principles, such as DeMorgan or Distribution as part of their inference rules. So, there are some systems, the best known one of which is probably Copi's system (with Conditional Proof (CP) and Indirect Proof (with IP), that have some of those additional inference rules, but that have these strictly nested subproof structures as well.

Answer 2

What's unnatural about trees? They're an elegant way of capturing the structure of the proof: each node of the tree is labeled by a sentence and the deduction rule used to conclude that sentence, and the children of the node are the premises used by the rule.

If you just want to be able to arrange your proof on paper in a more efficient way, you can just make a numbered list of sentences, and next to each one indicate the rule used to conclude it, together with the numbers of the premises used. As long as you make sure that each item on the list (except the conclusion of the proof) is used as a premise for exactly one later item on this list, such a list captures exactly the same information as a proof tree.

In a comment to Bram28's answer, you write "I was thinking about paper friendly way of writing natural deduction rules (or very similar rules) so I can use it in my everyday work". If your everyday work is proof theory, then I can see the need for an efficient way of writing down formal proofs. But if your everyday work is doing (ordinary) mathematics, I'll suggest a much more efficient way of writing proofs, that mathematicians have been effectively using for centuries: natural language.