ABSTRACT
We have examined natural deduction systems for the last two chapters. These are not the only way to present a logic - another way is what has come to be known as a Hilbert system. A Hilbert system for a logic is a way of generating a set of formulae, called the theorems in the logic. These are the logical truths. They are generated from a list of axioms and a list of primitive rules. The set of theorems is the smallest set containing all of the axioms and which is closed under all of the rules. A Hilbert proof is a list in which every element is an axiom or follows from earlier elements in the list by way of one of the rules. Here is an example Hilbert system for the logic DMALL[o, ---+, 1\, v, rv], the exponential-free fragment of linear logic, with distribution added. (Or equivalently, R without contraction.) The axiomatisation has two rules
A, B ===} A 1\ B A, A---+ B ===} B
These rules are read as follows. If A and B are both theorems of the logic, so is A 1\ B. If A and A ---+ B are theorems of the logic, so is B. The comma in these rules is not related to the comma as a punctuation mark in structures.
