Definition of proof in natural deduction

Question

When working with a Hilbert system a proof is a sequence of formulae $\phi_1, \dots, \phi_n$ where each formula is an axiom or follows from previous formulas (by inference rules such as modus ponens).

But when working in a natural deduction calculus, the rules are to be interpreted in a context (previous assumed hypotheses), so this definition doesn't work for natural deductions calculi (unless one works with sequences $\Gamma\vdash\phi$ that record the hypotheses).

How can one precisely define a proof in a natural deduction system as a "tree"?

https://i.stack.imgur.com/REVAm.png

Answer 1

The typical solution is to let a proof be a sequence of things of the form $\Gamma\vdash\phi$.

There are various notations that try to hide the $\Gamma$, but they seem to me to be both cumbersome to specify from a technical point of view and rely confusingly on "action at a distance" for a human reader.

In order to define precisely what is a valid tree in the notation in your image, one would still need to have a $\Gamma$ (or something very much like in it) present in the definition of "valid proof", even if it's not explicitly visible on paper.

Answer 2

See e.g. :

• Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 54.

[page 7] Definition 2.1.2 A sequent is an expression ($Γ \vdash \psi$) where $\psi$ is a statement (the conclusion of the sequent) and $Γ$ is a set of statements (the assumptions of the sequent). We read the sequent as ‘$Γ$ entails $\psi$’. The sequent ($Γ \vdash \psi$) means

There is a proof whose conclusion is $\psi$ and whose undischarged assumptions are all in the set $Γ$.

After having introduced the usual Natural Deduction rules for the propositional conncetives, we have :

[page 54] Definition 3.4.1 Let $σ$ be a signature. Then a $σ$-derivation or, for short, a derivation is a left-and-right-labelled tree (drawn branching upwards) such that the following hold:

(a) Every node has arity $0, 1, 2 or 3$.

(b) Every left label is either a formula of $LP(σ)$, or a formula of $LP(σ)$ with a dandah [i.e. a "crossed formula"].

(c) Every node of arity $0$ [i.e. a leaf] carries the right-hand label (A).

(d) If $\nu$ is a node of arity $1$, then one of the following holds:

details regarding the rules follow;

(e) If $ν$ is a node of arity $2$, then one of the following holds:

[...]

(f) If $ν$ is a node of arity $3$, then

[...]

(g) If a node $\mu$ has left label $\chi$ with a dandah, then $\mu$ is a leaf, and [...]

The conclusion of the derivation is the left label on its root, and its undischarged assumptions are all the formulas that appear without dandahs as left labels on leaves. The derivation is a derivation of its conclusion.

Another definition is into :

• Dirk van Dalen, Logic and Structure (5th ed - 2013), page 32.