erence 
rules for upward and downward reflection, so it will have a 
considerably extended semantic theory which has not yet been fully 
worked out. It ought to be capable of describing meta-languages to 
any depth,in principle, though I imagine that it would rapidly become 
unworkable in practice beyond two metalevels.

However, none of these will be genuinely higher-order. All extensions 
of the language will be compact and have finite axiomatisations, and 
will be efficiently implementable.

Hope this he