BLD issue: non-disjointness of internal and external predicate symbols

There is an issue in BLD, which I unfortunately did not catch before.  I 
think it is probably an omission in the definition, but it is a 
substantive one.
If we all agree that it is indeed an omission, we can probably address 
the problem, create a new frozen version, and vote about publication in 
the next phone conference on Tuesday.
Personally, I am not ready to sign off on publication before this issue 
is resolved.

The issue is the following: in the definition of well-formed terms, the 
set of all symbols is partitioned into predicate symbols, function 
symbols, etc. however, no distinction is made between external and 
"internal" symbols.  The consequence is that the same function or 
predicate symbol can be used both in an external term and an internal 
term, and these two terms have different meanings, i.e., the same 
constant is interpreted differently based on the context, which is 
something we explicitly wanted to avoid in BLD.  So, a built-in function 
may be used outside an external term and will be uninterpreted.

The problem is easy to fix by defining additional sets of external 
predicate function symbols that are disjoint from the other sets of 
symbols and defining appropriate restrictions on external terms (i.e., 
the first function/predicate symbol in an external term must be an 
external symbol).
It becomes a bit more tricky when considering external frames, but 
probably all constants used in an external frame should be external 
individuals/functions/predicates.

Best, Jos
-- 
                          debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
One man that has a mind and knows it can
always beat ten men who haven't and don't.
   -- George Bernard Shaw