Talk:Existential instantiation

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search
WikiProject Requested articles  
WikiProject iconThis article is within the scope of WikiProject Requested articles, because it was formerly listed at Requested articles.
 ???  This article has not yet received a rating on the quality scale.

Not a Valid Rule[edit]

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)