(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)
(** {2 First-Order Logic} *)
type being
(** a type name *)
constant socrates : being
(** inhabitant of `being` *)
predicate is_human being
predicate is_mortal being
(** two predicates on `being` *)
goal socrates_is_mortal:
is_human socrates ->
(forall x:being. is_human x -> is_mortal x) ->
is_mortal socrates
predicate is_a_cat being
goal sophism:
is_mortal socrates ->
(forall x:being. is_a_cat x -> is_mortal x) ->
is_a_cat socrates
(** {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 *)