Induction with two variables in PA











up vote
1
down vote

favorite












This probably has been asked before, but apologies, I don't know how to locate it. I want to prove $forall x,y: P(x, y)$. My premises are:



$$P(0, 0) wedge \
[forall x: P(x, 0)] wedge \
[forall y: P(0, y)] wedge \
[forall x,y: P(x, y) Rightarrow P(Suc(x), Suc(y))]$$



I can prove some basic facts in PA, such as addition is comm, assoc, etc. I can also prove things about less than, such as less than is transitive. Also, if x is less than or equal to y, then there exists a z such x + z = y. But I'm not good at induction with two variables, and so cannot complete the proof.










share|cite|improve this question









New contributor




anon44508 is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.




















  • Not necessarily by double induction. You can prove $forall y P(n,y)$ by induction on $y$, with $n$ whatever. If the proof works without any specific assumption regarding $n$, you can generalize on it, getting : $forall x forall y P(x,y)$.
    – Mauro ALLEGRANZA
    Dec 2 at 13:24










  • See also the post : Induction on two integer variables.
    – Mauro ALLEGRANZA
    Dec 2 at 13:27












  • See also : Mathematical induction: variants and subtleties.
    – Mauro ALLEGRANZA
    Dec 2 at 13:28










  • $P(n, 0)$ is proven by the second assumption. However, I don't see how $forall y : P(n, y) Rightarrow P(n, Suc(y))$ is proven, because I only have $forall n, y : P(n, y) Rightarrow P(Suc(n), Suc(y))$. What am I not grasping? Also, I've seen those two links before, but thank you for sending them as they definitely contain helpful tricks for proof by induction.
    – anon44508
    Dec 2 at 14:27












  • Nevermind, the other contributor cleared it all up. Thank you for your help.
    – anon44508
    Dec 3 at 2:36















up vote
1
down vote

favorite












This probably has been asked before, but apologies, I don't know how to locate it. I want to prove $forall x,y: P(x, y)$. My premises are:



$$P(0, 0) wedge \
[forall x: P(x, 0)] wedge \
[forall y: P(0, y)] wedge \
[forall x,y: P(x, y) Rightarrow P(Suc(x), Suc(y))]$$



I can prove some basic facts in PA, such as addition is comm, assoc, etc. I can also prove things about less than, such as less than is transitive. Also, if x is less than or equal to y, then there exists a z such x + z = y. But I'm not good at induction with two variables, and so cannot complete the proof.










share|cite|improve this question









New contributor




anon44508 is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.




















  • Not necessarily by double induction. You can prove $forall y P(n,y)$ by induction on $y$, with $n$ whatever. If the proof works without any specific assumption regarding $n$, you can generalize on it, getting : $forall x forall y P(x,y)$.
    – Mauro ALLEGRANZA
    Dec 2 at 13:24










  • See also the post : Induction on two integer variables.
    – Mauro ALLEGRANZA
    Dec 2 at 13:27












  • See also : Mathematical induction: variants and subtleties.
    – Mauro ALLEGRANZA
    Dec 2 at 13:28










  • $P(n, 0)$ is proven by the second assumption. However, I don't see how $forall y : P(n, y) Rightarrow P(n, Suc(y))$ is proven, because I only have $forall n, y : P(n, y) Rightarrow P(Suc(n), Suc(y))$. What am I not grasping? Also, I've seen those two links before, but thank you for sending them as they definitely contain helpful tricks for proof by induction.
    – anon44508
    Dec 2 at 14:27












  • Nevermind, the other contributor cleared it all up. Thank you for your help.
    – anon44508
    Dec 3 at 2:36













up vote
1
down vote

favorite









up vote
1
down vote

favorite











This probably has been asked before, but apologies, I don't know how to locate it. I want to prove $forall x,y: P(x, y)$. My premises are:



$$P(0, 0) wedge \
[forall x: P(x, 0)] wedge \
[forall y: P(0, y)] wedge \
[forall x,y: P(x, y) Rightarrow P(Suc(x), Suc(y))]$$



I can prove some basic facts in PA, such as addition is comm, assoc, etc. I can also prove things about less than, such as less than is transitive. Also, if x is less than or equal to y, then there exists a z such x + z = y. But I'm not good at induction with two variables, and so cannot complete the proof.










share|cite|improve this question









New contributor




anon44508 is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.











This probably has been asked before, but apologies, I don't know how to locate it. I want to prove $forall x,y: P(x, y)$. My premises are:



