Stream: Coq users

Topic: ✔ Proof of a small scenario

Julin S (Jun 09 2022 at 11:22):

Suppose a guy has a baby.

Talking from the point of view of this guy,

• Everyone loves my baby (baby is so adorable).
• But my baby loves only me.

I once saw a proof online where it was possible to derive that 'I am my baby' from these assumptions.

I recreated that proof in Coq and it looks like this:

Section baby.
  Variable Person : Set.
  Variable loves : Person -> Person -> Prop.

  Axiom mybaby me : Person.
  Axiom everyoneLovesMybaby : forall person:Person,
    loves person mybaby.
  Axiom mybabyLovesOnlyMe : forall person:Person,
    loves mybaby person -> person = me.
  Theorem mybabyIsMe : mybaby = me.
  Proof.
    exact (mybabyLovesOnlyMe mybaby (everyoneLovesMybaby mybaby)).
  Qed.
End baby.

I suppose this was provable because of some fault in the way the axioms were formulated?

Is there any way by which we can prove that me ≠ mybaby while still holding true to the essence of this scenario?

Maybe if we modify mybabyLovesOnlyMe to

Axiom mybabyLovesOnlyMe : forall person:Person,
  person <> mybaby -> loves mybaby person -> person = me.

Can it help?

Li-yao (Jun 09 2022 at 11:31):

That allows you not to prove mybabe = me but won't allow you to prove the negation. When you introduce axioms there is always the risk of introducing a contradiction, in which case everything is provable. The alternative is to instantiate the axioms. Then you can show mybabe <> me in that specific model.

Julin S (Jun 09 2022 at 11:45):

Which instance of the axioms could be helpful?

Julin S (Jun 09 2022 at 11:45):

And what could be the 'least intrusive' hypothesis that we can add to the set of axioms to make mybaby <> me provable?

Gaëtan Gilbert (Jun 09 2022 at 11:46):

just adding it as an axiom may be least intrusive

Li-yao (Jun 09 2022 at 12:00):

There's a post-apocalyptic model where it's only you and your baby left in the world.

Gaëtan Gilbert (Jun 09 2022 at 12:06):

ah Variant person := me | baby

Julin S (Jun 09 2022 at 12:14):

Hadn't known about Variant.

Julin S (Jun 09 2022 at 12:14):

Like a stripped down version of Inductive, is it?

Gaëtan Gilbert (Jun 09 2022 at 12:15):

yup

Olivier Laurent (Jun 09 2022 at 12:18):

It seems you can derive loves mybaby me only because me = mybaby, while it seems to be part of the scenario anyway.
You could then consider an anti-narcissistic world:

Section baby.
  Variable Person : Set.
  Variable loves : Person -> Person -> Prop.

  Axiom antiNarcissistic : forall person1 person2,
    loves person1 person2 -> person1 <> person2.

  Axiom mybaby me : Person.
  Axiom everyoneLovesMybaby : forall person:Person,
    person <> mybaby -> loves person mybaby.
  Axiom mybabyLovesMe : loves mybaby me.
  Axiom mybabyLovesOnlyMe : forall person:Person,
    loves mybaby person -> person = me.
  Theorem mybabyIsNotMe : mybaby <> me.
  Proof. apply antiNarcissistic, mybabyLovesMe. Qed.
End baby.

Julin S (Jun 10 2022 at 03:21):

Thanks!

Notification Bot (Jun 10 2022 at 03:21):

Julin S has marked this topic as resolved.

Last updated: Sep 23 2023 at 14:01 UTC