Les logiques : notes en vrac

The Hilbert proof systems are systems based on a language with implication and contain a Modus Ponens rule as a rule of inference. They are usually called Hilbert style formalizations. We will call them here Hilbert style proof systems, or Hilbert systems, for short.

Modus Ponens is probably the oldest of all known rules of inference as it was already known to the Stoics (3rd century B.C.). It is also considered as the most ”natural” to our intuitive thinking and the proof systems containing it as the inference rule play a special role in logic. The Hilbert proof systems put major emphasis on logical axioms, keeping the rules of inference to minimum, often in propositional case, admitting only Modus Ponens, as the sole inference rule.

• Hilbert style. Every line is an unconditional tautology (or theorem).
• Gentzen style. Every line is a conditional tautology (or theorem) with zero or more conditions on the left.
• • Natural deduction. Every (conditional) line has exactly one asserted proposition on the right.
  • Sequent calculus. Every (conditional) line has zero or more asserted propositions on the right.

In other words, natural deduction and sequent calculus systems are particular distinct kinds of Gentzen-style systems. Hilbert-style systems typically have a very small number of inference rules, relying more on sets of axioms. Gentzen-style systems typically have very few axioms, if any, relying more on sets of rules.

Il semble que ce qui est appelé kind, est le type d’un type.