Re: [Core] updated safeness condition

I found that the definition is overly restrictive in the face of
disjunction; it required all variables to be safe in every disjunct,
even if the variable does not occur in the head. This is, however, a
situation we do want to allow.
I updated the definition yet again.

This disjunction in core is giving me a headache.
Would the difficulties of Jos with the definition of safeness be
sufficient grounds for getting rid of disjunction in core?  ;-)

Jos de Bruijn wrote:
> I updated the safeness condition to fix the technical problem I noticed
> during the telephone conference and to improve the presentation.  I hope
> it is now easier to follow.
> Please let me know if there are still problems in the presentation.
> 
> The problem with the previous version of the definition was that it
> allowed to assign "bound" to all variables, even those appearing only in
> external terms.
> I now make a distinction between safe and strongly safe variables, where
> the strongly safe variables are those that are made safe by non-external
> atoms.  It is required that all variables that are not strongly safe are
> assigned "unbound".
> 
> Please *read carefully* and criticize.
> And I remind you that it is not necessary to wait until the next
> telephone conference before starting to read the definition.
> 
> 
> Best, Jos
> 
> [1] http://www.w3.org/2005/rules/wiki/Core#Safeness

-- 
Jos de Bruijn            debruijn@inf.unibz.it
+390471016224         http://www.debruijn.net/
----------------------------------------------
No one who cannot rejoice in the discovery of
his own mistakes deserves to be called a
scholar.
  - Donald Foster