Natural deduction: predicate logic proof (Prenex form)

I'm pretty familiar with proofs in propositional logic, but not so much with predicate logic.

I'm trying to prove the following (which can be used during construction of prenex normal form).

If $x$ is not free in $psi$, then:
$forall xphirightarrow psi $
if and only if
$exists x(phi rightarrow psi)$

I personally use tree proofs, but any notation is fine.
I don't really know how to start this one to be honest.

edited Jan 24 at 13:06

Taroccoesbrocco

5,64271840

asked Nov 27 '18 at 20:10

NaborDH

304

add a comment |

I'm pretty familiar with proofs in propositional logic, but not so much with predicate logic.

I'm trying to prove the following (which can be used during construction of prenex normal form).

If $x$ is not free in $psi$, then:
$forall xphirightarrow psi $
if and only if
$exists x(phi rightarrow psi)$

I personally use tree proofs, but any notation is fine.
I don't really know how to start this one to be honest.

edited Jan 24 at 13:06

Taroccoesbrocco

5,64271840

asked Nov 27 '18 at 20:10

NaborDH

304

add a comment |

I'm pretty familiar with proofs in propositional logic, but not so much with predicate logic.

I'm trying to prove the following (which can be used during construction of prenex normal form).

If $x$ is not free in $psi$, then:
$forall xphirightarrow psi $
if and only if
$exists x(phi rightarrow psi)$

I personally use tree proofs, but any notation is fine.
I don't really know how to start this one to be honest.

edited Jan 24 at 13:06

Taroccoesbrocco

5,64271840

asked Nov 27 '18 at 20:10

NaborDH

304

I'm pretty familiar with proofs in propositional logic, but not so much with predicate logic.

I'm trying to prove the following (which can be used during construction of prenex normal form).

If $x$ is not free in $psi$, then:
$forall xphirightarrow psi $
if and only if
$exists x(phi rightarrow psi)$

I personally use tree proofs, but any notation is fine.
I don't really know how to start this one to be honest.

logic first-order-logic predicate-logic natural-deduction formal-proofs

edited Jan 24 at 13:06

Taroccoesbrocco

5,64271840

asked Nov 27 '18 at 20:10

NaborDH

304

edited Jan 24 at 13:06

Taroccoesbrocco

5,64271840

asked Nov 27 '18 at 20:10

NaborDH

304

edited Jan 24 at 13:06

Taroccoesbrocco

5,64271840

edited Jan 24 at 13:06

Taroccoesbrocco

5,64271840

edited Jan 24 at 13:06

Taroccoesbrocco

5,64271840

asked Nov 27 '18 at 20:10

NaborDH

304

asked Nov 27 '18 at 20:10

NaborDH

304

asked Nov 27 '18 at 20:10

NaborDH

304

add a comment |

2 Answers
2

active

oldest

votes

Here's a proof sketch for the "if" direction, where the proof more or less writes itself. Obviously you have to use $exists$-Elim, since you have an $exists$ premiss which you need to make use of. So you already know the proof has to look like this (Fitch style --re-arrange for a tree!)

$exists x(phi(x) to psi)\
quadquad |quad phi(a) to psi\
quadquad |quad vdots\
quadquad |quad forall xphi(x) to psi\
forall xvarphi(x) to psi$

Then how to fill in the dots is pretty obvious since you'll have to use Conditional Proof -- i.e. assume the antecedent of the conditional you want to prove and aim for the consequent. Easy!

The other direction is trickier. But try using reductio (always a good plan if nothing else looks an obvious move) so the overall shape of the proof will look like this:

$forall xvarphi(x) to psi\
quadquad |quad negexists x(phi(x) to psi)\
quadquad |quad vdots\
quadquad |quad bot\
negnegexists x(phi(x) to psi)\
exists x(phi(x) to psi)$

You can complete the proof like this (think through why this is now an obvious way, and what justifies each step).

Fill in the dots by propositional calculus reasoning. $forall$ intro is justified from $phi(a)$ since $a$ appears in no undischarged assumption on which $phi(a)$ depends.

edited Nov 30 '18 at 13:47

answered Nov 27 '18 at 23:31

Peter Smith

40.9k340120

$begingroup$
Thank you for the very clear explanation.
$endgroup$
– NaborDH
Nov 29 '18 at 20:34

add a comment |

-1

Here's an informal deduction. Express it in your own formal system.

Take the premise: $forall x~phi ~to~psi$

Derive the contraposition: $lnotpsitolnotforall x~phi$

Assuming $lnotpsi$, derive that there is some $x$ where $lnotphi$.

Deduce then that, there is some $x$ where $lnotpsitolnotphi$, which is to say $phitopsi$

Therefore $exists x~(phitopsi)$ is derived from the premise

Take the premise: $exists x~(phitopsi)$

Thence there is some witness $x$ where $phitopsi$ holds

Assuming $forall x~phi$, derive that for the witness, $phi$ holds, and apply modus ponens.

Thus deduce that $forall x~phi ~to~psi$ is derivable from the premise.

