Mixing
Proving certain obvious tautologies in the calculus of constructions
$begingroup$
I'm trying to prove that $lnot (exists y : S.Py) rightarrow exists y : S. lnot Py$ (let me know if the encoding of $exists$ matters!). I don't have any good ideas about how to do that, but I've tried various subgoals that look promising, but they bring more questions than answers.
My first attempt is first proving $lnot (exists y : S.Py) rightarrow Pi y:S.lnot Py$ (this is easy) and then proving $Pi y:S.Py rightarrow exists y:S.Py$ (I probably don't care about negation for this lemma and it's useful in its full generality, so I dropped the $lnot$). The second part turns out to be surprisingly hard, and I failed at that, since I need to present a real witness of the existence, which I cannot do without any prior knowledge about $S$. Is it possible to prove it?
Then, a different subgoal that would have helped me is to get $bot$ from $Pi x : S.P x$ and $Pi x : S.lnot P x$, but I failed here too. The best I could get is $Pi x:S. bot$, but I cannot reduce this to $bot$ without some inhabitant of $S$ that I don't know a priori (and this also has a striking resemblance to the blocker on the first point!). Is this one provable too?
And, disregarding those two points, what's the best way to prove the original implication?
I'm working in the calculus of constructions, but I have "axiomatic" terms in my context that represent double-negation elimination or the law of excluded third, shall it only be provable in classical predicate logic.
logic predicate-logic proof-theory type-theory
edited Jan 29 at 2:35
J. W. Tanner
4,0611320
asked Jan 29 at 1:22
0xd34df00d0xd34df00d
433212
$endgroup$
add a comment |
$begingroup$
I'm trying to prove that $lnot (exists y : S.Py) rightarrow exists y : S. lnot Py$ (let me know if the encoding of $exists$ matters!). I don't have any good ideas about how to do that, but I've tried various subgoals that look promising, but they bring more questions than answers.
My first attempt is first proving $lnot (exists y : S.Py) rightarrow Pi y:S.lnot Py$ (this is easy) and then proving $Pi y:S.Py rightarrow exists y:S.Py$ (I probably don't care about negation for this lemma and it's useful in its full generality, so I dropped the $lnot$). The second part turns out to be surprisingly hard, and I failed at that, since I need to present a real witness of the existence, which I cannot do without any prior knowledge about $S$. Is it possible to prove it?
Then, a different subgoal that would have helped me is to get $bot$ from $Pi x : S.P x$ and $Pi x : S.lnot P x$, but I failed here too. The best I could get is $Pi x:S. bot$, but I cannot reduce this to $bot$ without some inhabitant of $S$ that I don't know a priori (and this also has a striking resemblance to the blocker on the first point!). Is this one provable too?
And, disregarding those two points, what's the best way to prove the original implication?
I'm working in the calculus of constructions, but I have "axiomatic" terms in my context that represent double-negation elimination or the law of excluded third, shall it only be provable in classical predicate logic.
logic predicate-logic proof-theory type-theory
edited Jan 29 at 2:35
J. W. Tanner
4,0611320
asked Jan 29 at 1:22
0xd34df00d0xd34df00d
433212
$endgroup$
4
$begingroup$
The statement you're trying to prove isn't true in general, because there might not be anything of type $S$.
$endgroup$
– Andreas Blass
Jan 29 at 1:39
$begingroup$
Ah, I see! Yeah, wrapping that into $Pi text{witness} : S$ solves all of my problems! And the key difference between this and tautologies starting with $lnot Pi x : S. Px$ is that in order to fail a $forall$, an actual witness of the inverse must be present! Thanks!
$endgroup$
– 0xd34df00d
Jan 29 at 1:56
add a comment |
$begingroup$
I'm trying to prove that $lnot (exists y : S.Py) rightarrow exists y : S. lnot Py$ (let me know if the encoding of $exists$ matters!). I don't have any good ideas about how to do that, but I've tried various subgoals that look promising, but they bring more questions than answers.
My first attempt is first proving $lnot (exists y : S.Py) rightarrow Pi y:S.lnot Py$ (this is easy) and then proving $Pi y:S.Py rightarrow exists y:S.Py$ (I probably don't care about negation for this lemma and it's useful in its full generality, so I dropped the $lnot$). The second part turns out to be surprisingly hard, and I failed at that, since I need to present a real witness of the existence, which I cannot do without any prior knowledge about $S$. Is it possible to prove it?
Then, a different subgoal that would have helped me is to get $bot$ from $Pi x : S.P x$ and $Pi x : S.lnot P x$, but I failed here too. The best I could get is $Pi x:S. bot$, but I cannot reduce this to $bot$ without some inhabitant of $S$ that I don't know a priori (and this also has a striking resemblance to the blocker on the first point!). Is this one provable too?
And, disregarding those two points, what's the best way to prove the original implication?
I'm working in the calculus of constructions, but I have "axiomatic" terms in my context that represent double-negation elimination or the law of excluded third, shall it only be provable in classical predicate logic.
logic predicate-logic proof-theory type-theory
edited Jan 29 at 2:35
J. W. Tanner
4,0611320
asked Jan 29 at 1:22
0xd34df00d0xd34df00d
433212
$endgroup$
I'm trying to prove that $lnot (exists y : S.Py) rightarrow exists y : S. lnot Py$ (let me know if the encoding of $exists$ matters!). I don't have any good ideas about how to do that, but I've tried various subgoals that look promising, but they bring more questions than answers.
My first attempt is first proving $lnot (exists y : S.Py) rightarrow Pi y:S.lnot Py$ (this is easy) and then proving $Pi y:S.Py rightarrow exists y:S.Py$ (I probably don't care about negation for this lemma and it's useful in its full generality, so I dropped the $lnot$). The second part turns out to be surprisingly hard, and I failed at that, since I need to present a real witness of the existence, which I cannot do without any prior knowledge about $S$. Is it possible to prove it?
Then, a different subgoal that would have helped me is to get $bot$ from $Pi x : S.P x$ and $Pi x : S.lnot P x$, but I failed here too. The best I could get is $Pi x:S. bot$, but I cannot reduce this to $bot$ without some inhabitant of $S$ that I don't know a priori (and this also has a striking resemblance to the blocker on the first point!). Is this one provable too?
And, disregarding those two points, what's the best way to prove the original implication?
I'm working in the calculus of constructions, but I have "axiomatic" terms in my context that represent double-negation elimination or the law of excluded third, shall it only be provable in classical predicate logic.
logic predicate-logic proof-theory type-theory
logic predicate-logic proof-theory type-theory
edited Jan 29 at 2:35
J. W. Tanner
4,0611320
asked Jan 29 at 1:22
0xd34df00d0xd34df00d
433212
edited Jan 29 at 2:35
J. W. Tanner
4,0611320
asked Jan 29 at 1:22
0xd34df00d0xd34df00d
433212
edited Jan 29 at 2:35
J. W. Tanner
4,0611320
edited Jan 29 at 2:35
J. W. Tanner
4,0611320
edited Jan 29 at 2:35
J. W. Tanner
4,0611320
4,0611320
asked Jan 29 at 1:22
0xd34df00d0xd34df00d
433212
asked Jan 29 at 1:22
0xd34df00d0xd34df00d
433212
asked Jan 29 at 1:22
0xd34df00d0xd34df00d
433212
433212
4
$begingroup$
The statement you're trying to prove isn't true in general, because there might not be anything of type $S$.
$endgroup$
– Andreas Blass
Jan 29 at 1:39
$begingroup$
Ah, I see! Yeah, wrapping that into $Pi text{witness} : S$ solves all of my problems! And the key difference between this and tautologies starting with $lnot Pi x : S. Px$ is that in order to fail a $forall$, an actual witness of the inverse must be present! Thanks!
$endgroup$
– 0xd34df00d
Jan 29 at 1:56
add a comment |
4
$begingroup$
The statement you're trying to prove isn't true in general, because there might not be anything of type $S$.
$endgroup$
– Andreas Blass
Jan 29 at 1:39
$begingroup$
Ah, I see! Yeah, wrapping that into $Pi text{witness} : S$ solves all of my problems! And the key difference between this and tautologies starting with $lnot Pi x : S. Px$ is that in order to fail a $forall$, an actual witness of the inverse must be present! Thanks!
$endgroup$
– 0xd34df00d
Jan 29 at 1:56
4
4
$begingroup$
The statement you're trying to prove isn't true in general, because there might not be anything of type $S$.
$endgroup$
– Andreas Blass
Jan 29 at 1:39
$begingroup$
The statement you're trying to prove isn't true in general, because there might not be anything of type $S$.
$endgroup$
– Andreas Blass
Jan 29 at 1:39
$begingroup$
Ah, I see! Yeah, wrapping that into $Pi text{witness} : S$ solves all of my problems! And the key difference between this and tautologies starting with $lnot Pi x : S. Px$ is that in order to fail a $forall$, an actual witness of the inverse must be present! Thanks!
$endgroup$
– 0xd34df00d
Jan 29 at 1:56
$begingroup$
Ah, I see! Yeah, wrapping that into $Pi text{witness} : S$ solves all of my problems! And the key difference between this and tautologies starting with $lnot Pi x : S. Px$ is that in order to fail a $forall$, an actual witness of the inverse must be present! Thanks!
$endgroup$
– 0xd34df00d
Jan 29 at 1:56
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
- No, it is not possible to prove this because if $S$ is the null set, then the hypothesis that $(forall y in S)(Py)$ will be true while the conclusion $(exists yin S)(Py)$ will be false since $S$ is not the null set.
However, let's say $S$ is not the null set. That is, we know of some $y_0$ such that $y_0in S$. Then, how do we go about proving this conditional?
Well, first we use Universal Elimination to go from $(forall y in S)(Py)$ to $Py_0$. Then, we use Existential Introduction to go from $Py_0$ to $(exists yin S)(Py)$
- No, this contradiction is also not provable because $(forall y in S)(Py)$ and $(forall yin S)(neg Py)$ are not inherently contradictory statements: If $S$ is the null set, both of these statements are vacuously true.
However, again, let's say $S$ is not the null set. Given $y_0 in S$, how do we derive a contradiction from these statements?
Well, use Universal Elimination on both universal statements to get $Py_0$ and $neg Py_0$. Then, use Contradiction Introduction to derive $bot$.
The original conditional is only true if $S$ is not the null set. Therefore, I think I answered 3 in my sidenote to 1.
answered Jan 29 at 1:59
Noble MushtakNoble Mushtak
15.3k1835
$endgroup$
add a comment |
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%2f3091622%2fproving-certain-obvious-tautologies-in-the-calculus-of-constructions%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$
- No, it is not possible to prove this because if $S$ is the null set, then the hypothesis that $(forall y in S)(Py)$ will be true while the conclusion $(exists yin S)(Py)$ will be false since $S$ is not the null set.
However, let's say $S$ is not the null set. That is, we know of some $y_0$ such that $y_0in S$. Then, how do we go about proving this conditional?
Well, first we use Universal Elimination to go from $(forall y in S)(Py)$ to $Py_0$. Then, we use Existential Introduction to go from $Py_0$ to $(exists yin S)(Py)$
- No, this contradiction is also not provable because $(forall y in S)(Py)$ and $(forall yin S)(neg Py)$ are not inherently contradictory statements: If $S$ is the null set, both of these statements are vacuously true.
However, again, let's say $S$ is not the null set. Given $y_0 in S$, how do we derive a contradiction from these statements?
Well, use Universal Elimination on both universal statements to get $Py_0$ and $neg Py_0$. Then, use Contradiction Introduction to derive $bot$.
The original conditional is only true if $S$ is not the null set. Therefore, I think I answered 3 in my sidenote to 1.
answered Jan 29 at 1:59
Noble MushtakNoble Mushtak
15.3k1835
$endgroup$
add a comment |
$begingroup$
- No, it is not possible to prove this because if $S$ is the null set, then the hypothesis that $(forall y in S)(Py)$ will be true while the conclusion $(exists yin S)(Py)$ will be false since $S$ is not the null set.
However, let's say $S$ is not the null set. That is, we know of some $y_0$ such that $y_0in S$. Then, how do we go about proving this conditional?
Well, first we use Universal Elimination to go from $(forall y in S)(Py)$ to $Py_0$. Then, we use Existential Introduction to go from $Py_0$ to $(exists yin S)(Py)$
- No, this contradiction is also not provable because $(forall y in S)(Py)$ and $(forall yin S)(neg Py)$ are not inherently contradictory statements: If $S$ is the null set, both of these statements are vacuously true.
However, again, let's say $S$ is not the null set. Given $y_0 in S$, how do we derive a contradiction from these statements?
Well, use Universal Elimination on both universal statements to get $Py_0$ and $neg Py_0$. Then, use Contradiction Introduction to derive $bot$.
The original conditional is only true if $S$ is not the null set. Therefore, I think I answered 3 in my sidenote to 1.
answered Jan 29 at 1:59
Noble MushtakNoble Mushtak
15.3k1835
$endgroup$
add a comment |
$begingroup$
- No, it is not possible to prove this because if $S$ is the null set, then the hypothesis that $(forall y in S)(Py)$ will be true while the conclusion $(exists yin S)(Py)$ will be false since $S$ is not the null set.
However, let's say $S$ is not the null set. That is, we know of some $y_0$ such that $y_0in S$. Then, how do we go about proving this conditional?
Well, first we use Universal Elimination to go from $(forall y in S)(Py)$ to $Py_0$. Then, we use Existential Introduction to go from $Py_0$ to $(exists yin S)(Py)$
- No, this contradiction is also not provable because $(forall y in S)(Py)$ and $(forall yin S)(neg Py)$ are not inherently contradictory statements: If $S$ is the null set, both of these statements are vacuously true.
However, again, let's say $S$ is not the null set. Given $y_0 in S$, how do we derive a contradiction from these statements?
Well, use Universal Elimination on both universal statements to get $Py_0$ and $neg Py_0$. Then, use Contradiction Introduction to derive $bot$.
The original conditional is only true if $S$ is not the null set. Therefore, I think I answered 3 in my sidenote to 1.
answered Jan 29 at 1:59
Noble MushtakNoble Mushtak
15.3k1835
$endgroup$
- No, it is not possible to prove this because if $S$ is the null set, then the hypothesis that $(forall y in S)(Py)$ will be true while the conclusion $(exists yin S)(Py)$ will be false since $S$ is not the null set.
However, let's say $S$ is not the null set. That is, we know of some $y_0$ such that $y_0in S$. Then, how do we go about proving this conditional?
Well, first we use Universal Elimination to go from $(forall y in S)(Py)$ to $Py_0$. Then, we use Existential Introduction to go from $Py_0$ to $(exists yin S)(Py)$
- No, this contradiction is also not provable because $(forall y in S)(Py)$ and $(forall yin S)(neg Py)$ are not inherently contradictory statements: If $S$ is the null set, both of these statements are vacuously true.
However, again, let's say $S$ is not the null set. Given $y_0 in S$, how do we derive a contradiction from these statements?
Well, use Universal Elimination on both universal statements to get $Py_0$ and $neg Py_0$. Then, use Contradiction Introduction to derive $bot$.
The original conditional is only true if $S$ is not the null set. Therefore, I think I answered 3 in my sidenote to 1.
answered Jan 29 at 1:59
Noble MushtakNoble Mushtak
15.3k1835
answered Jan 29 at 1:59
Noble MushtakNoble Mushtak
15.3k1835
answered Jan 29 at 1:59
Noble MushtakNoble Mushtak
15.3k1835
answered Jan 29 at 1:59
Noble MushtakNoble Mushtak
15.3k1835
15.3k1835
add a comment |
add a comment |
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%2f3091622%2fproving-certain-obvious-tautologies-in-the-calculus-of-constructions%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
4
$begingroup$
The statement you're trying to prove isn't true in general, because there might not be anything of type $S$.
$endgroup$
– Andreas Blass
Jan 29 at 1:39
$begingroup$
Ah, I see! Yeah, wrapping that into $Pi text{witness} : S$ solves all of my problems! And the key difference between this and tautologies starting with $lnot Pi x : S. Px$ is that in order to fail a $forall$, an actual witness of the inverse must be present! Thanks!
$endgroup$
– 0xd34df00d
Jan 29 at 1:56