# Calculational proofs and Natural Deduction system.

We are all familiar with calculational reasoning. A proof by calculational reasoning basically proceeds by forming a chain of intermediate results that are meant to be composed by basic principles, such as transitivity of =,<, ≤ (or similar relations).

Is the calculational style orthogonal to the Natural Deduction calculus? I mean, is it possible to compose a calculational proof using only the inference rules in Gentzen's Natural Deduction? What formal systems are usually used along with caclulational proofs? I always see calculational proofs along with axiomatic systems (not with ND). Maybe this is due to the difficulty to formalize in a calculation the introduction of hypothesis that are later discharged under certain conditions.

Can a proof using the Natural Deduction calculus be formalized in a calculational style?

What formal systems are usually used along with calculational proofs?

## 1 Answer

Your question seems to be based on a false premise. Natural deduction systems for first-order logic prove exactly the same theorems as Hilbert-style deductive systems for first-order logic. People don't often use natural deduction systems not because it is hard to use for certain kinds of proofs (in fact it is much easier than using Hilbert-style calculii), but because it is less well-known. Few have heard of it compared to how many people have come across boolean algebra and equivalence proofs of tautologies or the like.

In almost all formal system, even in Hilbert-style systems, what you call calculational proofs are not directly supported because usually people include rather minimal rules. Instead, all they have are usually something equivalent to equality introduction and elimination rules. Similarly, inequality chains are derivable via repeated application of transitivity axioms, and so do not need to be directly supported by the formal system.

Note that I am talking about mathematical specifications of formal systems, not necessarily the ones you find in proof assistants, since computers can be easily programmed to apply much more rules than the bare minimum necessary for the formal system to work.