edited Nov 27 '18 at 23:28

answered Nov 27 '18 at 23:03

Graham Kemp

86.8k43579

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
});

}
});

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});

Post as a guest

Name

Required, but never shown

StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3016248%2fnatural-deduction-predicate-logic-proof-prenex-form%23new-answer', 'question_page');
}
);

Post as a guest

Name

Required, but never shown

2 Answers
2

active

oldest

votes

2 Answers
2

active

oldest

votes

$exists x(phi(x) to psi)\
quadquad |quad phi(a) to psi\
quadquad |quad vdots\
quadquad |quad forall xphi(x) to psi\
forall xvarphi(x) to psi$

Then how to fill in the dots is pretty obvious since you'll have to use Conditional Proof -- i.e. assume the antecedent of the conditional you want to prove and aim for the consequent. Easy!

The other direction is trickier. But try using reductio (always a good plan if nothing else looks an obvious move) so the overall shape of the proof will look like this:

$forall xvarphi(x) to psi\
quadquad |quad negexists x(phi(x) to psi)\
quadquad |quad vdots\
quadquad |quad bot\
negnegexists x(phi(x) to psi)\
exists x(phi(x) to psi)$

You can complete the proof like this (think through why this is now an obvious way, and what justifies each step).

Fill in the dots by propositional calculus reasoning. $forall$ intro is justified from $phi(a)$ since $a$ appears in no undischarged assumption on which $phi(a)$ depends.

edited Nov 30 '18 at 13:47

answered Nov 27 '18 at 23:31

Peter Smith

40.9k340120

$begingroup$
Thank you for the very clear explanation.
$endgroup$
– NaborDH
Nov 29 '18 at 20:34

add a comment |

$exists x(phi(x) to psi)\
quadquad |quad phi(a) to psi\
quadquad |quad vdots\
quadquad |quad forall xphi(x) to psi\
forall xvarphi(x) to psi$

Then how to fill in the dots is pretty obvious since you'll have to use Conditional Proof -- i.e. assume the antecedent of the conditional you want to prove and aim for the consequent. Easy!

The other direction is trickier. But try using reductio (always a good plan if nothing else looks an obvious move) so the overall shape of the proof will look like this:

$forall xvarphi(x) to psi\
quadquad |quad negexists x(phi(x) to psi)\
quadquad |quad vdots\
quadquad |quad bot\
negnegexists x(phi(x) to psi)\
exists x(phi(x) to psi)$

You can complete the proof like this (think through why this is now an obvious way, and what justifies each step).

Fill in the dots by propositional calculus reasoning. $forall$ intro is justified from $phi(a)$ since $a$ appears in no undischarged assumption on which $phi(a)$ depends.

edited Nov 30 '18 at 13:47

answered Nov 27 '18 at 23:31

Peter Smith

40.9k340120

$begingroup$
Thank you for the very clear explanation.
$endgroup$
– NaborDH
Nov 29 '18 at 20:34

add a comment |

$exists x(phi(x) to psi)\
quadquad |quad phi(a) to psi\
quadquad |quad vdots\
quadquad |quad forall xphi(x) to psi\
forall xvarphi(x) to psi$

Then how to fill in the dots is pretty obvious since you'll have to use Conditional Proof -- i.e. assume the antecedent of the conditional you want to prove and aim for the consequent. Easy!

The other direction is trickier. But try using reductio (always a good plan if nothing else looks an obvious move) so the overall shape of the proof will look like this:

$forall xvarphi(x) to psi\
quadquad |quad negexists x(phi(x) to psi)\
quadquad |quad vdots\
quadquad |quad bot\
negnegexists x(phi(x) to psi)\
exists x(phi(x) to psi)$

You can complete the proof like this (think through why this is now an obvious way, and what justifies each step).

Fill in the dots by propositional calculus reasoning. $forall$ intro is justified from $phi(a)$ since $a$ appears in no undischarged assumption on which $phi(a)$ depends.

edited Nov 30 '18 at 13:47

answered Nov 27 '18 at 23:31

Peter Smith

40.9k340120

$exists x(phi(x) to psi)\
quadquad |quad phi(a) to psi\
quadquad |quad vdots\
quadquad |quad forall xphi(x) to psi\
forall xvarphi(x) to psi$

Then how to fill in the dots is pretty obvious since you'll have to use Conditional Proof -- i.e. assume the antecedent of the conditional you want to prove and aim for the consequent. Easy!

The other direction is trickier. But try using reductio (always a good plan if nothing else looks an obvious move) so the overall shape of the proof will look like this:

$forall xvarphi(x) to psi\
quadquad |quad negexists x(phi(x) to psi)\
quadquad |quad vdots\
quadquad |quad bot\
negnegexists x(phi(x) to psi)\
exists x(phi(x) to psi)$

You can complete the proof like this (think through why this is now an obvious way, and what justifies each step).

Fill in the dots by propositional calculus reasoning. $forall$ intro is justified from $phi(a)$ since $a$ appears in no undischarged assumption on which $phi(a)$ depends.

