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?
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.Sign up to join this community
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.
"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/