Mixing
Would a proof predicate change if a stronger system used despite sharing language?
Clash Royale CLAN TAG#URR8PPP
up vote
1
down vote
favorite
This is a follow-up question from Proof predicate in PA and stronger system
Suppose that two theories $T_1$ and $T_2$ share the same language - thus only axioms differ such that $T_2$ is a stronger theory relative to $T_1$.
Do/can $T_1$ and $T_2$ share the same proof predicate $Proof(x,y)$ where $x$ is Godel encoding of proof of Godel decoding of $y$? If not, why would it be? From my understanding, $Proof$ predicate is really about decoding $x$ and $y$, demonstrating that $x$ follows the right rule of inference or deduction and arriving at Godel decoding of $y$. And adding axioms does not necessarily change rule of inference or deduction. Thus, it seems that proof predicate does not have to change.
logic peano-axioms provability
asked Jul 21 at 1:00
Mullock Brian
204
add a comment |Â
up vote
1
down vote
favorite
This is a follow-up question from Proof predicate in PA and stronger system
Suppose that two theories $T_1$ and $T_2$ share the same language - thus only axioms differ such that $T_2$ is a stronger theory relative to $T_1$.
Do/can $T_1$ and $T_2$ share the same proof predicate $Proof(x,y)$ where $x$ is Godel encoding of proof of Godel decoding of $y$? If not, why would it be? From my understanding, $Proof$ predicate is really about decoding $x$ and $y$, demonstrating that $x$ follows the right rule of inference or deduction and arriving at Godel decoding of $y$. And adding axioms does not necessarily change rule of inference or deduction. Thus, it seems that proof predicate does not have to change.
logic peano-axioms provability
asked Jul 21 at 1:00
Mullock Brian
204
2
Yes it does change. Verifying a proof involves checking if certain statements are axioms or not. Thus if the axioms change, the verification procedure the proof predicate encodes changes, so the proof predicate changes.
– spaceisdarkgreen
Jul 21 at 1:26
add a comment |Â
up vote
1
down vote
favorite
up vote
1
down vote
favorite
This is a follow-up question from Proof predicate in PA and stronger system
Suppose that two theories $T_1$ and $T_2$ share the same language - thus only axioms differ such that $T_2$ is a stronger theory relative to $T_1$.
Do/can $T_1$ and $T_2$ share the same proof predicate $Proof(x,y)$ where $x$ is Godel encoding of proof of Godel decoding of $y$? If not, why would it be? From my understanding, $Proof$ predicate is really about decoding $x$ and $y$, demonstrating that $x$ follows the right rule of inference or deduction and arriving at Godel decoding of $y$. And adding axioms does not necessarily change rule of inference or deduction. Thus, it seems that proof predicate does not have to change.
logic peano-axioms provability
asked Jul 21 at 1:00
Mullock Brian
204
This is a follow-up question from Proof predicate in PA and stronger system
Suppose that two theories $T_1$ and $T_2$ share the same language - thus only axioms differ such that $T_2$ is a stronger theory relative to $T_1$.
Do/can $T_1$ and $T_2$ share the same proof predicate $Proof(x,y)$ where $x$ is Godel encoding of proof of Godel decoding of $y$? If not, why would it be? From my understanding, $Proof$ predicate is really about decoding $x$ and $y$, demonstrating that $x$ follows the right rule of inference or deduction and arriving at Godel decoding of $y$. And adding axioms does not necessarily change rule of inference or deduction. Thus, it seems that proof predicate does not have to change.
logic peano-axioms provability
asked Jul 21 at 1:00
Mullock Brian
204
asked Jul 21 at 1:00
Mullock Brian
204
asked Jul 21 at 1:00
Mullock Brian
204
asked Jul 21 at 1:00
Mullock Brian
204
204
2
Yes it does change. Verifying a proof involves checking if certain statements are axioms or not. Thus if the axioms change, the verification procedure the proof predicate encodes changes, so the proof predicate changes.
– spaceisdarkgreen
Jul 21 at 1:26
add a comment |Â
2
Yes it does change. Verifying a proof involves checking if certain statements are axioms or not. Thus if the axioms change, the verification procedure the proof predicate encodes changes, so the proof predicate changes.
– spaceisdarkgreen
Jul 21 at 1:26
2
2
Yes it does change. Verifying a proof involves checking if certain statements are axioms or not. Thus if the axioms change, the verification procedure the proof predicate encodes changes, so the proof predicate changes.
– spaceisdarkgreen
Jul 21 at 1:26
Yes it does change. Verifying a proof involves checking if certain statements are axioms or not. Thus if the axioms change, the verification procedure the proof predicate encodes changes, so the proof predicate changes.
– spaceisdarkgreen
Jul 21 at 1:26
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
2
down vote
You've argued that the non-"initial" steps in a proof don't depend on the ambient theory, but we also have to consider the "initial" steps: steps in a proof where a statement is asserted without previous justification within the proof itself. This is exactly where the ambient theory comes in.
Amongst the properties that (the thing coded by) $x$ must have, in order to be a proof of (the thing coded by) $y$ in a theory $T$, is that it can only use "axioms" which are actually axioms of $T$. (This is actually an inference rule: in a proof from $T$, we can at any point assert any of the axioms of $T$.) In particular, the sequence $langlevarphirangle$ is a proof of $varphi$ from $T$ iff $varphiin T$ (EDIT: or $varphi$ is a logical axiom). So any two different sets of axioms have different proof predicates. For example, "$langle forall x(S(x)not=0)rangle$" is a valid proof of $forall x(S(x)not=0)$ from the axioms of Peano arithmetic, but not from, say, the theory $forall x(S(x)=x)$.
Of course, if $T$ is a theory and $varphi$ is a theorem of $T$, then for some $psi_1,...,psi_nin T$ we have $emptysetvdash (psi_1wedge...wedgepsi_n)impliesvarphi$, so in a sense all proof predicates reduce to the proof predicate for the empty theory. But that's not what you asked
answered Jul 21 at 1:41
Noah Schweber
111k9140261
Nitpick: $left<varphiright>$ could also be a proof of $varphi$ if $varphi$ is an instance of a logical axiom in the proof system you're using.
– Henning Makholm
Jul 21 at 10:46
@HenningMakholm Bah, quite right; edited!
– Noah Schweber
Jul 21 at 16:27
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
2
down vote
You've argued that the non-"initial" steps in a proof don't depend on the ambient theory, but we also have to consider the "initial" steps: steps in a proof where a statement is asserted without previous justification within the proof itself. This is exactly where the ambient theory comes in.
Amongst the properties that (the thing coded by) $x$ must have, in order to be a proof of (the thing coded by) $y$ in a theory $T$, is that it can only use "axioms" which are actually axioms of $T$. (This is actually an inference rule: in a proof from $T$, we can at any point assert any of the axioms of $T$.) In particular, the sequence $langlevarphirangle$ is a proof of $varphi$ from $T$ iff $varphiin T$ (EDIT: or $varphi$ is a logical axiom). So any two different sets of axioms have different proof predicates. For example, "$langle forall x(S(x)not=0)rangle$" is a valid proof of $forall x(S(x)not=0)$ from the axioms of Peano arithmetic, but not from, say, the theory $forall x(S(x)=x)$.
Of course, if $T$ is a theory and $varphi$ is a theorem of $T$, then for some $psi_1,...,psi_nin T$ we have $emptysetvdash (psi_1wedge...wedgepsi_n)impliesvarphi$, so in a sense all proof predicates reduce to the proof predicate for the empty theory. But that's not what you asked
answered Jul 21 at 1:41
Noah Schweber
111k9140261
Nitpick: $left<varphiright>$ could also be a proof of $varphi$ if $varphi$ is an instance of a logical axiom in the proof system you're using.
– Henning Makholm
Jul 21 at 10:46
@HenningMakholm Bah, quite right; edited!
– Noah Schweber
Jul 21 at 16:27
add a comment |Â
up vote
2
down vote
You've argued that the non-"initial" steps in a proof don't depend on the ambient theory, but we also have to consider the "initial" steps: steps in a proof where a statement is asserted without previous justification within the proof itself. This is exactly where the ambient theory comes in.
Amongst the properties that (the thing coded by) $x$ must have, in order to be a proof of (the thing coded by) $y$ in a theory $T$, is that it can only use "axioms" which are actually axioms of $T$. (This is actually an inference rule: in a proof from $T$, we can at any point assert any of the axioms of $T$.) In particular, the sequence $langlevarphirangle$ is a proof of $varphi$ from $T$ iff $varphiin T$ (EDIT: or $varphi$ is a logical axiom). So any two different sets of axioms have different proof predicates. For example, "$langle forall x(S(x)not=0)rangle$" is a valid proof of $forall x(S(x)not=0)$ from the axioms of Peano arithmetic, but not from, say, the theory $forall x(S(x)=x)$.
Of course, if $T$ is a theory and $varphi$ is a theorem of $T$, then for some $psi_1,...,psi_nin T$ we have $emptysetvdash (psi_1wedge...wedgepsi_n)impliesvarphi$, so in a sense all proof predicates reduce to the proof predicate for the empty theory. But that's not what you asked
answered Jul 21 at 1:41
Noah Schweber
111k9140261
Nitpick: $left<varphiright>$ could also be a proof of $varphi$ if $varphi$ is an instance of a logical axiom in the proof system you're using.
– Henning Makholm
Jul 21 at 10:46
@HenningMakholm Bah, quite right; edited!
– Noah Schweber
Jul 21 at 16:27
add a comment |Â
up vote
2
down vote
up vote
2
down vote
You've argued that the non-"initial" steps in a proof don't depend on the ambient theory, but we also have to consider the "initial" steps: steps in a proof where a statement is asserted without previous justification within the proof itself. This is exactly where the ambient theory comes in.
Amongst the properties that (the thing coded by) $x$ must have, in order to be a proof of (the thing coded by) $y$ in a theory $T$, is that it can only use "axioms" which are actually axioms of $T$. (This is actually an inference rule: in a proof from $T$, we can at any point assert any of the axioms of $T$.) In particular, the sequence $langlevarphirangle$ is a proof of $varphi$ from $T$ iff $varphiin T$ (EDIT: or $varphi$ is a logical axiom). So any two different sets of axioms have different proof predicates. For example, "$langle forall x(S(x)not=0)rangle$" is a valid proof of $forall x(S(x)not=0)$ from the axioms of Peano arithmetic, but not from, say, the theory $forall x(S(x)=x)$.
Of course, if $T$ is a theory and $varphi$ is a theorem of $T$, then for some $psi_1,...,psi_nin T$ we have $emptysetvdash (psi_1wedge...wedgepsi_n)impliesvarphi$, so in a sense all proof predicates reduce to the proof predicate for the empty theory. But that's not what you asked
answered Jul 21 at 1:41
Noah Schweber
111k9140261
You've argued that the non-"initial" steps in a proof don't depend on the ambient theory, but we also have to consider the "initial" steps: steps in a proof where a statement is asserted without previous justification within the proof itself. This is exactly where the ambient theory comes in.
Amongst the properties that (the thing coded by) $x$ must have, in order to be a proof of (the thing coded by) $y$ in a theory $T$, is that it can only use "axioms" which are actually axioms of $T$. (This is actually an inference rule: in a proof from $T$, we can at any point assert any of the axioms of $T$.) In particular, the sequence $langlevarphirangle$ is a proof of $varphi$ from $T$ iff $varphiin T$ (EDIT: or $varphi$ is a logical axiom). So any two different sets of axioms have different proof predicates. For example, "$langle forall x(S(x)not=0)rangle$" is a valid proof of $forall x(S(x)not=0)$ from the axioms of Peano arithmetic, but not from, say, the theory $forall x(S(x)=x)$.
Of course, if $T$ is a theory and $varphi$ is a theorem of $T$, then for some $psi_1,...,psi_nin T$ we have $emptysetvdash (psi_1wedge...wedgepsi_n)impliesvarphi$, so in a sense all proof predicates reduce to the proof predicate for the empty theory. But that's not what you asked
answered Jul 21 at 1:41
Noah Schweber
111k9140261
edited Jul 21 at 16:27
answered Jul 21 at 1:41
Noah Schweber
111k9140261
answered Jul 21 at 1:41
Noah Schweber
111k9140261
answered Jul 21 at 1:41
Noah Schweber
111k9140261
111k9140261
Nitpick: $left<varphiright>$ could also be a proof of $varphi$ if $varphi$ is an instance of a logical axiom in the proof system you're using.
– Henning Makholm
Jul 21 at 10:46
@HenningMakholm Bah, quite right; edited!
– Noah Schweber
Jul 21 at 16:27
add a comment |Â
Nitpick: $left<varphiright>$ could also be a proof of $varphi$ if $varphi$ is an instance of a logical axiom in the proof system you're using.
– Henning Makholm
Jul 21 at 10:46
@HenningMakholm Bah, quite right; edited!
– Noah Schweber
Jul 21 at 16:27
Nitpick: $left<varphiright>$ could also be a proof of $varphi$ if $varphi$ is an instance of a logical axiom in the proof system you're using.
– Henning Makholm
Jul 21 at 10:46
Nitpick: $left<varphiright>$ could also be a proof of $varphi$ if $varphi$ is an instance of a logical axiom in the proof system you're using.
– Henning Makholm
Jul 21 at 10:46
@HenningMakholm Bah, quite right; edited!
– Noah Schweber
Jul 21 at 16:27
@HenningMakholm Bah, quite right; edited!
– Noah Schweber
Jul 21 at 16:27
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%2f2858147%2fwould-a-proof-predicate-change-if-a-stronger-system-used-despite-sharing-languag%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
2
Yes it does change. Verifying a proof involves checking if certain statements are axioms or not. Thus if the axioms change, the verification procedure the proof predicate encodes changes, so the proof predicate changes.
– spaceisdarkgreen
Jul 21 at 1:26