What is natural deduction used for outside of academia?

Question

Hello,

I am studying natural deduction as a part of my Formal Specification & Verification Computer Science course at University/College.

I find it interesting, however I learn much better when I can find a practical use for things.

Could anyone explain to me if and how natural deduction is used other than for formally verifying bits of code?

Thanks!

Answer 1

Natural deduction is very interesting and kind of cool, but it is very rarely used outside of academia. Formal proofs of correction on programs are tedious using natural deduction, and thus higher level tools are often used.

Answer 2

Should I cross the road here?

• There is a big bus about to pass.
• There is lava flowing down the road.
• There is a crossing 10 meters further along.

Deduction: Should not cross the road here.

Answer 3

Natural deduction isn't that much used in practical formal methods: sequent calculus is generally a better basis, because it is closer to the tableau methods used in constructing decision procedures for logics. Tableau methods are pretty central to practical applications of logic in computer science.

Natural deduction is most used in constructive type theory, and this gives it some leverage in programming language design. It's considered a nice-to-know, though, rather than a must know.

The main value of natural deduction is that it is the nicest way to learn formal inference, but this is a didactic application seen mostly in academia.