coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] [isabelle, Coq-Club, MetaMath] The Zande's Challenge

From: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
To: isabelle-users AT cl.cam.ac.uk
Cc: coq-club AT inria.fr, metamath AT googlegroups.com
Subject: [Coq-Club] [isabelle, Coq-Club, MetaMath] The Zande's Challenge
Date: Wed, 8 Aug 2018 05:21:14 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=josephcmac AT gmail.com; spf=Pass smtp.mailfrom=josephcmac AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f52.google.com
Ironport-phdr: 9a23:4zYqmBOJuiZkXbudn1Il6mtUPXoX/o7sNwtQ0KIMzox0Iv3/rarrMEGX3/hxlliBBdydt6oazbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlJiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkHOTA383zZhNJsg69Auh2tuwZyzpTIbI2JNvdzeL7Wc9MARWpGW8ZcTyhPAoSnb4wVF+UPOvxXr4/gp1QQqRuxHRWiBOTyxT9Sh3/20rA63PogEA7ewgEvBckBv27QrNXxKqgSS+e1x7TPwDXBaPNWwiny6JDIch89pPGDR65/fNHeyUkqDQzFj1GQpZb5MDOS0+QAqm6W5PduW+Kojm4osQBxoj63y8cukYnJmoUVykre+SV+2oY1KsW0SU58Yd65DJtQqjqVOJVsTsw+RGFovSA3waAFt56jZCUG1ogryhrFZ/GEc4WE+AzvWPueLDtihH9pZrSyjAuo/0e60O3zTMy03U5KriVbltnMsWgA1xnJ5ciGTvtx50ah2SqT2wzK5OFJIV44mbDUK54mxb4wmZ4TvlrZEiDqn0X2ibeadkQi+ue29+TqeqvqqoOYOoNuiQzzMr4iltKiDek3KAQDX3aX9fy51LL5/E35RLtKjucxkqncqJ3aJ8MbprWnDA9N0oYs9xO/AC2639kDknkHKUhKeBODj4TzJ17OJ/X4Ae+lg1uwiDdr2+zGPrr5D5rRKXjDia7tcqp5605B0wU+1stf5pJRCrEZOv3/QE7xtNrCDh84KQO42ejnCM8unr8ZDGOUC6WUNKff9EKT6/g0C+KIIoQcvXD0IL445K3Al3g8zH0aZiie+JIRdX28Kc5hL1+YbmfhkOAqGG0Dug4zVuui3F+FSjNLZ323VqkU6TQyCYbgBoDGENP+yIed1Tu2S8UFLltNDUqBRC+xJte0HswUYSfXGfdP1zkNVLyvUYgkjEj8uwrzyr4hJe3RqHRB6cDTkeNt7uiWrikcsCRuBp3EgW6IRmBw2GgPQm1uhf0tkQlG0l6GlJNArblYGNhUva4bVw47Mdvd07Q/BY2oHA3GediNRRCtRdD0WTw=

This post is just an intellectual challenge for people with a lot of free time this summer...

The Azande are an ethnic group of North Central Africa. Here, a documentary about these people: https://www.youtube.com/watch?v=Rmug_qvO15s

Anthropologists don't agree about which logical system could be the best one to express Zande's religion postulates in a consistent way. These postulates seem to be contradictory from the point of view of traditional mathematics.

I think that it will be interesting to think about this problem from the perspective of a proof assistant, trying to mechanize these religions postulates in a consistent way. Maybe someone reading this post will solve this anthropologic mystery and to publish a paper with the solution (anthropologists will be interested in this new information). Here is a reference to this problem from a rather mathematical point of view:

Salmon, Merrilee H. "Do Azande and Nuer use a non-standard logic?." Man (1978): 444-454. https://www.jstor.org/stable/2801940?seq=1#page_scan_tab_contents

Kind Regards,

Jose M.

[Coq-Club] [isabelle, Coq-Club, MetaMath] The Zande's Challenge, José Manuel Rodriguez Caballero, 08/08/2018