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?

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.

Which instance of the axioms could be helpful?

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

provable?

just adding it as an axiom may be least intrusive

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

ah `Variant person := me | baby`

Hadn't known about `Variant`

.

Like a stripped down version of `Inductive`

, is it?

yup

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.
```

Thanks!

Julin S has marked this topic as resolved.

Last updated: Sep 23 2023 at 14:01 UTC