Proving that ∀xG(x,a)⊢∃xG(a,x)

Question

Can I prove ∀xG(x,a)⊢∃xG(a,x) this way:

∀xG(x,a)   premise
G(a,a)     ∀xe
∃xG(a,x)   ∃xi

Seesm OK to me. Why the doubt? – Henno Brandsma Apr 09 '17 at 12:43 — Henno Brandsma, Apr 09 '17 at 12:43
Because G(a,a) is the result of applying x = a to G(x,a). – Måns Nilsson Apr 09 '17 at 12:46 — Måns Nilsson, Apr 09 '17 at 12:46
That's a valid rule AFAIK. – Henno Brandsma Apr 09 '17 at 12:51 — Henno Brandsma, Apr 09 '17 at 12:51

score 2 · Answer 1 · answered Apr 09 '17 at 14:56

Your proof is correct. I think you are doubting yourself because in going from $G(a,a)$, is it ok to not replace all $a$'s with $x$'s? This is a common concern.

But yes, this is indeed ok!

In general:

When you eliminate a quantifier, then you do need to replace all variables that were quantified by that quantifier using a constant.

But when you introduce a quantifier, you do not have to replace all constants that you quantify by the variable you use for that quantifier.

score 1 · Accepted Answer · answered Apr 09 '17 at 13:05

1

Yeah, you can prove it that way.

Here is another way. The tableau $$ \forall x G(x, a) \\ \lnot \exists x G(a, x) \\ G(a, a) \\ \lnot G(a, a) $$ is closed, so the result holds. (It's a proof by contradiction.)

answered Apr 09 '17 at 13:05

Shaun

44,997

1

So in both G(x,a) and G(a,x) you then have to substitute x = a for the proof by contradiction to work? – Måns Nilsson Apr 09 '17 at 13:22
Yes: $\lnot \exists x G(a, x)$ is the same as $\forall x\lnot G(a, x)$. What I've done is take $\forall x G(x, a)$ as a premise then assume $\lnot \exists x G(a, x)$. – Shaun Apr 09 '17 at 13:27

Proving that ∀xG(x,a)⊢∃xG(a,x)

2 Answers2