The Coq mailing list

[r.h.huijben AT student.tue.nl]

I'm looking for a way to prove that something is not a tautology, but not
necesarily a contradiction either. I have the following model:

Variable e t : Set.

Variable Woman Man Person Human Bird Creature: (e -> t).
Variable Fly Walk Run Move Sleep Snore Dream: (e -> t).
Variable A The No Each Implies: (e -> t) -> (e -> t) -> t.
Variable Is_A: e -> (e -> t) -> t.
Variable Who: (e -> t) -> (e -> t) -> e -> t.
Variable Implies : t -> t -> t.
Variable IsTrue: t -> Prop.

Axiom TrueImplies: forall x y, (IsTrue x -> IsTrue y) <-> Implies x y.
Axiom TrueA: forall x y, IsTrue (A x y) <-> (exists o, IsTrue (o ’Is A’ x) /\
IsTrue (y o)).
Axiom TrueNo: forall x y, IsTrue (No x y) <-> ~(exists o, IsTrue (o ’Is A’
x) /\ IsTrue (y o)).
Axiom TrueEach: forall x y, IsTrue (Each x y) <-> (forall o, IsTrue (o ’Is A’
x) -> IsTrue(y o)).
Axiom TrueThe: forall x y, IsTrue (The x y) <-> exists o, IsTrue(y o) /\
IsTrue(o ’Is A’ x) /\ forall z, (IsTrue(z ’Is A’ x)) ->  z = o.
Axiom TrueWho: forall x y z, IsTrue(x ’Is A’ (y ’Who’ z)) <-> IsTrue(x ’Is A’
y) /\ IsTrue (z x).

Axiom TrueAnd: forall x y, IsTrue (x ’And’ y) <-> (IsTrue x /\ IsTrue y).
Axiom TrueOr: forall x y, IsTrue (x ’Or’ y) <-> (IsTrue x \/ IsTrue y).
Axiom TrueNot: forall x, IsTrue (Not x) <-> ~(IsTrue x).
(Rather oversimplified version, there is a lot more going on that isn't
relevant to the problem)

This allows me to make terms like (A Person Walk). These terms represent real
world propositions and I would like to be able to prove them when they are
true but also be able to show that they are unproveable when they are. For
example the term ((A Woman Walk) ’Implies’ A Bird Fly) is clearly nonsense,
but currently I am unable to prove that.

I have tried a number of solutions (converting either IsTrue or Implies to
inductive types, reconstructing everything into fixpoint operators etc.) but
those only seemed to move the problem and I am kind of stuck here, so could
you help me with this?

Regards,

Rutger