Mixing
Gödel's Completeness Theorem: Did Gödel show how to construct derivations?
$begingroup$
Gödel's Completeness Theorem for first-order logic states that there is a proof system with a finite number of rules and axioms that is both sound and complete for first-order logic: that there exists a derivation within such a proof system for all valid statement from first-order logic.
My question is: did Gödel merely prove that there exists some such a derivation, or did Gödel's proof show what such a derivation would actually look like, i.e. how to derive any valid statement?
Of course, given the truth of the Completeness Theorem, we can always obtain a derivation as follows: systematically iterate through all possible derivations (which is possible, since the set of derivations is enumerable), and if the statement is valid, then eventually we'll run into a derivation for it.
However, pointing to such an algorithm will of course not prove that there is a derivation. So, I was wondering if maybe Gödel had an algorithm that he pointed to and for which he proved that it would always create a derivation of any valid statement. Or, at the very least: does Gödel's proof naturally translate itself into such an algorithm?
If not, is there a well-known alternative proof of the Completeness Theorem that does provide such an algorithmic proof?
logic first-order-logic
edited Jan 10 at 6:51
mrtaurho
4,12621234
asked Jan 6 at 21:13
Bram28Bram28
61.1k44591
$endgroup$
|
show 7 more comments
$begingroup$
Gödel's Completeness Theorem for first-order logic states that there is a proof system with a finite number of rules and axioms that is both sound and complete for first-order logic: that there exists a derivation within such a proof system for all valid statement from first-order logic.
My question is: did Gödel merely prove that there exists some such a derivation, or did Gödel's proof show what such a derivation would actually look like, i.e. how to derive any valid statement?
Of course, given the truth of the Completeness Theorem, we can always obtain a derivation as follows: systematically iterate through all possible derivations (which is possible, since the set of derivations is enumerable), and if the statement is valid, then eventually we'll run into a derivation for it.
However, pointing to such an algorithm will of course not prove that there is a derivation. So, I was wondering if maybe Gödel had an algorithm that he pointed to and for which he proved that it would always create a derivation of any valid statement. Or, at the very least: does Gödel's proof naturally translate itself into such an algorithm?
If not, is there a well-known alternative proof of the Completeness Theorem that does provide such an algorithmic proof?
logic first-order-logic
edited Jan 10 at 6:51
mrtaurho
4,12621234
asked Jan 6 at 21:13
Bram28Bram28
61.1k44591
$endgroup$
1
$begingroup$
See en.wikipedia.org/wiki/…
$endgroup$
– J.G.
Jan 6 at 21:21
$begingroup$
@J.G. Yeah, I saw that, and I also went to: en.wikipedia.org/wiki/… but I couldn't quite figure it out from there ... it doesn't look like he is producing an algorithm ...
$endgroup$
– Bram28
Jan 6 at 21:29
$begingroup$
You may want to look at the semantic (or analytic) tableau approach.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:30
$begingroup$
@FabioSomenzi Yes, that;'s exactly what I was thinking: it seems like we should be able to make that into an algorithmic proof ... do you know if anyone has actually done that? Also, any tableaux can be converted into a more traditional natural deduction style proof ... so even before these tableaux were around, I am thinking someone must have had the insight to effectively use the basic method of tableaux (one big proof by contradiciton, and then just exploring al possible options for satisfiability) in a more traditional style proof ... who was the first to think of this?
$endgroup$
– Bram28
Jan 6 at 23:32
$begingroup$
Perhaps, you want to take a look at Melvin Fitting's First-Order Logic and Automated Theorem Proving, Springer 1996? A naive implementation of the semantic tableau approach for first-order logic does not guarantee that the tableau will be closed whenever it's possible, but there ways to obviate that.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:42
|
show 7 more comments
$begingroup$
Gödel's Completeness Theorem for first-order logic states that there is a proof system with a finite number of rules and axioms that is both sound and complete for first-order logic: that there exists a derivation within such a proof system for all valid statement from first-order logic.
My question is: did Gödel merely prove that there exists some such a derivation, or did Gödel's proof show what such a derivation would actually look like, i.e. how to derive any valid statement?
Of course, given the truth of the Completeness Theorem, we can always obtain a derivation as follows: systematically iterate through all possible derivations (which is possible, since the set of derivations is enumerable), and if the statement is valid, then eventually we'll run into a derivation for it.
However, pointing to such an algorithm will of course not prove that there is a derivation. So, I was wondering if maybe Gödel had an algorithm that he pointed to and for which he proved that it would always create a derivation of any valid statement. Or, at the very least: does Gödel's proof naturally translate itself into such an algorithm?
If not, is there a well-known alternative proof of the Completeness Theorem that does provide such an algorithmic proof?
logic first-order-logic
edited Jan 10 at 6:51
mrtaurho
4,12621234
asked Jan 6 at 21:13
Bram28Bram28
61.1k44591
$endgroup$
Gödel's Completeness Theorem for first-order logic states that there is a proof system with a finite number of rules and axioms that is both sound and complete for first-order logic: that there exists a derivation within such a proof system for all valid statement from first-order logic.
My question is: did Gödel merely prove that there exists some such a derivation, or did Gödel's proof show what such a derivation would actually look like, i.e. how to derive any valid statement?
Of course, given the truth of the Completeness Theorem, we can always obtain a derivation as follows: systematically iterate through all possible derivations (which is possible, since the set of derivations is enumerable), and if the statement is valid, then eventually we'll run into a derivation for it.
However, pointing to such an algorithm will of course not prove that there is a derivation. So, I was wondering if maybe Gödel had an algorithm that he pointed to and for which he proved that it would always create a derivation of any valid statement. Or, at the very least: does Gödel's proof naturally translate itself into such an algorithm?
If not, is there a well-known alternative proof of the Completeness Theorem that does provide such an algorithmic proof?
logic first-order-logic
logic first-order-logic
edited Jan 10 at 6:51
mrtaurho
4,12621234
asked Jan 6 at 21:13
Bram28Bram28
61.1k44591
edited Jan 10 at 6:51
mrtaurho
4,12621234
asked Jan 6 at 21:13
Bram28Bram28
61.1k44591
edited Jan 10 at 6:51
mrtaurho
4,12621234
edited Jan 10 at 6:51
mrtaurho
4,12621234
edited Jan 10 at 6:51
mrtaurho
4,12621234
4,12621234
asked Jan 6 at 21:13
Bram28Bram28
61.1k44591
asked Jan 6 at 21:13
Bram28Bram28
61.1k44591
asked Jan 6 at 21:13
Bram28Bram28
61.1k44591
61.1k44591
1
$begingroup$
See en.wikipedia.org/wiki/…
$endgroup$
– J.G.
Jan 6 at 21:21
$begingroup$
@J.G. Yeah, I saw that, and I also went to: en.wikipedia.org/wiki/… but I couldn't quite figure it out from there ... it doesn't look like he is producing an algorithm ...
$endgroup$
– Bram28
Jan 6 at 21:29
$begingroup$
You may want to look at the semantic (or analytic) tableau approach.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:30
$begingroup$
@FabioSomenzi Yes, that;'s exactly what I was thinking: it seems like we should be able to make that into an algorithmic proof ... do you know if anyone has actually done that? Also, any tableaux can be converted into a more traditional natural deduction style proof ... so even before these tableaux were around, I am thinking someone must have had the insight to effectively use the basic method of tableaux (one big proof by contradiciton, and then just exploring al possible options for satisfiability) in a more traditional style proof ... who was the first to think of this?
$endgroup$
– Bram28
Jan 6 at 23:32
$begingroup$
Perhaps, you want to take a look at Melvin Fitting's First-Order Logic and Automated Theorem Proving, Springer 1996? A naive implementation of the semantic tableau approach for first-order logic does not guarantee that the tableau will be closed whenever it's possible, but there ways to obviate that.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:42
|
show 7 more comments
1
$begingroup$
See en.wikipedia.org/wiki/…
$endgroup$
– J.G.
Jan 6 at 21:21
$begingroup$
@J.G. Yeah, I saw that, and I also went to: en.wikipedia.org/wiki/… but I couldn't quite figure it out from there ... it doesn't look like he is producing an algorithm ...
$endgroup$
– Bram28
Jan 6 at 21:29
$begingroup$
You may want to look at the semantic (or analytic) tableau approach.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:30
$begingroup$
@FabioSomenzi Yes, that;'s exactly what I was thinking: it seems like we should be able to make that into an algorithmic proof ... do you know if anyone has actually done that? Also, any tableaux can be converted into a more traditional natural deduction style proof ... so even before these tableaux were around, I am thinking someone must have had the insight to effectively use the basic method of tableaux (one big proof by contradiciton, and then just exploring al possible options for satisfiability) in a more traditional style proof ... who was the first to think of this?
$endgroup$
– Bram28
Jan 6 at 23:32
$begingroup$
Perhaps, you want to take a look at Melvin Fitting's First-Order Logic and Automated Theorem Proving, Springer 1996? A naive implementation of the semantic tableau approach for first-order logic does not guarantee that the tableau will be closed whenever it's possible, but there ways to obviate that.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:42
1
1
$begingroup$
See en.wikipedia.org/wiki/…
$endgroup$
– J.G.
Jan 6 at 21:21
$begingroup$
See en.wikipedia.org/wiki/…
$endgroup$
– J.G.
Jan 6 at 21:21
$begingroup$
@J.G. Yeah, I saw that, and I also went to: en.wikipedia.org/wiki/… but I couldn't quite figure it out from there ... it doesn't look like he is producing an algorithm ...
$endgroup$
– Bram28
Jan 6 at 21:29
$begingroup$
@J.G. Yeah, I saw that, and I also went to: en.wikipedia.org/wiki/… but I couldn't quite figure it out from there ... it doesn't look like he is producing an algorithm ...
$endgroup$
– Bram28
Jan 6 at 21:29
$begingroup$
You may want to look at the semantic (or analytic) tableau approach.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:30
$begingroup$
You may want to look at the semantic (or analytic) tableau approach.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:30
$begingroup$
@FabioSomenzi Yes, that;'s exactly what I was thinking: it seems like we should be able to make that into an algorithmic proof ... do you know if anyone has actually done that? Also, any tableaux can be converted into a more traditional natural deduction style proof ... so even before these tableaux were around, I am thinking someone must have had the insight to effectively use the basic method of tableaux (one big proof by contradiciton, and then just exploring al possible options for satisfiability) in a more traditional style proof ... who was the first to think of this?
$endgroup$
– Bram28
Jan 6 at 23:32
$begingroup$
@FabioSomenzi Yes, that;'s exactly what I was thinking: it seems like we should be able to make that into an algorithmic proof ... do you know if anyone has actually done that? Also, any tableaux can be converted into a more traditional natural deduction style proof ... so even before these tableaux were around, I am thinking someone must have had the insight to effectively use the basic method of tableaux (one big proof by contradiciton, and then just exploring al possible options for satisfiability) in a more traditional style proof ... who was the first to think of this?
$endgroup$
– Bram28
Jan 6 at 23:32
$begingroup$
Perhaps, you want to take a look at Melvin Fitting's First-Order Logic and Automated Theorem Proving, Springer 1996? A naive implementation of the semantic tableau approach for first-order logic does not guarantee that the tableau will be closed whenever it's possible, but there ways to obviate that.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:42
$begingroup$
Perhaps, you want to take a look at Melvin Fitting's First-Order Logic and Automated Theorem Proving, Springer 1996? A naive implementation of the semantic tableau approach for first-order logic does not guarantee that the tableau will be closed whenever it's possible, but there ways to obviate that.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:42
|
show 7 more comments
1 Answer
1
active
oldest
votes
$begingroup$
No, the completeness theorem is far from algorithmic. It uses the axion of choice and in fact is equivalent to the ultrafilter lemma, a weaker form of choice.
answered Jan 6 at 21:26
Ittay WeissIttay Weiss
63.8k6101183
$endgroup$
$begingroup$
OK, thanks ... but there are algorithms to construct derivations, assuming derivations exist, right? I mean the 'dumb' brute force method I describe is one such algorithm. But are there more directly algorithmic proofs? If so, who was the first to do so?
$endgroup$
– Bram28
Jan 6 at 21:31
$begingroup$
Only needs axiom of choice for uncountable languages, (and I don't think Godel's original version covered uncountable languages).
$endgroup$
– spaceisdarkgreen
Jan 6 at 21:32
$begingroup$
@Bram28 The brute force method you described is not an algorithm: if the statement is valid, you'll find a proof, but if the statement is not valid, you will run forever. In fact, there is no algorithm in many cases.
$endgroup$
– Ted
Jan 6 at 21:34
$begingroup$
@Ted I am well aware of that. The 'dumb' brute force method I describe will of course run forever if the statement is not valid. And yet, for all the valid ones I will eventually get a derivation. I am wondering if there are more efficient ways to produce a derivation for the valid ones, even if that way will sometimes run forever for the invalid ones. If you don't want to call that an algorithm, ok, let's just call it a set of instructions then.
$endgroup$
– Bram28
Jan 6 at 21:38
$begingroup$
@Bram28 you may be refrring to automatic theorem provers. This is a very active area of research.
$endgroup$
– Ittay Weiss
Jan 6 at 21:46
|
show 3 more comments
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
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%2f3064398%2fg%25c3%25b6dels-completeness-theorem-did-g%25c3%25b6del-show-how-to-construct-derivations%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
No, the completeness theorem is far from algorithmic. It uses the axion of choice and in fact is equivalent to the ultrafilter lemma, a weaker form of choice.
answered Jan 6 at 21:26
Ittay WeissIttay Weiss
63.8k6101183
$endgroup$
$begingroup$
OK, thanks ... but there are algorithms to construct derivations, assuming derivations exist, right? I mean the 'dumb' brute force method I describe is one such algorithm. But are there more directly algorithmic proofs? If so, who was the first to do so?
$endgroup$
– Bram28
Jan 6 at 21:31
$begingroup$
Only needs axiom of choice for uncountable languages, (and I don't think Godel's original version covered uncountable languages).
$endgroup$
– spaceisdarkgreen
Jan 6 at 21:32
$begingroup$
@Bram28 The brute force method you described is not an algorithm: if the statement is valid, you'll find a proof, but if the statement is not valid, you will run forever. In fact, there is no algorithm in many cases.
$endgroup$
– Ted
Jan 6 at 21:34
$begingroup$
@Ted I am well aware of that. The 'dumb' brute force method I describe will of course run forever if the statement is not valid. And yet, for all the valid ones I will eventually get a derivation. I am wondering if there are more efficient ways to produce a derivation for the valid ones, even if that way will sometimes run forever for the invalid ones. If you don't want to call that an algorithm, ok, let's just call it a set of instructions then.
$endgroup$
– Bram28
Jan 6 at 21:38
$begingroup$
@Bram28 you may be refrring to automatic theorem provers. This is a very active area of research.
$endgroup$
– Ittay Weiss
Jan 6 at 21:46
|
show 3 more comments
$begingroup$
No, the completeness theorem is far from algorithmic. It uses the axion of choice and in fact is equivalent to the ultrafilter lemma, a weaker form of choice.
answered Jan 6 at 21:26
Ittay WeissIttay Weiss
63.8k6101183
$endgroup$
$begingroup$
OK, thanks ... but there are algorithms to construct derivations, assuming derivations exist, right? I mean the 'dumb' brute force method I describe is one such algorithm. But are there more directly algorithmic proofs? If so, who was the first to do so?
$endgroup$
– Bram28
Jan 6 at 21:31
$begingroup$
Only needs axiom of choice for uncountable languages, (and I don't think Godel's original version covered uncountable languages).
$endgroup$
– spaceisdarkgreen
Jan 6 at 21:32
$begingroup$
@Bram28 The brute force method you described is not an algorithm: if the statement is valid, you'll find a proof, but if the statement is not valid, you will run forever. In fact, there is no algorithm in many cases.
$endgroup$
– Ted
Jan 6 at 21:34
$begingroup$
@Ted I am well aware of that. The 'dumb' brute force method I describe will of course run forever if the statement is not valid. And yet, for all the valid ones I will eventually get a derivation. I am wondering if there are more efficient ways to produce a derivation for the valid ones, even if that way will sometimes run forever for the invalid ones. If you don't want to call that an algorithm, ok, let's just call it a set of instructions then.
$endgroup$
– Bram28
Jan 6 at 21:38
$begingroup$
@Bram28 you may be refrring to automatic theorem provers. This is a very active area of research.
$endgroup$
– Ittay Weiss
Jan 6 at 21:46
|
show 3 more comments
$begingroup$
No, the completeness theorem is far from algorithmic. It uses the axion of choice and in fact is equivalent to the ultrafilter lemma, a weaker form of choice.
answered Jan 6 at 21:26
Ittay WeissIttay Weiss
63.8k6101183
$endgroup$
No, the completeness theorem is far from algorithmic. It uses the axion of choice and in fact is equivalent to the ultrafilter lemma, a weaker form of choice.
answered Jan 6 at 21:26
Ittay WeissIttay Weiss
63.8k6101183
answered Jan 6 at 21:26
Ittay WeissIttay Weiss
63.8k6101183
answered Jan 6 at 21:26
Ittay WeissIttay Weiss
63.8k6101183
answered Jan 6 at 21:26
Ittay WeissIttay Weiss
63.8k6101183
63.8k6101183
$begingroup$
OK, thanks ... but there are algorithms to construct derivations, assuming derivations exist, right? I mean the 'dumb' brute force method I describe is one such algorithm. But are there more directly algorithmic proofs? If so, who was the first to do so?
$endgroup$
– Bram28
Jan 6 at 21:31
$begingroup$
Only needs axiom of choice for uncountable languages, (and I don't think Godel's original version covered uncountable languages).
$endgroup$
– spaceisdarkgreen
Jan 6 at 21:32
$begingroup$
@Bram28 The brute force method you described is not an algorithm: if the statement is valid, you'll find a proof, but if the statement is not valid, you will run forever. In fact, there is no algorithm in many cases.
$endgroup$
– Ted
Jan 6 at 21:34
$begingroup$
@Ted I am well aware of that. The 'dumb' brute force method I describe will of course run forever if the statement is not valid. And yet, for all the valid ones I will eventually get a derivation. I am wondering if there are more efficient ways to produce a derivation for the valid ones, even if that way will sometimes run forever for the invalid ones. If you don't want to call that an algorithm, ok, let's just call it a set of instructions then.
$endgroup$
– Bram28
Jan 6 at 21:38
$begingroup$
@Bram28 you may be refrring to automatic theorem provers. This is a very active area of research.
$endgroup$
– Ittay Weiss
Jan 6 at 21:46
|
show 3 more comments
$begingroup$
OK, thanks ... but there are algorithms to construct derivations, assuming derivations exist, right? I mean the 'dumb' brute force method I describe is one such algorithm. But are there more directly algorithmic proofs? If so, who was the first to do so?
$endgroup$
– Bram28
Jan 6 at 21:31
$begingroup$
Only needs axiom of choice for uncountable languages, (and I don't think Godel's original version covered uncountable languages).
$endgroup$
– spaceisdarkgreen
Jan 6 at 21:32
$begingroup$
@Bram28 The brute force method you described is not an algorithm: if the statement is valid, you'll find a proof, but if the statement is not valid, you will run forever. In fact, there is no algorithm in many cases.
$endgroup$
– Ted
Jan 6 at 21:34
$begingroup$
@Ted I am well aware of that. The 'dumb' brute force method I describe will of course run forever if the statement is not valid. And yet, for all the valid ones I will eventually get a derivation. I am wondering if there are more efficient ways to produce a derivation for the valid ones, even if that way will sometimes run forever for the invalid ones. If you don't want to call that an algorithm, ok, let's just call it a set of instructions then.
$endgroup$
– Bram28
Jan 6 at 21:38
$begingroup$
@Bram28 you may be refrring to automatic theorem provers. This is a very active area of research.
$endgroup$
– Ittay Weiss
Jan 6 at 21:46
$begingroup$
OK, thanks ... but there are algorithms to construct derivations, assuming derivations exist, right? I mean the 'dumb' brute force method I describe is one such algorithm. But are there more directly algorithmic proofs? If so, who was the first to do so?
$endgroup$
– Bram28
Jan 6 at 21:31
$begingroup$
OK, thanks ... but there are algorithms to construct derivations, assuming derivations exist, right? I mean the 'dumb' brute force method I describe is one such algorithm. But are there more directly algorithmic proofs? If so, who was the first to do so?
$endgroup$
– Bram28
Jan 6 at 21:31
$begingroup$
Only needs axiom of choice for uncountable languages, (and I don't think Godel's original version covered uncountable languages).
$endgroup$
– spaceisdarkgreen
Jan 6 at 21:32
$begingroup$
Only needs axiom of choice for uncountable languages, (and I don't think Godel's original version covered uncountable languages).
$endgroup$
– spaceisdarkgreen
Jan 6 at 21:32
$begingroup$
@Bram28 The brute force method you described is not an algorithm: if the statement is valid, you'll find a proof, but if the statement is not valid, you will run forever. In fact, there is no algorithm in many cases.
$endgroup$
– Ted
Jan 6 at 21:34
$begingroup$
@Bram28 The brute force method you described is not an algorithm: if the statement is valid, you'll find a proof, but if the statement is not valid, you will run forever. In fact, there is no algorithm in many cases.
$endgroup$
– Ted
Jan 6 at 21:34
$begingroup$
@Ted I am well aware of that. The 'dumb' brute force method I describe will of course run forever if the statement is not valid. And yet, for all the valid ones I will eventually get a derivation. I am wondering if there are more efficient ways to produce a derivation for the valid ones, even if that way will sometimes run forever for the invalid ones. If you don't want to call that an algorithm, ok, let's just call it a set of instructions then.
$endgroup$
– Bram28
Jan 6 at 21:38
$begingroup$
@Ted I am well aware of that. The 'dumb' brute force method I describe will of course run forever if the statement is not valid. And yet, for all the valid ones I will eventually get a derivation. I am wondering if there are more efficient ways to produce a derivation for the valid ones, even if that way will sometimes run forever for the invalid ones. If you don't want to call that an algorithm, ok, let's just call it a set of instructions then.
$endgroup$
– Bram28
Jan 6 at 21:38
$begingroup$
@Bram28 you may be refrring to automatic theorem provers. This is a very active area of research.
$endgroup$
– Ittay Weiss
Jan 6 at 21:46
$begingroup$
@Bram28 you may be refrring to automatic theorem provers. This is a very active area of research.
$endgroup$
– Ittay Weiss
Jan 6 at 21:46
|
show 3 more comments
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
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%2f3064398%2fg%25c3%25b6dels-completeness-theorem-did-g%25c3%25b6del-show-how-to-construct-derivations%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
$begingroup$
See en.wikipedia.org/wiki/…
$endgroup$
– J.G.
Jan 6 at 21:21
$begingroup$
@J.G. Yeah, I saw that, and I also went to: en.wikipedia.org/wiki/… but I couldn't quite figure it out from there ... it doesn't look like he is producing an algorithm ...
$endgroup$
– Bram28
Jan 6 at 21:29
$begingroup$
You may want to look at the semantic (or analytic) tableau approach.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:30
$begingroup$
@FabioSomenzi Yes, that;'s exactly what I was thinking: it seems like we should be able to make that into an algorithmic proof ... do you know if anyone has actually done that? Also, any tableaux can be converted into a more traditional natural deduction style proof ... so even before these tableaux were around, I am thinking someone must have had the insight to effectively use the basic method of tableaux (one big proof by contradiciton, and then just exploring al possible options for satisfiability) in a more traditional style proof ... who was the first to think of this?
$endgroup$
– Bram28
Jan 6 at 23:32
$begingroup$
Perhaps, you want to take a look at Melvin Fitting's First-Order Logic and Automated Theorem Proving, Springer 1996? A naive implementation of the semantic tableau approach for first-order logic does not guarantee that the tableau will be closed whenever it's possible, but there ways to obviate that.
$endgroup$
– Fabio Somenzi
Jan 6 at 23:42