Proof Theory Landscape

Strength of the Logical System

Depending on the particular rules and connectives chosen, any of the following styles of rule systems may be used to define minimal, intuitionistic, or classical versions of propositional or predicate logic. The strength of the logic refers to the set of formulas that are provable in the system rather than the method of proof.

Proof Systems

Rule system	Primary characteristic	Proof trees with assumptions at leaves ("non-sequent-style")	Proof trees with assumptions managed at each node ("sequent-style")	Proofs as lists
Hilbert system	Many axioms, but only one inference rule: modus ponens	Typical presentation	Possible, but not typical because nothing interesting is done to the context of assumptions as it is carried along	This historically preceded thinking of proofs as trees and would have been the original method of doing Hilbert-style proofs; it is trivally applicable to any rule system since there is no substantial difference from trees: do a topological sort of the nodes of the proof tree and use pointers to identify parent nodes
Natural deduction	Rules divided into introduction and elimination rules	A common presentation; originated with Jaskowski (1929); not extensively used in proof theory until Prawitz (1960s); perfect isomorphism with simply-typed lambda-calculus	Also common; originated with Gentzen (1935)
Sequent calculus	Rules divided into left and right introduction rules	Does not make sense since left rules affect the context of assumptions	The original method (Gentzen, 1935)

Further Distinctions

The management of contexts at the nodes of the proof tree in sequent-style proofs allows for two more dimensions of flexibility:

• The mathematical structure used to hold assumptions, e.g. sets, multisets, lists, maps
• Additive vs. multiplicative contexts (multiplicative much more common)

Furthermore, these choices interact with the rule system because one may want or need to add structural rules depending on the choices made.

Finally, it is interesting to note that in order to define a sequent-style natural deduction system that is isomorphic to the non-sequent-style system that Prawitz used, one must choose among the above options carefully. In particular, the most simple and obvious ones won't work.