Everything is Christian (inconsistency)

[anka-213]

This rule https://github.com/ontologyportal/sumo/blob/695651ba721642cc3b9595ef1e23df5fe33a8202/People.kif#L797-L801

in the reverse direction implies that as long as there is any (member ?INDIVIDUAL Christianity), then for any arbitrary value ?CH, it is an (instance ?CH Christian).

This means that everything, including Christian itself is an instance of Christian, which contradicts (instance Christian SetOrClass), since those can't be instances of themselves.

---

I think the correct version would be something like

(<=>
 (exists (?CH)
   (and
     (attribute ?INDIVIDUAL ?CH)
     (instance ?CH Christian)))
 (member ?INDIVIDUAL Christianity))

but I'm not entirely sure.

Full proof generated by EProver

``` 1. (forall (?VAR1 ?VAR2) (=> (instance ?VAR2 Object) (and (=> (and (attribute ?VAR2 ?VAR1) (instance ?VAR1 Christian)) (member ?VAR2 Christianity)) (=> (member ?VAR2 Christianity) (and (attribute ?VAR2 ?VAR1) (instance ?VAR1 Christian)))))) [ kb_SUMO_5] 2. (forall (?VAR1) (=> (instance ?VAR1 Collection) (exists (?VAR2) (and (instance ?VAR2 Object) (member ?VAR2 ?VAR1))))) [ kb_SUMO_12977] 3. (instance immediateInstance IrreflexiveRelation) [ kb_SUMO_74086] 4. (forall (?VAR1 ?VAR2) (=> (instance ?VAR2 SetOrClass) (=> (instance ?VAR1 ?VAR2) (immediateInstance ?VAR1 ?VAR2)))) [ kb_SUMO_4447] 5. (instance Christianity Collection) [ kb_SUMO_31811] 6. (instance Christian SetOrClass) [ kb_SUMO_24195] 7. (forall (?VAR1) (or (not (instance immediateInstance IrreflexiveRelation)) (not (immediateInstance ?VAR1 ?VAR1)))) 8 [shift_quantors] 8. (forall (?VAR1 ?VAR2) (and (or (or (or (not (attribute ?VAR2 ?VAR1)) (not (instance ?VAR1 Christian))) (member ?VAR2 Christianity)) (not (instance ?VAR2 Object))) (or (or (attribute ?VAR2 ?VAR1) (not (member ?VAR2 Christianity))) (not (instance ?VAR2 Object))) (or (or (instance ?VAR1 Christian) (not (member ?VAR2 Christianity))) (not (instance ?VAR2 Object))))) 1 [distribute] 9. (forall (?VAR1) (and (or (instance (?VAR1) Object) (not (instance ?VAR1 Collection))) (or (member (?VAR1) ?VAR1) (not (instance ?VAR1 Collection))))) 2 [distribute] 10. (or (not (immediateInstance ?VAR1 ?VAR1)) (not (instance immediateInstance IrreflexiveRelation))) 7 [split_conjunct] 11. (forall (?VAR1 ?VAR2) (or (not (instance ?VAR2 SetOrClass)) (not (instance ?VAR1 ?VAR2)) (immediateInstance ?VAR1 ?VAR2))) 4 [variable_rename] 12. (or (instance ?VAR1 Christian) (not (instance ?VAR2 Object)) (not (member ?VAR2 Christianity))) 8 [split_conjunct] 13. (or (member (?VAR1) ?VAR1) (not (instance ?VAR1 Collection))) 9 [split_conjunct] 14. (not (immediateInstance ?VAR1 ?VAR1)) 10 3 [cn] 15. (or (immediateInstance ?VAR1 ?VAR2) (not (instance ?VAR1 ?VAR2)) (not (instance ?VAR2 SetOrClass))) 11 [split_conjunct] 16. (or (instance ?VAR1 Christian) (not (instance (Christianity) Object))) 12 13 5 [cn] 17. (or (instance (?VAR1) Object) (not (instance ?VAR1 Collection))) 9 [split_conjunct] 18. (or (not (instance ?VAR1 SetOrClass)) (not (instance ?VAR1 ?VAR1))) 14 15 [spm] 19. (instance ?VAR1 Christian) 16 17 5 [cn] 20. QED 18 6 19 [cn] ```

[apease]

This rule says that if there's an individual who is a Christian then that individual (not all individuals) is a member of Christianity. It also says (reading the bi-implication in the reverse direction) that if there is a particular member of Christianity then that individual has the attribute of being a Christian.

[apease]

The cause of the contradiction appears to be step 4, which is a rule that does not exist in the current version of SUMO. Are you using the current version?

[anka-213]

Ok, I'm not entirely sure about the scoping rules, but I'm pretty sure that the reverse direction reads (see also step 8, which only depends on step 1)

