Predicate Logic Natural Deduction: $∃x P(x) ⊢P(x)$
$begingroup$
I am really puzzled right now.
To solve the issue, I need to prove this formular:
$$ exists x P(x) vdash P(x) $$
with the natural deduction rules for propositional and predicate logic.
I am sure this example should not be that difficult but, yep, now I am here.
For me, it should not be a counter example, so it should be solvable. I started to use exists elimination to get rid of the $exists$, but than I end up with something like this:
begin{align} exists x P(x) vdash P(x) \
1.& exists x P(x) text{(prem)} \
2.& P(x_0) text{($x_0$ fresh/free)} \
3.& dots (get x instead of x_0)\
4.& P(x)
end{align}
So I miss the little hint how I can transform the new variable to the existing one.
I hope someone can guide me.
Thank you.
logic first-order-logic predicate-logic natural-deduction formal-proofs
edited Dec 30 '18 at 18:07
Taroccoesbrocco
5,87471840
asked Dec 30 '18 at 13:40
whati001whati001
162
$endgroup$
|
show 4 more comments
$begingroup$
I am really puzzled right now.
To solve the issue, I need to prove this formular:
$$ exists x P(x) vdash P(x) $$
with the natural deduction rules for propositional and predicate logic.
I am sure this example should not be that difficult but, yep, now I am here.
For me, it should not be a counter example, so it should be solvable. I started to use exists elimination to get rid of the $exists$, but than I end up with something like this:
begin{align} exists x P(x) vdash P(x) \
1.& exists x P(x) text{(prem)} \
2.& P(x_0) text{($x_0$ fresh/free)} \
3.& dots (get x instead of x_0)\
4.& P(x)
end{align}
So I miss the little hint how I can transform the new variable to the existing one.
I hope someone can guide me.
Thank you.
logic first-order-logic predicate-logic natural-deduction formal-proofs
edited Dec 30 '18 at 18:07
Taroccoesbrocco
5,87471840
asked Dec 30 '18 at 13:40
whati001whati001
162
$endgroup$
$begingroup$
How are your rules defined? There are many systems of natural deduction, each with their own rules. And, given that $vdash$ means: 'can be derived using the rules of the system we're working with', we'd need to know those rules before we can help you.
$endgroup$
– Bram28
Dec 30 '18 at 14:17
7
$begingroup$
This should not be possible to derive. If, for example, we're working in $mathbb N$ and $P(x)$ is $x=0$, then $exists x(x=0)$ is true, but $x=0$ is not in general true -- and you shouldn't be able to derive anything but truths when you start with truths.
$endgroup$
– Henning Makholm
Dec 30 '18 at 14:24
$begingroup$
Rules: teaching.iaik.tugraz.at/_media/lub/deduction.pdf
$endgroup$
– whati001
Dec 30 '18 at 14:27
$begingroup$
@whati001 As Henning says, the statement you're trying to prove is false.
$endgroup$
– Alex Kruckman
Dec 30 '18 at 17:48
2
$begingroup$
It might be a good idea to backtrack to the problem you were trying to solve before setting your heart on proving the false claim presented above.
$endgroup$
– hardmath
Dec 30 '18 at 18:15
|
show 4 more comments
$begingroup$
I am really puzzled right now.
To solve the issue, I need to prove this formular:
$$ exists x P(x) vdash P(x) $$
with the natural deduction rules for propositional and predicate logic.
I am sure this example should not be that difficult but, yep, now I am here.
For me, it should not be a counter example, so it should be solvable. I started to use exists elimination to get rid of the $exists$, but than I end up with something like this:
begin{align} exists x P(x) vdash P(x) \
1.& exists x P(x) text{(prem)} \
2.& P(x_0) text{($x_0$ fresh/free)} \
3.& dots (get x instead of x_0)\
4.& P(x)
end{align}
So I miss the little hint how I can transform the new variable to the existing one.
I hope someone can guide me.
Thank you.
logic first-order-logic predicate-logic natural-deduction formal-proofs
edited Dec 30 '18 at 18:07
Taroccoesbrocco
5,87471840
asked Dec 30 '18 at 13:40
whati001whati001
162
$endgroup$
I am really puzzled right now.
To solve the issue, I need to prove this formular:
$$ exists x P(x) vdash P(x) $$
with the natural deduction rules for propositional and predicate logic.
I am sure this example should not be that difficult but, yep, now I am here.
For me, it should not be a counter example, so it should be solvable. I started to use exists elimination to get rid of the $exists$, but than I end up with something like this:
begin{align} exists x P(x) vdash P(x) \
1.& exists x P(x) text{(prem)} \
2.& P(x_0) text{($x_0$ fresh/free)} \
3.& dots (get x instead of x_0)\
4.& P(x)
end{align}
So I miss the little hint how I can transform the new variable to the existing one.
I hope someone can guide me.
Thank you.
logic first-order-logic predicate-logic natural-deduction formal-proofs
logic first-order-logic predicate-logic natural-deduction formal-proofs
edited Dec 30 '18 at 18:07
Taroccoesbrocco
5,87471840
asked Dec 30 '18 at 13:40
whati001whati001
162
edited Dec 30 '18 at 18:07
Taroccoesbrocco
5,87471840
asked Dec 30 '18 at 13:40
whati001whati001
162
edited Dec 30 '18 at 18:07
Taroccoesbrocco
5,87471840
edited Dec 30 '18 at 18:07
Taroccoesbrocco
5,87471840
edited Dec 30 '18 at 18:07
Taroccoesbrocco
5,87471840
5,87471840
asked Dec 30 '18 at 13:40
whati001whati001
162
asked Dec 30 '18 at 13:40
whati001whati001
162
asked Dec 30 '18 at 13:40
whati001whati001
162
162
$begingroup$
How are your rules defined? There are many systems of natural deduction, each with their own rules. And, given that $vdash$ means: 'can be derived using the rules of the system we're working with', we'd need to know those rules before we can help you.
$endgroup$
– Bram28
Dec 30 '18 at 14:17
7
$begingroup$
This should not be possible to derive. If, for example, we're working in $mathbb N$ and $P(x)$ is $x=0$, then $exists x(x=0)$ is true, but $x=0$ is not in general true -- and you shouldn't be able to derive anything but truths when you start with truths.
$endgroup$
– Henning Makholm
Dec 30 '18 at 14:24
$begingroup$
Rules: teaching.iaik.tugraz.at/_media/lub/deduction.pdf
$endgroup$
– whati001
Dec 30 '18 at 14:27
$begingroup$
@whati001 As Henning says, the statement you're trying to prove is false.
$endgroup$
– Alex Kruckman
Dec 30 '18 at 17:48
2
$begingroup$
It might be a good idea to backtrack to the problem you were trying to solve before setting your heart on proving the false claim presented above.
$endgroup$
– hardmath
Dec 30 '18 at 18:15
|
show 4 more comments
$begingroup$
How are your rules defined? There are many systems of natural deduction, each with their own rules. And, given that $vdash$ means: 'can be derived using the rules of the system we're working with', we'd need to know those rules before we can help you.
$endgroup$
– Bram28
Dec 30 '18 at 14:17
7
$begingroup$
This should not be possible to derive. If, for example, we're working in $mathbb N$ and $P(x)$ is $x=0$, then $exists x(x=0)$ is true, but $x=0$ is not in general true -- and you shouldn't be able to derive anything but truths when you start with truths.
$endgroup$
– Henning Makholm
Dec 30 '18 at 14:24
$begingroup$
Rules: teaching.iaik.tugraz.at/_media/lub/deduction.pdf
$endgroup$
– whati001
Dec 30 '18 at 14:27
$begingroup$
@whati001 As Henning says, the statement you're trying to prove is false.
$endgroup$
– Alex Kruckman
Dec 30 '18 at 17:48
2
$begingroup$
It might be a good idea to backtrack to the problem you were trying to solve before setting your heart on proving the false claim presented above.
$endgroup$
– hardmath
Dec 30 '18 at 18:15
$begingroup$
How are your rules defined? There are many systems of natural deduction, each with their own rules. And, given that $vdash$ means: 'can be derived using the rules of the system we're working with', we'd need to know those rules before we can help you.
$endgroup$
– Bram28
Dec 30 '18 at 14:17
$begingroup$
How are your rules defined? There are many systems of natural deduction, each with their own rules. And, given that $vdash$ means: 'can be derived using the rules of the system we're working with', we'd need to know those rules before we can help you.
$endgroup$
– Bram28
Dec 30 '18 at 14:17
7
7
$begingroup$
This should not be possible to derive. If, for example, we're working in $mathbb N$ and $P(x)$ is $x=0$, then $exists x(x=0)$ is true, but $x=0$ is not in general true -- and you shouldn't be able to derive anything but truths when you start with truths.
$endgroup$
– Henning Makholm
Dec 30 '18 at 14:24
$begingroup$
This should not be possible to derive. If, for example, we're working in $mathbb N$ and $P(x)$ is $x=0$, then $exists x(x=0)$ is true, but $x=0$ is not in general true -- and you shouldn't be able to derive anything but truths when you start with truths.
$endgroup$
– Henning Makholm
Dec 30 '18 at 14:24
$begingroup$
Rules: teaching.iaik.tugraz.at/_media/lub/deduction.pdf
$endgroup$
– whati001
Dec 30 '18 at 14:27
$begingroup$
Rules: teaching.iaik.tugraz.at/_media/lub/deduction.pdf
$endgroup$
– whati001
Dec 30 '18 at 14:27
$begingroup$
@whati001 As Henning says, the statement you're trying to prove is false.
$endgroup$
– Alex Kruckman
Dec 30 '18 at 17:48
$begingroup$
@whati001 As Henning says, the statement you're trying to prove is false.
$endgroup$
– Alex Kruckman
Dec 30 '18 at 17:48
2
2
$begingroup$
It might be a good idea to backtrack to the problem you were trying to solve before setting your heart on proving the false claim presented above.
$endgroup$
– hardmath
Dec 30 '18 at 18:15
$begingroup$
It might be a good idea to backtrack to the problem you were trying to solve before setting your heart on proving the false claim presented above.
$endgroup$
– hardmath
Dec 30 '18 at 18:15
|
show 4 more comments
1 Answer
1
active
oldest
votes
$begingroup$
As suggested by Henning Makholm's comment, $exists x P(x) vdash P(x)$ is not provable. If it were provable then you could take a derivation of $exists x P(x) vdash P(x)$ and, by applying the rule $forall_I$ in your list for natural deduction, you would get a derivation of $exists x P(x) vdash forall x P(x)$, which is not provable. Indeed, $exists x P(x) vdash forall x P(x)$ means that if there exists something with the property $P$ then everything has the property $P$, which is clearly falsifiable: take $mathbb{N}$ as domain, and let $P(x)$ be the property "$x$ is even", so that in this structure $exists x P(x)$ is true but $forall x P(x)$ is false.
Said differently, there is no way to fill the dots in your attempt of derivation, using natural deduction inference rules.
answered Dec 30 '18 at 18:01
TaroccoesbroccoTaroccoesbrocco
5,87471840
$endgroup$
add a comment |
Your Answer
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%2f3056842%2fpredicate-logic-natural-deduction-%25e2%2588%2583x-px-%25e2%258a%25a2px%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$
As suggested by Henning Makholm's comment, $exists x P(x) vdash P(x)$ is not provable. If it were provable then you could take a derivation of $exists x P(x) vdash P(x)$ and, by applying the rule $forall_I$ in your list for natural deduction, you would get a derivation of $exists x P(x) vdash forall x P(x)$, which is not provable. Indeed, $exists x P(x) vdash forall x P(x)$ means that if there exists something with the property $P$ then everything has the property $P$, which is clearly falsifiable: take $mathbb{N}$ as domain, and let $P(x)$ be the property "$x$ is even", so that in this structure $exists x P(x)$ is true but $forall x P(x)$ is false.
Said differently, there is no way to fill the dots in your attempt of derivation, using natural deduction inference rules.
answered Dec 30 '18 at 18:01
TaroccoesbroccoTaroccoesbrocco
5,87471840
$endgroup$
add a comment |
$begingroup$
As suggested by Henning Makholm's comment, $exists x P(x) vdash P(x)$ is not provable. If it were provable then you could take a derivation of $exists x P(x) vdash P(x)$ and, by applying the rule $forall_I$ in your list for natural deduction, you would get a derivation of $exists x P(x) vdash forall x P(x)$, which is not provable. Indeed, $exists x P(x) vdash forall x P(x)$ means that if there exists something with the property $P$ then everything has the property $P$, which is clearly falsifiable: take $mathbb{N}$ as domain, and let $P(x)$ be the property "$x$ is even", so that in this structure $exists x P(x)$ is true but $forall x P(x)$ is false.
Said differently, there is no way to fill the dots in your attempt of derivation, using natural deduction inference rules.
answered Dec 30 '18 at 18:01
TaroccoesbroccoTaroccoesbrocco
5,87471840
$endgroup$
add a comment |
$begingroup$
As suggested by Henning Makholm's comment, $exists x P(x) vdash P(x)$ is not provable. If it were provable then you could take a derivation of $exists x P(x) vdash P(x)$ and, by applying the rule $forall_I$ in your list for natural deduction, you would get a derivation of $exists x P(x) vdash forall x P(x)$, which is not provable. Indeed, $exists x P(x) vdash forall x P(x)$ means that if there exists something with the property $P$ then everything has the property $P$, which is clearly falsifiable: take $mathbb{N}$ as domain, and let $P(x)$ be the property "$x$ is even", so that in this structure $exists x P(x)$ is true but $forall x P(x)$ is false.
Said differently, there is no way to fill the dots in your attempt of derivation, using natural deduction inference rules.
answered Dec 30 '18 at 18:01
TaroccoesbroccoTaroccoesbrocco
5,87471840
$endgroup$
As suggested by Henning Makholm's comment, $exists x P(x) vdash P(x)$ is not provable. If it were provable then you could take a derivation of $exists x P(x) vdash P(x)$ and, by applying the rule $forall_I$ in your list for natural deduction, you would get a derivation of $exists x P(x) vdash forall x P(x)$, which is not provable. Indeed, $exists x P(x) vdash forall x P(x)$ means that if there exists something with the property $P$ then everything has the property $P$, which is clearly falsifiable: take $mathbb{N}$ as domain, and let $P(x)$ be the property "$x$ is even", so that in this structure $exists x P(x)$ is true but $forall x P(x)$ is false.
Said differently, there is no way to fill the dots in your attempt of derivation, using natural deduction inference rules.
answered Dec 30 '18 at 18:01
TaroccoesbroccoTaroccoesbrocco
5,87471840
edited Dec 30 '18 at 18:10
answered Dec 30 '18 at 18:01
TaroccoesbroccoTaroccoesbrocco
5,87471840
answered Dec 30 '18 at 18:01
TaroccoesbroccoTaroccoesbrocco
5,87471840
answered Dec 30 '18 at 18:01
TaroccoesbroccoTaroccoesbrocco
5,87471840
5,87471840
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%2f3056842%2fpredicate-logic-natural-deduction-%25e2%2588%2583x-px-%25e2%258a%25a2px%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$
How are your rules defined? There are many systems of natural deduction, each with their own rules. And, given that $vdash$ means: 'can be derived using the rules of the system we're working with', we'd need to know those rules before we can help you.
$endgroup$
– Bram28
Dec 30 '18 at 14:17
7
$begingroup$
This should not be possible to derive. If, for example, we're working in $mathbb N$ and $P(x)$ is $x=0$, then $exists x(x=0)$ is true, but $x=0$ is not in general true -- and you shouldn't be able to derive anything but truths when you start with truths.
$endgroup$
– Henning Makholm
Dec 30 '18 at 14:24
$begingroup$
Rules: teaching.iaik.tugraz.at/_media/lub/deduction.pdf
$endgroup$
– whati001
Dec 30 '18 at 14:27
$begingroup$
@whati001 As Henning says, the statement you're trying to prove is false.
$endgroup$
– Alex Kruckman
Dec 30 '18 at 17:48
2
$begingroup$
It might be a good idea to backtrack to the problem you were trying to solve before setting your heart on proving the false claim presented above.
$endgroup$
– hardmath
Dec 30 '18 at 18:15