Questions in proof theory (PRA-provability of an EA-axiom, Girards Book from '87)
$begingroup$
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.
On page 67 there are exercises 1.4.4.
Part one is to show that some axioms of EA (presented on page 53) are provable in PRA. I can't do it with axiom (xv), the others were no problem. Still I think it's probably not difficult.
I also don't know even how to start with part two.
Thanks for your help.
Regards,
Ettore
PS: I can't find online a similar axiomatization of PRA like in the book, also I would have to describe the predicate calculus in the style of the book and maybe quote a number of theorems. Thats why I can't provide more details here and refer only to scholars using the book. Sorry about that.
PPS: However...axiom (xv) is $x<y lor x=y lor y<x$.
You can see what PRA is about for example here: https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic
Many logic textbooks may have some axiomatization of it as well.
Part two of the exercise is to show that for each quantifier-free formula $A$ (with free variables among $x_1, .., x_n$) in the language of PRA there is an n-ary predicate letter $p$ in the language of PRA such that
$PRA vdash p (x_1, ..., x_n) leftrightarrow A[x_1, ... x_n] $ .
It might work somehow with induction on the construction of the formulas.
PPPS:
In fact, induction on the construction of the formulas seems to work. I figured a sketch to myself yesterday evening, some details are still unclear to me.
The key is that essentially all formulas are predicates with (propositional) connectives between them.
Hence, for the base case, A being a predicate, you already have the predicate, namely the predicate that is A.
Then, for example, for the conjunction of two formulas one can take the sum of the characteristic functions of the two predicates of the two formulas. For this sum, being a function, one has by definition a predicate, and this predicate suffices for the formula that is the conjunction of the former two formulas.
And so on for other connectives...
The part that is not really doubious, but still in detail not clear to me is the formal system can not only express the sum of two functions but also prove that it is 0 if and only if the other two functions are zero. Similarly it's not fully clear to me how to prove basic properties of the other necessary constructed functions that express some connection of formulas.
logic foundations proof-theory provability
asked Nov 28 '18 at 16:32
EttoreEttore
989
$endgroup$
|
show 1 more comment
$begingroup$
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.
On page 67 there are exercises 1.4.4.
Part one is to show that some axioms of EA (presented on page 53) are provable in PRA. I can't do it with axiom (xv), the others were no problem. Still I think it's probably not difficult.
I also don't know even how to start with part two.
Thanks for your help.
Regards,
Ettore
PS: I can't find online a similar axiomatization of PRA like in the book, also I would have to describe the predicate calculus in the style of the book and maybe quote a number of theorems. Thats why I can't provide more details here and refer only to scholars using the book. Sorry about that.
PPS: However...axiom (xv) is $x<y lor x=y lor y<x$.
You can see what PRA is about for example here: https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic
Many logic textbooks may have some axiomatization of it as well.
Part two of the exercise is to show that for each quantifier-free formula $A$ (with free variables among $x_1, .., x_n$) in the language of PRA there is an n-ary predicate letter $p$ in the language of PRA such that
$PRA vdash p (x_1, ..., x_n) leftrightarrow A[x_1, ... x_n] $ .
It might work somehow with induction on the construction of the formulas.
PPPS:
In fact, induction on the construction of the formulas seems to work. I figured a sketch to myself yesterday evening, some details are still unclear to me.
The key is that essentially all formulas are predicates with (propositional) connectives between them.
Hence, for the base case, A being a predicate, you already have the predicate, namely the predicate that is A.
Then, for example, for the conjunction of two formulas one can take the sum of the characteristic functions of the two predicates of the two formulas. For this sum, being a function, one has by definition a predicate, and this predicate suffices for the formula that is the conjunction of the former two formulas.
And so on for other connectives...
The part that is not really doubious, but still in detail not clear to me is the formal system can not only express the sum of two functions but also prove that it is 0 if and only if the other two functions are zero. Similarly it's not fully clear to me how to prove basic properties of the other necessary constructed functions that express some connection of formulas.
logic foundations proof-theory provability
asked Nov 28 '18 at 16:32
EttoreEttore
989
$endgroup$
2
$begingroup$
Can’t you reproduce enough information here that someone could help without having the book in front of them? It looks like the bulk of your question is showing a single axiom is provable in PRA.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 16:50
$begingroup$
You're right, I am sorry, yes I need you to have the book. It would really take a very long time formulating everything necessary in latex here, like a big chunk of the book, thats to much...
$endgroup$
– Ettore
Nov 28 '18 at 17:01
1
$begingroup$
I really don’t see how all that much is necessary to ask if a single axiom is provable in PRA (can’t you write down the axiom?) but if you think the answerer needs the book, then that’s fine, I’m sure someone has it.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 17:14
$begingroup$
@Ettore: You will be much more likely to get answers if you try to make the question more self-contained. Of course it’s impossible to include all the background, but it’s usually possible to make the question self-contained enough that people can start thinking about it without needing the reference. imagine you’re writing for, say, someone who read the book a few years ago, and remembers the general mathematical content but not the exact theorem numbering.
$endgroup$
– Peter LeFanu Lumsdaine
Dec 1 '18 at 15:03
$begingroup$
Thanks again, Peter. Makes sense..I think I'll give it a try..
$endgroup$
– Ettore
Dec 2 '18 at 21:51
|
show 1 more comment
$begingroup$
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.
On page 67 there are exercises 1.4.4.
Part one is to show that some axioms of EA (presented on page 53) are provable in PRA. I can't do it with axiom (xv), the others were no problem. Still I think it's probably not difficult.
I also don't know even how to start with part two.
Thanks for your help.
Regards,
Ettore
PS: I can't find online a similar axiomatization of PRA like in the book, also I would have to describe the predicate calculus in the style of the book and maybe quote a number of theorems. Thats why I can't provide more details here and refer only to scholars using the book. Sorry about that.
PPS: However...axiom (xv) is $x<y lor x=y lor y<x$.
You can see what PRA is about for example here: https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic
Many logic textbooks may have some axiomatization of it as well.
Part two of the exercise is to show that for each quantifier-free formula $A$ (with free variables among $x_1, .., x_n$) in the language of PRA there is an n-ary predicate letter $p$ in the language of PRA such that
$PRA vdash p (x_1, ..., x_n) leftrightarrow A[x_1, ... x_n] $ .
It might work somehow with induction on the construction of the formulas.
PPPS:
In fact, induction on the construction of the formulas seems to work. I figured a sketch to myself yesterday evening, some details are still unclear to me.
The key is that essentially all formulas are predicates with (propositional) connectives between them.
Hence, for the base case, A being a predicate, you already have the predicate, namely the predicate that is A.
Then, for example, for the conjunction of two formulas one can take the sum of the characteristic functions of the two predicates of the two formulas. For this sum, being a function, one has by definition a predicate, and this predicate suffices for the formula that is the conjunction of the former two formulas.
And so on for other connectives...
The part that is not really doubious, but still in detail not clear to me is the formal system can not only express the sum of two functions but also prove that it is 0 if and only if the other two functions are zero. Similarly it's not fully clear to me how to prove basic properties of the other necessary constructed functions that express some connection of formulas.
logic foundations proof-theory provability
asked Nov 28 '18 at 16:32
EttoreEttore
989
$endgroup$
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.
On page 67 there are exercises 1.4.4.
Part one is to show that some axioms of EA (presented on page 53) are provable in PRA. I can't do it with axiom (xv), the others were no problem. Still I think it's probably not difficult.
I also don't know even how to start with part two.
Thanks for your help.
Regards,
Ettore
PS: I can't find online a similar axiomatization of PRA like in the book, also I would have to describe the predicate calculus in the style of the book and maybe quote a number of theorems. Thats why I can't provide more details here and refer only to scholars using the book. Sorry about that.
PPS: However...axiom (xv) is $x<y lor x=y lor y<x$.
You can see what PRA is about for example here: https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic
Many logic textbooks may have some axiomatization of it as well.
Part two of the exercise is to show that for each quantifier-free formula $A$ (with free variables among $x_1, .., x_n$) in the language of PRA there is an n-ary predicate letter $p$ in the language of PRA such that
$PRA vdash p (x_1, ..., x_n) leftrightarrow A[x_1, ... x_n] $ .
It might work somehow with induction on the construction of the formulas.
PPPS:
In fact, induction on the construction of the formulas seems to work. I figured a sketch to myself yesterday evening, some details are still unclear to me.
The key is that essentially all formulas are predicates with (propositional) connectives between them.
Hence, for the base case, A being a predicate, you already have the predicate, namely the predicate that is A.
Then, for example, for the conjunction of two formulas one can take the sum of the characteristic functions of the two predicates of the two formulas. For this sum, being a function, one has by definition a predicate, and this predicate suffices for the formula that is the conjunction of the former two formulas.
And so on for other connectives...
The part that is not really doubious, but still in detail not clear to me is the formal system can not only express the sum of two functions but also prove that it is 0 if and only if the other two functions are zero. Similarly it's not fully clear to me how to prove basic properties of the other necessary constructed functions that express some connection of formulas.
logic foundations proof-theory provability
logic foundations proof-theory provability
asked Nov 28 '18 at 16:32
EttoreEttore
989
asked Nov 28 '18 at 16:32
EttoreEttore
989
edited Dec 4 '18 at 12:33
Ettore
asked Nov 28 '18 at 16:32
EttoreEttore
989
asked Nov 28 '18 at 16:32
EttoreEttore
989
asked Nov 28 '18 at 16:32
EttoreEttore
989
989
2
$begingroup$
Can’t you reproduce enough information here that someone could help without having the book in front of them? It looks like the bulk of your question is showing a single axiom is provable in PRA.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 16:50
$begingroup$
You're right, I am sorry, yes I need you to have the book. It would really take a very long time formulating everything necessary in latex here, like a big chunk of the book, thats to much...
$endgroup$
– Ettore
Nov 28 '18 at 17:01
1
$begingroup$
I really don’t see how all that much is necessary to ask if a single axiom is provable in PRA (can’t you write down the axiom?) but if you think the answerer needs the book, then that’s fine, I’m sure someone has it.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 17:14
$begingroup$
@Ettore: You will be much more likely to get answers if you try to make the question more self-contained. Of course it’s impossible to include all the background, but it’s usually possible to make the question self-contained enough that people can start thinking about it without needing the reference. imagine you’re writing for, say, someone who read the book a few years ago, and remembers the general mathematical content but not the exact theorem numbering.
$endgroup$
– Peter LeFanu Lumsdaine
Dec 1 '18 at 15:03
$begingroup$
Thanks again, Peter. Makes sense..I think I'll give it a try..
$endgroup$
– Ettore
Dec 2 '18 at 21:51
|
show 1 more comment
2
$begingroup$
Can’t you reproduce enough information here that someone could help without having the book in front of them? It looks like the bulk of your question is showing a single axiom is provable in PRA.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 16:50
$begingroup$
You're right, I am sorry, yes I need you to have the book. It would really take a very long time formulating everything necessary in latex here, like a big chunk of the book, thats to much...
$endgroup$
– Ettore
Nov 28 '18 at 17:01
1
$begingroup$
I really don’t see how all that much is necessary to ask if a single axiom is provable in PRA (can’t you write down the axiom?) but if you think the answerer needs the book, then that’s fine, I’m sure someone has it.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 17:14
$begingroup$
@Ettore: You will be much more likely to get answers if you try to make the question more self-contained. Of course it’s impossible to include all the background, but it’s usually possible to make the question self-contained enough that people can start thinking about it without needing the reference. imagine you’re writing for, say, someone who read the book a few years ago, and remembers the general mathematical content but not the exact theorem numbering.
$endgroup$
– Peter LeFanu Lumsdaine
Dec 1 '18 at 15:03
$begingroup$
Thanks again, Peter. Makes sense..I think I'll give it a try..
$endgroup$
– Ettore
Dec 2 '18 at 21:51
2
2
$begingroup$
Can’t you reproduce enough information here that someone could help without having the book in front of them? It looks like the bulk of your question is showing a single axiom is provable in PRA.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 16:50
$begingroup$
Can’t you reproduce enough information here that someone could help without having the book in front of them? It looks like the bulk of your question is showing a single axiom is provable in PRA.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 16:50
$begingroup$
You're right, I am sorry, yes I need you to have the book. It would really take a very long time formulating everything necessary in latex here, like a big chunk of the book, thats to much...
$endgroup$
– Ettore
Nov 28 '18 at 17:01
$begingroup$
You're right, I am sorry, yes I need you to have the book. It would really take a very long time formulating everything necessary in latex here, like a big chunk of the book, thats to much...
$endgroup$
– Ettore
Nov 28 '18 at 17:01
1
1
$begingroup$
I really don’t see how all that much is necessary to ask if a single axiom is provable in PRA (can’t you write down the axiom?) but if you think the answerer needs the book, then that’s fine, I’m sure someone has it.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 17:14
$begingroup$
I really don’t see how all that much is necessary to ask if a single axiom is provable in PRA (can’t you write down the axiom?) but if you think the answerer needs the book, then that’s fine, I’m sure someone has it.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 17:14
$begingroup$
@Ettore: You will be much more likely to get answers if you try to make the question more self-contained. Of course it’s impossible to include all the background, but it’s usually possible to make the question self-contained enough that people can start thinking about it without needing the reference. imagine you’re writing for, say, someone who read the book a few years ago, and remembers the general mathematical content but not the exact theorem numbering.
$endgroup$
– Peter LeFanu Lumsdaine
Dec 1 '18 at 15:03
$begingroup$
@Ettore: You will be much more likely to get answers if you try to make the question more self-contained. Of course it’s impossible to include all the background, but it’s usually possible to make the question self-contained enough that people can start thinking about it without needing the reference. imagine you’re writing for, say, someone who read the book a few years ago, and remembers the general mathematical content but not the exact theorem numbering.
$endgroup$
– Peter LeFanu Lumsdaine
Dec 1 '18 at 15:03
$begingroup$
Thanks again, Peter. Makes sense..I think I'll give it a try..
$endgroup$
– Ettore
Dec 2 '18 at 21:51
$begingroup$
Thanks again, Peter. Makes sense..I think I'll give it a try..
$endgroup$
– Ettore
Dec 2 '18 at 21:51
|
show 1 more comment
0
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%2f3017346%2fquestions-in-proof-theory-pra-provability-of-an-ea-axiom-girards-book-from-87%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%2f3017346%2fquestions-in-proof-theory-pra-provability-of-an-ea-axiom-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
2
$begingroup$
Can’t you reproduce enough information here that someone could help without having the book in front of them? It looks like the bulk of your question is showing a single axiom is provable in PRA.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 16:50
$begingroup$
You're right, I am sorry, yes I need you to have the book. It would really take a very long time formulating everything necessary in latex here, like a big chunk of the book, thats to much...
$endgroup$
– Ettore
Nov 28 '18 at 17:01
1
$begingroup$
I really don’t see how all that much is necessary to ask if a single axiom is provable in PRA (can’t you write down the axiom?) but if you think the answerer needs the book, then that’s fine, I’m sure someone has it.
$endgroup$
– spaceisdarkgreen
Nov 28 '18 at 17:14
$begingroup$
@Ettore: You will be much more likely to get answers if you try to make the question more self-contained. Of course it’s impossible to include all the background, but it’s usually possible to make the question self-contained enough that people can start thinking about it without needing the reference. imagine you’re writing for, say, someone who read the book a few years ago, and remembers the general mathematical content but not the exact theorem numbering.
$endgroup$
– Peter LeFanu Lumsdaine
Dec 1 '18 at 15:03
$begingroup$
Thanks again, Peter. Makes sense..I think I'll give it a try..
$endgroup$
– Ettore
Dec 2 '18 at 21:51