(forall (?VAR1 ?VAR2)
    (=>
        (instance ?VAR2 Object)
        (=>
                (member ?VAR2 Christianity)
                (and
                    (attribute ?VAR2 ?VAR1)
                    (instance ?VAR1 Christian)))))

Which can be expanded to (if A => B & C, then (A => B) & (A => C)):

(forall (?VAR1 ?VAR2)
    (=>
        (instance ?VAR2 Object)
        (and
                (=>
                    (member ?VAR2 Christianity)
                    (attribute ?VAR2 ?VAR1)
                (=>
                    (member ?VAR2 Christianity)
                    (instance ?VAR1 Christian))))))

in other words. If ?VAR2 is a member of christianity, then any ?VAR1 will be an instance of Christian and for any ?VAR1, we have (attribute ?VAR2 ?VAR1) .

What you say is probably the intended meaning, but I believe it is not the actual meaning.

[anka-213]

But yes, I'm using the latest version.

[apease]

?VAR1 is a class of Attribute. ?VAR2 is the (presumably Human) individual. So, yes if ?VAR2 is a member of the group Christianity then he or she will have a particular attribute and that attribute will be an instance of the class Christian. That is accurate. This may be clearer if you refer to the various kinds of Christian sects listed in People.kif and imagine a particular example. Let's take John the Baptist

(attribute John Baptist)

The rule says that if John is a Baptist (and he is) and Baptist is an instance of Christian (and it is) then John (not all individuals) will be a member of the group Christianity. We could also take the other case of where we say that John is a member of Christianity, then the rule says that there must exist some instance of Attribute that is an instance of the class Christian.

[apease]

could you send your config.xml and SUMO.tptp file? Step 4 does not appear in my SUMO.tptp output.

[anka-213]

The proof that everything is Christian does not depend on step 4 at all. It's just the contradiction part that depends on step 4.

I do understand what the intention is, but if you look carefully at the reverse direction in step 1 it doesn't say that. The forall is outside of the implication, which means that nothing constrains what ?VAR1 can be, we just get proofs of (invalid) properties about it.

