Adding constants to formal system
$begingroup$
I wonder how can we formalize in logic the fact that we sometimes add additional constants for the sake of readability.
Consider, for example, that in some formal system we prove that if $a,i$ are variables that:
$$exists !i (forall a( ai=a)).$$
Then, one says something like "we have shown that there is a unique right identity (or any other funny name) and let us from now on denote it by $1$". I guess what is actually happening is that we construct a new formal system where we redefine things like terms and formulas as necessary to include $1$ and we add new formal symbol $1$. But that means that it is not the same formal system anymore. But we are still interested in the one before adding $1$.
Question 1: Are there some standard procedures or ways to deal with adding constants to formal system in a way that we can reason about the theory which is obtained before adding new constants?
Question 2: Kleene in "Mathematical Logic" states that we can add $1$ in such case to our list of formal symbols and also add a new axiom "$forall a(a1=a)$". Why would we want to add this axiom? On one hand, this gives some rules about constant $1$ without which we do not know how to apply it in our reasoning. On the other hand, we are adding a new axiom - how do we know it doesn't lead to a contradiction? For example, how do we know that we do not get more results from it than if we had only original axioms?
Ideally, I would want some procedure of adding constants in a way that new formal theory has some way of translating all of the sentences of new constants in terms of old formal theory, and that it does not introduce any new results - it can prove only those theorems that could be proven without adding those constants.
I hope my question is clear and if not please let me know and I will try to improve it, thanks!
logic formal-systems
asked Dec 22 '18 at 7:31
Daniels KrimansDaniels Krimans
51939
$endgroup$
add a comment |
$begingroup$
I wonder how can we formalize in logic the fact that we sometimes add additional constants for the sake of readability.
Consider, for example, that in some formal system we prove that if $a,i$ are variables that:
$$exists !i (forall a( ai=a)).$$
Then, one says something like "we have shown that there is a unique right identity (or any other funny name) and let us from now on denote it by $1$". I guess what is actually happening is that we construct a new formal system where we redefine things like terms and formulas as necessary to include $1$ and we add new formal symbol $1$. But that means that it is not the same formal system anymore. But we are still interested in the one before adding $1$.
Question 1: Are there some standard procedures or ways to deal with adding constants to formal system in a way that we can reason about the theory which is obtained before adding new constants?
Question 2: Kleene in "Mathematical Logic" states that we can add $1$ in such case to our list of formal symbols and also add a new axiom "$forall a(a1=a)$". Why would we want to add this axiom? On one hand, this gives some rules about constant $1$ without which we do not know how to apply it in our reasoning. On the other hand, we are adding a new axiom - how do we know it doesn't lead to a contradiction? For example, how do we know that we do not get more results from it than if we had only original axioms?
Ideally, I would want some procedure of adding constants in a way that new formal theory has some way of translating all of the sentences of new constants in terms of old formal theory, and that it does not introduce any new results - it can prove only those theorems that could be proven without adding those constants.
I hope my question is clear and if not please let me know and I will try to improve it, thanks!
logic formal-systems
asked Dec 22 '18 at 7:31
Daniels KrimansDaniels Krimans
51939
$endgroup$
$begingroup$
If we can prove in the formal system that such a unique $1$ exists, then adding this existence as an axiom can never lead to a new contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:36
$begingroup$
@HennoBrandsma Why?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:38
$begingroup$
Imagine the proof of the new contradiction. It must use the new axiom. But we could have replaced the use of the new axiom with the proof we have from the original axioms. Hence the original axioms already proved the contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:40
$begingroup$
@HennoBrandsma I think my question is how do you translate the use of new symbol like "$1$" in new formal system by what you have in the old formal system. Assume you had a proof of contradiction in the new formal system that used $"1"$. How do you translate it back to the old system without "$1$"?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:45
add a comment |
$begingroup$
I wonder how can we formalize in logic the fact that we sometimes add additional constants for the sake of readability.
Consider, for example, that in some formal system we prove that if $a,i$ are variables that:
$$exists !i (forall a( ai=a)).$$
Then, one says something like "we have shown that there is a unique right identity (or any other funny name) and let us from now on denote it by $1$". I guess what is actually happening is that we construct a new formal system where we redefine things like terms and formulas as necessary to include $1$ and we add new formal symbol $1$. But that means that it is not the same formal system anymore. But we are still interested in the one before adding $1$.
Question 1: Are there some standard procedures or ways to deal with adding constants to formal system in a way that we can reason about the theory which is obtained before adding new constants?
Question 2: Kleene in "Mathematical Logic" states that we can add $1$ in such case to our list of formal symbols and also add a new axiom "$forall a(a1=a)$". Why would we want to add this axiom? On one hand, this gives some rules about constant $1$ without which we do not know how to apply it in our reasoning. On the other hand, we are adding a new axiom - how do we know it doesn't lead to a contradiction? For example, how do we know that we do not get more results from it than if we had only original axioms?
Ideally, I would want some procedure of adding constants in a way that new formal theory has some way of translating all of the sentences of new constants in terms of old formal theory, and that it does not introduce any new results - it can prove only those theorems that could be proven without adding those constants.
I hope my question is clear and if not please let me know and I will try to improve it, thanks!
logic formal-systems
asked Dec 22 '18 at 7:31
Daniels KrimansDaniels Krimans
51939
$endgroup$
I wonder how can we formalize in logic the fact that we sometimes add additional constants for the sake of readability.
Consider, for example, that in some formal system we prove that if $a,i$ are variables that:
$$exists !i (forall a( ai=a)).$$
Then, one says something like "we have shown that there is a unique right identity (or any other funny name) and let us from now on denote it by $1$". I guess what is actually happening is that we construct a new formal system where we redefine things like terms and formulas as necessary to include $1$ and we add new formal symbol $1$. But that means that it is not the same formal system anymore. But we are still interested in the one before adding $1$.
Question 1: Are there some standard procedures or ways to deal with adding constants to formal system in a way that we can reason about the theory which is obtained before adding new constants?
Question 2: Kleene in "Mathematical Logic" states that we can add $1$ in such case to our list of formal symbols and also add a new axiom "$forall a(a1=a)$". Why would we want to add this axiom? On one hand, this gives some rules about constant $1$ without which we do not know how to apply it in our reasoning. On the other hand, we are adding a new axiom - how do we know it doesn't lead to a contradiction? For example, how do we know that we do not get more results from it than if we had only original axioms?
Ideally, I would want some procedure of adding constants in a way that new formal theory has some way of translating all of the sentences of new constants in terms of old formal theory, and that it does not introduce any new results - it can prove only those theorems that could be proven without adding those constants.
I hope my question is clear and if not please let me know and I will try to improve it, thanks!
logic formal-systems
logic formal-systems
asked Dec 22 '18 at 7:31
Daniels KrimansDaniels Krimans
51939
asked Dec 22 '18 at 7:31
Daniels KrimansDaniels Krimans
51939
asked Dec 22 '18 at 7:31
Daniels KrimansDaniels Krimans
51939
asked Dec 22 '18 at 7:31
Daniels KrimansDaniels Krimans
51939
asked Dec 22 '18 at 7:31
Daniels KrimansDaniels Krimans
51939
51939
$begingroup$
If we can prove in the formal system that such a unique $1$ exists, then adding this existence as an axiom can never lead to a new contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:36
$begingroup$
@HennoBrandsma Why?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:38
$begingroup$
Imagine the proof of the new contradiction. It must use the new axiom. But we could have replaced the use of the new axiom with the proof we have from the original axioms. Hence the original axioms already proved the contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:40
$begingroup$
@HennoBrandsma I think my question is how do you translate the use of new symbol like "$1$" in new formal system by what you have in the old formal system. Assume you had a proof of contradiction in the new formal system that used $"1"$. How do you translate it back to the old system without "$1$"?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:45
add a comment |
$begingroup$
If we can prove in the formal system that such a unique $1$ exists, then adding this existence as an axiom can never lead to a new contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:36
$begingroup$
@HennoBrandsma Why?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:38
$begingroup$
Imagine the proof of the new contradiction. It must use the new axiom. But we could have replaced the use of the new axiom with the proof we have from the original axioms. Hence the original axioms already proved the contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:40
$begingroup$
@HennoBrandsma I think my question is how do you translate the use of new symbol like "$1$" in new formal system by what you have in the old formal system. Assume you had a proof of contradiction in the new formal system that used $"1"$. How do you translate it back to the old system without "$1$"?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:45
$begingroup$
If we can prove in the formal system that such a unique $1$ exists, then adding this existence as an axiom can never lead to a new contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:36
$begingroup$
If we can prove in the formal system that such a unique $1$ exists, then adding this existence as an axiom can never lead to a new contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:36
$begingroup$
@HennoBrandsma Why?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:38
$begingroup$
@HennoBrandsma Why?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:38
$begingroup$
Imagine the proof of the new contradiction. It must use the new axiom. But we could have replaced the use of the new axiom with the proof we have from the original axioms. Hence the original axioms already proved the contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:40
$begingroup$
Imagine the proof of the new contradiction. It must use the new axiom. But we could have replaced the use of the new axiom with the proof we have from the original axioms. Hence the original axioms already proved the contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:40
$begingroup$
@HennoBrandsma I think my question is how do you translate the use of new symbol like "$1$" in new formal system by what you have in the old formal system. Assume you had a proof of contradiction in the new formal system that used $"1"$. How do you translate it back to the old system without "$1$"?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:45
$begingroup$
@HennoBrandsma I think my question is how do you translate the use of new symbol like "$1$" in new formal system by what you have in the old formal system. Assume you had a proof of contradiction in the new formal system that used $"1"$. How do you translate it back to the old system without "$1$"?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:45
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Okay, let's consider the case of $1,$ added to some reasonable arithmetic system via the axiom that it is the multiplicative identity $$ forall y(ycdot1=y)$$ and we'll assume the system is strong enough to prove the sentence $$ exists x forall y(ycdot x=y)land forall x forall z(forall y(ycdot x = y)landforall y(ycdot z=y)to x=z)$$ that $1$ exists and is uniquely defined by this axiom.
Now let's write a true statement about $1$ (more-or less chosen randomly): $$ forall x exists y(y=x+1).$$ We can write an equivalent statement in the language without $1$ as follows: $$ exists z (forall w(wcdot z=w) land forall xexists y(y=x+z)).$$ To prove the abbreviated statement implies this, take the conjunction of it and the axiom and use existential generalization. To prove this implies the abbreviated statement, instantiate $z$, then use the left conjunct and the uniqueness statement to prove $z=1,$ then substitute $1$ in for $z$ in the right conjunct.
This is quite general. If we have a defining formula $phi(x)$ where we can prove $exists! xphi(x)$ and we extend the language with the constant $c$ and the theory with the axiom $phi(c),$ then we can translate any sentence $psi(c)$ in the extended language back into the initial language as $$ exists x(phi(x)landpsi(x)).$$ Similar things can be said about defined functions. Defined relations are easier since you can literally just replace an instance like $R(x,y)$ with its defining formula $phi_R(x,y).$
This process is called definitional extension, and hopefully this makes it clearer than these extensions are always conservative.
answered Dec 22 '18 at 8:12
spaceisdarkgreenspaceisdarkgreen
32.8k21753
$endgroup$
$begingroup$
Thanks! I think this is exactly what I wanted! Why for an equivalent statement without $1$ you write just $exists z$ instead of $exists !z$. Is there a reason for that?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:21
$begingroup$
Sure, it is an abbreviation. But still, why don't we use it for translating back to the original language. Because intuitively (intuition is bad, I know) I feel like we want to say that there is a unique x such that $phi(x) land psi(x)$ because our constant was uniquely defined.
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:25
$begingroup$
Oh, I misunderstood your question, sorry. You don't need the uniqueness statement because it's already provable in our theory that such a $z$ will be unique, since it satisfies the defining formula, for which it is assumed $exists !x phi(x)$ is provable. (There would be no harm adding it, though).
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:29
$begingroup$
I guess it makes sense, thank you very much! I hope you don't mind if I don't accept your answer until I go through it carefully
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:30
$begingroup$
Of course not, no problem.
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:31
|
show 4 more comments
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%2f3049196%2fadding-constants-to-formal-system%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
Okay, let's consider the case of $1,$ added to some reasonable arithmetic system via the axiom that it is the multiplicative identity $$ forall y(ycdot1=y)$$ and we'll assume the system is strong enough to prove the sentence $$ exists x forall y(ycdot x=y)land forall x forall z(forall y(ycdot x = y)landforall y(ycdot z=y)to x=z)$$ that $1$ exists and is uniquely defined by this axiom.
Now let's write a true statement about $1$ (more-or less chosen randomly): $$ forall x exists y(y=x+1).$$ We can write an equivalent statement in the language without $1$ as follows: $$ exists z (forall w(wcdot z=w) land forall xexists y(y=x+z)).$$ To prove the abbreviated statement implies this, take the conjunction of it and the axiom and use existential generalization. To prove this implies the abbreviated statement, instantiate $z$, then use the left conjunct and the uniqueness statement to prove $z=1,$ then substitute $1$ in for $z$ in the right conjunct.
This is quite general. If we have a defining formula $phi(x)$ where we can prove $exists! xphi(x)$ and we extend the language with the constant $c$ and the theory with the axiom $phi(c),$ then we can translate any sentence $psi(c)$ in the extended language back into the initial language as $$ exists x(phi(x)landpsi(x)).$$ Similar things can be said about defined functions. Defined relations are easier since you can literally just replace an instance like $R(x,y)$ with its defining formula $phi_R(x,y).$
This process is called definitional extension, and hopefully this makes it clearer than these extensions are always conservative.
answered Dec 22 '18 at 8:12
spaceisdarkgreenspaceisdarkgreen
32.8k21753
$endgroup$
$begingroup$
Thanks! I think this is exactly what I wanted! Why for an equivalent statement without $1$ you write just $exists z$ instead of $exists !z$. Is there a reason for that?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:21
$begingroup$
Sure, it is an abbreviation. But still, why don't we use it for translating back to the original language. Because intuitively (intuition is bad, I know) I feel like we want to say that there is a unique x such that $phi(x) land psi(x)$ because our constant was uniquely defined.
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:25
$begingroup$
Oh, I misunderstood your question, sorry. You don't need the uniqueness statement because it's already provable in our theory that such a $z$ will be unique, since it satisfies the defining formula, for which it is assumed $exists !x phi(x)$ is provable. (There would be no harm adding it, though).
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:29
$begingroup$
I guess it makes sense, thank you very much! I hope you don't mind if I don't accept your answer until I go through it carefully
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:30
$begingroup$
Of course not, no problem.
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:31
|
show 4 more comments
$begingroup$
Okay, let's consider the case of $1,$ added to some reasonable arithmetic system via the axiom that it is the multiplicative identity $$ forall y(ycdot1=y)$$ and we'll assume the system is strong enough to prove the sentence $$ exists x forall y(ycdot x=y)land forall x forall z(forall y(ycdot x = y)landforall y(ycdot z=y)to x=z)$$ that $1$ exists and is uniquely defined by this axiom.
Now let's write a true statement about $1$ (more-or less chosen randomly): $$ forall x exists y(y=x+1).$$ We can write an equivalent statement in the language without $1$ as follows: $$ exists z (forall w(wcdot z=w) land forall xexists y(y=x+z)).$$ To prove the abbreviated statement implies this, take the conjunction of it and the axiom and use existential generalization. To prove this implies the abbreviated statement, instantiate $z$, then use the left conjunct and the uniqueness statement to prove $z=1,$ then substitute $1$ in for $z$ in the right conjunct.
This is quite general. If we have a defining formula $phi(x)$ where we can prove $exists! xphi(x)$ and we extend the language with the constant $c$ and the theory with the axiom $phi(c),$ then we can translate any sentence $psi(c)$ in the extended language back into the initial language as $$ exists x(phi(x)landpsi(x)).$$ Similar things can be said about defined functions. Defined relations are easier since you can literally just replace an instance like $R(x,y)$ with its defining formula $phi_R(x,y).$
This process is called definitional extension, and hopefully this makes it clearer than these extensions are always conservative.
answered Dec 22 '18 at 8:12
spaceisdarkgreenspaceisdarkgreen
32.8k21753
$endgroup$
$begingroup$
Thanks! I think this is exactly what I wanted! Why for an equivalent statement without $1$ you write just $exists z$ instead of $exists !z$. Is there a reason for that?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:21
$begingroup$
Sure, it is an abbreviation. But still, why don't we use it for translating back to the original language. Because intuitively (intuition is bad, I know) I feel like we want to say that there is a unique x such that $phi(x) land psi(x)$ because our constant was uniquely defined.
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:25
$begingroup$
Oh, I misunderstood your question, sorry. You don't need the uniqueness statement because it's already provable in our theory that such a $z$ will be unique, since it satisfies the defining formula, for which it is assumed $exists !x phi(x)$ is provable. (There would be no harm adding it, though).
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:29
$begingroup$
I guess it makes sense, thank you very much! I hope you don't mind if I don't accept your answer until I go through it carefully
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:30
$begingroup$
Of course not, no problem.
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:31
|
show 4 more comments
$begingroup$
Okay, let's consider the case of $1,$ added to some reasonable arithmetic system via the axiom that it is the multiplicative identity $$ forall y(ycdot1=y)$$ and we'll assume the system is strong enough to prove the sentence $$ exists x forall y(ycdot x=y)land forall x forall z(forall y(ycdot x = y)landforall y(ycdot z=y)to x=z)$$ that $1$ exists and is uniquely defined by this axiom.
Now let's write a true statement about $1$ (more-or less chosen randomly): $$ forall x exists y(y=x+1).$$ We can write an equivalent statement in the language without $1$ as follows: $$ exists z (forall w(wcdot z=w) land forall xexists y(y=x+z)).$$ To prove the abbreviated statement implies this, take the conjunction of it and the axiom and use existential generalization. To prove this implies the abbreviated statement, instantiate $z$, then use the left conjunct and the uniqueness statement to prove $z=1,$ then substitute $1$ in for $z$ in the right conjunct.
This is quite general. If we have a defining formula $phi(x)$ where we can prove $exists! xphi(x)$ and we extend the language with the constant $c$ and the theory with the axiom $phi(c),$ then we can translate any sentence $psi(c)$ in the extended language back into the initial language as $$ exists x(phi(x)landpsi(x)).$$ Similar things can be said about defined functions. Defined relations are easier since you can literally just replace an instance like $R(x,y)$ with its defining formula $phi_R(x,y).$
This process is called definitional extension, and hopefully this makes it clearer than these extensions are always conservative.
answered Dec 22 '18 at 8:12
spaceisdarkgreenspaceisdarkgreen
32.8k21753
$endgroup$
Okay, let's consider the case of $1,$ added to some reasonable arithmetic system via the axiom that it is the multiplicative identity $$ forall y(ycdot1=y)$$ and we'll assume the system is strong enough to prove the sentence $$ exists x forall y(ycdot x=y)land forall x forall z(forall y(ycdot x = y)landforall y(ycdot z=y)to x=z)$$ that $1$ exists and is uniquely defined by this axiom.
Now let's write a true statement about $1$ (more-or less chosen randomly): $$ forall x exists y(y=x+1).$$ We can write an equivalent statement in the language without $1$ as follows: $$ exists z (forall w(wcdot z=w) land forall xexists y(y=x+z)).$$ To prove the abbreviated statement implies this, take the conjunction of it and the axiom and use existential generalization. To prove this implies the abbreviated statement, instantiate $z$, then use the left conjunct and the uniqueness statement to prove $z=1,$ then substitute $1$ in for $z$ in the right conjunct.
This is quite general. If we have a defining formula $phi(x)$ where we can prove $exists! xphi(x)$ and we extend the language with the constant $c$ and the theory with the axiom $phi(c),$ then we can translate any sentence $psi(c)$ in the extended language back into the initial language as $$ exists x(phi(x)landpsi(x)).$$ Similar things can be said about defined functions. Defined relations are easier since you can literally just replace an instance like $R(x,y)$ with its defining formula $phi_R(x,y).$
This process is called definitional extension, and hopefully this makes it clearer than these extensions are always conservative.
answered Dec 22 '18 at 8:12
spaceisdarkgreenspaceisdarkgreen
32.8k21753
edited Dec 22 '18 at 8:17
answered Dec 22 '18 at 8:12
spaceisdarkgreenspaceisdarkgreen
32.8k21753
answered Dec 22 '18 at 8:12
spaceisdarkgreenspaceisdarkgreen
32.8k21753
answered Dec 22 '18 at 8:12
spaceisdarkgreenspaceisdarkgreen
32.8k21753
32.8k21753
$begingroup$
Thanks! I think this is exactly what I wanted! Why for an equivalent statement without $1$ you write just $exists z$ instead of $exists !z$. Is there a reason for that?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:21
$begingroup$
Sure, it is an abbreviation. But still, why don't we use it for translating back to the original language. Because intuitively (intuition is bad, I know) I feel like we want to say that there is a unique x such that $phi(x) land psi(x)$ because our constant was uniquely defined.
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:25
$begingroup$
Oh, I misunderstood your question, sorry. You don't need the uniqueness statement because it's already provable in our theory that such a $z$ will be unique, since it satisfies the defining formula, for which it is assumed $exists !x phi(x)$ is provable. (There would be no harm adding it, though).
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:29
$begingroup$
I guess it makes sense, thank you very much! I hope you don't mind if I don't accept your answer until I go through it carefully
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:30
$begingroup$
Of course not, no problem.
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:31
|
show 4 more comments
$begingroup$
Thanks! I think this is exactly what I wanted! Why for an equivalent statement without $1$ you write just $exists z$ instead of $exists !z$. Is there a reason for that?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:21
$begingroup$
Sure, it is an abbreviation. But still, why don't we use it for translating back to the original language. Because intuitively (intuition is bad, I know) I feel like we want to say that there is a unique x such that $phi(x) land psi(x)$ because our constant was uniquely defined.
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:25
$begingroup$
Oh, I misunderstood your question, sorry. You don't need the uniqueness statement because it's already provable in our theory that such a $z$ will be unique, since it satisfies the defining formula, for which it is assumed $exists !x phi(x)$ is provable. (There would be no harm adding it, though).
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:29
$begingroup$
I guess it makes sense, thank you very much! I hope you don't mind if I don't accept your answer until I go through it carefully
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:30
$begingroup$
Of course not, no problem.
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:31
$begingroup$
Thanks! I think this is exactly what I wanted! Why for an equivalent statement without $1$ you write just $exists z$ instead of $exists !z$. Is there a reason for that?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:21
$begingroup$
Thanks! I think this is exactly what I wanted! Why for an equivalent statement without $1$ you write just $exists z$ instead of $exists !z$. Is there a reason for that?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:21
$begingroup$
Sure, it is an abbreviation. But still, why don't we use it for translating back to the original language. Because intuitively (intuition is bad, I know) I feel like we want to say that there is a unique x such that $phi(x) land psi(x)$ because our constant was uniquely defined.
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:25
$begingroup$
Sure, it is an abbreviation. But still, why don't we use it for translating back to the original language. Because intuitively (intuition is bad, I know) I feel like we want to say that there is a unique x such that $phi(x) land psi(x)$ because our constant was uniquely defined.
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:25
$begingroup$
Oh, I misunderstood your question, sorry. You don't need the uniqueness statement because it's already provable in our theory that such a $z$ will be unique, since it satisfies the defining formula, for which it is assumed $exists !x phi(x)$ is provable. (There would be no harm adding it, though).
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:29
$begingroup$
Oh, I misunderstood your question, sorry. You don't need the uniqueness statement because it's already provable in our theory that such a $z$ will be unique, since it satisfies the defining formula, for which it is assumed $exists !x phi(x)$ is provable. (There would be no harm adding it, though).
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:29
$begingroup$
I guess it makes sense, thank you very much! I hope you don't mind if I don't accept your answer until I go through it carefully
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:30
$begingroup$
I guess it makes sense, thank you very much! I hope you don't mind if I don't accept your answer until I go through it carefully
$endgroup$
– Daniels Krimans
Dec 22 '18 at 8:30
$begingroup$
Of course not, no problem.
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:31
$begingroup$
Of course not, no problem.
$endgroup$
– spaceisdarkgreen
Dec 22 '18 at 8:31
|
show 4 more comments
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%2f3049196%2fadding-constants-to-formal-system%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$
If we can prove in the formal system that such a unique $1$ exists, then adding this existence as an axiom can never lead to a new contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:36
$begingroup$
@HennoBrandsma Why?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:38
$begingroup$
Imagine the proof of the new contradiction. It must use the new axiom. But we could have replaced the use of the new axiom with the proof we have from the original axioms. Hence the original axioms already proved the contradiction.
$endgroup$
– Henno Brandsma
Dec 22 '18 at 7:40
$begingroup$
@HennoBrandsma I think my question is how do you translate the use of new symbol like "$1$" in new formal system by what you have in the old formal system. Assume you had a proof of contradiction in the new formal system that used $"1"$. How do you translate it back to the old system without "$1$"?
$endgroup$
– Daniels Krimans
Dec 22 '18 at 7:45