$$P(0, 0) wedge \
[forall x: P(x, 0)] wedge \
[forall y: P(0, y)] wedge \
[forall x,y: P(x, y) Rightarrow P(Suc(x), Suc(y))]$$



I can prove some basic facts in PA, such as addition is comm, assoc, etc. I can also prove things about less than, such as less than is transitive. Also, if x is less than or equal to y, then there exists a z such x + z = y. But I'm not good at induction with two variables, and so cannot complete the proof.







logic induction peano-axioms formal-proofs






share|cite|improve this question









New contributor




anon44508 is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.











share|cite|improve this question









New contributor




anon44508 is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.









share|cite|improve this question




share|cite|improve this question








edited Dec 2 at 21:14









Bram28

58.7k44185




58.7k44185






New contributor




anon44508 is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.









asked Dec 2 at 13:14









anon44508

82




82




New contributor




anon44508 is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.





New contributor





anon44508 is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.






anon44508 is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.












  • Not necessarily by double induction. You can prove $forall y P(n,y)$ by induction on $y$, with $n$ whatever. If the proof works without any specific assumption regarding $n$, you can generalize on it, getting : $forall x forall y P(x,y)$.
    – Mauro ALLEGRANZA
    Dec 2 at 13:24










  • See also the post : Induction on two integer variables.
    – Mauro ALLEGRANZA
    Dec 2 at 13:27












  • See also : Mathematical induction: variants and subtleties.
    – Mauro ALLEGRANZA
    Dec 2 at 13:28










  • $P(n, 0)$ is proven by the second assumption. However, I don't see how $forall y : P(n, y) Rightarrow P(n, Suc(y))$ is proven, because I only have $forall n, y : P(n, y) Rightarrow P(Suc(n), Suc(y))$. What am I not grasping? Also, I've seen those two links before, but thank you for sending them as they definitely contain helpful tricks for proof by induction.
    – anon44508
    Dec 2 at 14:27












  • Nevermind, the other contributor cleared it all up. Thank you for your help.
    – anon44508
    Dec 3 at 2:36


















  • Not necessarily by double induction. You can prove $forall y P(n,y)$ by induction on $y$, with $n$ whatever. If the proof works without any specific assumption regarding $n$, you can generalize on it, getting : $forall x forall y P(x,y)$.
    – Mauro ALLEGRANZA
    Dec 2 at 13:24










  • See also the post : Induction on two integer variables.
    – Mauro ALLEGRANZA
    Dec 2 at 13:27












  • See also : Mathematical induction: variants and subtleties.
    – Mauro ALLEGRANZA
    Dec 2 at 13:28










  • $P(n, 0)$ is proven by the second assumption. However, I don't see how $forall y : P(n, y) Rightarrow P(n, Suc(y))$ is proven, because I only have $forall n, y : P(n, y) Rightarrow P(Suc(n), Suc(y))$. What am I not grasping? Also, I've seen those two links before, but thank you for sending them as they definitely contain helpful tricks for proof by induction.
    – anon44508
    Dec 2 at 14:27












  • Nevermind, the other contributor cleared it all up. Thank you for your help.
    – anon44508
    Dec 3 at 2:36
















Not necessarily by double induction. You can prove $forall y P(n,y)$ by induction on $y$, with $n$ whatever. If the proof works without any specific assumption regarding $n$, you can generalize on it, getting : $forall x forall y P(x,y)$.
– Mauro ALLEGRANZA
Dec 2 at 13:24




Not necessarily by double induction. You can prove $forall y P(n,y)$ by induction on $y$, with $n$ whatever. If the proof works without any specific assumption regarding $n$, you can generalize on it, getting : $forall x forall y P(x,y)$.
– Mauro ALLEGRANZA
Dec 2 at 13:24












See also the post : Induction on two integer variables.
– Mauro ALLEGRANZA
Dec 2 at 13:27






See also the post : Induction on two integer variables.
– Mauro ALLEGRANZA
Dec 2 at 13:27














See also : Mathematical induction: variants and subtleties.
– Mauro ALLEGRANZA
Dec 2 at 13:28




See also : Mathematical induction: variants and subtleties.
– Mauro ALLEGRANZA
Dec 2 at 13:28












$P(n, 0)$ is proven by the second assumption. However, I don't see how $forall y : P(n, y) Rightarrow P(n, Suc(y))$ is proven, because I only have $forall n, y : P(n, y) Rightarrow P(Suc(n), Suc(y))$. What am I not grasping? Also, I've seen those two links before, but thank you for sending them as they definitely contain helpful tricks for proof by induction.
– anon44508
Dec 2 at 14:27