edited Nov 30 '18 at 13:47

answered Nov 27 '18 at 23:31

Peter Smith

40.9k340120

edited Nov 30 '18 at 13:47

answered Nov 27 '18 at 23:31

Peter Smith

40.9k340120

answered Nov 27 '18 at 23:31

Peter Smith

40.9k340120

answered Nov 27 '18 at 23:31

Peter Smith

40.9k340120

$begingroup$
Thank you for the very clear explanation.
$endgroup$
– NaborDH
Nov 29 '18 at 20:34

add a comment |

$begingroup$
Thank you for the very clear explanation.
$endgroup$
– NaborDH
Nov 29 '18 at 20:34

Thank you for the very clear explanation.

– NaborDH
Nov 29 '18 at 20:34

add a comment |

-1

Here's an informal deduction. Express it in your own formal system.

Take the premise: $forall x~phi ~to~psi$

Derive the contraposition: $lnotpsitolnotforall x~phi$

Assuming $lnotpsi$, derive that there is some $x$ where $lnotphi$.

Deduce then that, there is some $x$ where $lnotpsitolnotphi$, which is to say $phitopsi$

Therefore $exists x~(phitopsi)$ is derived from the premise

Take the premise: $exists x~(phitopsi)$

Thence there is some witness $x$ where $phitopsi$ holds

Assuming $forall x~phi$, derive that for the witness, $phi$ holds, and apply modus ponens.

Thus deduce that $forall x~phi ~to~psi$ is derivable from the premise.

edited Nov 27 '18 at 23:28

answered Nov 27 '18 at 23:03

Graham Kemp

86.8k43579

add a comment |

-1

Here's an informal deduction. Express it in your own formal system.

Take the premise: $forall x~phi ~to~psi$

Derive the contraposition: $lnotpsitolnotforall x~phi$

Assuming $lnotpsi$, derive that there is some $x$ where $lnotphi$.

Deduce then that, there is some $x$ where $lnotpsitolnotphi$, which is to say $phitopsi$

Therefore $exists x~(phitopsi)$ is derived from the premise

Take the premise: $exists x~(phitopsi)$

Thence there is some witness $x$ where $phitopsi$ holds

Assuming $forall x~phi$, derive that for the witness, $phi$ holds, and apply modus ponens.

Thus deduce that $forall x~phi ~to~psi$ is derivable from the premise.

edited Nov 27 '18 at 23:28

answered Nov 27 '18 at 23:03

Graham Kemp

86.8k43579

add a comment |

-1

Here's an informal deduction. Express it in your own formal system.

Take the premise: $forall x~phi ~to~psi$

Derive the contraposition: $lnotpsitolnotforall x~phi$

Assuming $lnotpsi$, derive that there is some $x$ where $lnotphi$.

Deduce then that, there is some $x$ where $lnotpsitolnotphi$, which is to say $phitopsi$

Therefore $exists x~(phitopsi)$ is derived from the premise

Take the premise: $exists x~(phitopsi)$

Thence there is some witness $x$ where $phitopsi$ holds

Assuming $forall x~phi$, derive that for the witness, $phi$ holds, and apply modus ponens.

Thus deduce that $forall x~phi ~to~psi$ is derivable from the premise.

edited Nov 27 '18 at 23:28

answered Nov 27 '18 at 23:03

Graham Kemp

86.8k43579

Here's an informal deduction. Express it in your own formal system.

Take the premise: $forall x~phi ~to~psi$

Derive the contraposition: $lnotpsitolnotforall x~phi$

Assuming $lnotpsi$, derive that there is some $x$ where $lnotphi$.

Deduce then that, there is some $x$ where $lnotpsitolnotphi$, which is to say $phitopsi$

Therefore $exists x~(phitopsi)$ is derived from the premise

Take the premise: $exists x~(phitopsi)$

Thence there is some witness $x$ where $phitopsi$ holds

Assuming $forall x~phi$, derive that for the witness, $phi$ holds, and apply modus ponens.

Thus deduce that $forall x~phi ~to~psi$ is derivable from the premise.

edited Nov 27 '18 at 23:28

answered Nov 27 '18 at 23:03

Graham Kemp

86.8k43579

edited Nov 27 '18 at 23:28

answered Nov 27 '18 at 23:03

Graham Kemp

86.8k43579

answered Nov 27 '18 at 23:03

Graham Kemp

86.8k43579

answered Nov 27 '18 at 23:03

Graham Kemp

86.8k43579

add a comment |

draft saved

draft discarded

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.

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});

Post as a guest

Name

Required, but never shown

Post as a guest

Name

Required, but never shown

Sign up or log in

StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});

Post as a guest

Name

Required, but never shown

Sign up or log in

StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});

Post as a guest

Name

Required, but never shown

Sign up or log in

StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});

Post as a guest

Name

Required, but never shown

Name

Required, but never shown

Name

Required, but never shown

This page is only for reference, If you need detailed information, please check here

Search This Blog

Ufyukyu