liamoc.net
my forest
1\date{2025-11-25T20:14:40Z}
2\author{liamoc}
3\title{Existential Quantifiers}
4\taxon{Definition}
5\parent{isa-0002}
6\import{shiki-macros}
7\put\shiki/language{Isabelle Theory}
8
9\shiki{axiomatization
10 Ex :: ‹('a ⇒ bool) ⇒ bool› (binder "∃" 10)
11where
12 exI : ‹⟦ P x ⟧ ⟹ ∃a. P a› and
13 exE : ‹⟦ ∃ x. P x ; ⋀a. P a ⟹ R ⟧ ⟹ R›
14}