What is a natural deduction proof system, formally?

Question

I asked a similar question a while ago, but I didn't get a good response. A Hilbert-style proof is a non-empty sequence of statements, all of which are either axioms, or follows from previous steps by inference rules. Note that a sequence can be defined set-theoretically, so in fact a Hilbert-style proof can be defined set-theoretically. In natural deduction proofs, there are subproofs, or proofs within proofs. Also, there are meta-inference rules, like the rule for conditional introduction. Is there a paper or book that formalizes what a natural deduction proof system actually is?

Answer 1

"Nested structures" like natural deduction arguments are really just trees - or rather, labelled trees - and these are no more difficult to implement set-theoretically than sequences. For example, the following approach works:

• A finite tree is a finite set $T$ of finite sequences of natural numbers which is closed downwards (if $t\in T$ and $s\prec t$ then $s\in T$).

• A labelled finite tree is a pair $(T, l)$ where $T$ is a finite tree and $l$ is a function with domain $T$.

A natural deduction proof is then a certain type of labelled finite tree. The codomain of $l$ is the set of all grammatically correct sequents, and the inference rules describe a class of "legal" labellings. For example, we might have the rule:

If $s$ is a terminal node of $T$ then $l(s)=$ "$\Sigma\vdash p$" for some $\Sigma\ni p$.

Note that the informally-presented sequent manipulation rules translate automatically to formal requirements of the labelling functions. The result is a perfectly formal, if messy to write out in full, definition.