In the context of computer science, natural deduction has a very important role to play. The structure of proofs in natural deduction can be read as simple functional programs with a reduction semantics given by the way the introduction and elimination rules for a certain connective fit together.
For example, consider a proof of (A ^ B) => (B ^ A). In natural deduction, this can be written
--------------x ---------------x
A ^ B |- A ^ B A ^ B |- A ^ B
-------------- ^E2 ----------------^E1
A ^ B |- B A ^ B |- A
-------------------------------^I
A ^ B |- B ^ A
---------------^I(x)
|- A^B => B^A
A more concise way of writing this proof would would be (fun x = <#2 x, #1 x>)
. In other words, it's a function that takes a pair of values, and returns a pair of the second component followed by the first component.
In this interpretation of programs as proofs, the propositions proven true in natural deduction give a type system. By making sense of other logical connectives in terms of natural deduction, we get new type systems and sometimes new program constructs in the programming language.
This idea is frequently referred to as the Curry-Howard Correspondence, which forms the basis of a great deal of modern programming language research.