Suppose a guy has a baby.
Talking from the point of view of this guy,
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
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.
Variant person := me | baby
Hadn't known about
Like a stripped down version of
Inductive, is it?
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 has marked this topic as resolved.
Last updated: Sep 23 2023 at 14:01 UTC