Mixing
Relationship between sequent calculus and Hilbert systems, natural deduction, etc
up vote
1
down vote
favorite
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?
logic propositional-calculus natural-deduction sequent-calculus hilbert-calculus
asked 2 days ago
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
|
show 1 more comment
up vote
1
down vote
favorite
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?
logic propositional-calculus natural-deduction sequent-calculus hilbert-calculus
asked 2 days ago
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
1
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
2 days ago
1
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
2 days ago
1
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
2 days ago
1
"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
2 days ago
Unfortunately there is no short answer to this question. They are adjectives, describing certain aspects of logical systems. For instance, "modal" generally means there are the $square$ and $Diamond$ connectives in the language (and little else unless qualified further). "Intuitionistic" generally means negation behaves differently than classically, although often a very specific theory like intuitionistic propositional or predicate logic is intended. "Paraconsistent" is fairly broad and just means there are nontrivial inconsistent theories. "Fuzzy" means the semantics are $[0,1]$-valued.
– spaceisdarkgreen
yesterday
|
show 1 more comment
up vote
1
down vote
favorite
up vote
1
down vote
favorite
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?
logic propositional-calculus natural-deduction sequent-calculus hilbert-calculus
asked 2 days ago
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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?
logic propositional-calculus natural-deduction sequent-calculus hilbert-calculus
logic propositional-calculus natural-deduction sequent-calculus hilbert-calculus
asked 2 days ago
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 2 days ago
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 2 days ago
Brandon L
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 2 days ago
Brandon L
184
asked 2 days ago
Brandon L
184
184
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
New contributor
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
Brandon L is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
1
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
2 days ago
1
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
2 days ago
1
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
2 days ago
1
"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
2 days ago
Unfortunately there is no short answer to this question. They are adjectives, describing certain aspects of logical systems. For instance, "modal" generally means there are the $square$ and $Diamond$ connectives in the language (and little else unless qualified further). "Intuitionistic" generally means negation behaves differently than classically, although often a very specific theory like intuitionistic propositional or predicate logic is intended. "Paraconsistent" is fairly broad and just means there are nontrivial inconsistent theories. "Fuzzy" means the semantics are $[0,1]$-valued.
– spaceisdarkgreen
yesterday
|
show 1 more comment
1
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
2 days ago
1
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
2 days ago
1
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
2 days ago
1
"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
2 days ago
Unfortunately there is no short answer to this question. They are adjectives, describing certain aspects of logical systems. For instance, "modal" generally means there are the $square$ and $Diamond$ connectives in the language (and little else unless qualified further). "Intuitionistic" generally means negation behaves differently than classically, although often a very specific theory like intuitionistic propositional or predicate logic is intended. "Paraconsistent" is fairly broad and just means there are nontrivial inconsistent theories. "Fuzzy" means the semantics are $[0,1]$-valued.
– spaceisdarkgreen
yesterday
1
1
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
2 days ago
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
2 days ago
1
1
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
2 days ago
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
2 days ago
1
1
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
2 days ago
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
2 days ago
1
1
"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
2 days ago
"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
2 days ago
Unfortunately there is no short answer to this question. They are adjectives, describing certain aspects of logical systems. For instance, "modal" generally means there are the $square$ and $Diamond$ connectives in the language (and little else unless qualified further). "Intuitionistic" generally means negation behaves differently than classically, although often a very specific theory like intuitionistic propositional or predicate logic is intended. "Paraconsistent" is fairly broad and just means there are nontrivial inconsistent theories. "Fuzzy" means the semantics are $[0,1]$-valued.
– spaceisdarkgreen
yesterday
Unfortunately there is no short answer to this question. They are adjectives, describing certain aspects of logical systems. For instance, "modal" generally means there are the $square$ and $Diamond$ connectives in the language (and little else unless qualified further). "Intuitionistic" generally means negation behaves differently than classically, although often a very specific theory like intuitionistic propositional or predicate logic is intended. "Paraconsistent" is fairly broad and just means there are nontrivial inconsistent theories. "Fuzzy" means the semantics are $[0,1]$-valued.
– spaceisdarkgreen
yesterday
|
show 1 more comment
1 Answer
1
active
oldest
votes
up vote
1
down vote
accepted
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.
answered yesterday
Derek Elkins
15.8k11336
add a comment |
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
accepted
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.
answered yesterday
Derek Elkins
15.8k11336
add a comment |
up vote
1
down vote
accepted
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.
answered yesterday
Derek Elkins
15.8k11336
add a comment |
up vote
1
down vote
accepted
up vote
1
down vote
accepted
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.
answered yesterday
Derek Elkins
15.8k11336
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.
answered yesterday
Derek Elkins
15.8k11336
answered yesterday
Derek Elkins
15.8k11336
answered yesterday
Derek Elkins
15.8k11336
answered yesterday
Derek Elkins
15.8k11336
15.8k11336
add a comment |
add a comment |
Brandon L is a new contributor. Be nice, and check out our Code of Conduct.
Brandon L is a new contributor. Be nice, and check out our Code of Conduct.
Brandon L is a new contributor. Be nice, and check out our Code of Conduct.
Brandon L is a new contributor. Be nice, and check out our Code of Conduct.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3005369%2frelationship-between-sequent-calculus-and-hilbert-systems-natural-deduction-et%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
1
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
2 days ago
1
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
2 days ago
1
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
2 days ago
1
"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
2 days ago
Unfortunately there is no short answer to this question. They are adjectives, describing certain aspects of logical systems. For instance, "modal" generally means there are the $square$ and $Diamond$ connectives in the language (and little else unless qualified further). "Intuitionistic" generally means negation behaves differently than classically, although often a very specific theory like intuitionistic propositional or predicate logic is intended. "Paraconsistent" is fairly broad and just means there are nontrivial inconsistent theories. "Fuzzy" means the semantics are $[0,1]$-valued.
– spaceisdarkgreen
yesterday