(* Title: ZF/Constructible/MetaExists.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
section\<open>The meta-existential quantifier\<close>
theory MetaExists imports ZF begin
text\<open>Allows quantification over any term. Used to quantify over classes.
Yields a proposition rather than a FOL formula.\<close>
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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
