CODEWITHSUNDEEP
isabelle
Luiz Martins
Luiz Martins

Reputation: 1724

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?

Upvotes: 1

Views: 145

Answers (1)

Mathias Fleury
Mathias Fleury

Reputation: 2261

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.

Upvotes: 2

Related Questions