The Coq mailing list

[Dimitri Hendriks <diem AT xs4all.nl>]

Hi Rutger,

To prove that walking women do not imply birds flying, we need one woman who 
walks, and that no bird flies. So you need to add these facts to obtain a 
model doing that (at the moment your domain e could even be empty). 

I don't know why you set up things in the way you do, but I can imagine that 
if you later want to prove things on all such first-order formulas, it is 
more convenient to define them inductively, and define a function IsTrue on 
top. That would also be less cumbersome to work with, than with these axioms.

Your code did not run, and some things were missing.
I added the axiom TrueA2 : forall x o, IsTrue (x o) -> IsTrue (Is_A o x),
(but a definition Is_A o x := x o would be more convenient).

I import the Setoid library in order to use <-> as a congruence relation
(to allow for the rewrite steps).

Greetings, 
Dimitri

---
Require Setoid.

Section TuE.

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: (e -> t) -> (e -> t) -> t.
Variable Is_A: e -> (e -> t) -> t.
Variable Who: (e -> t) -> (e -> t) -> e -> t.
Variable Not : t -> t.
Variable And Or Imp : t -> t -> t.
Variable IsTrue: t -> Prop.

Axiom TrueImp: forall x y, (IsTrue x -> IsTrue y) <-> (IsTrue (Imp x y)).
Axiom TrueA: forall x y, IsTrue (A x y) <-> (exists o, IsTrue (Is_A o x) /\ 
IsTrue (y o)).
Axiom TrueA2 : forall x o, IsTrue (x o) -> IsTrue (Is_A o x).
Axiom TrueNo: forall x y, IsTrue (No x y) <-> ~(exists o, IsTrue (Is_A o x) 
/\ IsTrue (y o)).
Axiom TrueEach: forall x y, IsTrue (Each x y) <-> (forall o, IsTrue (Is_A o 
x) -> IsTrue (y o)).
Axiom TrueThe: forall x y, IsTrue (The x y) <-> exists o, IsTrue(y o) /\ 
IsTrue(Is_A o x) /\ forall z, (IsTrue(Is_A z x)) ->  z = o.
Axiom TrueWho: forall x y z, IsTrue(Is_A x (Who y z)) <-> IsTrue(Is_A x y) /\ 
IsTrue (z x).

Axiom TrueAnd: forall x y, IsTrue (And x y) <-> (IsTrue x /\ IsTrue y).
Axiom TrueOr: forall x y, IsTrue (Or x y) <-> (IsTrue x \/ IsTrue y).
Axiom TrueNot: forall x, IsTrue (Not x) <-> ~(IsTrue x).

Variable Tweety : e.

Hypothesis WomanTweety : IsTrue (Woman Tweety).
Hypothesis WalkTweety : IsTrue (Walk Tweety).

Hypothesis PenguinsOnly : IsTrue (Not (A Bird Fly)).

Lemma aa : IsTrue (Not (Imp (A Woman Walk) (A Bird Fly))).
Proof.
  rewrite -> TrueNot.
  rewrite <- TrueImp.
  intros H.
  apply (proj1 (TrueNot (A Bird Fly)) PenguinsOnly).
  apply H.
  rewrite TrueA.
  exists Tweety; split.
  apply TrueA2.
  exact WomanTweety.
  exact WalkTweety.
Qed. 

End TuE.
---


On Mar 26, 2013, at 10:30 , 
r.h.huijben AT student.tue.nl
 wrote:

> 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