Talk:Existential instantiation

Not a Valid Rule

This is obviously not a valid rule:

    G |- exists x A(x)
    ------------------ a not in G
         G |- A(a)

Its very easy to see, just take the rule for Universal generalization:

         G |- A(a)
    ------------------ a not in G
    G |- forall x A(x)

So the existential instantion would basically also say that we can replace existential

quantifier by forall quantifier in the conclusion, which is of course not a sound inference.

Jan Burse (talk) 00:26, 17 February 2018 (UTC)

Of course, a rule is not sound or complete on its own; the important question is whether a particular system of rules is together sound and compete. There are systems with EI that are sound and complete. But it can take a particular combination of other rules to achieve this. Normally, I think of UG as only replacing variables, while EI only adds new constant symbols (not variables). — Carl (CBM · talk) 03:59, 17 February 2018 (UTC)

Anyway, I've edited the article according to that understanding. It would be ideal for someone to look up a reference that has this rule, to see their entire system. — Carl (CBM · talk) 04:02, 17 February 2018 (UTC)