Questions in proof theory (PRA-provability of EA-theorems, Girards book from '87)
I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there.
I would be glad if someone can help me with some of the exercises, clarify things when I can't work out the sense/meaning or help with the understanding of the proofs.
This is about the proof of theorem 1.4.7 (i).
It states: $PRA vdash Thm_{EA}[langle overline{9}, langle overline{5}, Num(x), Num (y) rangle, Num(x+y) rangle]$
I think I basically understood the overall frame of the argument, still I have many concerns though.
1) In the statement of the theorem, does he mean to prove it for any natural numbers x and y as metavariables, or are x and y intended to be formal variables available in the system? I would assume the latter, but then, what is $overline{x}$, $overline{x+y}$ etc. supposed to mean? The overline is a ${meta}$symbol to have an easier writing of numerals of the system, it is not available as a symbol ${in}$ the system.
He seems to mean something like "the numeral of the value that the term that could be placed here instead of the x represents", but what function would that be, and is it expressible ${in}$ the theory?
The overline occurs everywhere, the proof is full of it, it shouldn't be a simple typo..
Accordingly, I don't understand the paragraph on page 70 in between the two formal parts or the paragraph at the end of the proof, page 72, especially the occuring equalities.
For example: "...PRA proves that $ulcorner S overline{y} urcorner = ulcorner overline{Sy} urcorner$...i.e. $Num(Sy)=langle ulcorner S urcorner , Num(y) rangle$...
2) When beginning with the (sketch of the) formal proof of the induction step on page 71 he notes the hypothesis $lh(f(x,y))=l+overline{1}$.
Is this a formal hypothesis in PRA (he does not seem to use it formally), or just a meta-assumption?
If the former, then why is there no overline, (and is l a fixed value or a variable of the system)? If the latter, then why is there an overline on 1? If the function lh is prim. rec. shouldn't we be able to acutually compute the value of it, or anyway exactly represent it?
When he uses the projection function $(.)_i$ to list every derived formula, he writes the argument i as the sum of l and a numeral. Since this is a meta-usage - the formulas aren't really part of the system, they only denote a real formula - why is it written as numeral? He never wrote this argument as numeral before. If for some reason a numeral makes sense, why is there no overall bar, but just on the number, not on the l?
To prove his induction step, he doesn't seem to use his induction hypothesis $Pr_{EA}(ulcorner vdash overline{x}+overline{y}=overline{x+y} urcorner)$.
He writes "the proof is not complete, we must prove the endless atomic formulas". What does he mean? Aren't the formulas correctly derived?
Thanks for any help,
Regards,
Ettore
logic foundations proof-theory meta-math provability
asked Nov 29 at 12:23
Ettore
798
|
show 2 more comments
I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there.
I would be glad if someone can help me with some of the exercises, clarify things when I can't work out the sense/meaning or help with the understanding of the proofs.
This is about the proof of theorem 1.4.7 (i).
It states: $PRA vdash Thm_{EA}[langle overline{9}, langle overline{5}, Num(x), Num (y) rangle, Num(x+y) rangle]$
I think I basically understood the overall frame of the argument, still I have many concerns though.
1) In the statement of the theorem, does he mean to prove it for any natural numbers x and y as metavariables, or are x and y intended to be formal variables available in the system? I would assume the latter, but then, what is $overline{x}$, $overline{x+y}$ etc. supposed to mean? The overline is a ${meta}$symbol to have an easier writing of numerals of the system, it is not available as a symbol ${in}$ the system.
He seems to mean something like "the numeral of the value that the term that could be placed here instead of the x represents", but what function would that be, and is it expressible ${in}$ the theory?
The overline occurs everywhere, the proof is full of it, it shouldn't be a simple typo..
Accordingly, I don't understand the paragraph on page 70 in between the two formal parts or the paragraph at the end of the proof, page 72, especially the occuring equalities.
For example: "...PRA proves that $ulcorner S overline{y} urcorner = ulcorner overline{Sy} urcorner$...i.e. $Num(Sy)=langle ulcorner S urcorner , Num(y) rangle$...
2) When beginning with the (sketch of the) formal proof of the induction step on page 71 he notes the hypothesis $lh(f(x,y))=l+overline{1}$.
Is this a formal hypothesis in PRA (he does not seem to use it formally), or just a meta-assumption?
If the former, then why is there no overline, (and is l a fixed value or a variable of the system)? If the latter, then why is there an overline on 1? If the function lh is prim. rec. shouldn't we be able to acutually compute the value of it, or anyway exactly represent it?
When he uses the projection function $(.)_i$ to list every derived formula, he writes the argument i as the sum of l and a numeral. Since this is a meta-usage - the formulas aren't really part of the system, they only denote a real formula - why is it written as numeral? He never wrote this argument as numeral before. If for some reason a numeral makes sense, why is there no overall bar, but just on the number, not on the l?
To prove his induction step, he doesn't seem to use his induction hypothesis $Pr_{EA}(ulcorner vdash overline{x}+overline{y}=overline{x+y} urcorner)$.
He writes "the proof is not complete, we must prove the endless atomic formulas". What does he mean? Aren't the formulas correctly derived?
Thanks for any help,
Regards,
Ettore
logic foundations proof-theory meta-math provability
asked Nov 29 at 12:23
Ettore
798
Usually "overline(number)" is a numeral i.e. a term of the language of arithmetic used as name for a number. See page 66 : $overline 0$ is the term naming the number zero. Thus, when we write $overline 1$ we really mean $S overline 0$, and so on.
– Mauro ALLEGRANZA
Nov 29 at 12:30
Godel numbers are numbers that represent symbols and expressions of the language. In general, the G-number of the term $overline n$ is not the number $n$. See page 48 : $text {Num}(a)$ is the G-number of the $a$-th numeral. Thus $text {Num}(0)=1$ because the G-number of $overline 0$ is $1$ (see page 46).
– Mauro ALLEGRANZA
Nov 29 at 12:47
on the overline: Hi Mauro, thanks for your interest. I am familiar with the overline-symbol. But it only makes sense on numbers, as part of your metalanguage, as you yourself also explained, thus, it is not a part of the formal language, thus, x,y couldn't be variables of the system. I still have the impression thats what he means though, otherwise he would have used n and m I think.
– Ettore
Dec 1 at 10:30
on the gödel-numbering: Yes, that's the way I understood it. I think Num is prim.rec., hence expressible in the system formally, if I am right. But on which terms is it formally computable in the system? I guess on all closed terms. But anyway...in my questions above I tried to express other troubles...
– Ettore
Dec 1 at 10:33
Frankly speaking, what is not clear to me is [page 70] : "for trivial reasons $ulcorner overline 0 urcorner = ulcorner overline {overline 0} urcorner$ (i.e. $text {Num} (overline 0 ) = ulcorner overline 0 urcorner$)." The author defines [page 48] : $text {Num} (overline n ) = ulcorner overline n urcorner$. Thus, $text {Num} (overline 0 )=1$ and $text {Num} (overline 1 ) = text {Num} (S overline 0) = < 3, text {Num} (overline 0) > = 2^3 cdot 3^1=8 cdot 3=24$. But what does it mean $ ulcorner overline {overline 0} urcorner$ ?
– Mauro ALLEGRANZA
Dec 1 at 11:27
|
show 2 more comments
I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there.
I would be glad if someone can help me with some of the exercises, clarify things when I can't work out the sense/meaning or help with the understanding of the proofs.
This is about the proof of theorem 1.4.7 (i).
It states: $PRA vdash Thm_{EA}[langle overline{9}, langle overline{5}, Num(x), Num (y) rangle, Num(x+y) rangle]$
I think I basically understood the overall frame of the argument, still I have many concerns though.
1) In the statement of the theorem, does he mean to prove it for any natural numbers x and y as metavariables, or are x and y intended to be formal variables available in the system? I would assume the latter, but then, what is $overline{x}$, $overline{x+y}$ etc. supposed to mean? The overline is a ${meta}$symbol to have an easier writing of numerals of the system, it is not available as a symbol ${in}$ the system.
He seems to mean something like "the numeral of the value that the term that could be placed here instead of the x represents", but what function would that be, and is it expressible ${in}$ the theory?
The overline occurs everywhere, the proof is full of it, it shouldn't be a simple typo..
Accordingly, I don't understand the paragraph on page 70 in between the two formal parts or the paragraph at the end of the proof, page 72, especially the occuring equalities.
For example: "...PRA proves that $ulcorner S overline{y} urcorner = ulcorner overline{Sy} urcorner$...i.e. $Num(Sy)=langle ulcorner S urcorner , Num(y) rangle$...
2) When beginning with the (sketch of the) formal proof of the induction step on page 71 he notes the hypothesis $lh(f(x,y))=l+overline{1}$.
Is this a formal hypothesis in PRA (he does not seem to use it formally), or just a meta-assumption?
If the former, then why is there no overline, (and is l a fixed value or a variable of the system)? If the latter, then why is there an overline on 1? If the function lh is prim. rec. shouldn't we be able to acutually compute the value of it, or anyway exactly represent it?
When he uses the projection function $(.)_i$ to list every derived formula, he writes the argument i as the sum of l and a numeral. Since this is a meta-usage - the formulas aren't really part of the system, they only denote a real formula - why is it written as numeral? He never wrote this argument as numeral before. If for some reason a numeral makes sense, why is there no overall bar, but just on the number, not on the l?
To prove his induction step, he doesn't seem to use his induction hypothesis $Pr_{EA}(ulcorner vdash overline{x}+overline{y}=overline{x+y} urcorner)$.
He writes "the proof is not complete, we must prove the endless atomic formulas". What does he mean? Aren't the formulas correctly derived?
Thanks for any help,
Regards,
Ettore
logic foundations proof-theory meta-math provability
asked Nov 29 at 12:23
Ettore
798
I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there.
I would be glad if someone can help me with some of the exercises, clarify things when I can't work out the sense/meaning or help with the understanding of the proofs.
This is about the proof of theorem 1.4.7 (i).
It states: $PRA vdash Thm_{EA}[langle overline{9}, langle overline{5}, Num(x), Num (y) rangle, Num(x+y) rangle]$
I think I basically understood the overall frame of the argument, still I have many concerns though.
1) In the statement of the theorem, does he mean to prove it for any natural numbers x and y as metavariables, or are x and y intended to be formal variables available in the system? I would assume the latter, but then, what is $overline{x}$, $overline{x+y}$ etc. supposed to mean? The overline is a ${meta}$symbol to have an easier writing of numerals of the system, it is not available as a symbol ${in}$ the system.
He seems to mean something like "the numeral of the value that the term that could be placed here instead of the x represents", but what function would that be, and is it expressible ${in}$ the theory?
The overline occurs everywhere, the proof is full of it, it shouldn't be a simple typo..
Accordingly, I don't understand the paragraph on page 70 in between the two formal parts or the paragraph at the end of the proof, page 72, especially the occuring equalities.
For example: "...PRA proves that $ulcorner S overline{y} urcorner = ulcorner overline{Sy} urcorner$...i.e. $Num(Sy)=langle ulcorner S urcorner , Num(y) rangle$...
2) When beginning with the (sketch of the) formal proof of the induction step on page 71 he notes the hypothesis $lh(f(x,y))=l+overline{1}$.
Is this a formal hypothesis in PRA (he does not seem to use it formally), or just a meta-assumption?
If the former, then why is there no overline, (and is l a fixed value or a variable of the system)? If the latter, then why is there an overline on 1? If the function lh is prim. rec. shouldn't we be able to acutually compute the value of it, or anyway exactly represent it?
When he uses the projection function $(.)_i$ to list every derived formula, he writes the argument i as the sum of l and a numeral. Since this is a meta-usage - the formulas aren't really part of the system, they only denote a real formula - why is it written as numeral? He never wrote this argument as numeral before. If for some reason a numeral makes sense, why is there no overall bar, but just on the number, not on the l?
To prove his induction step, he doesn't seem to use his induction hypothesis $Pr_{EA}(ulcorner vdash overline{x}+overline{y}=overline{x+y} urcorner)$.
He writes "the proof is not complete, we must prove the endless atomic formulas". What does he mean? Aren't the formulas correctly derived?
Thanks for any help,
Regards,
Ettore
logic foundations proof-theory meta-math provability
logic foundations proof-theory meta-math provability
asked Nov 29 at 12:23
Ettore
798
asked Nov 29 at 12:23
Ettore
798
edited Dec 2 at 22:32
asked Nov 29 at 12:23
Ettore
798
asked Nov 29 at 12:23
Ettore
798
asked Nov 29 at 12:23
Ettore
798
798
Usually "overline(number)" is a numeral i.e. a term of the language of arithmetic used as name for a number. See page 66 : $overline 0$ is the term naming the number zero. Thus, when we write $overline 1$ we really mean $S overline 0$, and so on.
– Mauro ALLEGRANZA
Nov 29 at 12:30
Godel numbers are numbers that represent symbols and expressions of the language. In general, the G-number of the term $overline n$ is not the number $n$. See page 48 : $text {Num}(a)$ is the G-number of the $a$-th numeral. Thus $text {Num}(0)=1$ because the G-number of $overline 0$ is $1$ (see page 46).
– Mauro ALLEGRANZA
Nov 29 at 12:47
on the overline: Hi Mauro, thanks for your interest. I am familiar with the overline-symbol. But it only makes sense on numbers, as part of your metalanguage, as you yourself also explained, thus, it is not a part of the formal language, thus, x,y couldn't be variables of the system. I still have the impression thats what he means though, otherwise he would have used n and m I think.
– Ettore
Dec 1 at 10:30
on the gödel-numbering: Yes, that's the way I understood it. I think Num is prim.rec., hence expressible in the system formally, if I am right. But on which terms is it formally computable in the system? I guess on all closed terms. But anyway...in my questions above I tried to express other troubles...
– Ettore
Dec 1 at 10:33
Frankly speaking, what is not clear to me is [page 70] : "for trivial reasons $ulcorner overline 0 urcorner = ulcorner overline {overline 0} urcorner$ (i.e. $text {Num} (overline 0 ) = ulcorner overline 0 urcorner$)." The author defines [page 48] : $text {Num} (overline n ) = ulcorner overline n urcorner$. Thus, $text {Num} (overline 0 )=1$ and $text {Num} (overline 1 ) = text {Num} (S overline 0) = < 3, text {Num} (overline 0) > = 2^3 cdot 3^1=8 cdot 3=24$. But what does it mean $ ulcorner overline {overline 0} urcorner$ ?
– Mauro ALLEGRANZA
Dec 1 at 11:27
|
show 2 more comments
Usually "overline(number)" is a numeral i.e. a term of the language of arithmetic used as name for a number. See page 66 : $overline 0$ is the term naming the number zero. Thus, when we write $overline 1$ we really mean $S overline 0$, and so on.
– Mauro ALLEGRANZA
Nov 29 at 12:30
Godel numbers are numbers that represent symbols and expressions of the language. In general, the G-number of the term $overline n$ is not the number $n$. See page 48 : $text {Num}(a)$ is the G-number of the $a$-th numeral. Thus $text {Num}(0)=1$ because the G-number of $overline 0$ is $1$ (see page 46).
– Mauro ALLEGRANZA
Nov 29 at 12:47
on the overline: Hi Mauro, thanks for your interest. I am familiar with the overline-symbol. But it only makes sense on numbers, as part of your metalanguage, as you yourself also explained, thus, it is not a part of the formal language, thus, x,y couldn't be variables of the system. I still have the impression thats what he means though, otherwise he would have used n and m I think.
– Ettore
Dec 1 at 10:30
on the gödel-numbering: Yes, that's the way I understood it. I think Num is prim.rec., hence expressible in the system formally, if I am right. But on which terms is it formally computable in the system? I guess on all closed terms. But anyway...in my questions above I tried to express other troubles...
– Ettore
Dec 1 at 10:33
Frankly speaking, what is not clear to me is [page 70] : "for trivial reasons $ulcorner overline 0 urcorner = ulcorner overline {overline 0} urcorner$ (i.e. $text {Num} (overline 0 ) = ulcorner overline 0 urcorner$)." The author defines [page 48] : $text {Num} (overline n ) = ulcorner overline n urcorner$. Thus, $text {Num} (overline 0 )=1$ and $text {Num} (overline 1 ) = text {Num} (S overline 0) = < 3, text {Num} (overline 0) > = 2^3 cdot 3^1=8 cdot 3=24$. But what does it mean $ ulcorner overline {overline 0} urcorner$ ?
– Mauro ALLEGRANZA
Dec 1 at 11:27
Usually "overline(number)" is a numeral i.e. a term of the language of arithmetic used as name for a number. See page 66 : $overline 0$ is the term naming the number zero. Thus, when we write $overline 1$ we really mean $S overline 0$, and so on.
– Mauro ALLEGRANZA
Nov 29 at 12:30
Usually "overline(number)" is a numeral i.e. a term of the language of arithmetic used as name for a number. See page 66 : $overline 0$ is the term naming the number zero. Thus, when we write $overline 1$ we really mean $S overline 0$, and so on.
– Mauro ALLEGRANZA
Nov 29 at 12:30
Godel numbers are numbers that represent symbols and expressions of the language. In general, the G-number of the term $overline n$ is not the number $n$. See page 48 : $text {Num}(a)$ is the G-number of the $a$-th numeral. Thus $text {Num}(0)=1$ because the G-number of $overline 0$ is $1$ (see page 46).
– Mauro ALLEGRANZA
Nov 29 at 12:47
Godel numbers are numbers that represent symbols and expressions of the language. In general, the G-number of the term $overline n$ is not the number $n$. See page 48 : $text {Num}(a)$ is the G-number of the $a$-th numeral. Thus $text {Num}(0)=1$ because the G-number of $overline 0$ is $1$ (see page 46).
– Mauro ALLEGRANZA
Nov 29 at 12:47
on the overline: Hi Mauro, thanks for your interest. I am familiar with the overline-symbol. But it only makes sense on numbers, as part of your metalanguage, as you yourself also explained, thus, it is not a part of the formal language, thus, x,y couldn't be variables of the system. I still have the impression thats what he means though, otherwise he would have used n and m I think.
– Ettore
Dec 1 at 10:30
on the overline: Hi Mauro, thanks for your interest. I am familiar with the overline-symbol. But it only makes sense on numbers, as part of your metalanguage, as you yourself also explained, thus, it is not a part of the formal language, thus, x,y couldn't be variables of the system. I still have the impression thats what he means though, otherwise he would have used n and m I think.
– Ettore
Dec 1 at 10:30
on the gödel-numbering: Yes, that's the way I understood it. I think Num is prim.rec., hence expressible in the system formally, if I am right. But on which terms is it formally computable in the system? I guess on all closed terms. But anyway...in my questions above I tried to express other troubles...
– Ettore
Dec 1 at 10:33
on the gödel-numbering: Yes, that's the way I understood it. I think Num is prim.rec., hence expressible in the system formally, if I am right. But on which terms is it formally computable in the system? I guess on all closed terms. But anyway...in my questions above I tried to express other troubles...
– Ettore
Dec 1 at 10:33
Frankly speaking, what is not clear to me is [page 70] : "for trivial reasons $ulcorner overline 0 urcorner = ulcorner overline {overline 0} urcorner$ (i.e. $text {Num} (overline 0 ) = ulcorner overline 0 urcorner$)." The author defines [page 48] : $text {Num} (overline n ) = ulcorner overline n urcorner$. Thus, $text {Num} (overline 0 )=1$ and $text {Num} (overline 1 ) = text {Num} (S overline 0) = < 3, text {Num} (overline 0) > = 2^3 cdot 3^1=8 cdot 3=24$. But what does it mean $ ulcorner overline {overline 0} urcorner$ ?
– Mauro ALLEGRANZA
Dec 1 at 11:27
Frankly speaking, what is not clear to me is [page 70] : "for trivial reasons $ulcorner overline 0 urcorner = ulcorner overline {overline 0} urcorner$ (i.e. $text {Num} (overline 0 ) = ulcorner overline 0 urcorner$)." The author defines [page 48] : $text {Num} (overline n ) = ulcorner overline n urcorner$. Thus, $text {Num} (overline 0 )=1$ and $text {Num} (overline 1 ) = text {Num} (S overline 0) = < 3, text {Num} (overline 0) > = 2^3 cdot 3^1=8 cdot 3=24$. But what does it mean $ ulcorner overline {overline 0} urcorner$ ?
– Mauro ALLEGRANZA
Dec 1 at 11:27
|
show 2 more comments
active
oldest
votes
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3018554%2fquestions-in-proof-theory-pra-provability-of-ea-theorems-girards-book-from-87%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
active
oldest
votes
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.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- 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.
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%2f3018554%2fquestions-in-proof-theory-pra-provability-of-ea-theorems-girards-book-from-87%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
Usually "overline(number)" is a numeral i.e. a term of the language of arithmetic used as name for a number. See page 66 : $overline 0$ is the term naming the number zero. Thus, when we write $overline 1$ we really mean $S overline 0$, and so on.
– Mauro ALLEGRANZA
Nov 29 at 12:30
Godel numbers are numbers that represent symbols and expressions of the language. In general, the G-number of the term $overline n$ is not the number $n$. See page 48 : $text {Num}(a)$ is the G-number of the $a$-th numeral. Thus $text {Num}(0)=1$ because the G-number of $overline 0$ is $1$ (see page 46).
– Mauro ALLEGRANZA
Nov 29 at 12:47
on the overline: Hi Mauro, thanks for your interest. I am familiar with the overline-symbol. But it only makes sense on numbers, as part of your metalanguage, as you yourself also explained, thus, it is not a part of the formal language, thus, x,y couldn't be variables of the system. I still have the impression thats what he means though, otherwise he would have used n and m I think.
– Ettore
Dec 1 at 10:30
on the gödel-numbering: Yes, that's the way I understood it. I think Num is prim.rec., hence expressible in the system formally, if I am right. But on which terms is it formally computable in the system? I guess on all closed terms. But anyway...in my questions above I tried to express other troubles...
– Ettore
Dec 1 at 10:33
Frankly speaking, what is not clear to me is [page 70] : "for trivial reasons $ulcorner overline 0 urcorner = ulcorner overline {overline 0} urcorner$ (i.e. $text {Num} (overline 0 ) = ulcorner overline 0 urcorner$)." The author defines [page 48] : $text {Num} (overline n ) = ulcorner overline n urcorner$. Thus, $text {Num} (overline 0 )=1$ and $text {Num} (overline 1 ) = text {Num} (S overline 0) = < 3, text {Num} (overline 0) > = 2^3 cdot 3^1=8 cdot 3=24$. But what does it mean $ ulcorner overline {overline 0} urcorner$ ?
– Mauro ALLEGRANZA
Dec 1 at 11:27