Mixing
Proving ∀x(A(x) ∨ B) → ∀xA(x) ∨ B, with x is not in B, by natural deduction
how can prove ∀x(A(x) ∨ B) → ∀xA(x) ∨ B where x is not in B using natural deduction.
i am not sure how should use for all introduction rule here.
any help wpuld be highly appreciate.
Cheers
logic first-order-logic natural-deduction
asked Nov 21 '18 at 16:06
Norman
167
|
show 1 more comment
how can prove ∀x(A(x) ∨ B) → ∀xA(x) ∨ B where x is not in B using natural deduction.
i am not sure how should use for all introduction rule here.
any help wpuld be highly appreciate.
Cheers
logic first-order-logic natural-deduction
asked Nov 21 '18 at 16:06
Norman
167
2
I think you need some variation of the law of excluded middle here. If $B$ is true, then you're done. But if $B$ is false then $A(x)lor B$ implies $A(x)$.
– Henning Makholm
Nov 21 '18 at 16:13
1
What are the rules of the system you have to work with? there are many different systems of this kind, each with slightly different rules.
– Bram28
Nov 21 '18 at 19:47
@Hennnin Makholm. No, LEM is not needed here.
– Graham Kemp
Nov 21 '18 at 22:29
@GrahamKemp I'm pretty sure the statement isn't valid in intuitionistic first-order logic. For example (heuristic argument, might not be a full proof) in the topos $mathbb{R}$, if $A_n = (-infty, frac{1}{n})$ and $B = (0, infty)$, then $forall n in mathbb{N}, (A_n vee B)$ would be $mathbb{R}$ whereas $(forall n in mathbb{N}, A_n) vee B$ would be $(-infty, 0) cup (0, infty)$. Or, in terms of a computability interpretation: even if you had a computable function which for each $x$ returns a proof of $A(x)$ or a proof of $B$...
– Daniel Schepler
Nov 21 '18 at 23:17
in general you wouldn't be able to compute whether the function ever returns a proof of $B$, or whether it always returns a proof of $A(x)$.
– Daniel Schepler
Nov 21 '18 at 23:18
|
show 1 more comment
how can prove ∀x(A(x) ∨ B) → ∀xA(x) ∨ B where x is not in B using natural deduction.
i am not sure how should use for all introduction rule here.
any help wpuld be highly appreciate.
Cheers
logic first-order-logic natural-deduction
asked Nov 21 '18 at 16:06
Norman
167
how can prove ∀x(A(x) ∨ B) → ∀xA(x) ∨ B where x is not in B using natural deduction.
i am not sure how should use for all introduction rule here.
any help wpuld be highly appreciate.
Cheers
logic first-order-logic natural-deduction
logic first-order-logic natural-deduction
asked Nov 21 '18 at 16:06
Norman
167
asked Nov 21 '18 at 16:06
Norman
167
asked Nov 21 '18 at 16:06
Norman
167
asked Nov 21 '18 at 16:06
Norman
167
asked Nov 21 '18 at 16:06
Norman
167
167
2
I think you need some variation of the law of excluded middle here. If $B$ is true, then you're done. But if $B$ is false then $A(x)lor B$ implies $A(x)$.
– Henning Makholm
Nov 21 '18 at 16:13
1
What are the rules of the system you have to work with? there are many different systems of this kind, each with slightly different rules.
– Bram28
Nov 21 '18 at 19:47
@Hennnin Makholm. No, LEM is not needed here.
– Graham Kemp
Nov 21 '18 at 22:29
@GrahamKemp I'm pretty sure the statement isn't valid in intuitionistic first-order logic. For example (heuristic argument, might not be a full proof) in the topos $mathbb{R}$, if $A_n = (-infty, frac{1}{n})$ and $B = (0, infty)$, then $forall n in mathbb{N}, (A_n vee B)$ would be $mathbb{R}$ whereas $(forall n in mathbb{N}, A_n) vee B$ would be $(-infty, 0) cup (0, infty)$. Or, in terms of a computability interpretation: even if you had a computable function which for each $x$ returns a proof of $A(x)$ or a proof of $B$...
– Daniel Schepler
Nov 21 '18 at 23:17
in general you wouldn't be able to compute whether the function ever returns a proof of $B$, or whether it always returns a proof of $A(x)$.
– Daniel Schepler
Nov 21 '18 at 23:18
|
show 1 more comment
2
I think you need some variation of the law of excluded middle here. If $B$ is true, then you're done. But if $B$ is false then $A(x)lor B$ implies $A(x)$.
– Henning Makholm
Nov 21 '18 at 16:13
1
What are the rules of the system you have to work with? there are many different systems of this kind, each with slightly different rules.
– Bram28
Nov 21 '18 at 19:47
@Hennnin Makholm. No, LEM is not needed here.
– Graham Kemp
Nov 21 '18 at 22:29
@GrahamKemp I'm pretty sure the statement isn't valid in intuitionistic first-order logic. For example (heuristic argument, might not be a full proof) in the topos $mathbb{R}$, if $A_n = (-infty, frac{1}{n})$ and $B = (0, infty)$, then $forall n in mathbb{N}, (A_n vee B)$ would be $mathbb{R}$ whereas $(forall n in mathbb{N}, A_n) vee B$ would be $(-infty, 0) cup (0, infty)$. Or, in terms of a computability interpretation: even if you had a computable function which for each $x$ returns a proof of $A(x)$ or a proof of $B$...
– Daniel Schepler
Nov 21 '18 at 23:17
in general you wouldn't be able to compute whether the function ever returns a proof of $B$, or whether it always returns a proof of $A(x)$.
– Daniel Schepler
Nov 21 '18 at 23:18
2
2
I think you need some variation of the law of excluded middle here. If $B$ is true, then you're done. But if $B$ is false then $A(x)lor B$ implies $A(x)$.
– Henning Makholm
Nov 21 '18 at 16:13
I think you need some variation of the law of excluded middle here. If $B$ is true, then you're done. But if $B$ is false then $A(x)lor B$ implies $A(x)$.
– Henning Makholm
Nov 21 '18 at 16:13
1
1
What are the rules of the system you have to work with? there are many different systems of this kind, each with slightly different rules.
– Bram28
Nov 21 '18 at 19:47
What are the rules of the system you have to work with? there are many different systems of this kind, each with slightly different rules.
– Bram28
Nov 21 '18 at 19:47
@Hennnin Makholm. No, LEM is not needed here.
– Graham Kemp
Nov 21 '18 at 22:29
@Hennnin Makholm. No, LEM is not needed here.
– Graham Kemp
Nov 21 '18 at 22:29
@GrahamKemp I'm pretty sure the statement isn't valid in intuitionistic first-order logic. For example (heuristic argument, might not be a full proof) in the topos $mathbb{R}$, if $A_n = (-infty, frac{1}{n})$ and $B = (0, infty)$, then $forall n in mathbb{N}, (A_n vee B)$ would be $mathbb{R}$ whereas $(forall n in mathbb{N}, A_n) vee B$ would be $(-infty, 0) cup (0, infty)$. Or, in terms of a computability interpretation: even if you had a computable function which for each $x$ returns a proof of $A(x)$ or a proof of $B$...
– Daniel Schepler
Nov 21 '18 at 23:17
@GrahamKemp I'm pretty sure the statement isn't valid in intuitionistic first-order logic. For example (heuristic argument, might not be a full proof) in the topos $mathbb{R}$, if $A_n = (-infty, frac{1}{n})$ and $B = (0, infty)$, then $forall n in mathbb{N}, (A_n vee B)$ would be $mathbb{R}$ whereas $(forall n in mathbb{N}, A_n) vee B$ would be $(-infty, 0) cup (0, infty)$. Or, in terms of a computability interpretation: even if you had a computable function which for each $x$ returns a proof of $A(x)$ or a proof of $B$...
– Daniel Schepler
Nov 21 '18 at 23:17
in general you wouldn't be able to compute whether the function ever returns a proof of $B$, or whether it always returns a proof of $A(x)$.
– Daniel Schepler
Nov 21 '18 at 23:18
in general you wouldn't be able to compute whether the function ever returns a proof of $B$, or whether it always returns a proof of $A(x)$.
– Daniel Schepler
Nov 21 '18 at 23:18
|
show 1 more comment
1 Answer
1
active
oldest
votes
If you are using a Fitch style proof system (i.e. One with Introduction and Elimination rules), I would set this up as a proof by contradiction: Assume $neg (forall x A(x) lor B)$, use your rules to derive $neg forall x A(x))$ and $neg B$, and use those in combination with your $forall x (A(x) lor B)$ to derive a contradiction (this should not be hard: from $neg forall x A(x)$ you should be able to derive $exists x neg A(x)$ (this may require its own proof by contradiction), then witness that existential with an $a$ to get $neg A(a)$, instantiate the universal to get $(A(a) lor B)$, and combine those two and the $neg B$ to get the contradiction)
answered Nov 21 '18 at 19:54
Bram28
60.3k44590
Example proof: pastebin.com/raw/2pZGPusy
– Quelklef
Nov 24 '18 at 21:54
@quelklef Very nice!
– Bram28
Nov 24 '18 at 22:00
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%2f3007927%2fproving-%25e2%2588%2580xax-%25e2%2588%25a8-b-%25e2%2586%2592-%25e2%2588%2580xax-%25e2%2588%25a8-b-with-x-is-not-in-b-by-natural-deduction%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
If you are using a Fitch style proof system (i.e. One with Introduction and Elimination rules), I would set this up as a proof by contradiction: Assume $neg (forall x A(x) lor B)$, use your rules to derive $neg forall x A(x))$ and $neg B$, and use those in combination with your $forall x (A(x) lor B)$ to derive a contradiction (this should not be hard: from $neg forall x A(x)$ you should be able to derive $exists x neg A(x)$ (this may require its own proof by contradiction), then witness that existential with an $a$ to get $neg A(a)$, instantiate the universal to get $(A(a) lor B)$, and combine those two and the $neg B$ to get the contradiction)
answered Nov 21 '18 at 19:54
Bram28
60.3k44590
Example proof: pastebin.com/raw/2pZGPusy
– Quelklef
Nov 24 '18 at 21:54
@quelklef Very nice!
– Bram28
Nov 24 '18 at 22:00
add a comment |
If you are using a Fitch style proof system (i.e. One with Introduction and Elimination rules), I would set this up as a proof by contradiction: Assume $neg (forall x A(x) lor B)$, use your rules to derive $neg forall x A(x))$ and $neg B$, and use those in combination with your $forall x (A(x) lor B)$ to derive a contradiction (this should not be hard: from $neg forall x A(x)$ you should be able to derive $exists x neg A(x)$ (this may require its own proof by contradiction), then witness that existential with an $a$ to get $neg A(a)$, instantiate the universal to get $(A(a) lor B)$, and combine those two and the $neg B$ to get the contradiction)
answered Nov 21 '18 at 19:54
Bram28
60.3k44590
Example proof: pastebin.com/raw/2pZGPusy
– Quelklef
Nov 24 '18 at 21:54
@quelklef Very nice!
– Bram28
Nov 24 '18 at 22:00
add a comment |
If you are using a Fitch style proof system (i.e. One with Introduction and Elimination rules), I would set this up as a proof by contradiction: Assume $neg (forall x A(x) lor B)$, use your rules to derive $neg forall x A(x))$ and $neg B$, and use those in combination with your $forall x (A(x) lor B)$ to derive a contradiction (this should not be hard: from $neg forall x A(x)$ you should be able to derive $exists x neg A(x)$ (this may require its own proof by contradiction), then witness that existential with an $a$ to get $neg A(a)$, instantiate the universal to get $(A(a) lor B)$, and combine those two and the $neg B$ to get the contradiction)
answered Nov 21 '18 at 19:54
Bram28
60.3k44590
If you are using a Fitch style proof system (i.e. One with Introduction and Elimination rules), I would set this up as a proof by contradiction: Assume $neg (forall x A(x) lor B)$, use your rules to derive $neg forall x A(x))$ and $neg B$, and use those in combination with your $forall x (A(x) lor B)$ to derive a contradiction (this should not be hard: from $neg forall x A(x)$ you should be able to derive $exists x neg A(x)$ (this may require its own proof by contradiction), then witness that existential with an $a$ to get $neg A(a)$, instantiate the universal to get $(A(a) lor B)$, and combine those two and the $neg B$ to get the contradiction)
answered Nov 21 '18 at 19:54
Bram28
60.3k44590
edited Nov 21 '18 at 23:07
answered Nov 21 '18 at 19:54
Bram28
60.3k44590
answered Nov 21 '18 at 19:54
Bram28
60.3k44590
answered Nov 21 '18 at 19:54
Bram28
60.3k44590
60.3k44590
Example proof: pastebin.com/raw/2pZGPusy
– Quelklef
Nov 24 '18 at 21:54
@quelklef Very nice!
– Bram28
Nov 24 '18 at 22:00
add a comment |
Example proof: pastebin.com/raw/2pZGPusy
– Quelklef
Nov 24 '18 at 21:54
@quelklef Very nice!
– Bram28
Nov 24 '18 at 22:00
Example proof: pastebin.com/raw/2pZGPusy
– Quelklef
Nov 24 '18 at 21:54
Example proof: pastebin.com/raw/2pZGPusy
– Quelklef
Nov 24 '18 at 21:54
@quelklef Very nice!
– Bram28
Nov 24 '18 at 22:00
@quelklef Very nice!
– Bram28
Nov 24 '18 at 22:00
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.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- 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.
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%2f3007927%2fproving-%25e2%2588%2580xax-%25e2%2588%25a8-b-%25e2%2586%2592-%25e2%2588%2580xax-%25e2%2588%25a8-b-with-x-is-not-in-b-by-natural-deduction%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
I think you need some variation of the law of excluded middle here. If $B$ is true, then you're done. But if $B$ is false then $A(x)lor B$ implies $A(x)$.
– Henning Makholm
Nov 21 '18 at 16:13
1
What are the rules of the system you have to work with? there are many different systems of this kind, each with slightly different rules.
– Bram28
Nov 21 '18 at 19:47
@Hennnin Makholm. No, LEM is not needed here.
– Graham Kemp
Nov 21 '18 at 22:29
@GrahamKemp I'm pretty sure the statement isn't valid in intuitionistic first-order logic. For example (heuristic argument, might not be a full proof) in the topos $mathbb{R}$, if $A_n = (-infty, frac{1}{n})$ and $B = (0, infty)$, then $forall n in mathbb{N}, (A_n vee B)$ would be $mathbb{R}$ whereas $(forall n in mathbb{N}, A_n) vee B$ would be $(-infty, 0) cup (0, infty)$. Or, in terms of a computability interpretation: even if you had a computable function which for each $x$ returns a proof of $A(x)$ or a proof of $B$...
– Daniel Schepler
Nov 21 '18 at 23:17
in general you wouldn't be able to compute whether the function ever returns a proof of $B$, or whether it always returns a proof of $A(x)$.
– Daniel Schepler
Nov 21 '18 at 23:18