


HOME

NEWFOL: Sorts
Relativising Quantifiers

Version 1.001 2024-07-03

Author:: Richard Weyhrauch (IBUKI)
Note:: This is a personal document of Richard Weyhrauch hosted by IBUKI at http://rww.ibuki.com . This document is not in the public domain. The copyright is held by him and anyone wanting to reprint it must get his permission in writing. This document was written while he was employed by IBUKI but on his own time at at his own expense.

Sorting out Sorts

The original FOL notion of sort was a monadic predicate, S, with the implied axiom

(EXISTS object (S object))

that is, there was at least one object of that sort.

NEWFOL extends the the [language] of a NEWFOL []context] to includde the syntactic types sort constants and sort parameters: [sort] and [sortpar] respectively. As in FOL, we can treat any [sort] as a domain and define a partial order on [sort]s without using set theory and comprehension rules.

In NEWFOL you can specify that one sort is 'MORE-GENERAL', MG, than another. This introducedsthe implicit axiom

(FORALL object (IMPLIES (SORT2 objecT) (SORT1 object)))

NEWFOL also allows individual symbols to have a default [sort], changes the quantifier rules to account the partial order on sorted variables and acilitates building multi-sorted [context]s. theories. The changes to the quantifiwer rules are stated in the 1973 FOL Manual [Weyhtauch 1074] and a technical description (with proofs that the augmented rules are correct) can be found in [.... 19..].

For example, we could write

 (declare-sort CLASS?)
 (declare-indvar class CLASS?)
 (declare-sort SET?)
 (declare-indvar set SET?)
 (declare-more-general CLASS? SET?)
 (declare-predconst EPSILON 2)

meaning that (in the current context): the symbol 'CLASS?' was to be used as a predicate symbol and was specified to be a sort and 'class' was to be used as an individual variable that ranged over the sort 'CLASS?'. As a consequence

  (EXISTS obj (CLASS? obj)
  (FORALL class (CLASS? class))

likewise for 'SET?' and 'set'

  (EXISTS obj (SET? obj)
  (FORALL set (SET? set))

and finally

  (FORALL obj (IMPLIES (SET? obj) (CLASS? obj)))

  (FORALL set (CLASS? set))

EPSILON is declared with

  (declare-predconst EPSILON 2)

Here the '2' tells us that EPSILON takes 2 arguments.

NEWFOL also extended the declaration of function and predicste symbols to contain information about sort restrictions.

The power of this becomes clear if you want to use the set theory in [Godel 1940]. ,pre. Group A 1. (CLASS? set) 2' (IMPLIES (EPSILON class1 class2) (SET? class1)) 3. (IMPLIES (FORALL set (IFF (EPSILON set class1) (EPISLON set class2))) (EQAUAL class1 class2) ) 4 (FORALL set1 (FORALL set1 (EXISTS set3 (IFF (EPSILON set4 set3) (OR (EPISILON set4 set1) (EPISILON set4 set2)) ))))

If NEWFOL had used the [Wang 1940] notion of many-sorted logic it would have been mecessary to formalize set and classes as disjoint and to introduce four versions of EPSILON to account for its use with both sets and classes. This, of course, is doable but the axiomatization as presented by Godel is clear whereas the on using Wang is not, to my mind, straighforward. This is a clear case where a simple reworking of a traditional formalization of some notion allows for a sizable improvement in the naturalness of epression without leaving behind basic fiRst order semantics.

Relativising Reasoning

There is an even more interestion way of looking at this. Somewhere (written down by Kleene (I think} which I remember but cannot find a reference) there is a proof that the quantifier rules for expressions using bounded variables, i.e., whose range is a predicate the determines a non-empty subset of the domain of a model, (ie like the sorts above) are identical to the rules for expressions over variables over the full domain of the model (ptovided some additional properties hold (e.g., the restricted 'domain' is not empty)). This shows that the introduction of bounded qunatification is a conservative xtension of the original system.

Introducing the sort hierarchy as above opens another way of looking at this. It basically says that any non-empty subset of the domsin of the model can be considered a domain and can itself be considered everything.

In fact I prefer thinking of this in reverse, i.e., our theory could be a a relativized piece of any 'bigger' theory whose model is a superset of the model of our theory and satisfies some simple restrictions. This point of view allows us to imagine any theory as embedded in some possibly more comprehemsive environment.

[sort]s as an IBML [type]s

The IBUKI modeling Language, IBML, is a language for describimg things. IBUKI believes IBML types is expressive enough model real-world objects as finite data structures that can be used in autonomous systems as the 'mental models' of real-worlds objects whose semantics can be described by a NEWFOL [context].

(type [sortsym] subtype [symbol]
  (defined-by recognizer
    (|deflam*| (sym)
      (let ((name (sym-get-name sym)) )
        (AND
          (EQUAL (str-get-last-chr name) \#?)
          (ALL-CAPS-AND-DASH (str-substr name) 0 (1- (str-length name))) 
        ) ) ) ) )

When this type definition is processed by the IBUKI Context Builder the following things happen

 (declare-sort ?)
 (declare-more-general ? ?)

   what happens
   FOL declares  as a [sortsym]
   FOL declares 
   LSEUS defines a function

Technical Detains