# 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?

• because it is less well-known You'd think that people who created Metamath would have heard of natural deduction when they started the project -- I mean, I've heard of it, and I know much less. Anyway, my question about this could use more answers.