(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)
(** {2 First-Order Logic} *)
type being
(** a type name *)
constant socrate : being
(** inhabitant of `being` *)
predicate is_human being
predicate is_mortal being
(** two predicates on `being` *)
goal socrate_is_mortal:
is_human socrate ->
(forall x:being. is_human x -> is_mortal x) ->
is_mortal socrate
predicate is_a_cat being
goal sophism:
is_mortal socrate ->
(forall x:being. is_a_cat x -> is_mortal x) ->
is_a_cat socrate
(** {3 Drinker's paradox} *)
type customer
predicate drinks customer
goal drinkers_paradox: exists x:customer. drinks x -> (forall y:customer. drinks y)
(** valid because the logic is classical, and all types are assumed inhabited *)