circular paradox gizmo

[from the 2002-05-02 WebOnt WG telecon minutes]

> PeterPS: if we're after test cases that show the *problem*, see the
> circular paradox gizmo. It does use cardinalityQ; I could get rid of
> that using complementOf, but that gets hairier
>
> In IRC, PeterPS provided:
>
> _:1 fowl:onProperty rdf:type .
> _:1 fowl:hasClass _:2 .
> _:2 fowl:OneOf _:3 .
> _:3 fowl:first _:4 .
> _:3 fowl:rest fowl:nil .
> _:4 fowl:complementOf _:1 .
>
>   _:1 is the set of objects
>   that are related to a particular complement of _:1
>   via rdf:type
>
>   if x rdf:type _:1
>   then x rdf:type _:4
>   but _:1 and _:4 are complements
>
>   so not x rdf:type _:1
>   if not x rdf:type _:1
>   then x rdf:type _:4
>   because _:1 and _:4 are complements
>
>   but then x rdf:type _:1
>
>   the above is another problematic situation
>
> JimH: in sum, we're still working on SEM/dark triples stuff.

Peter, you seem to go like
either
  every formula has to exist in every model
  and one can write a paradoxical formula in OWL
  so there exists a paradox in every model
  and therefore the system is fundamentally broken
  --
  that sounds like a self fulfilling prophecy
  I find one of the most important characteristics
  of a model that it captures the *correspondence*
  between the-name-of-the-thing that we have in the
  assertional language and the-named-thing expressed
  in the object language (using e.g. URI decoupling)
  I just can't find such correpondence for a paradox
  so how could they exist in every model ???

or
  one wants to prove a paradox by assertion of its
  negation and finding a contradiction
  which is succeeding here, so the paradox is proved
  of course it is, you have *asserted* an inconsistency
  and one should not do that
  --
  I would make the claim that one cannot prove nor
  disprove a paradox, we just have incompleteness
  (no evidence/correspondence)

--
Jos

Received on Thursday, 2 May 2002 18:52:06 UTC