Mixing
Gödel's completeness theorem and the undecidability of first-order logic
up vote
13
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
asked 19 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
add a comment |
up vote
13
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
asked 19 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
10
+1 for all the homework you did before coming here for help, and for the care you took in formatting.
– Ethan Bolker
18 hours ago
3
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
17 hours ago
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
13 hours ago
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
3 hours ago
add a comment |
up vote
13
down vote
favorite
up vote
13
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
asked 19 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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
asked 19 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 19 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
edited 19 hours ago
asked 19 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 19 hours ago
Rebecca Bonham
13310
asked 19 hours ago
Rebecca Bonham
13310
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
10
+1 for all the homework you did before coming here for help, and for the care you took in formatting.
– Ethan Bolker
18 hours ago
3
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
17 hours ago
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
13 hours ago
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
3 hours ago
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
18 hours ago
3
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
17 hours ago
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
13 hours ago
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
3 hours ago
10
10
+1 for all the homework you did before coming here for help, and for the care you took in formatting.
– Ethan Bolker
18 hours ago
+1 for all the homework you did before coming here for help, and for the care you took in formatting.
– Ethan Bolker
18 hours ago
3
3
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
17 hours ago
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
17 hours ago
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
13 hours ago
@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
13 hours ago
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
3 hours ago
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
3 hours ago
add a comment |
2 Answers
2
active
oldest
votes
up vote
6
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!'
answered 19 hours ago
Bram28
58k44185
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
19 hours ago
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
19 hours ago
Got it, thanks.
– Rebecca Bonham
19 hours ago
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
19 hours ago
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
18 hours ago
|
show 2 more comments
up vote
5
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}$.
answered 16 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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
5 hours ago
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
5 hours ago
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
5 hours ago
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
3 hours ago
1
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
3 hours ago
|
show 2 more comments
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
6
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!'
answered 19 hours ago
Bram28
58k44185
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
19 hours ago
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
19 hours ago
Got it, thanks.
– Rebecca Bonham
19 hours ago
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
19 hours ago
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
18 hours ago
|
show 2 more comments
up vote
6
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!'
answered 19 hours ago
Bram28
58k44185
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
19 hours ago
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
19 hours ago
Got it, thanks.
– Rebecca Bonham
19 hours ago
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
19 hours ago
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
18 hours ago
|
show 2 more comments
up vote
6
down vote
accepted
up vote
6
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!'
answered 19 hours ago
Bram28
58k44185
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!'
answered 19 hours ago
Bram28
58k44185
edited 18 hours ago
answered 19 hours ago
Bram28
58k44185
answered 19 hours ago
Bram28
58k44185
answered 19 hours ago
Bram28
58k44185
58k44185
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
19 hours ago
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
19 hours ago
Got it, thanks.
– Rebecca Bonham
19 hours ago
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
19 hours ago
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
18 hours ago
|
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
19 hours ago
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
19 hours ago
Got it, thanks.
– Rebecca Bonham
19 hours ago
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
19 hours ago
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
18 hours ago
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
19 hours ago
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
19 hours ago
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
19 hours ago
@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
19 hours ago
Got it, thanks.
– Rebecca Bonham
19 hours ago
Got it, thanks.
– Rebecca Bonham
19 hours ago
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
19 hours ago
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
19 hours ago
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
18 hours ago
@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
18 hours ago
|
show 2 more comments
up vote
5
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}$.
answered 16 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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
5 hours ago
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
5 hours ago
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
5 hours ago
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
3 hours ago
1
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
3 hours ago
|
show 2 more comments
up vote
5
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}$.
answered 16 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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
5 hours ago
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
5 hours ago
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
5 hours ago
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
3 hours ago
1
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
3 hours ago
|
show 2 more comments
up vote
5
down vote
up vote
5
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}$.
answered 16 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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}$.
answered 16 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
edited 2 hours ago
answered 16 hours ago
Rebecca Bonham
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
answered 16 hours ago
Rebecca Bonham
13310
answered 16 hours ago
Rebecca Bonham
13310
13310
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
New contributor
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
Rebecca Bonham is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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
5 hours ago
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
5 hours ago
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
5 hours ago
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
3 hours ago
1
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
3 hours ago
|
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
5 hours ago
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
5 hours ago
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
5 hours ago
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
3 hours ago
1
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
3 hours ago
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
5 hours ago
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
5 hours ago
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
5 hours ago
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
5 hours ago
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
5 hours ago
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
5 hours ago
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
3 hours ago
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
3 hours ago
1
1
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
3 hours ago
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
3 hours ago
|
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
18 hours ago
3
Kind of you to say so! Thank you @EthanBolker
– Rebecca Bonham
17 hours ago
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
13 hours ago
@RushabhMehta Appreciate it! I value this site a lot and as a new contributor I am excited to do my best.
– Rebecca Bonham
3 hours ago