Talk:Existential instantiation

This article is within the scope of WikiProject Requested articles, because it is used for the administration of the Requested articles process or it was formerly listed at Requested articles.Requested articlesWikipedia:WikiProject Requested articlesTemplate:WikiProject Requested articlesRequested articles

Mathematics

	Mathematics portal This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles
???	This article has not yet received a rating on the project's priority scale.

Philosophy Low‑importance

	Philosophy portal This article is within the scope of WikiProject Philosophy, a collaborative effort to improve the coverage of content related to philosophy on Wikipedia. If you would like to support the project, please visit the project page, where you can get more details on how you can help, and where you can join the general discussion about philosophy content on Wikipedia.PhilosophyWikipedia:WikiProject PhilosophyTemplate:WikiProject PhilosophyPhilosophy articles
Low	This article has been rated as Low-importance on the project's importance 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)[reply]

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)[reply]

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)[reply]