Gödel's completeness theorem and the undecidability of first-order logic
up vote
15
down vote
favorite
I'm working through this module, "Undecidability of First-Order Logic" and would love to talk about the two exercises given immediately after the statement of Godel's completeness theorem.
First, note Definition 2.1 from the text: A sentence $varphi$ is valid if it is true in all models. In contrast, $varphi$ is satisfiable if it is true in some model. Then the exercises are given as follows:
Let $varphi$ be a sentence in first-order logic. Show that $varphi$ is valid if and only if $negvarphi$ is not satisfiable, and consequently that $varphi$ is satisfiable if and only if $negvarphi$ is not valid.
Suppose that we have an algorithm $mathcal{A}$ to tell whether a sentence of first-order logic is satisfiable or not. Show that we can use this to get an algorithm $mathcal{B}$ to tell whether a sentence of first-order logic is provable or not.
Conversely, suppose that we have an algorithm $mathcal{B}$ to tell whether a sentence of first-order logic is provable or not. Show that we can use this to get an algorithm $mathcal{A}$ to tell whether a sentence of first-order logic is satisfiable or not.
The first exercise seems pretty straightforward. My answer:
- Let $mathscr{M}$ be a model and read "$varphi$ is true in $mathscr{M}$" for $mathscr{M}modelsvarphi$. Then by the definitions above and basic facts of logic (such as DeMorgan's laws for quantifiers), the equivalence $forall mathscr{M} (mathscr{M}modelsvarphi) equiv negexists mathscr{M} (mathscr{M}modelsnegvarphi)$ holds as desired. The same goes for the restatement introduced by "consequently" in the exercise, i.e. $exists mathscr{M}(mathscr{M}models varphi) equiv negforall(mathscr{M}modelsnegvarphi)$.
Make sense? Anybody spot any errors, or feel like suggesting improvements of any kind?
Okay. Now the second exercise is where things get more interesting, at least for me, because I don't fully grasp this idea of correspondence between "valid" and "provable," which is the core of Gödel's completeness theorem.
Looking at what Wikipedia has to say about the theorem, I feel like I basically understand the result, but am still unsure how I would apply it in terms of the second exercise.
Take the first part of the problem: all I've got is an algorithm $mathcal{A}$ that decides satisfiability of $varphi$. The completeness theorem establishes an equivalence between syntactic provability and semantic validity. I can't figure out how to cross the chasm from satisfiability to validity, or otherwise find the logical connection I would need to use the theorem to solve my problem.
While searching for similar questions before posting, I found this one, which offers some stimulating food for thought but deals with different givens, namely: an algorithm that takes a $varphi$ and returns $varphi'$ such that $varphi$ is satisfiable iff $varphi'$ is valid. I can see that this is getting close to what I need, but again I can't see how to adapt it to my purposes.
Can anyone offer a hint, a suggestion, or pointer of any kind? I would much appreciate it.
logic first-order-logic computability incompleteness decidability
New contributor
add a comment |
up vote
15
down vote
favorite
I'm working through this module, "Undecidability of First-Order Logic" and would love to talk about the two exercises given immediately after the statement of Godel's completeness theorem.
First, note Definition 2.1 from the text: A sentence $varphi$ is valid if it is true in all models. In contrast, $varphi$ is satisfiable if it is true in some model. Then the exercises are given as follows:
Let $varphi$ be a sentence in first-order logic. Show that $varphi$ is valid if and only if $negvarphi$ is not satisfiable, and consequently that $varphi$ is satisfiable if and only if $negvarphi$ is not valid.
Suppose that we have an algorithm $mathcal{A}$ to tell whether a sentence of first-order logic is satisfiable or not. Show that we can use this to get an algorithm $mathcal{B}$ to tell whether a sentence of first-order logic is provable or not.
Conversely, suppose that we have an algorithm $mathcal{B}$ to tell whether a sentence of first-order logic is provable or not. Show that we can use this to get an algorithm $mathcal{A}$ to tell whether a sentence of first-order logic is satisfiable or not.
The first exercise seems pretty straightforward. My answer:
- Let $mathscr{M}$ be a model and read "$varphi$ is true in $mathscr{M}$" for $mathscr{M}modelsvarphi$. Then by the definitions above and basic facts of logic (such as DeMorgan's laws for quantifiers), the equivalence $forall mathscr{M} (mathscr{M}modelsvarphi) equiv negexists mathscr{M} (mathscr{M}modelsnegvarphi)$ holds as desired. The same goes for the restatement introduced by "consequently" in the exercise, i.e. $exists mathscr{M}(mathscr{M}models varphi) equiv negforall(mathscr{M}modelsnegvarphi)$.
Make sense? Anybody spot any errors, or feel like suggesting improvements of any kind?
Okay. Now the second exercise is where things get more interesting, at least for me, because I don't fully grasp this idea of correspondence between "valid" and "provable," which is the core of Gödel's completeness theorem.
Looking at what Wikipedia has to say about the theorem, I feel like I basically understand the result, but am still unsure how I would apply it in terms of the second exercise.
Take the first part of the problem: all I've got is an algorithm $mathcal{A}$ that decides satisfiability of $varphi$. The completeness theorem establishes an equivalence between syntactic provability and semantic validity. I can't figure out how to cross the chasm from satisfiability to validity, or otherwise find the logical connection I would need to use the theorem to solve my problem.
While searching for similar questions before posting, I found this one, which offers some stimulating food for thought but deals with different givens, namely: an algorithm that takes a $varphi$ and returns $varphi'$ such that $varphi$ is satisfiable iff $varphi'$ is valid. I can see that this is getting close to what I need, but again I can't see how to adapt it to my purposes.
Can anyone offer a hint, a suggestion, or pointer of any kind? I would much appreciate it.
logic first-order-logic computability incompleteness decidability
New contributor
10
+1 for all the homework you did before coming here for help, and for the care you took in formatting.
– Ethan Bolker
Nov 19 at 1:15
3
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
Nov 19 at 2:28
2
@RebeccaBonham It's questions like these among all of the slush on this site that make me want to come back each day.
– Rushabh Mehta
Nov 19 at 6:41
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
Nov 19 at 16:43
add a comment |
up vote
15
down vote
favorite
up vote
15
down vote
favorite
I'm working through this module, "Undecidability of First-Order Logic" and would love to talk about the two exercises given immediately after the statement of Godel's completeness theorem.
First, note Definition 2.1 from the text: A sentence $varphi$ is valid if it is true in all models. In contrast, $varphi$ is satisfiable if it is true in some model. Then the exercises are given as follows:
Let $varphi$ be a sentence in first-order logic. Show that $varphi$ is valid if and only if $negvarphi$ is not satisfiable, and consequently that $varphi$ is satisfiable if and only if $negvarphi$ is not valid.
Suppose that we have an algorithm $mathcal{A}$ to tell whether a sentence of first-order logic is satisfiable or not. Show that we can use this to get an algorithm $mathcal{B}$ to tell whether a sentence of first-order logic is provable or not.
Conversely, suppose that we have an algorithm $mathcal{B}$ to tell whether a sentence of first-order logic is provable or not. Show that we can use this to get an algorithm $mathcal{A}$ to tell whether a sentence of first-order logic is satisfiable or not.
The first exercise seems pretty straightforward. My answer:
- Let $mathscr{M}$ be a model and read "$varphi$ is true in $mathscr{M}$" for $mathscr{M}modelsvarphi$. Then by the definitions above and basic facts of logic (such as DeMorgan's laws for quantifiers), the equivalence $forall mathscr{M} (mathscr{M}modelsvarphi) equiv negexists mathscr{M} (mathscr{M}modelsnegvarphi)$ holds as desired. The same goes for the restatement introduced by "consequently" in the exercise, i.e. $exists mathscr{M}(mathscr{M}models varphi) equiv negforall(mathscr{M}modelsnegvarphi)$.
Make sense? Anybody spot any errors, or feel like suggesting improvements of any kind?
Okay. Now the second exercise is where things get more interesting, at least for me, because I don't fully grasp this idea of correspondence between "valid" and "provable," which is the core of Gödel's completeness theorem.
Looking at what Wikipedia has to say about the theorem, I feel like I basically understand the result, but am still unsure how I would apply it in terms of the second exercise.
Take the first part of the problem: all I've got is an algorithm $mathcal{A}$ that decides satisfiability of $varphi$. The completeness theorem establishes an equivalence between syntactic provability and semantic validity. I can't figure out how to cross the chasm from satisfiability to validity, or otherwise find the logical connection I would need to use the theorem to solve my problem.
While searching for similar questions before posting, I found this one, which offers some stimulating food for thought but deals with different givens, namely: an algorithm that takes a $varphi$ and returns $varphi'$ such that $varphi$ is satisfiable iff $varphi'$ is valid. I can see that this is getting close to what I need, but again I can't see how to adapt it to my purposes.
Can anyone offer a hint, a suggestion, or pointer of any kind? I would much appreciate it.
logic first-order-logic computability incompleteness decidability
New contributor
I'm working through this module, "Undecidability of First-Order Logic" and would love to talk about the two exercises given immediately after the statement of Godel's completeness theorem.
First, note Definition 2.1 from the text: A sentence $varphi$ is valid if it is true in all models. In contrast, $varphi$ is satisfiable if it is true in some model. Then the exercises are given as follows:
Let $varphi$ be a sentence in first-order logic. Show that $varphi$ is valid if and only if $negvarphi$ is not satisfiable, and consequently that $varphi$ is satisfiable if and only if $negvarphi$ is not valid.
Suppose that we have an algorithm $mathcal{A}$ to tell whether a sentence of first-order logic is satisfiable or not. Show that we can use this to get an algorithm $mathcal{B}$ to tell whether a sentence of first-order logic is provable or not.
Conversely, suppose that we have an algorithm $mathcal{B}$ to tell whether a sentence of first-order logic is provable or not. Show that we can use this to get an algorithm $mathcal{A}$ to tell whether a sentence of first-order logic is satisfiable or not.
The first exercise seems pretty straightforward. My answer:
- Let $mathscr{M}$ be a model and read "$varphi$ is true in $mathscr{M}$" for $mathscr{M}modelsvarphi$. Then by the definitions above and basic facts of logic (such as DeMorgan's laws for quantifiers), the equivalence $forall mathscr{M} (mathscr{M}modelsvarphi) equiv negexists mathscr{M} (mathscr{M}modelsnegvarphi)$ holds as desired. The same goes for the restatement introduced by "consequently" in the exercise, i.e. $exists mathscr{M}(mathscr{M}models varphi) equiv negforall(mathscr{M}modelsnegvarphi)$.
Make sense? Anybody spot any errors, or feel like suggesting improvements of any kind?
Okay. Now the second exercise is where things get more interesting, at least for me, because I don't fully grasp this idea of correspondence between "valid" and "provable," which is the core of Gödel's completeness theorem.
Looking at what Wikipedia has to say about the theorem, I feel like I basically understand the result, but am still unsure how I would apply it in terms of the second exercise.
Take the first part of the problem: all I've got is an algorithm $mathcal{A}$ that decides satisfiability of $varphi$. The completeness theorem establishes an equivalence between syntactic provability and semantic validity. I can't figure out how to cross the chasm from satisfiability to validity, or otherwise find the logical connection I would need to use the theorem to solve my problem.
While searching for similar questions before posting, I found this one, which offers some stimulating food for thought but deals with different givens, namely: an algorithm that takes a $varphi$ and returns $varphi'$ such that $varphi$ is satisfiable iff $varphi'$ is valid. I can see that this is getting close to what I need, but again I can't see how to adapt it to my purposes.
Can anyone offer a hint, a suggestion, or pointer of any kind? I would much appreciate it.
logic first-order-logic computability incompleteness decidability
logic first-order-logic computability incompleteness decidability
New contributor
New contributor
edited Nov 19 at 1:06
New contributor
asked Nov 19 at 0:43
Rebecca Bonham
15310
15310
New contributor
New contributor
10
+1 for all the homework you did before coming here for help, and for the care you took in formatting.
– Ethan Bolker
Nov 19 at 1:15
3
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
Nov 19 at 2:28
2
@RebeccaBonham It's questions like these among all of the slush on this site that make me want to come back each day.
– Rushabh Mehta
Nov 19 at 6:41
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
Nov 19 at 16:43
add a comment |
10
+1 for all the homework you did before coming here for help, and for the care you took in formatting.
– Ethan Bolker
Nov 19 at 1:15
3
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
Nov 19 at 2:28
2
@RebeccaBonham It's questions like these among all of the slush on this site that make me want to come back each day.
– Rushabh Mehta
Nov 19 at 6:41
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
Nov 19 at 16:43
10
10
+1 for all the homework you did before coming here for help, and for the care you took in formatting.
– Ethan Bolker
Nov 19 at 1:15
+1 for all the homework you did before coming here for help, and for the care you took in formatting.
– Ethan Bolker
Nov 19 at 1:15
3
3
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
Nov 19 at 2:28
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
Nov 19 at 2:28
2
2
@RebeccaBonham It's questions like these among all of the slush on this site that make me want to come back each day.
– Rushabh Mehta
Nov 19 at 6:41
@RebeccaBonham It's questions like these among all of the slush on this site that make me want to come back each day.
– Rushabh Mehta
Nov 19 at 6:41
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
Nov 19 at 16:43
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
Nov 19 at 16:43
add a comment |
2 Answers
2
active
oldest
votes
up vote
7
down vote
accepted
You got the right idea for part 1, but it is unusual to use the logical notation that you do: $neg$, $forall$, and $exists$ are logical operators, but $models$ is a metalogic symbol; purists will not like you mixing those up. So, it may be better to use the English 'some' and 'all' and 'not'
For part 2: here is where you use the result of part 1! In particular, in order to decide whether $varphi$ is valid or not, you can decide whether $neg varphi$ is satisfiable or not: if $neg varphi$ is satisfiable, then $varphi$ is not valid, but if $neg varphi$ is not satisfiable, then $varphi$ is valid. And now you just combine that with Godel's completeness result (to be precise: the theorem that a statement is provable if and only if it is valid ... the more difficult 'if' part of which is the completeness theorem): if $varphi$ is valid, then it is provable, and if $varphi$ is not valid, then it is not provable.
So for that first part: if you have algorithm $mathcal{A}$ that can figure put whether $varphi$ is satisfiable or not for any $varphi$, then design algorithm $mathcal{B}$ that is trying to figure out whether $varphi$ is provable or not as follows:
Take in $varphi$
Negate $varphi$
Call algorithm $mathcal{A}$ with $neg varphi$
4a. If algorithm $mathcal{A}$ says that $neg varphi$ is satisfiable, then print '$varphi$ is not provable!'
4b. If algorithm $mathcal{A}$ says that $neg varphi$ is not satisfiable, then print '$varphi$ is provable!'
Thanks, appreciate the suggestion! I will note this for the future. (An aside: could you say a few words on what you mean, specifically, by "metalogic"?)
– Rebecca Bonham
Nov 19 at 1:00
1
@RebeccaBonham $models$ is a 'meta-logic' symbol in that it is used to express a statement about a logic statement. That is, $varphi$ is a logic statement, and $mathscr{M}modelsvarphi$ is a statement about that logic statement.
– Bram28
Nov 19 at 1:03
Got it, thanks.
– Rebecca Bonham
Nov 19 at 1:04
2
Strictly speaking I think "Gödel's completeness result" is only "if $varphi$ is valid then it is provable". The other direction is soundness of FOL, which is generally considered too obvious to have anyone's name attached to it.
– Henning Makholm
Nov 19 at 1:08
1
@HenningMakholm quite so .. the document the OP is working with kind of hides this as well ... they put the 'if and only if' as a theorem proved by Godel .. yet refer to it as the Completeness theorem
– Bram28
Nov 19 at 1:16
|
show 2 more comments
up vote
6
down vote
For my own purposes, I'm archiving here my best attempt at integrating, in a compact manner, everything that was mentioned in the answers to my original question. Any comments or critiques of any kind are always welcome. Thanks again to the contributors.
Definitions. A sentence $varphi$ is valid if it is true in all models. In contrast, $varphi$ is satisfiable if it is true in some model.
Completeness theorem with soundness. A sentence in first-order logic is provable if and only if it is valid.
Then the answers to the problems stated above can be given as follows:
Let $mathscr{M}_x$ be a model, $xinmathbb{N}$. Let $varphi$ be a sentence in first-order logic. Let $P(x)$ be the predicate "$varphi$ is true in $mathscr{M}_x$." Then $forall x P(x) equiv neg exists x P(x)$ and $exists x P(x) equiv neg forall x neg P(x)$ by the above definitions and De Morgan's laws.
Suppose we have $mathcal{A}$. Let $mathcal{B}$ be the algorithm defined by the following procedure. Step 1: take $varphi$ as input. Step 2: negate $varphi$. Step 3: call $mathcal{A}$ with input $negvarphi$, written $mathcal{A}(negvarphi)$. Step 4, case (a): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is satisfiable," then by the above equivalences $varphi$ is not valid and by the completeness theorem it is not provable. Step 4, case (b): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is not satisfiable," then by the above equivalences $varphi$ is valid and by the completeness theorem it is provable. Thus by making use of $mathcal{A}$ we have obtained $mathcal{B}$ such that $mathcal{B}$ decides whether $varphi$ is provable or not. By a symmetric argument we can obtain $mathcal{A}$ if given $mathcal{B}$.
New contributor
2
For 1. The $mathscr{M}_x$ is a little weird ... what is the index here? Again, it may be better just to avoid formal logic notation completely here, since this is all meta-logic, rather than formal logic. So, for example, I would say: $varphi$ is valid if and only (by definition of valid) if $varphi$ is true in all possible models if and only if (by pure logic) there is no model in which $varphi$ is false if and only if (by semantics) there is no model in which $neg varphi$ is true if and only if (by definition satisfiability) $neg varphi$ is not satisfiable.
– Bram28
Nov 19 at 14:56
1
For 2. The completeness theorem is that a statement is provable if it is valid. But in order to answer this question, you need to stronger Theorem that a statement is provable if it and only if is valid. Remember that you need a decision procedure, meaning that if $varphi$ is provable, then $mathcal{B}$ will say it is provable, and if $varphi$ is not provable, then $mathcal{B}$ will say it is not provable. So, if you find that $neg varphi$ is not valid, then you need to be able to conclude it is not provable, which you can only do if you have an 'if and only if'
– Bram28
Nov 19 at 15:02
1
Indeed, this is the key difference between the completeness of first-order logic and the undecidability of first-order logic: it is complete in that if a formula is valid, it can be proven ... and indeed there is an algorithm that, when given that formula, will be able to say that it is provable (and in fact it can even produce a proof). But such a complete algorithm is not a decision procedure, since for that, it also needs to say that a formula that is not valid is not provable. And as it turns out (and as the document tries to show) there cannot be such a decision procedure.
– Bram28
Nov 19 at 15:06
1
1. I was thinking of "the $mathscr{M}_x$'s" as an enumeration of models, following a kind of notation one of my professors sometimes uses, and which I've kind of become accustomed to. My rewritten answer to the first exercise was an attempt to reformulate my idea into logical statements, staying away from symbols like $models$, etc. But I think you're right, and clarity is best served by plain English. I'll treat is as an exercise for myself, to make the effort to find a precise wording without leaning on technical notation.
– Rebecca Bonham
Nov 19 at 16:51
2
Right. The completeness theorem is only in one direction ... but to transform the one decision procedure (algorithm) into the other you need both directions ... which is what the theorem in the document expresses. And yes, the other direction (soundness) is fairly easy, but still, you can't just point to completeness in a proof that the algorithms can be transformed into each other.
– Bram28
Nov 19 at 17:10
|
show 2 more comments
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
7
down vote
accepted
You got the right idea for part 1, but it is unusual to use the logical notation that you do: $neg$, $forall$, and $exists$ are logical operators, but $models$ is a metalogic symbol; purists will not like you mixing those up. So, it may be better to use the English 'some' and 'all' and 'not'
For part 2: here is where you use the result of part 1! In particular, in order to decide whether $varphi$ is valid or not, you can decide whether $neg varphi$ is satisfiable or not: if $neg varphi$ is satisfiable, then $varphi$ is not valid, but if $neg varphi$ is not satisfiable, then $varphi$ is valid. And now you just combine that with Godel's completeness result (to be precise: the theorem that a statement is provable if and only if it is valid ... the more difficult 'if' part of which is the completeness theorem): if $varphi$ is valid, then it is provable, and if $varphi$ is not valid, then it is not provable.
So for that first part: if you have algorithm $mathcal{A}$ that can figure put whether $varphi$ is satisfiable or not for any $varphi$, then design algorithm $mathcal{B}$ that is trying to figure out whether $varphi$ is provable or not as follows:
Take in $varphi$
Negate $varphi$
Call algorithm $mathcal{A}$ with $neg varphi$
4a. If algorithm $mathcal{A}$ says that $neg varphi$ is satisfiable, then print '$varphi$ is not provable!'
4b. If algorithm $mathcal{A}$ says that $neg varphi$ is not satisfiable, then print '$varphi$ is provable!'
Thanks, appreciate the suggestion! I will note this for the future. (An aside: could you say a few words on what you mean, specifically, by "metalogic"?)
– Rebecca Bonham
Nov 19 at 1:00
1
@RebeccaBonham $models$ is a 'meta-logic' symbol in that it is used to express a statement about a logic statement. That is, $varphi$ is a logic statement, and $mathscr{M}modelsvarphi$ is a statement about that logic statement.
– Bram28
Nov 19 at 1:03
Got it, thanks.
– Rebecca Bonham
Nov 19 at 1:04
2
Strictly speaking I think "Gödel's completeness result" is only "if $varphi$ is valid then it is provable". The other direction is soundness of FOL, which is generally considered too obvious to have anyone's name attached to it.
– Henning Makholm
Nov 19 at 1:08
1
@HenningMakholm quite so .. the document the OP is working with kind of hides this as well ... they put the 'if and only if' as a theorem proved by Godel .. yet refer to it as the Completeness theorem
– Bram28
Nov 19 at 1:16
|
show 2 more comments
up vote
7
down vote
accepted
You got the right idea for part 1, but it is unusual to use the logical notation that you do: $neg$, $forall$, and $exists$ are logical operators, but $models$ is a metalogic symbol; purists will not like you mixing those up. So, it may be better to use the English 'some' and 'all' and 'not'
For part 2: here is where you use the result of part 1! In particular, in order to decide whether $varphi$ is valid or not, you can decide whether $neg varphi$ is satisfiable or not: if $neg varphi$ is satisfiable, then $varphi$ is not valid, but if $neg varphi$ is not satisfiable, then $varphi$ is valid. And now you just combine that with Godel's completeness result (to be precise: the theorem that a statement is provable if and only if it is valid ... the more difficult 'if' part of which is the completeness theorem): if $varphi$ is valid, then it is provable, and if $varphi$ is not valid, then it is not provable.
So for that first part: if you have algorithm $mathcal{A}$ that can figure put whether $varphi$ is satisfiable or not for any $varphi$, then design algorithm $mathcal{B}$ that is trying to figure out whether $varphi$ is provable or not as follows:
Take in $varphi$
Negate $varphi$
Call algorithm $mathcal{A}$ with $neg varphi$
4a. If algorithm $mathcal{A}$ says that $neg varphi$ is satisfiable, then print '$varphi$ is not provable!'
4b. If algorithm $mathcal{A}$ says that $neg varphi$ is not satisfiable, then print '$varphi$ is provable!'
Thanks, appreciate the suggestion! I will note this for the future. (An aside: could you say a few words on what you mean, specifically, by "metalogic"?)
– Rebecca Bonham
Nov 19 at 1:00
1
@RebeccaBonham $models$ is a 'meta-logic' symbol in that it is used to express a statement about a logic statement. That is, $varphi$ is a logic statement, and $mathscr{M}modelsvarphi$ is a statement about that logic statement.
– Bram28
Nov 19 at 1:03
Got it, thanks.
– Rebecca Bonham
Nov 19 at 1:04
2
Strictly speaking I think "Gödel's completeness result" is only "if $varphi$ is valid then it is provable". The other direction is soundness of FOL, which is generally considered too obvious to have anyone's name attached to it.
– Henning Makholm
Nov 19 at 1:08
1
@HenningMakholm quite so .. the document the OP is working with kind of hides this as well ... they put the 'if and only if' as a theorem proved by Godel .. yet refer to it as the Completeness theorem
– Bram28
Nov 19 at 1:16
|
show 2 more comments
up vote
7
down vote
accepted
up vote
7
down vote
accepted
You got the right idea for part 1, but it is unusual to use the logical notation that you do: $neg$, $forall$, and $exists$ are logical operators, but $models$ is a metalogic symbol; purists will not like you mixing those up. So, it may be better to use the English 'some' and 'all' and 'not'
For part 2: here is where you use the result of part 1! In particular, in order to decide whether $varphi$ is valid or not, you can decide whether $neg varphi$ is satisfiable or not: if $neg varphi$ is satisfiable, then $varphi$ is not valid, but if $neg varphi$ is not satisfiable, then $varphi$ is valid. And now you just combine that with Godel's completeness result (to be precise: the theorem that a statement is provable if and only if it is valid ... the more difficult 'if' part of which is the completeness theorem): if $varphi$ is valid, then it is provable, and if $varphi$ is not valid, then it is not provable.
So for that first part: if you have algorithm $mathcal{A}$ that can figure put whether $varphi$ is satisfiable or not for any $varphi$, then design algorithm $mathcal{B}$ that is trying to figure out whether $varphi$ is provable or not as follows:
Take in $varphi$
Negate $varphi$
Call algorithm $mathcal{A}$ with $neg varphi$
4a. If algorithm $mathcal{A}$ says that $neg varphi$ is satisfiable, then print '$varphi$ is not provable!'
4b. If algorithm $mathcal{A}$ says that $neg varphi$ is not satisfiable, then print '$varphi$ is provable!'
You got the right idea for part 1, but it is unusual to use the logical notation that you do: $neg$, $forall$, and $exists$ are logical operators, but $models$ is a metalogic symbol; purists will not like you mixing those up. So, it may be better to use the English 'some' and 'all' and 'not'
For part 2: here is where you use the result of part 1! In particular, in order to decide whether $varphi$ is valid or not, you can decide whether $neg varphi$ is satisfiable or not: if $neg varphi$ is satisfiable, then $varphi$ is not valid, but if $neg varphi$ is not satisfiable, then $varphi$ is valid. And now you just combine that with Godel's completeness result (to be precise: the theorem that a statement is provable if and only if it is valid ... the more difficult 'if' part of which is the completeness theorem): if $varphi$ is valid, then it is provable, and if $varphi$ is not valid, then it is not provable.
So for that first part: if you have algorithm $mathcal{A}$ that can figure put whether $varphi$ is satisfiable or not for any $varphi$, then design algorithm $mathcal{B}$ that is trying to figure out whether $varphi$ is provable or not as follows:
Take in $varphi$
Negate $varphi$
Call algorithm $mathcal{A}$ with $neg varphi$
4a. If algorithm $mathcal{A}$ says that $neg varphi$ is satisfiable, then print '$varphi$ is not provable!'
4b. If algorithm $mathcal{A}$ says that $neg varphi$ is not satisfiable, then print '$varphi$ is provable!'
edited Nov 19 at 1:32
answered Nov 19 at 0:58
Bram28
58.3k44185
58.3k44185
Thanks, appreciate the suggestion! I will note this for the future. (An aside: could you say a few words on what you mean, specifically, by "metalogic"?)
– Rebecca Bonham
Nov 19 at 1:00
1
@RebeccaBonham $models$ is a 'meta-logic' symbol in that it is used to express a statement about a logic statement. That is, $varphi$ is a logic statement, and $mathscr{M}modelsvarphi$ is a statement about that logic statement.
– Bram28
Nov 19 at 1:03
Got it, thanks.
– Rebecca Bonham
Nov 19 at 1:04
2
Strictly speaking I think "Gödel's completeness result" is only "if $varphi$ is valid then it is provable". The other direction is soundness of FOL, which is generally considered too obvious to have anyone's name attached to it.
– Henning Makholm
Nov 19 at 1:08
1
@HenningMakholm quite so .. the document the OP is working with kind of hides this as well ... they put the 'if and only if' as a theorem proved by Godel .. yet refer to it as the Completeness theorem
– Bram28
Nov 19 at 1:16
|
show 2 more comments
Thanks, appreciate the suggestion! I will note this for the future. (An aside: could you say a few words on what you mean, specifically, by "metalogic"?)
– Rebecca Bonham
Nov 19 at 1:00
1
@RebeccaBonham $models$ is a 'meta-logic' symbol in that it is used to express a statement about a logic statement. That is, $varphi$ is a logic statement, and $mathscr{M}modelsvarphi$ is a statement about that logic statement.
– Bram28
Nov 19 at 1:03
Got it, thanks.
– Rebecca Bonham
Nov 19 at 1:04
2
Strictly speaking I think "Gödel's completeness result" is only "if $varphi$ is valid then it is provable". The other direction is soundness of FOL, which is generally considered too obvious to have anyone's name attached to it.
– Henning Makholm
Nov 19 at 1:08
1
@HenningMakholm quite so .. the document the OP is working with kind of hides this as well ... they put the 'if and only if' as a theorem proved by Godel .. yet refer to it as the Completeness theorem
– Bram28
Nov 19 at 1:16
Thanks, appreciate the suggestion! I will note this for the future. (An aside: could you say a few words on what you mean, specifically, by "metalogic"?)
– Rebecca Bonham
Nov 19 at 1:00
Thanks, appreciate the suggestion! I will note this for the future. (An aside: could you say a few words on what you mean, specifically, by "metalogic"?)
– Rebecca Bonham
Nov 19 at 1:00
1
1
@RebeccaBonham $models$ is a 'meta-logic' symbol in that it is used to express a statement about a logic statement. That is, $varphi$ is a logic statement, and $mathscr{M}modelsvarphi$ is a statement about that logic statement.
– Bram28
Nov 19 at 1:03
@RebeccaBonham $models$ is a 'meta-logic' symbol in that it is used to express a statement about a logic statement. That is, $varphi$ is a logic statement, and $mathscr{M}modelsvarphi$ is a statement about that logic statement.
– Bram28
Nov 19 at 1:03
Got it, thanks.
– Rebecca Bonham
Nov 19 at 1:04
Got it, thanks.
– Rebecca Bonham
Nov 19 at 1:04
2
2
Strictly speaking I think "Gödel's completeness result" is only "if $varphi$ is valid then it is provable". The other direction is soundness of FOL, which is generally considered too obvious to have anyone's name attached to it.
– Henning Makholm
Nov 19 at 1:08
Strictly speaking I think "Gödel's completeness result" is only "if $varphi$ is valid then it is provable". The other direction is soundness of FOL, which is generally considered too obvious to have anyone's name attached to it.
– Henning Makholm
Nov 19 at 1:08
1
1
@HenningMakholm quite so .. the document the OP is working with kind of hides this as well ... they put the 'if and only if' as a theorem proved by Godel .. yet refer to it as the Completeness theorem
– Bram28
Nov 19 at 1:16
@HenningMakholm quite so .. the document the OP is working with kind of hides this as well ... they put the 'if and only if' as a theorem proved by Godel .. yet refer to it as the Completeness theorem
– Bram28
Nov 19 at 1:16
|
show 2 more comments
up vote
6
down vote
For my own purposes, I'm archiving here my best attempt at integrating, in a compact manner, everything that was mentioned in the answers to my original question. Any comments or critiques of any kind are always welcome. Thanks again to the contributors.
Definitions. A sentence $varphi$ is valid if it is true in all models. In contrast, $varphi$ is satisfiable if it is true in some model.
Completeness theorem with soundness. A sentence in first-order logic is provable if and only if it is valid.
Then the answers to the problems stated above can be given as follows:
Let $mathscr{M}_x$ be a model, $xinmathbb{N}$. Let $varphi$ be a sentence in first-order logic. Let $P(x)$ be the predicate "$varphi$ is true in $mathscr{M}_x$." Then $forall x P(x) equiv neg exists x P(x)$ and $exists x P(x) equiv neg forall x neg P(x)$ by the above definitions and De Morgan's laws.
Suppose we have $mathcal{A}$. Let $mathcal{B}$ be the algorithm defined by the following procedure. Step 1: take $varphi$ as input. Step 2: negate $varphi$. Step 3: call $mathcal{A}$ with input $negvarphi$, written $mathcal{A}(negvarphi)$. Step 4, case (a): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is satisfiable," then by the above equivalences $varphi$ is not valid and by the completeness theorem it is not provable. Step 4, case (b): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is not satisfiable," then by the above equivalences $varphi$ is valid and by the completeness theorem it is provable. Thus by making use of $mathcal{A}$ we have obtained $mathcal{B}$ such that $mathcal{B}$ decides whether $varphi$ is provable or not. By a symmetric argument we can obtain $mathcal{A}$ if given $mathcal{B}$.
New contributor
2
For 1. The $mathscr{M}_x$ is a little weird ... what is the index here? Again, it may be better just to avoid formal logic notation completely here, since this is all meta-logic, rather than formal logic. So, for example, I would say: $varphi$ is valid if and only (by definition of valid) if $varphi$ is true in all possible models if and only if (by pure logic) there is no model in which $varphi$ is false if and only if (by semantics) there is no model in which $neg varphi$ is true if and only if (by definition satisfiability) $neg varphi$ is not satisfiable.
– Bram28
Nov 19 at 14:56
1
For 2. The completeness theorem is that a statement is provable if it is valid. But in order to answer this question, you need to stronger Theorem that a statement is provable if it and only if is valid. Remember that you need a decision procedure, meaning that if $varphi$ is provable, then $mathcal{B}$ will say it is provable, and if $varphi$ is not provable, then $mathcal{B}$ will say it is not provable. So, if you find that $neg varphi$ is not valid, then you need to be able to conclude it is not provable, which you can only do if you have an 'if and only if'
– Bram28
Nov 19 at 15:02
1
Indeed, this is the key difference between the completeness of first-order logic and the undecidability of first-order logic: it is complete in that if a formula is valid, it can be proven ... and indeed there is an algorithm that, when given that formula, will be able to say that it is provable (and in fact it can even produce a proof). But such a complete algorithm is not a decision procedure, since for that, it also needs to say that a formula that is not valid is not provable. And as it turns out (and as the document tries to show) there cannot be such a decision procedure.
– Bram28
Nov 19 at 15:06
1
1. I was thinking of "the $mathscr{M}_x$'s" as an enumeration of models, following a kind of notation one of my professors sometimes uses, and which I've kind of become accustomed to. My rewritten answer to the first exercise was an attempt to reformulate my idea into logical statements, staying away from symbols like $models$, etc. But I think you're right, and clarity is best served by plain English. I'll treat is as an exercise for myself, to make the effort to find a precise wording without leaning on technical notation.
– Rebecca Bonham
Nov 19 at 16:51
2
Right. The completeness theorem is only in one direction ... but to transform the one decision procedure (algorithm) into the other you need both directions ... which is what the theorem in the document expresses. And yes, the other direction (soundness) is fairly easy, but still, you can't just point to completeness in a proof that the algorithms can be transformed into each other.
– Bram28
Nov 19 at 17:10
|
show 2 more comments
up vote
6
down vote
For my own purposes, I'm archiving here my best attempt at integrating, in a compact manner, everything that was mentioned in the answers to my original question. Any comments or critiques of any kind are always welcome. Thanks again to the contributors.
Definitions. A sentence $varphi$ is valid if it is true in all models. In contrast, $varphi$ is satisfiable if it is true in some model.
Completeness theorem with soundness. A sentence in first-order logic is provable if and only if it is valid.
Then the answers to the problems stated above can be given as follows:
Let $mathscr{M}_x$ be a model, $xinmathbb{N}$. Let $varphi$ be a sentence in first-order logic. Let $P(x)$ be the predicate "$varphi$ is true in $mathscr{M}_x$." Then $forall x P(x) equiv neg exists x P(x)$ and $exists x P(x) equiv neg forall x neg P(x)$ by the above definitions and De Morgan's laws.
Suppose we have $mathcal{A}$. Let $mathcal{B}$ be the algorithm defined by the following procedure. Step 1: take $varphi$ as input. Step 2: negate $varphi$. Step 3: call $mathcal{A}$ with input $negvarphi$, written $mathcal{A}(negvarphi)$. Step 4, case (a): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is satisfiable," then by the above equivalences $varphi$ is not valid and by the completeness theorem it is not provable. Step 4, case (b): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is not satisfiable," then by the above equivalences $varphi$ is valid and by the completeness theorem it is provable. Thus by making use of $mathcal{A}$ we have obtained $mathcal{B}$ such that $mathcal{B}$ decides whether $varphi$ is provable or not. By a symmetric argument we can obtain $mathcal{A}$ if given $mathcal{B}$.
New contributor
2
For 1. The $mathscr{M}_x$ is a little weird ... what is the index here? Again, it may be better just to avoid formal logic notation completely here, since this is all meta-logic, rather than formal logic. So, for example, I would say: $varphi$ is valid if and only (by definition of valid) if $varphi$ is true in all possible models if and only if (by pure logic) there is no model in which $varphi$ is false if and only if (by semantics) there is no model in which $neg varphi$ is true if and only if (by definition satisfiability) $neg varphi$ is not satisfiable.
– Bram28
Nov 19 at 14:56
1
For 2. The completeness theorem is that a statement is provable if it is valid. But in order to answer this question, you need to stronger Theorem that a statement is provable if it and only if is valid. Remember that you need a decision procedure, meaning that if $varphi$ is provable, then $mathcal{B}$ will say it is provable, and if $varphi$ is not provable, then $mathcal{B}$ will say it is not provable. So, if you find that $neg varphi$ is not valid, then you need to be able to conclude it is not provable, which you can only do if you have an 'if and only if'
– Bram28
Nov 19 at 15:02
1
Indeed, this is the key difference between the completeness of first-order logic and the undecidability of first-order logic: it is complete in that if a formula is valid, it can be proven ... and indeed there is an algorithm that, when given that formula, will be able to say that it is provable (and in fact it can even produce a proof). But such a complete algorithm is not a decision procedure, since for that, it also needs to say that a formula that is not valid is not provable. And as it turns out (and as the document tries to show) there cannot be such a decision procedure.
– Bram28
Nov 19 at 15:06
1
1. I was thinking of "the $mathscr{M}_x$'s" as an enumeration of models, following a kind of notation one of my professors sometimes uses, and which I've kind of become accustomed to. My rewritten answer to the first exercise was an attempt to reformulate my idea into logical statements, staying away from symbols like $models$, etc. But I think you're right, and clarity is best served by plain English. I'll treat is as an exercise for myself, to make the effort to find a precise wording without leaning on technical notation.
– Rebecca Bonham
Nov 19 at 16:51
2
Right. The completeness theorem is only in one direction ... but to transform the one decision procedure (algorithm) into the other you need both directions ... which is what the theorem in the document expresses. And yes, the other direction (soundness) is fairly easy, but still, you can't just point to completeness in a proof that the algorithms can be transformed into each other.
– Bram28
Nov 19 at 17:10
|
show 2 more comments
up vote
6
down vote
up vote
6
down vote
For my own purposes, I'm archiving here my best attempt at integrating, in a compact manner, everything that was mentioned in the answers to my original question. Any comments or critiques of any kind are always welcome. Thanks again to the contributors.
Definitions. A sentence $varphi$ is valid if it is true in all models. In contrast, $varphi$ is satisfiable if it is true in some model.
Completeness theorem with soundness. A sentence in first-order logic is provable if and only if it is valid.
Then the answers to the problems stated above can be given as follows:
Let $mathscr{M}_x$ be a model, $xinmathbb{N}$. Let $varphi$ be a sentence in first-order logic. Let $P(x)$ be the predicate "$varphi$ is true in $mathscr{M}_x$." Then $forall x P(x) equiv neg exists x P(x)$ and $exists x P(x) equiv neg forall x neg P(x)$ by the above definitions and De Morgan's laws.
Suppose we have $mathcal{A}$. Let $mathcal{B}$ be the algorithm defined by the following procedure. Step 1: take $varphi$ as input. Step 2: negate $varphi$. Step 3: call $mathcal{A}$ with input $negvarphi$, written $mathcal{A}(negvarphi)$. Step 4, case (a): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is satisfiable," then by the above equivalences $varphi$ is not valid and by the completeness theorem it is not provable. Step 4, case (b): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is not satisfiable," then by the above equivalences $varphi$ is valid and by the completeness theorem it is provable. Thus by making use of $mathcal{A}$ we have obtained $mathcal{B}$ such that $mathcal{B}$ decides whether $varphi$ is provable or not. By a symmetric argument we can obtain $mathcal{A}$ if given $mathcal{B}$.
New contributor
For my own purposes, I'm archiving here my best attempt at integrating, in a compact manner, everything that was mentioned in the answers to my original question. Any comments or critiques of any kind are always welcome. Thanks again to the contributors.
Definitions. A sentence $varphi$ is valid if it is true in all models. In contrast, $varphi$ is satisfiable if it is true in some model.
Completeness theorem with soundness. A sentence in first-order logic is provable if and only if it is valid.
Then the answers to the problems stated above can be given as follows:
Let $mathscr{M}_x$ be a model, $xinmathbb{N}$. Let $varphi$ be a sentence in first-order logic. Let $P(x)$ be the predicate "$varphi$ is true in $mathscr{M}_x$." Then $forall x P(x) equiv neg exists x P(x)$ and $exists x P(x) equiv neg forall x neg P(x)$ by the above definitions and De Morgan's laws.
Suppose we have $mathcal{A}$. Let $mathcal{B}$ be the algorithm defined by the following procedure. Step 1: take $varphi$ as input. Step 2: negate $varphi$. Step 3: call $mathcal{A}$ with input $negvarphi$, written $mathcal{A}(negvarphi)$. Step 4, case (a): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is satisfiable," then by the above equivalences $varphi$ is not valid and by the completeness theorem it is not provable. Step 4, case (b): If $mathcal{A}(negvarphi)$ returns "$negvarphi$ is not satisfiable," then by the above equivalences $varphi$ is valid and by the completeness theorem it is provable. Thus by making use of $mathcal{A}$ we have obtained $mathcal{B}$ such that $mathcal{B}$ decides whether $varphi$ is provable or not. By a symmetric argument we can obtain $mathcal{A}$ if given $mathcal{B}$.
New contributor
edited Nov 19 at 17:26
New contributor
answered Nov 19 at 3:12
Rebecca Bonham
15310
15310
New contributor
New contributor
2
For 1. The $mathscr{M}_x$ is a little weird ... what is the index here? Again, it may be better just to avoid formal logic notation completely here, since this is all meta-logic, rather than formal logic. So, for example, I would say: $varphi$ is valid if and only (by definition of valid) if $varphi$ is true in all possible models if and only if (by pure logic) there is no model in which $varphi$ is false if and only if (by semantics) there is no model in which $neg varphi$ is true if and only if (by definition satisfiability) $neg varphi$ is not satisfiable.
– Bram28
Nov 19 at 14:56
1
For 2. The completeness theorem is that a statement is provable if it is valid. But in order to answer this question, you need to stronger Theorem that a statement is provable if it and only if is valid. Remember that you need a decision procedure, meaning that if $varphi$ is provable, then $mathcal{B}$ will say it is provable, and if $varphi$ is not provable, then $mathcal{B}$ will say it is not provable. So, if you find that $neg varphi$ is not valid, then you need to be able to conclude it is not provable, which you can only do if you have an 'if and only if'
– Bram28
Nov 19 at 15:02
1
Indeed, this is the key difference between the completeness of first-order logic and the undecidability of first-order logic: it is complete in that if a formula is valid, it can be proven ... and indeed there is an algorithm that, when given that formula, will be able to say that it is provable (and in fact it can even produce a proof). But such a complete algorithm is not a decision procedure, since for that, it also needs to say that a formula that is not valid is not provable. And as it turns out (and as the document tries to show) there cannot be such a decision procedure.
– Bram28
Nov 19 at 15:06
1
1. I was thinking of "the $mathscr{M}_x$'s" as an enumeration of models, following a kind of notation one of my professors sometimes uses, and which I've kind of become accustomed to. My rewritten answer to the first exercise was an attempt to reformulate my idea into logical statements, staying away from symbols like $models$, etc. But I think you're right, and clarity is best served by plain English. I'll treat is as an exercise for myself, to make the effort to find a precise wording without leaning on technical notation.
– Rebecca Bonham
Nov 19 at 16:51
2
Right. The completeness theorem is only in one direction ... but to transform the one decision procedure (algorithm) into the other you need both directions ... which is what the theorem in the document expresses. And yes, the other direction (soundness) is fairly easy, but still, you can't just point to completeness in a proof that the algorithms can be transformed into each other.
– Bram28
Nov 19 at 17:10
|
show 2 more comments
2
For 1. The $mathscr{M}_x$ is a little weird ... what is the index here? Again, it may be better just to avoid formal logic notation completely here, since this is all meta-logic, rather than formal logic. So, for example, I would say: $varphi$ is valid if and only (by definition of valid) if $varphi$ is true in all possible models if and only if (by pure logic) there is no model in which $varphi$ is false if and only if (by semantics) there is no model in which $neg varphi$ is true if and only if (by definition satisfiability) $neg varphi$ is not satisfiable.
– Bram28
Nov 19 at 14:56
1
For 2. The completeness theorem is that a statement is provable if it is valid. But in order to answer this question, you need to stronger Theorem that a statement is provable if it and only if is valid. Remember that you need a decision procedure, meaning that if $varphi$ is provable, then $mathcal{B}$ will say it is provable, and if $varphi$ is not provable, then $mathcal{B}$ will say it is not provable. So, if you find that $neg varphi$ is not valid, then you need to be able to conclude it is not provable, which you can only do if you have an 'if and only if'
– Bram28
Nov 19 at 15:02
1
Indeed, this is the key difference between the completeness of first-order logic and the undecidability of first-order logic: it is complete in that if a formula is valid, it can be proven ... and indeed there is an algorithm that, when given that formula, will be able to say that it is provable (and in fact it can even produce a proof). But such a complete algorithm is not a decision procedure, since for that, it also needs to say that a formula that is not valid is not provable. And as it turns out (and as the document tries to show) there cannot be such a decision procedure.
– Bram28
Nov 19 at 15:06
1
1. I was thinking of "the $mathscr{M}_x$'s" as an enumeration of models, following a kind of notation one of my professors sometimes uses, and which I've kind of become accustomed to. My rewritten answer to the first exercise was an attempt to reformulate my idea into logical statements, staying away from symbols like $models$, etc. But I think you're right, and clarity is best served by plain English. I'll treat is as an exercise for myself, to make the effort to find a precise wording without leaning on technical notation.
– Rebecca Bonham
Nov 19 at 16:51
2
Right. The completeness theorem is only in one direction ... but to transform the one decision procedure (algorithm) into the other you need both directions ... which is what the theorem in the document expresses. And yes, the other direction (soundness) is fairly easy, but still, you can't just point to completeness in a proof that the algorithms can be transformed into each other.
– Bram28
Nov 19 at 17:10
2
2
For 1. The $mathscr{M}_x$ is a little weird ... what is the index here? Again, it may be better just to avoid formal logic notation completely here, since this is all meta-logic, rather than formal logic. So, for example, I would say: $varphi$ is valid if and only (by definition of valid) if $varphi$ is true in all possible models if and only if (by pure logic) there is no model in which $varphi$ is false if and only if (by semantics) there is no model in which $neg varphi$ is true if and only if (by definition satisfiability) $neg varphi$ is not satisfiable.
– Bram28
Nov 19 at 14:56
For 1. The $mathscr{M}_x$ is a little weird ... what is the index here? Again, it may be better just to avoid formal logic notation completely here, since this is all meta-logic, rather than formal logic. So, for example, I would say: $varphi$ is valid if and only (by definition of valid) if $varphi$ is true in all possible models if and only if (by pure logic) there is no model in which $varphi$ is false if and only if (by semantics) there is no model in which $neg varphi$ is true if and only if (by definition satisfiability) $neg varphi$ is not satisfiable.
– Bram28
Nov 19 at 14:56
1
1
For 2. The completeness theorem is that a statement is provable if it is valid. But in order to answer this question, you need to stronger Theorem that a statement is provable if it and only if is valid. Remember that you need a decision procedure, meaning that if $varphi$ is provable, then $mathcal{B}$ will say it is provable, and if $varphi$ is not provable, then $mathcal{B}$ will say it is not provable. So, if you find that $neg varphi$ is not valid, then you need to be able to conclude it is not provable, which you can only do if you have an 'if and only if'
– Bram28
Nov 19 at 15:02
For 2. The completeness theorem is that a statement is provable if it is valid. But in order to answer this question, you need to stronger Theorem that a statement is provable if it and only if is valid. Remember that you need a decision procedure, meaning that if $varphi$ is provable, then $mathcal{B}$ will say it is provable, and if $varphi$ is not provable, then $mathcal{B}$ will say it is not provable. So, if you find that $neg varphi$ is not valid, then you need to be able to conclude it is not provable, which you can only do if you have an 'if and only if'
– Bram28
Nov 19 at 15:02
1
1
Indeed, this is the key difference between the completeness of first-order logic and the undecidability of first-order logic: it is complete in that if a formula is valid, it can be proven ... and indeed there is an algorithm that, when given that formula, will be able to say that it is provable (and in fact it can even produce a proof). But such a complete algorithm is not a decision procedure, since for that, it also needs to say that a formula that is not valid is not provable. And as it turns out (and as the document tries to show) there cannot be such a decision procedure.
– Bram28
Nov 19 at 15:06
Indeed, this is the key difference between the completeness of first-order logic and the undecidability of first-order logic: it is complete in that if a formula is valid, it can be proven ... and indeed there is an algorithm that, when given that formula, will be able to say that it is provable (and in fact it can even produce a proof). But such a complete algorithm is not a decision procedure, since for that, it also needs to say that a formula that is not valid is not provable. And as it turns out (and as the document tries to show) there cannot be such a decision procedure.
– Bram28
Nov 19 at 15:06
1
1
1. I was thinking of "the $mathscr{M}_x$'s" as an enumeration of models, following a kind of notation one of my professors sometimes uses, and which I've kind of become accustomed to. My rewritten answer to the first exercise was an attempt to reformulate my idea into logical statements, staying away from symbols like $models$, etc. But I think you're right, and clarity is best served by plain English. I'll treat is as an exercise for myself, to make the effort to find a precise wording without leaning on technical notation.
– Rebecca Bonham
Nov 19 at 16:51
1. I was thinking of "the $mathscr{M}_x$'s" as an enumeration of models, following a kind of notation one of my professors sometimes uses, and which I've kind of become accustomed to. My rewritten answer to the first exercise was an attempt to reformulate my idea into logical statements, staying away from symbols like $models$, etc. But I think you're right, and clarity is best served by plain English. I'll treat is as an exercise for myself, to make the effort to find a precise wording without leaning on technical notation.
– Rebecca Bonham
Nov 19 at 16:51
2
2
Right. The completeness theorem is only in one direction ... but to transform the one decision procedure (algorithm) into the other you need both directions ... which is what the theorem in the document expresses. And yes, the other direction (soundness) is fairly easy, but still, you can't just point to completeness in a proof that the algorithms can be transformed into each other.
– Bram28
Nov 19 at 17:10
Right. The completeness theorem is only in one direction ... but to transform the one decision procedure (algorithm) into the other you need both directions ... which is what the theorem in the document expresses. And yes, the other direction (soundness) is fairly easy, but still, you can't just point to completeness in a proof that the algorithms can be transformed into each other.
– Bram28
Nov 19 at 17:10
|
show 2 more comments
Rebecca Bonham is a new contributor. Be nice, and check out our Code of Conduct.
Rebecca Bonham is a new contributor. Be nice, and check out our Code of Conduct.
Rebecca Bonham is a new contributor. Be nice, and check out our Code of Conduct.
Rebecca Bonham 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%2f3004349%2fg%25c3%25b6dels-completeness-theorem-and-the-undecidability-of-first-order-logic%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
10
+1 for all the homework you did before coming here for help, and for the care you took in formatting.
– Ethan Bolker
Nov 19 at 1:15
3
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
Nov 19 at 2:28
2
@RebeccaBonham It's questions like these among all of the slush on this site that make me want to come back each day.
– Rushabh Mehta
Nov 19 at 6:41
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
Nov 19 at 16:43