Formal definitions in natural deduction

Question

I am searching a formal definition of natural deduction rules and a formal definition of derivation in natural deduction.

For example how does one formalize hypothetical derivations?

Answer 1

A reference for natural deduction inference rules can be found on the right side of Klement's natural deduction, Fitch-style proof checker. The text forallx goes into each rule in more detail.

In particular the OP would like to how one formalizes hypothetical derivations. Wikipedia describes these as "reasoning from assumptions". This allows one to derive and if-then statement.

The authors of forallx describe this as "conditional introduction". (Section 15.3, page 106)

The general pattern at work here is the following. We first make an additional assumption, A; and from that additional assumption, we prove B. In that case, we know the following: If A, then B. This is wrapped up in the rule for conditional introduction:

The above would be their formal definition and a guide for using their proof checker.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

"Natural deduction" Wikipedia https://en.wikipedia.org/wiki/Natural_deduction

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/