Re: So let me get this right: (Was: NFNF vs 1NF ...)
Date: Sun, 13 Feb 2005 10:58:13 GMT
Message-ID: <9pGPd.10637$UW7.486527_at_phobos.telenet-ops.be>
Dan wrote:
> "Jan Hidders" <jan.hidders_at_REMOVETHIS.pandora.be> wrote in message
> news:65qPd.9956$ve3.633922_at_phobos.telenet-ops.be...
>
>>paul c wrote: >>
>
> Hello Jan,
Hi Dan,
Btw. apologies in advance if I drop out out of the discussion without notice. My job can sometimes quite unexpectedly get very time demanding and my personal life has also gotten a bit busier lately.
>>>i'm sure your motives are pure. that's not my question. i'd just like >>>to know: "what is the theoretical problem with RVA's?" >> >>There are no theoretical problems with RVA's. Usually they are typed,
>
> I'm not sure what you mean by typed. Are you referring to domains and a
> declaration of them? Or is this a new activity in typing RVA variables by
> associating pre-declared domains and higher order relation variables in some
> manner?
Both. It means that in your logic all your variables and constants have types associated with them and that for these types you have in advance defined what all the possible values are. These possible sets should be defined in a non-recursive way, as is required by type theory. Note, btw., that this does not exclude recursive types as long as they can be defined as subsets of non-recursively defined types.
>>which prevent's Russel's paradox, but even if you don't like that, then >>you can prevent it by restricting yourself to non-recursive values, and >>even if that is too strict for you you can use non-well-founded sets and >>still not have any problems with paradoxes.
>
> Given the gap between the internal and external predicate in a system, I
> don't know how one could guarantee this, even theoretically. It would seem
> reasonable to allow a set of redundant recursive domains within a nested
> structure where the FOL predicate does not result in a paradox. Can a model
> discern potential paradoxes without understanding the semantics of the set
> of predicates?
No, but it doesn't have to. The point is that the model (or actually the meta-model, to be more exact) introduces restrictions on which type of sets you can specify and how you must specify them in order to avoid the type of undefinedness you see in R's paradox. If a modeller then wants the specify a certain set that does not fit into this framework then he or she will notice this because it will simply not be possible to specify it.
- Jan Hidders