$P(n, 0)$ is proven by the second assumption. However, I don't see how $forall y : P(n, y) Rightarrow P(n, Suc(y))$ is proven, because I only have $forall n, y : P(n, y) Rightarrow P(Suc(n), Suc(y))$. What am I not grasping? Also, I've seen those two links before, but thank you for sending them as they definitely contain helpful tricks for proof by induction.
– anon44508
Dec 2 at 14:27














Nevermind, the other contributor cleared it all up. Thank you for your help.
– anon44508
Dec 3 at 2:36




Nevermind, the other contributor cleared it all up. Thank you for your help.
– anon44508
Dec 3 at 2:36










1 Answer
1






active

oldest

votes

















up vote
0
down vote



accepted










Here's a proof in Fitch, which has a built in Peano Induction rule:



enter image description here



As you can see, the only 'trick' is to just ignore the inductive hypothesis for the inside inductive proof, but instead to use the inductive hypothesis for the outside inductive proof






share|cite|improve this answer





















  • Thanks for the mechanically verified proof!
    – anon44508
    Dec 3 at 2:33










  • @anon44508 You're welcome! :)
    – Bram28
    Dec 3 at 12:06











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


}
});






anon44508 is a new contributor. Be nice, and check out our Code of Conduct.










draft saved

draft discarded


















StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3022626%2finduction-with-two-variables-in-pa%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








up vote
0
down vote



accepted










Here's a proof in Fitch, which has a built in Peano Induction rule:



enter image description here



As you can see, the only 'trick' is to just ignore the inductive hypothesis for the inside inductive proof, but instead to use the inductive hypothesis for the outside inductive proof






share|cite|improve this answer





















  • Thanks for the mechanically verified proof!
    – anon44508
    Dec 3 at 2:33










  • @anon44508 You're welcome! :)
    – Bram28
    Dec 3 at 12:06















up vote
0
down vote



accepted










Here's a proof in Fitch, which has a built in Peano Induction rule:



enter image description here



As you can see, the only 'trick' is to just ignore the inductive hypothesis for the inside inductive proof, but instead to use the inductive hypothesis for the outside inductive proof






share|cite|improve this answer





















  • Thanks for the mechanically verified proof!
    – anon44508
    Dec 3 at 2:33










  • @anon44508 You're welcome! :)
    – Bram28
    Dec 3 at 12:06













up vote
0
down vote



accepted







up vote
0
down vote



accepted






Here's a proof in Fitch, which has a built in Peano Induction rule:



enter image description here



As you can see, the only 'trick' is to just ignore the inductive hypothesis for the inside inductive proof, but instead to use the inductive hypothesis for the outside inductive proof






share|cite|improve this answer












Here's a proof in Fitch, which has a built in Peano Induction rule:



enter image description here



As you can see, the only 'trick' is to just ignore the inductive hypothesis for the inside inductive proof, but instead to use the inductive hypothesis for the outside inductive proof







share|cite|improve this answer












share|cite|improve this answer



share|cite|improve this answer










answered Dec 2 at 20:55









Bram28

58.7k44185




58.7k44185












  • Thanks for the mechanically verified proof!
    – anon44508
    Dec 3 at 2:33










  • @anon44508 You're welcome! :)
    – Bram28
    Dec 3 at 12:06


















  • Thanks for the mechanically verified proof!
    – anon44508
    Dec 3 at 2:33










  • @anon44508 You're welcome! :)
    – Bram28
    Dec 3 at 12:06
















Thanks for the mechanically verified proof!
– anon44508
Dec 3 at 2:33




Thanks for the mechanically verified proof!
– anon44508
Dec 3 at 2:33












@anon44508 You're welcome! :)
– Bram28
Dec 3 at 12:06




@anon44508 You're welcome! :)
– Bram28
Dec 3 at 12:06










anon44508 is a new contributor. Be nice, and check out our Code of Conduct.










draft saved

draft discarded


















anon44508 is a new contributor. Be nice, and check out our Code of Conduct.













anon44508 is a new contributor. Be nice, and check out our Code of Conduct.












anon44508 is a new contributor. Be nice, and check out our Code of Conduct.
















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.




draft saved


draft discarded














StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3022626%2finduction-with-two-variables-in-pa%23new-answer', 'question_page');
}
);

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







Popular posts from this blog

Måne

Storängen

VLT Carioca