Editing Sequent calculus (section)

===Hilbert-style deduction systems===
{{Main|Hilbert system}}
One way to classify different styles of deduction systems is to look at the form of ''[[Judgment (mathematical logic)|judgments]]'' in the system, ''i.e.'', which things may appear as the conclusion of a (sub)proof. The simplest judgment form is used in [[Hilbert system|Hilbert-style deduction systems]], where a judgment has the form
:<math>B</math>
where <math>B</math> is any [[Well-formed formula|formula]] of first-order logic (or whatever logic the deduction system applies to, ''e.g.'', propositional calculus or a [[higher-order logic]] or a [[modal logic]]). The theorems are those formulas that appear as the concluding judgment in a valid proof. A Hilbert-style system needs no distinction between formulas and judgments; we make one here solely for comparison with the cases that follow.

The price paid for the simple syntax of a Hilbert-style system is that complete formal proofs tend to get extremely long. Concrete arguments about proofs in such a system almost always appeal to the [[deduction theorem]]. This leads to the idea of including the deduction theorem as a formal rule in the system, which happens in [[natural deduction]].