(Unless I've completely misunderstood how the system works, which is also perfectly possible)

---

I'll try to see if we can extract those from sigmakee.

[apease]

It's possible that the confusion is that SUMO is a sorted logic. So ?VAR1 is constrained to be a subclass of Attribute. Unless there's a bug in the translation to TPTP, you should see type guards that implement the constraint for TPTP

[inariksit]

@apease I'm afraid that the original knowledge base that produced rule 4 isn't there anymore. I started learning SUMO yesterday, and I was typing bunch of random stuff about potatoes in a .kif file and figured that E would tell me if I'm being inconsistent. As I did this, I found out that all my random stuff was QED'd with always the same proof from E, that was based on everything being Christian. The log that @anka-213 gave you was from one of those "let's extend the KB with random stuff about potatoes" tests.

But the "everything is Christian" comes up even with a fresh SUMO, after I removed my random malformed stuff. What happens when you try (instance PotatoTuber Christian) in the Ask/Tell view of sigma?

Here's an example output when I ask for a proof that PotatoTuber is a Holiday. (Just to demonstrate that it invokes the Christian proof without me mentioning it at all. https://listenmaa.fi/b/Sigma_Potato_is_Holiday.htm)

[inariksit]

(Side note: when I chose Vampire for testing my random (certainly malformed) inferences, I would get QED with always the same proof about Puerto Rico simultaneously being and not being a geopolitical area. I don't know much about theorem provers, is that the expected behaviour? :-D)

[anka-213]

It's possible that the confusion is that SUMO is a sorted logic. So ?VAR1 is constrained to be a subclass of Attribute. Unless there's a bug in the translation to TPTP, you should see type guards that implement the constraint for TPTP

Ah, right, so the sorted logic means that, if we have

(forall (?VAR1)
  (=>
    (member JohnTheBaptist Christianity)
    (attribute JohnTheBaptist ?VAR1)))

then ?VAR1 is constrained to be a subclass of attribute?

It still seems problematic to me, since it would then say that all attributes will be true for JohnTheBaptist regardless of what they are (assuming he is a member of Christianity). But maybe that's not what the implication means?

[apease]

@inariksit step #4 still appears in your html and seems to me to be the problem. It's not a rule that's in SUMO. For your next question, yes, once you have a contradiction in a logical theory, from "false" one can conclude anything. That's a standard property of a two valued (true/false) logic

[apease]

@anka-213 the rule you're listing is missing a literal from the original in SUMO

[apease]

It's great that you're working with SUMO and with inference. I'd recommend reading a bit more about SUMO before jumping to conclusions that there's a problem (even though I'm sure there are bugs I haven't found!)

[anka-213]

@apease Sorry for jumping to conclusions too quickly.

I still don't understand how it could possibly be correct though. Is it the case that these two are equivalent in sumo?

(forall (?INDIVIDUAL ?CH)
 (=>
   (member ?INDIVIDUAL Christianity)
   (and
     (attribute ?INDIVIDUAL ?CH)
     (instance ?CH Christian))))

(forall (?INDIVIDUAL)
  (=>
  (member ?INDIVIDUAL Christianity)
  (exists (?CH)
   (and
     (attribute ?INDIVIDUAL ?CH)
     (instance ?CH Christian)))))

or is there something else I'm missing?

Once again, sorry, I admit that I was (and probably still am) way too arrogant. 😞

[anka-213]

@apease

The rule says that if John is a Baptist (and he is) and Baptist is an instance of Christian (and it is) then John (not all individuals) will be a member of the group Christianity. We could also take the other case of where we say that John is a member of Christianity, then the rule says that there must exist some instance of Attribute that is an instance of the class Christian.

This is specifically what I am thinking of. You're translating it to "there exists some instance", but the original translation into step 1 of the proof says "(forall (?CH) ...)". Is this translation correct?

As far as I can tell, it means that all attributes of a member of Christianity is an instance of Christian. What is missing from my interpretation?

---

Really sorry for the rough start and I hope you don't see me as too much of an asshole.

[inariksit]

@inariksit step #4 still appears in your html

Oops, when I ran the query with "potato is christian", rule 4 wasn't there. But it indeed is there for "potato is holiday" query. I was too quick to upload that file. (But of course, maybe "potato is christian" just contains some other rule that comes from my random axioms instead of SUMO. :-P) I had removed all the kif files that I added by clicking Remove on them in the Manifest, but maybe I misunderstood and need to remove it in other places too. I'll investigate it more, now I have a concrete criteria that tells me if I succeeded (i.e. whether rule 4 is there or not for that inference).

I apologize that we've been taking your time, and I appreciate your kind answers. I accept if the answer to this mystery is that my random axioms interfered with the existing axioms in ways that made SUMO act weirdly. I didn't write anything that directly mentioned neither SetOrClass nor immediateInstance, but I understand that there's a big complex graph of interconnected knowledge, and it can break in unexpected ways.

(Finally, in case you're wondering why do these random people appear and talk about potatoes, this is what I was trying to do :-D we're just at an exploration stage, but so far I've been impressed by SUMO and its coverage and expressivity!)

[apease]

No worries! I’m excited you’re using sumo and I eager to help you get what you need. I’ll be able to reply in more detail late today pacific time

Sent from my iPhone http://www.ontologyportal.org

On Aug 27, 2020, at 10:13 AM, Inari Listenmaa notifications@github.com wrote:



@inariksithttps://github.com/inariksit step #4https://github.com/ontologyportal/sumo/issues/4 still appears in your html

Oops, when I ran the query with "potato is christian", rule 4 wasn't there. But it indeed is there for "potato is holiday" query. I was too quick to upload that file. (But of course, maybe "potato is christian" just contains some other rule that comes from my random axioms instead of SUMO. :-P) I had removed all the kif files that I added by clicking Remove on them in the Manifest, but maybe I misunderstood and need to remove it in other places too. I'll investigate it more, now I have a concrete criteria that tells me if I succeeded (i.e. whether rule 4 is there or not for that inference).

I apologize that we've been taking your time, and I appreciate your kind answers. I accept if the answer to this mystery is that my random axioms interfered with the existing axioms in ways that made SUMO act weirdly. I didn't write anything that directly mentioned neither SetOrClass nor immediateInstance, but I understand that there's a big complex graph of interconnected knowledge, and it can break in unexpected ways.

(Finally, in case you're wondering why do these random people appear and talk about potatoes, thishttps://github.com/smucclaw/complaw/tree/master/doc/ex-20200806-hello-world-rules#in-sumo is what I was trying to do :-D we're just at an exploration stage, but so far I've been impressed by SUMO and its coverage and expressivity!)

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHubhttps://github.com/ontologyportal/sumo/issues/228#issuecomment-682080153, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAQG6HJDZWBZGS37QSUDWO3SC2H4TANCNFSM4QM7P7PQ.

[inariksit]

I'm happy that you're interested in helping out! I'm in Europe so I'll read your reply tomorrow. (Just in case you get some information out of the "x is christian" proof, here's one without step 4. https://listenmaa.fi/b/Sigma_PuertoRico_is_Christian.htm But as I said, it may as well contain some other rule that comes from my potato axioms. Do what you want with it, and I'll continue debugging my sigma setup tomorrow!)

[arademaker]

I hope my example of the banana slug in http://leanprover.github.io can help clarify how SUMO is translated to complete FOL. Hope this help and not introduce more confusion.

BTW, @inariksit, for a while, I tried to explore https://github.com/GrammaticalFramework/gf-contrib/tree/master/SUMO and map the ideas to Lean, but I ended up concluding that the goals are quite different.

[kharus]

I tried to narrow down working set for this issue and use only collection and some random elements from SUMO.

  <kb name="SUMO" >
    <constituent filename="Merge.kif" />
  </kb>

I run following

$JAVA_HOME/bin/java -Xmx6G -classpath "$SIGMA_SRC/build/classes:$SIGMA_SRC/build/lib/*" com.articulate.sigma.KB -av "(and (not (instance RealNumber Collection)) (instance RealNumber Collection))"

And Vampire produces proof - which is too long to reproduce here.

KB.main(): proof: [1. (forall (?VAR1)
  (and
    (=>
      (exists (?VAR2)
        (and
          (and
            (and
              (=>
                (forall (?VAR3 ?VAR4 ?VAR5)
                  (=>
                    (and
                      (instance ?VAR5 SetOrClass)
                      (instance ?VAR3 PositiveInteger))

It looks to me like Vampire found an answer to (A & ~A)

[apease]

If you post the exact KIF files you used and are sure there are no statements included that are not in the current version of SUMO I can try to reproduce the problem

[kharus]

I think issue with Vampire is something else I can't reproduce it in eprover. Please ignore it I will file it separately.

[kharus]

For (instance PuertoRico Christian) SUMO I pulled just a few hours ago. KB config.

  <kb name="SUMO" >
    <constituent filename="CountriesAndRegions.kif" />
    <constituent filename="Merge.kif" />
    <constituent filename="People.kif" />
  </kb>

Just in case I attached files in zip but they should be exactly the same as the repo.

kifs.zip

I then reduced KB to merge and people

  <kb name="SUMO" >
    <constituent filename="Merge.kif" />
    <constituent filename="People.kif" />
  </kb>

And used RealNumber instead of PuertoRico

$JAVA_HOME/bin/java -Xmx6G -classpath "$SIGMA_SRC/build/classes:$SIGMA_SRC/build/lib/*" com.articulate.sigma.KB -ae "(instance RealNumber Christian)"
...
KB.main(): proof: [1. (forall (?VAR1)
  (=>
    (instance ?VAR1 Collection)
    (exists (?VAR2)
      (and
        (instance ?VAR2 Object)
        (member ?VAR2 ?VAR1))))) []  kb_SUMO_3115
, 2. (instance RealNumber Christian) []  conj1
, 3. (instance Christianity Collection) []  kb_SUMO_5166
, 4. (forall (?VAR1 ?VAR2)
  (and
....

Finds proof

$JAVA_HOME/bin/java -Xmx6G -classpath "$SIGMA_SRC/build/classes:$SIGMA_SRC/build/lib/*" com.articulate.sigma.KB -ae "(instance RealNumber Collection)"
...
KB.main(): proof: [1. (instance immediateInstance IrreflexiveRelation) []  kb_SUMO_8776
, 2. (forall (?VAR1 ?VAR2)
  (=>
    (instance ?VAR2 SetOrClass)
    (=>
      (instance ?VAR1 ?VAR2)
      (immediateInstance ?VAR1 ?VAR2)))) []  kb_SUMO_1135
, 3. (forall (?VAR1 ?VAR2)
...

Also finds proof.

But if I reduce KB to Merge only

  <kb name="SUMO" >
    <constituent filename="Merge.kif" />
  </kb>

the same command doesn't find proof

$JAVA_HOME/bin/java -Xmx6G -classpath "$SIGMA_SRC/build/classes:$SIGMA_SRC/build/lib/*" com.articulate.sigma.KB -ae "(instance RealNumber Collection)"
...
KB.main(): proof: []

[Regermeister]

Sorry if this is the wrong place to ask questions, but I read through the whole issue and still have the same questions/concerns that anka described.

The rule

(<=>
  (and
    (attribute ?INDIVIDUAL ?CH)
    (instance ?CH Christian))
  (member ?INDIVIDUAL Christianity))

implies that the following holds

(=>
  (member ?INDIVIDUAL Christianity)
  (and
    (attribute ?INDIVIDUAL ?CH)
    (instance ?CH Christian)))

so it makes claims about a variable ?CH that doesn't appear in the antecedent.

My understanding so far has been that any variable that is not explicitly quantified is implicitly universally quantified in the very top/outer level of the formula. That would mean that whenever an ?INDIVIDUAL is a member of Christianity, they have every attribute and every attribute is an instance of Christian.

What am I missing? Are variables that only appear in the consequent of an implication treated differently?

[apease]

I agree that the iff is incorrect and should be simply implication. I'll fix and upload shortly.