Relationship between sequent calculus and Hilbert systems, natural deduction, etc

I am trying to learn the basics of logic and I'm confused on how these proof systems work together. The big ones I see are Hilbert style, and then Gentzen style which includes natural deduction, and sequent calculus. I also see "intuitionistic logic" and "minimal logic" and "modal logic" and "fuzzy logic" but I don't know where these fit.

Are all of these systems different ways of proving the same propositional statements, merely using different sets of rules? Do any of these systems offer power that the others do not?

• Hilbert-style, Natural Deduction, Truth Trees (aka Tableaux method), Sequent calculus: basically, different equivalent proof systems : for a fixed "semantics", like e.g. classical logic. – Mauro ALLEGRANZA Nov 19 '18 at 19:13
• They can be used for logics based on different "principles", like e.g. Intuitionistic, Paraconsistent, Fuzzy logic that share with classical logic some but not all the basic inference rules. – Mauro ALLEGRANZA Nov 19 '18 at 19:14
• This means that you can have an Hilbert-style proof system for e.g Intuitionistic Logic as well as a Natural Deduction one, etc. – Mauro ALLEGRANZA Nov 19 '18 at 19:15
• "Hilbert / natural deduction / truth trees / sequent calculus" as proof systems are distinct from "classical / intuitionistic / paraconsistent / modal / fuzzy"? What are the latter called? I had assumed these were proof systems too – Brandon L Nov 19 '18 at 19:28
• You can start from the initial chapters of a textbook : Katalin Bimbo, [Proof Theory : Sequent Calculi and Related Formalisms](ttps://books.google.it/books?id=ulzOBQAAQBAJ&printsec=frontcover), CRC (2015) – Mauro ALLEGRANZA Nov 20 '18 at 7:55

To define a logic you need to specify a language of formulas, and then you need to provide either 1) a semantics, or 2) a proof system (i.e. a collection of rules of inference).

For commonly discussed logics, we usually have definitions both in terms of semantics and proof systems, and we have meta-theorems which connect specific pairs of semantics and proof systems. These are the soundness and completeness meta-theorems. Saying "classical propositional logic" means "the logic defined by any of these equivalent semantics or any of these equivalent proof systems" for a specific value of "these semantics/proof systems" e.g. truth table semantics. You can have nonequivalent semantics/proof systems and this leads to different logics. You can also have different languages of formulas and this too can lead to different logics.

Classical, intuitionistic, and minimal logic can be presented so that they use the same language. In fact, they can be presented (in multiple ways) so that the rules of inference given for minimal logic are a strict subset of those given for intuitionistic logic which are in turn a strict subset of those given for classical logic. Modal logic and fuzzy logic have a different language than classical logic.

To talk about a (formal) proof, you need a proof system. What constitutes a proof depends on the proof system and there can be many for a given logic. For a specific logic, these will be necessarily equivalent since they define the same logic. For our purposes, "equivalent" here means that the same collection of formulas have proofs. Those proofs will look different between different proof systems, but the fact that some proof exists will be the same between them.

Hilbert-style, sequent calculi, and natural deduction systems are three "styles" for organizing the rules of a proof system. This Wikipedia page lists dozens of distinct Hilbert-style proof systems. All the proof systems in section 1 are equivalent, but they aren't equivalent to the proof systems in section 3, say. The Wikipedia page for the sequent calculus primarily focuses on LK but presents multiple variations of that. Some equivalent and some, like LJ, nonequivalent. Similarly for the natural deduction page. As illustrated on that page (and as is more generally true), all of these "styles" are applicable to different languages, e.g. the language used by modal logic.

Hilbert-style systems try to reduce the number of rules of inference and replace them with logical axioms. This makes the meta-theory of Hilbert-style systems much simpler but tends to make using them very unpleasant. Sequent calculi and natural deduction systems go the other direction and minimize or even eliminate logical axioms in preference to rules of inference. This allows connectives to be characterized by rules which involve only that connective. This makes these proof systems modular in that you can easily add or remove connectives just by adding/removing the relevant rules. These proof systems make it easier to generic "structural" properties of connectives, rules of inference, and the logic itself whereas everything tends to serve multiple purposes and be interdependent in Hilbert-style systems. The rules of natural deduction systems focus on the formula you're proving which tends to make building proofs fairly natural. In contrast, sequent calculi also focus on assumptions which tends to be unintuitive. On the other hand, building a proof in a natural deduction system has a kind of outside-in feel while in a sequent calculus you build proofs in a bottom-up fashion. This makes sequent calculi easier to prove things about.

Via the Curry-Howard correspondence, each of these styles lead to different ways of relating to type theory/programming. Hilbert-style systems correspond to combinatory logic. Natural deduction systems to typed lambda calculi with constructors and destructors. The sequent calculus case is a bit more subtle and technical.