section‹The meta-existential quantifier›
theory MetaExists imports ZF begin
text‹Allows quantification over any term. Used to quantify over classes.
Yields a proposition rather than a FOL formula.›
definition
ex :: "(('a::{}) ⇒ prop) ⇒ prop" (binder ‹⋁› 0) where
"ex(P) == (⋀Q. (⋀x. PROP P(x) ⟹ PROP Q) ⟹ PROP Q)"
lemma meta_exI: "PROP P(x) ==> (⋁x. PROP P(x))"
proof (unfold ex_def)
assume P: "PROP P(x)"
fix Q
assume PQ: "⋀x. PROP P(x) ⟹ PROP Q"
from P show "PROP Q" by (rule PQ)
qed
lemma meta_exE: "[|⋁x. PROP P(x); ⋀x. PROP P(x) ==> PROP R |] ==> PROP R"
proof (unfold ex_def)
assume QPQ: "⋀Q. (⋀x. PROP P(x) ⟹ PROP Q) ⟹ PROP Q"
assume PR: "⋀x. PROP P(x) ⟹ PROP R"
from PR show "PROP R" by (rule QPQ)
qed
end