2
$\begingroup$

I am looking to prove that $\forall x \forall y \; P(x,y) \vdash \forall x \; P(x,x)$ and I wonder if this is allowed: 1. ∀x ∀y P(x,y) Premise 2. | x0 fresh variable 3. | ∀y P(x0, y) ∀-elimination (1) 4. | P(x0, x0) ∀-elimination (3) 5. ∀x P(x, x) ∀-introduction (4)

It's the second forall elimination that I am worried about being incorrect. If this is not allowed, I would like to know why that is the case.

$\endgroup$
  • $\begingroup$ It's fine.${{}}$ $\endgroup$ – Git Gud Sep 22 '16 at 13:34
  • $\begingroup$ @GitGud, do you happen to have a source of sort that points towards this? I am reading the book "Logic in Computer Science" by Huth and Ryan, but I cannot find anything that supports this. $\endgroup$ – GLaDER Sep 22 '16 at 13:40
  • $\begingroup$ The rules themselves support it. Sorry, I don't know about any source that singles out this issue specifically. $\endgroup$ – Git Gud Sep 22 '16 at 13:44
  • $\begingroup$ See page 109: "The rule] says: If $∀xφ$ is true, then you could replace the $x$ in $φ$ by any [emphasis added] term $t$ (given, as usual, the side condition that $t$ be free for $x$ in $φ$) and conclude that $φ[t/x]$ is true as well." When we have "nested" universal quantifiers, the condition still apply : any term $t$. The intuition is : "for all" means ... for all. $\endgroup$ – Mauro ALLEGRANZA Sep 22 '16 at 13:52
0
$\begingroup$

Using the proof checker associated with forallx, both linked below, the proof as you presented it is correct.

Here is the proof:

enter image description here

For the second forall elimination any name may be used to stand for the variable $y$ including the name used for the first forall elimination of variable $x$.


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.