Search code examples
isabelle

Meta symbol for existential quantification in Isabelle

There are meta symbols for implication and universal quantification in Isabelle/Pure (⟹ and ⋀), which behave differently from its HOL counterparts (∀ and →).

Is there a meta symbol for existential quantification? If not, is there a specific reason for this decision?

Solution

  • Pure is based on intuistionistic logic and there is no existential quantifier in this logic.

    The rough equivalent is obtains:

    lemma
  assumes "P"
  obtains x where "Q x"

    The generated lemma is P ⟹ (⋀x. Q x ⟹ thesis) ⟹ thesis. It does not contain an existential quantifier, but only an implication. However it plays a similar rule: by instantiation of thesis with any other goal, you can exhibit the existence of an x such that Q x.