Mixing
Proof predicate in PA and stronger system
Clash Royale CLAN TAG#URR8PPP
up vote
0
down vote
favorite
It is said that proof predicate of PA is primitive recursive, but I cannot find explicit form of the proof predicate, or how it is defined. What is this proof predicate? What about defining for other theories stronger than PA?
logic peano-axioms provability
edited Jul 20 at 11:39
Andrés E. Caicedo
63.2k7151235
asked Jul 20 at 3:50
Mullock Brian
204
add a comment |Â
up vote
0
down vote
favorite
It is said that proof predicate of PA is primitive recursive, but I cannot find explicit form of the proof predicate, or how it is defined. What is this proof predicate? What about defining for other theories stronger than PA?
logic peano-axioms provability
edited Jul 20 at 11:39
Andrés E. Caicedo
63.2k7151235
asked Jul 20 at 3:50
Mullock Brian
204
add a comment |Â
up vote
0
down vote
favorite
up vote
0
down vote
favorite
It is said that proof predicate of PA is primitive recursive, but I cannot find explicit form of the proof predicate, or how it is defined. What is this proof predicate? What about defining for other theories stronger than PA?
logic peano-axioms provability
edited Jul 20 at 11:39
Andrés E. Caicedo
63.2k7151235
asked Jul 20 at 3:50
Mullock Brian
204
It is said that proof predicate of PA is primitive recursive, but I cannot find explicit form of the proof predicate, or how it is defined. What is this proof predicate? What about defining for other theories stronger than PA?
logic peano-axioms provability
edited Jul 20 at 11:39
Andrés E. Caicedo
63.2k7151235
asked Jul 20 at 3:50
Mullock Brian
204
edited Jul 20 at 11:39
Andrés E. Caicedo
63.2k7151235
edited Jul 20 at 11:39
Andrés E. Caicedo
63.2k7151235
edited Jul 20 at 11:39
Andrés E. Caicedo
63.2k7151235
63.2k7151235
asked Jul 20 at 3:50
Mullock Brian
204
asked Jul 20 at 3:50
Mullock Brian
204
asked Jul 20 at 3:50
Mullock Brian
204
204
add a comment |Â
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
1
down vote
accepted
A proof predicate is a fairly complicated arithmetical formula, and although its definition is completely constructive, it is a bit tedious. I recommend you consult a textbook on the incompleteness theorems (Smith and Smullyan are both very good).
In brief, given a formal language and an effective deductive system, we can encode statements and proofs by numbers, just with a simple translation of the syntax. A proof predicate $P(m,n)$ is an arithmetic formula expressing the fact $m$ encodes a proof of the statement encoded by $n.$ Computing this predicate only requires you to translate the Gödel numbers and then check that the proof uses axioms and rules of inference correctly and has the correct conclusion. Intuitively, this can be done with a computer program, moreover one that only uses ‘for loops’, no ‘while loops,’ so it is a primitive recursive predicate. This implies that it can be expressed by an arithmetic formula (in fact one that only has bounded quatifiers)... essentially we just turn the computer program above into some combination of addition, multiplication and logic. Note that there are many ways to implement the above procedure, so many different possible proof predicates.
Also note that I have said precisely nothing about PA so far. I just said a formal language and an effective deductive system. The only important thing was that formal proofs could be checked by an algorithm. So axiomatic systems where there is an effective way to check if a statement is an axiom and if a statement follows from another by a rule of inference qualify. In particular PA does. Also any axiomatizable extension of PA does: it’s just a matter of adding some additional axiom schemes for the program to check against. So yes, stronger systems can have a proof predicate. In fact ZFC (which is in a different language but much stronger in a precise sense) has a proof predicate as well, since at the end of the day it’s just a recursive set of axioms with first order logic as a deductive system, just like PA.
answered Jul 20 at 18:06
spaceisdarkgreen
27.5k21547
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
accepted
A proof predicate is a fairly complicated arithmetical formula, and although its definition is completely constructive, it is a bit tedious. I recommend you consult a textbook on the incompleteness theorems (Smith and Smullyan are both very good).
In brief, given a formal language and an effective deductive system, we can encode statements and proofs by numbers, just with a simple translation of the syntax. A proof predicate $P(m,n)$ is an arithmetic formula expressing the fact $m$ encodes a proof of the statement encoded by $n.$ Computing this predicate only requires you to translate the Gödel numbers and then check that the proof uses axioms and rules of inference correctly and has the correct conclusion. Intuitively, this can be done with a computer program, moreover one that only uses ‘for loops’, no ‘while loops,’ so it is a primitive recursive predicate. This implies that it can be expressed by an arithmetic formula (in fact one that only has bounded quatifiers)... essentially we just turn the computer program above into some combination of addition, multiplication and logic. Note that there are many ways to implement the above procedure, so many different possible proof predicates.
Also note that I have said precisely nothing about PA so far. I just said a formal language and an effective deductive system. The only important thing was that formal proofs could be checked by an algorithm. So axiomatic systems where there is an effective way to check if a statement is an axiom and if a statement follows from another by a rule of inference qualify. In particular PA does. Also any axiomatizable extension of PA does: it’s just a matter of adding some additional axiom schemes for the program to check against. So yes, stronger systems can have a proof predicate. In fact ZFC (which is in a different language but much stronger in a precise sense) has a proof predicate as well, since at the end of the day it’s just a recursive set of axioms with first order logic as a deductive system, just like PA.
answered Jul 20 at 18:06
spaceisdarkgreen
27.5k21547
add a comment |Â
up vote
1
down vote
accepted
A proof predicate is a fairly complicated arithmetical formula, and although its definition is completely constructive, it is a bit tedious. I recommend you consult a textbook on the incompleteness theorems (Smith and Smullyan are both very good).
In brief, given a formal language and an effective deductive system, we can encode statements and proofs by numbers, just with a simple translation of the syntax. A proof predicate $P(m,n)$ is an arithmetic formula expressing the fact $m$ encodes a proof of the statement encoded by $n.$ Computing this predicate only requires you to translate the Gödel numbers and then check that the proof uses axioms and rules of inference correctly and has the correct conclusion. Intuitively, this can be done with a computer program, moreover one that only uses ‘for loops’, no ‘while loops,’ so it is a primitive recursive predicate. This implies that it can be expressed by an arithmetic formula (in fact one that only has bounded quatifiers)... essentially we just turn the computer program above into some combination of addition, multiplication and logic. Note that there are many ways to implement the above procedure, so many different possible proof predicates.
Also note that I have said precisely nothing about PA so far. I just said a formal language and an effective deductive system. The only important thing was that formal proofs could be checked by an algorithm. So axiomatic systems where there is an effective way to check if a statement is an axiom and if a statement follows from another by a rule of inference qualify. In particular PA does. Also any axiomatizable extension of PA does: it’s just a matter of adding some additional axiom schemes for the program to check against. So yes, stronger systems can have a proof predicate. In fact ZFC (which is in a different language but much stronger in a precise sense) has a proof predicate as well, since at the end of the day it’s just a recursive set of axioms with first order logic as a deductive system, just like PA.
answered Jul 20 at 18:06
spaceisdarkgreen
27.5k21547
add a comment |Â
up vote
1
down vote
accepted
up vote
1
down vote
accepted
A proof predicate is a fairly complicated arithmetical formula, and although its definition is completely constructive, it is a bit tedious. I recommend you consult a textbook on the incompleteness theorems (Smith and Smullyan are both very good).
In brief, given a formal language and an effective deductive system, we can encode statements and proofs by numbers, just with a simple translation of the syntax. A proof predicate $P(m,n)$ is an arithmetic formula expressing the fact $m$ encodes a proof of the statement encoded by $n.$ Computing this predicate only requires you to translate the Gödel numbers and then check that the proof uses axioms and rules of inference correctly and has the correct conclusion. Intuitively, this can be done with a computer program, moreover one that only uses ‘for loops’, no ‘while loops,’ so it is a primitive recursive predicate. This implies that it can be expressed by an arithmetic formula (in fact one that only has bounded quatifiers)... essentially we just turn the computer program above into some combination of addition, multiplication and logic. Note that there are many ways to implement the above procedure, so many different possible proof predicates.
Also note that I have said precisely nothing about PA so far. I just said a formal language and an effective deductive system. The only important thing was that formal proofs could be checked by an algorithm. So axiomatic systems where there is an effective way to check if a statement is an axiom and if a statement follows from another by a rule of inference qualify. In particular PA does. Also any axiomatizable extension of PA does: it’s just a matter of adding some additional axiom schemes for the program to check against. So yes, stronger systems can have a proof predicate. In fact ZFC (which is in a different language but much stronger in a precise sense) has a proof predicate as well, since at the end of the day it’s just a recursive set of axioms with first order logic as a deductive system, just like PA.
answered Jul 20 at 18:06
spaceisdarkgreen
27.5k21547
A proof predicate is a fairly complicated arithmetical formula, and although its definition is completely constructive, it is a bit tedious. I recommend you consult a textbook on the incompleteness theorems (Smith and Smullyan are both very good).
In brief, given a formal language and an effective deductive system, we can encode statements and proofs by numbers, just with a simple translation of the syntax. A proof predicate $P(m,n)$ is an arithmetic formula expressing the fact $m$ encodes a proof of the statement encoded by $n.$ Computing this predicate only requires you to translate the Gödel numbers and then check that the proof uses axioms and rules of inference correctly and has the correct conclusion. Intuitively, this can be done with a computer program, moreover one that only uses ‘for loops’, no ‘while loops,’ so it is a primitive recursive predicate. This implies that it can be expressed by an arithmetic formula (in fact one that only has bounded quatifiers)... essentially we just turn the computer program above into some combination of addition, multiplication and logic. Note that there are many ways to implement the above procedure, so many different possible proof predicates.
Also note that I have said precisely nothing about PA so far. I just said a formal language and an effective deductive system. The only important thing was that formal proofs could be checked by an algorithm. So axiomatic systems where there is an effective way to check if a statement is an axiom and if a statement follows from another by a rule of inference qualify. In particular PA does. Also any axiomatizable extension of PA does: it’s just a matter of adding some additional axiom schemes for the program to check against. So yes, stronger systems can have a proof predicate. In fact ZFC (which is in a different language but much stronger in a precise sense) has a proof predicate as well, since at the end of the day it’s just a recursive set of axioms with first order logic as a deductive system, just like PA.
answered Jul 20 at 18:06
spaceisdarkgreen
27.5k21547
answered Jul 20 at 18:06
spaceisdarkgreen
27.5k21547
answered Jul 20 at 18:06
spaceisdarkgreen
27.5k21547
answered Jul 20 at 18:06
spaceisdarkgreen
27.5k21547
27.5k21547
add a comment |Â
add a comment |Â
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
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2857256%2fproof-predicate-in-pa-and-stronger-system%23new-answer', 'question_page');
);
Post as a guest
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
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
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