Validity of “rank” construction in Manin's proof of Lemma 6.7 for Gödel's completeness theorem
$begingroup$
The question is about the proof of Lemma 6.7 in Yuri Manin's "A Course in Mathematical Logic", which is part of the proof of Gödel's completeness theorem.
Lemma 6.7 If $mathcal{E}$ is consistent and contains $text{Ax }L$, then there exist:
(a) a language $L'$ whose alphabet is obtained from the alphabet of $L$ by adding a set of new constants having cardinality $leq$ card (alphabet of $L$) + $aleph_0$.
(b) a set of formulas $mathcal{E'}$ in $L'$ which is consistent, contains $mathcal{E}$ and $text{Ax }L'$, and has the property that the alphabet of $L'$ is sufficient for $mathcal{E'}$.
Part (a) of the claim is proven by simply adding to the alphabet of $L$ a set of new constants of cardinality card (alphabet of L) + $aleph_0$, and creating a new language $L'$ using this alphabet. The proof then shows that $mathcal{E} cup text{Ax }L$ is consistent, and I am okay with this part.
This particular section of the proof is confusing:
(c) We consider the set $S$ of formulas $P(x)$ containing one free variable $x$ and such that $negforall x P(x) in mathcal{E} cup text{Ax }L'$. For each $P(x)$ in $S$ we choose a new constant $c_P$ subject to the following restriction: each $c_P$ can be assigned a natural number, its rank, in such a way that if a constant of rank $n$ occurs in $P(x)$ then $c_P$ has rank $gt n$.
The set $text{Ax }L'$ consists of the tautologies of $L'$ and logical quantifier axioms. But a proposition of the form $negforall x P(x)$ cannot be either of those.
It cannot be a tautology because tautologies are logical polynomials over a finite set of base propositions, whose truth value is $1$ independently of the choice of truth value for each base proposition (section 3.4). Since $negforall x P(x)$ contains only a single connective $neg$ (quantifiers cannot show up as connectives), either $negforall x P(x)$ or $forall x P(x)$ must be the base proposition, and clearly in both cases the truth value is dependent on the truth value of the base proposition.
The formula $negforall x P(x)$ cannot either be a logical quantifier axiom because the quantifier axioms have one of the following structures, none of which fit the structure of $negforall x P(x)$ (section 3.5):
(a) $forall x (P implies Q) implies (P implies forall x Q)$
(b) $forall x neg P iff neg exists x P$
(c) $forall x P(x) implies P(t)$
Therefore we must have "$negforall x P(x)$" $in mathcal{E}$. But in that case, there cannot be any new constants $c_P$ of $L'$ contained in that formula since it lies in the original language $L$ which does not have this extended alphabet.
With that reasoning, it would seem that the rank of $c_P$ can always be chosen as $1$, because there are no constants of rank $geq 1$ contained in $P(x)$. So the notion of "rank" seems to be useless for the proof.
Did I miss something which makes it essential to introduce the rank, or can the proof carry on without it?
logic proof-explanation first-order-logic proof-theory
asked Dec 22 '18 at 9:37
Tob ErnackTob Ernack
2,279418
$endgroup$
|
show 4 more comments
$begingroup$
The question is about the proof of Lemma 6.7 in Yuri Manin's "A Course in Mathematical Logic", which is part of the proof of Gödel's completeness theorem.
Lemma 6.7 If $mathcal{E}$ is consistent and contains $text{Ax }L$, then there exist:
(a) a language $L'$ whose alphabet is obtained from the alphabet of $L$ by adding a set of new constants having cardinality $leq$ card (alphabet of $L$) + $aleph_0$.
(b) a set of formulas $mathcal{E'}$ in $L'$ which is consistent, contains $mathcal{E}$ and $text{Ax }L'$, and has the property that the alphabet of $L'$ is sufficient for $mathcal{E'}$.
Part (a) of the claim is proven by simply adding to the alphabet of $L$ a set of new constants of cardinality card (alphabet of L) + $aleph_0$, and creating a new language $L'$ using this alphabet. The proof then shows that $mathcal{E} cup text{Ax }L$ is consistent, and I am okay with this part.
This particular section of the proof is confusing:
(c) We consider the set $S$ of formulas $P(x)$ containing one free variable $x$ and such that $negforall x P(x) in mathcal{E} cup text{Ax }L'$. For each $P(x)$ in $S$ we choose a new constant $c_P$ subject to the following restriction: each $c_P$ can be assigned a natural number, its rank, in such a way that if a constant of rank $n$ occurs in $P(x)$ then $c_P$ has rank $gt n$.
The set $text{Ax }L'$ consists of the tautologies of $L'$ and logical quantifier axioms. But a proposition of the form $negforall x P(x)$ cannot be either of those.
It cannot be a tautology because tautologies are logical polynomials over a finite set of base propositions, whose truth value is $1$ independently of the choice of truth value for each base proposition (section 3.4). Since $negforall x P(x)$ contains only a single connective $neg$ (quantifiers cannot show up as connectives), either $negforall x P(x)$ or $forall x P(x)$ must be the base proposition, and clearly in both cases the truth value is dependent on the truth value of the base proposition.
The formula $negforall x P(x)$ cannot either be a logical quantifier axiom because the quantifier axioms have one of the following structures, none of which fit the structure of $negforall x P(x)$ (section 3.5):
(a) $forall x (P implies Q) implies (P implies forall x Q)$
(b) $forall x neg P iff neg exists x P$
(c) $forall x P(x) implies P(t)$
Therefore we must have "$negforall x P(x)$" $in mathcal{E}$. But in that case, there cannot be any new constants $c_P$ of $L'$ contained in that formula since it lies in the original language $L$ which does not have this extended alphabet.
With that reasoning, it would seem that the rank of $c_P$ can always be chosen as $1$, because there are no constants of rank $geq 1$ contained in $P(x)$. So the notion of "rank" seems to be useless for the proof.
Did I miss something which makes it essential to introduce the rank, or can the proof carry on without it?
logic proof-explanation first-order-logic proof-theory
asked Dec 22 '18 at 9:37
Tob ErnackTob Ernack
2,279418
$endgroup$
$begingroup$
The construction is a little bit convoluted... You have to start from a formula of the basic language (and thus - as you said - without "added" constant $c_p$) and then add the new formula. As long as you have done this, you have generated a lot of new formulas (in the language extended with $c_p$) and thus you have to iterate the process.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 10:11
$begingroup$
I am not exactly sure where the iteration occurs. In Lemma 6.7 all the new formulas that are created after adding $c_P$ are either tautologies, quantifier axioms, or formulas of the type $R_P: negforall x P(x) implies neg P(c_P)$. None of these will generate new formulas of the form $negforall x P(x)$ to which we could apply the process again, except those that were already in $L$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:22
$begingroup$
I think there is some sort of iteration happening in Lemma 6.8 in order to make the set both complete and have sufficient alphabet, but that doesn't seem to be for the same reasons.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:24
$begingroup$
Maybe I would need to see a specific example of a case where you would need $c_P$ with rank $geq 2$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:29
$begingroup$
Maybe we can check on Henkin's original proof.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 11:39
|
show 4 more comments
$begingroup$
The question is about the proof of Lemma 6.7 in Yuri Manin's "A Course in Mathematical Logic", which is part of the proof of Gödel's completeness theorem.
Lemma 6.7 If $mathcal{E}$ is consistent and contains $text{Ax }L$, then there exist:
(a) a language $L'$ whose alphabet is obtained from the alphabet of $L$ by adding a set of new constants having cardinality $leq$ card (alphabet of $L$) + $aleph_0$.
(b) a set of formulas $mathcal{E'}$ in $L'$ which is consistent, contains $mathcal{E}$ and $text{Ax }L'$, and has the property that the alphabet of $L'$ is sufficient for $mathcal{E'}$.
Part (a) of the claim is proven by simply adding to the alphabet of $L$ a set of new constants of cardinality card (alphabet of L) + $aleph_0$, and creating a new language $L'$ using this alphabet. The proof then shows that $mathcal{E} cup text{Ax }L$ is consistent, and I am okay with this part.
This particular section of the proof is confusing:
(c) We consider the set $S$ of formulas $P(x)$ containing one free variable $x$ and such that $negforall x P(x) in mathcal{E} cup text{Ax }L'$. For each $P(x)$ in $S$ we choose a new constant $c_P$ subject to the following restriction: each $c_P$ can be assigned a natural number, its rank, in such a way that if a constant of rank $n$ occurs in $P(x)$ then $c_P$ has rank $gt n$.
The set $text{Ax }L'$ consists of the tautologies of $L'$ and logical quantifier axioms. But a proposition of the form $negforall x P(x)$ cannot be either of those.
It cannot be a tautology because tautologies are logical polynomials over a finite set of base propositions, whose truth value is $1$ independently of the choice of truth value for each base proposition (section 3.4). Since $negforall x P(x)$ contains only a single connective $neg$ (quantifiers cannot show up as connectives), either $negforall x P(x)$ or $forall x P(x)$ must be the base proposition, and clearly in both cases the truth value is dependent on the truth value of the base proposition.
The formula $negforall x P(x)$ cannot either be a logical quantifier axiom because the quantifier axioms have one of the following structures, none of which fit the structure of $negforall x P(x)$ (section 3.5):
(a) $forall x (P implies Q) implies (P implies forall x Q)$
(b) $forall x neg P iff neg exists x P$
(c) $forall x P(x) implies P(t)$
Therefore we must have "$negforall x P(x)$" $in mathcal{E}$. But in that case, there cannot be any new constants $c_P$ of $L'$ contained in that formula since it lies in the original language $L$ which does not have this extended alphabet.
With that reasoning, it would seem that the rank of $c_P$ can always be chosen as $1$, because there are no constants of rank $geq 1$ contained in $P(x)$. So the notion of "rank" seems to be useless for the proof.
Did I miss something which makes it essential to introduce the rank, or can the proof carry on without it?
logic proof-explanation first-order-logic proof-theory
asked Dec 22 '18 at 9:37
Tob ErnackTob Ernack
2,279418
$endgroup$
The question is about the proof of Lemma 6.7 in Yuri Manin's "A Course in Mathematical Logic", which is part of the proof of Gödel's completeness theorem.
Lemma 6.7 If $mathcal{E}$ is consistent and contains $text{Ax }L$, then there exist:
(a) a language $L'$ whose alphabet is obtained from the alphabet of $L$ by adding a set of new constants having cardinality $leq$ card (alphabet of $L$) + $aleph_0$.
(b) a set of formulas $mathcal{E'}$ in $L'$ which is consistent, contains $mathcal{E}$ and $text{Ax }L'$, and has the property that the alphabet of $L'$ is sufficient for $mathcal{E'}$.
Part (a) of the claim is proven by simply adding to the alphabet of $L$ a set of new constants of cardinality card (alphabet of L) + $aleph_0$, and creating a new language $L'$ using this alphabet. The proof then shows that $mathcal{E} cup text{Ax }L$ is consistent, and I am okay with this part.
This particular section of the proof is confusing:
(c) We consider the set $S$ of formulas $P(x)$ containing one free variable $x$ and such that $negforall x P(x) in mathcal{E} cup text{Ax }L'$. For each $P(x)$ in $S$ we choose a new constant $c_P$ subject to the following restriction: each $c_P$ can be assigned a natural number, its rank, in such a way that if a constant of rank $n$ occurs in $P(x)$ then $c_P$ has rank $gt n$.
The set $text{Ax }L'$ consists of the tautologies of $L'$ and logical quantifier axioms. But a proposition of the form $negforall x P(x)$ cannot be either of those.
It cannot be a tautology because tautologies are logical polynomials over a finite set of base propositions, whose truth value is $1$ independently of the choice of truth value for each base proposition (section 3.4). Since $negforall x P(x)$ contains only a single connective $neg$ (quantifiers cannot show up as connectives), either $negforall x P(x)$ or $forall x P(x)$ must be the base proposition, and clearly in both cases the truth value is dependent on the truth value of the base proposition.
The formula $negforall x P(x)$ cannot either be a logical quantifier axiom because the quantifier axioms have one of the following structures, none of which fit the structure of $negforall x P(x)$ (section 3.5):
(a) $forall x (P implies Q) implies (P implies forall x Q)$
(b) $forall x neg P iff neg exists x P$
(c) $forall x P(x) implies P(t)$
Therefore we must have "$negforall x P(x)$" $in mathcal{E}$. But in that case, there cannot be any new constants $c_P$ of $L'$ contained in that formula since it lies in the original language $L$ which does not have this extended alphabet.
With that reasoning, it would seem that the rank of $c_P$ can always be chosen as $1$, because there are no constants of rank $geq 1$ contained in $P(x)$. So the notion of "rank" seems to be useless for the proof.
Did I miss something which makes it essential to introduce the rank, or can the proof carry on without it?
logic proof-explanation first-order-logic proof-theory
logic proof-explanation first-order-logic proof-theory
asked Dec 22 '18 at 9:37
Tob ErnackTob Ernack
2,279418
asked Dec 22 '18 at 9:37
Tob ErnackTob Ernack
2,279418
edited Dec 22 '18 at 10:04
Tob Ernack
asked Dec 22 '18 at 9:37
Tob ErnackTob Ernack
2,279418
asked Dec 22 '18 at 9:37
Tob ErnackTob Ernack
2,279418
asked Dec 22 '18 at 9:37
Tob ErnackTob Ernack
2,279418
2,279418
$begingroup$
The construction is a little bit convoluted... You have to start from a formula of the basic language (and thus - as you said - without "added" constant $c_p$) and then add the new formula. As long as you have done this, you have generated a lot of new formulas (in the language extended with $c_p$) and thus you have to iterate the process.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 10:11
$begingroup$
I am not exactly sure where the iteration occurs. In Lemma 6.7 all the new formulas that are created after adding $c_P$ are either tautologies, quantifier axioms, or formulas of the type $R_P: negforall x P(x) implies neg P(c_P)$. None of these will generate new formulas of the form $negforall x P(x)$ to which we could apply the process again, except those that were already in $L$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:22
$begingroup$
I think there is some sort of iteration happening in Lemma 6.8 in order to make the set both complete and have sufficient alphabet, but that doesn't seem to be for the same reasons.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:24
$begingroup$
Maybe I would need to see a specific example of a case where you would need $c_P$ with rank $geq 2$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:29
$begingroup$
Maybe we can check on Henkin's original proof.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 11:39
|
show 4 more comments
$begingroup$
The construction is a little bit convoluted... You have to start from a formula of the basic language (and thus - as you said - without "added" constant $c_p$) and then add the new formula. As long as you have done this, you have generated a lot of new formulas (in the language extended with $c_p$) and thus you have to iterate the process.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 10:11
$begingroup$
I am not exactly sure where the iteration occurs. In Lemma 6.7 all the new formulas that are created after adding $c_P$ are either tautologies, quantifier axioms, or formulas of the type $R_P: negforall x P(x) implies neg P(c_P)$. None of these will generate new formulas of the form $negforall x P(x)$ to which we could apply the process again, except those that were already in $L$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:22
$begingroup$
I think there is some sort of iteration happening in Lemma 6.8 in order to make the set both complete and have sufficient alphabet, but that doesn't seem to be for the same reasons.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:24
$begingroup$
Maybe I would need to see a specific example of a case where you would need $c_P$ with rank $geq 2$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:29
$begingroup$
Maybe we can check on Henkin's original proof.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 11:39
$begingroup$
The construction is a little bit convoluted... You have to start from a formula of the basic language (and thus - as you said - without "added" constant $c_p$) and then add the new formula. As long as you have done this, you have generated a lot of new formulas (in the language extended with $c_p$) and thus you have to iterate the process.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 10:11
$begingroup$
The construction is a little bit convoluted... You have to start from a formula of the basic language (and thus - as you said - without "added" constant $c_p$) and then add the new formula. As long as you have done this, you have generated a lot of new formulas (in the language extended with $c_p$) and thus you have to iterate the process.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 10:11
$begingroup$
I am not exactly sure where the iteration occurs. In Lemma 6.7 all the new formulas that are created after adding $c_P$ are either tautologies, quantifier axioms, or formulas of the type $R_P: negforall x P(x) implies neg P(c_P)$. None of these will generate new formulas of the form $negforall x P(x)$ to which we could apply the process again, except those that were already in $L$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:22
$begingroup$
I am not exactly sure where the iteration occurs. In Lemma 6.7 all the new formulas that are created after adding $c_P$ are either tautologies, quantifier axioms, or formulas of the type $R_P: negforall x P(x) implies neg P(c_P)$. None of these will generate new formulas of the form $negforall x P(x)$ to which we could apply the process again, except those that were already in $L$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:22
$begingroup$
I think there is some sort of iteration happening in Lemma 6.8 in order to make the set both complete and have sufficient alphabet, but that doesn't seem to be for the same reasons.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:24
$begingroup$
I think there is some sort of iteration happening in Lemma 6.8 in order to make the set both complete and have sufficient alphabet, but that doesn't seem to be for the same reasons.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:24
$begingroup$
Maybe I would need to see a specific example of a case where you would need $c_P$ with rank $geq 2$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:29
$begingroup$
Maybe I would need to see a specific example of a case where you would need $c_P$ with rank $geq 2$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:29
$begingroup$
Maybe we can check on Henkin's original proof.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 11:39
$begingroup$
Maybe we can check on Henkin's original proof.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 11:39
|
show 4 more comments
0
active
oldest
votes
Your Answer
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3049250%2fvalidity-of-rank-construction-in-manins-proof-of-lemma-6-7-for-g%25c3%25b6dels-comple%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
0
active
oldest
votes
0
active
oldest
votes
active
oldest
votes
active
oldest
votes
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3049250%2fvalidity-of-rank-construction-in-manins-proof-of-lemma-6-7-for-g%25c3%25b6dels-comple%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
$begingroup$
The construction is a little bit convoluted... You have to start from a formula of the basic language (and thus - as you said - without "added" constant $c_p$) and then add the new formula. As long as you have done this, you have generated a lot of new formulas (in the language extended with $c_p$) and thus you have to iterate the process.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 10:11
$begingroup$
I am not exactly sure where the iteration occurs. In Lemma 6.7 all the new formulas that are created after adding $c_P$ are either tautologies, quantifier axioms, or formulas of the type $R_P: negforall x P(x) implies neg P(c_P)$. None of these will generate new formulas of the form $negforall x P(x)$ to which we could apply the process again, except those that were already in $L$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:22
$begingroup$
I think there is some sort of iteration happening in Lemma 6.8 in order to make the set both complete and have sufficient alphabet, but that doesn't seem to be for the same reasons.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:24
$begingroup$
Maybe I would need to see a specific example of a case where you would need $c_P$ with rank $geq 2$.
$endgroup$
– Tob Ernack
Dec 22 '18 at 10:29
$begingroup$
Maybe we can check on Henkin's original proof.
$endgroup$
– Mauro ALLEGRANZA
Dec 22 '18 at 11:39