# Formal definitions in natural deduction

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?

• What's wrong with what's on Wikipedia? If you want to take "formal" very seriously, then there are also plenty of mechanized definitions in systems like Coq, Agda, Mizar, Isabelle/HOL, etc. It is often used as an exercise. (Also, "natural deduction" covers multiple logics and presentations of those logics, so there isn't one specific definition.) – Derek Elkins Aug 26 '18 at 5:00
• I would see how to formalize hypothetical derivations rules. – asv Aug 26 '18 at 6:13
• What is your motivation? Do you simply want a more clear explanation of natural deduction? IMHO many presentations of even basic natural deduction are needlessly complicated. The notation used in most for definitions might better be expressed in a more natural language. If you get stuck, you might review a few elementary proofs in, say, real analysis, and try to figure out what rules of logic were implicitly used. Figure out how, for example, mathematicians make generalizations on variables introduced in various ways and combinations. That is what I was eventually forced to do. – Dan Christensen Aug 26 '18 at 17:12
• See some textbook: van Dalen's one and Chiswell & Hodges. – Mauro ALLEGRANZA Aug 26 '18 at 19:57
• For example, I did a Coq formalization of natural deduction for propositional logic as an exercise (mostly leading towards formalizing the cut elimination theorem for sequent calculus): github.com/dschepler/coq-sequent-calculus/blob/master/… see the definition of classic_ND_proves . (Though my formalization heavily relies on Coq's notion of an inductively defined relation.) – Daniel Schepler Feb 13 at 1:44

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/

• Thank you, how is defined formally a rule? Is it a pair of formula? I would like a formal definition. Same for derivation. For example a graph is a pair G=(V,E) with soem properties. In substance a formal definition of the objects. – asv Feb 13 at 13:11
• @asv The formal definition is what is provided in the illustration for conditional introduction (or hypothetical derivations). Given an assumption $A$ and another derived line $B$ (which could be a reiteration of $A$, you can write the last line $A \rightarrow B$ with justification as stated. That would be the formal definition. The forallx text gives other such formal definitions. They are formalized also in the sense that the proof checker implements them as code. – Frank Hubeny Feb 13 at 13:19
• Ok, I was searching a formal way like this: books.google.co.uk/… Thank you for your answer. – asv Feb 13 at 16:43