This is very very preliminary - do NOT quote
This is tricky

We define [head] which has a name and
  a [Tsys]
  a [Csys]
  a [Lsys[
and a physics


Then we want to define the minimal practical head, [head0]
  Tsys0 (type system)
    contains type definitions that 
      use sentences of [Lsys0]
  Csys0 (computation system)
    containing the facility for manipulating types
    including
      [tree-type]s
      programs that are [program]s
  Lsys0  (logic system)
    contains the properties of and relations between types
    including sentences that
      containing [IndSym]s that name [type]s in [Tsys0]
      containing [FunSym]s that name [program]s in [Csys0]
     
------------------------------------------------------

(|type| [head] |subtype| [named-object]
  (|name| [headName])
  (|Tsys| [Tsys])
  (|Csys| [Csys])
  (|Lsys| [Lsys])
  (|context| [FOL context] )

(type [Tsys] subtype [obj]
  (name *type [TsysName])
  (typetable *type [TypeSpec] :range [0-INF])
  (types *type [TypeTree] :range [0-INF])
)

(type [Csys] subtype [obj]
  (name *type [CsysName])
)   

; this is a NEWFOL context
(type [Lsys] subtype [obj]
  (|name| [lsys-name])
  (|signature| [signature])
  (|language| [language] :where (= language.signature signature) )
  ([model| [model] :where (= model.signature signature) )
  (|facts| :type listOf[Fact] :where (isin (wffof facts.fact) language)
)

(type [signature] subtype [tuple]
(type [language] subtype [????]
  (signature  )
)
(type [model] subtype
  (signature  )
)
(type [fact] subtype

; note: this is amazingly incestuous

; The following go together
; (deftype [] subtype [type] ... )
;    
;   defines a type         called [name] and (ex [name] [symbol])
;   defines a [TypeDesc]     which is added to the [TypeTable] (in Tsys)                     
;   defines a [program]    called #'NAME? (in Csys) a [recognizer]
;   a [sortSym] called     NAME? (in Lsys) with attachment to #'NAME?
;
; in addition
;   wffize([program]) ex [wff]
;   programize([wffFunDef]) ex [program]
;   (attach funSym(wffFunDef) programName(program)) is implied   
;

;; Ur-Head 

(build Head0 in [head])

;; Tsys0

[top]

[obj| < [top]

; data types

[data-type-name] < [symbol]
  {[tag]
   [number]
   [character]
   [string]
   [symbol]
   [pair]
   [list]
   [sexp]}

;; [boolean]
[bool]  <=> { :true :false }
[idk]   <=> { :idk }
[bool+] <=> Union[[bool],[idk]]  

;; [integer]
[integer] <=> {x ex [obj] | (INTEGER? x) }
;; [rational]
[integer] <=> {x ex [obj] | (RATIONAL? x) }

;; [symbol]
[symbol] <=> {x ex [obj] | (SYMBOL? x) }

;; [character]
[character] <=> {x ex [obj] | (CHARACTER? x) }

;; [string]
[string] <=> {x ex [obj] | (STRING? x) }

;; [sexp]
[sexp] <=> Or[ [scaler] , listOf[sexp] ]

----------------------------------------------------
(type [type-name] subtype [symbol]
  (typedef [type-name] 
    {sym | (and (= (str-char (pname sym) 1) #\[)
                (= (str-char (pname stm) (length str)) #\]) ) }
   ) )

[tuple] <=> Tuple[[obj], ... , [obj]]
(type [typeDef] subtype [sexp]
   (typedef [type-def] Or[[type-name],[finite-set],[bounded-comprehension], ... ]) )

; Ctyp

[program]
[dmop]
[dmop] < [program]


;; Csys

; interface to implementation
(declare [dmop] '(#'EQUAL '([bool+] [obj] [obj])) 
(declare [dmop] '(#'OBJ? '([bool+] [obj])) 
(declare [dmop] '(#'SYMBOL? '([bool+] [obj])))

;; named programs

(define [program] BOOL? #'(lam (x) (or (= x :true) (= a :false)))
(define [program] IDK? #'(lam (x) (= x :idk))
(define [program] BOOL+? #'(lam (x) (or (bool x) (idk x)))
(define [program] OBJ? '#'OBJ?)
(define [program] SYMBOL? #'SYMBOL?)

(define [program] = #'EQUAL)

(define [program] subtype ...)

; Lsys
(declare [UniversalSort] OBJ?)
(declare [SortSym] SYMBOL?)  
(deflare [IndVar] x [obj])

; Tsym
(deflare [RelSym] Subtype 2)
(deflare [RelSym] Isin 2)
(deflare [RelSym] Example 2)

; Csym
(declare [SortSym] 'PROGRAM?)
(declare [SortSym] 'DATA?)
(declare [SortSym] 'COMPUTATION?)
(declare [SortSym] 'DONE?)
(mg [computation] [done])
(declare [SortSym] 'NCDONE?)
(mg [computation] [ncdone])
(declare [SortSym] 'LABELABLE?)
(declare [SortSym] 'RESOURSE?)
(declare [SortSym] 'LABEL?)
(declare [SortSym] 'RELABEL?)
(declare [SortSym] 'ENVIRONMENRT?)

(declare [IndVar] 'P [program])
(declare [IndVar] 'd [data])
(declare [IndVar] 'resource [resource])
(declare [IndVar] 'lab [label])
(declare [IndVar] 'env [env])
(declare [IndVar] 'args ListOf[data])
(declare [IndVar] 'cmps ListOf[computations])
(declare [RelSym] 'compat ([bool+] [computations] [computations]))
(declare [RelSym] 'run ([bool+] [computations] [data]))
(declare [FunSym] 'const {p | (imp (ex d [data]) (= p #'(lam (x) d))) }  ; this need review
(declare [FunSym] 'const {#'(lam (x) d | (ex d [data])}  ; maybe ???
(declare [RelSym] 'result ([data] [done]))
(declare [RelSym] 'apply ([computation] [program] [enviroment] ListOf[computation]))
(declare [RelSym] 'rcompose ([resource] [resource] [resource]))
(declare [RelSym] 'labsOf setOf[label] [program]))
(declare [RelSym] 'relabelApp ([program] [relabel] [program]))
(declare [RelSym] 'labsOf setOf[label] [computation]))
(declare [RelSym] 'relabelApp ([computation] [relabel] [computation]))
(declare [RelSym] 'step ([computation] [resource] [computation))
(declare [IndConst] 'yes [data])
(declare [IndConst] 'no [data])
(declare [IndConst] 'nc-cmp [ncdone])
(declare [IndConst] 'nc-pgm [program])
(declare [IndConst] 'mt-rsc [resource])
(declare [IndConst] 'mt-env [environment])

(declare [IndConst] 'MtList [list])
(declare [IndConst] 'MySet [mtset])
(declare [IndConst] 'MyMap [???])
(declare [IndConst] 'MyMap [???])

(assert C1-1 (DONE? (const d)) axiom)
(assert C1-2 (= result(const(d)) d) axiom)
(assert C2 (if (DONE? cmp) then (= (step resource cmp) cmp) axiom)
(assert C3-1 (= (step mt-rsc cmp) cmp) axiom)
(assert C3-2 (= (step (rcompose resource1 resource2) cmp)
                (step (resource1 (step resource2 cmp))) axiom)
(assert C4-1 (iff (NCCMp? cmp)
                  (forall resource (not (DONE? (step resource cmp))) )
             axiom)
(assert C4-2 (NCCMP? mtcmp) axiom)
(assert C5 (NCCMP? (appply nc-pgm anv cmps) axiom)
(assert C6 (forall resource1 resource2
  (if
    (and (DONE? (step resource1 cmp)) (DONE? (step resource2 cmp)) )














   then
    (= (result (step resource1 cmp)) (result (step resource2 cmp)) ) ) )
  axiom)  
(assert C7 (forall cmp1 cmp2
  (iff
    (compat cmp1 cmp2)
    (forall resource1 resource2
      (if
        (and (DONE? (step resource1 cmp)) (DONE? (step resource2 cmp)) )
       then
        (= (result (step resource1 cmp)) (result (step resource2 cmp)) ) ) ) )
))

(assert compat-1 (compat cmp cmp) lemma)
(assert compat-2 
  (if (compat cmp1 cmp2)
   then (compat (step rsc1 cmp1) (step rsc2 cmp1)) )
  lemma)
(assert compat-3 (compat cmp (step rsc cmp)) lemma)

(assert def-1
  (iff
    (stepper-fixed-point cmp)
    (and 
      (not (DONE? cmp))
      (forall resource env (= (step resource cmp) cmp)) ) )
  definition stepper-fixed-point)

;; needs work
(assert C8
  (if
    (and 
      (= (listLen cmps) (listlen args))
      (forall (i `(range 1 (listLen args))) (= (listElt cmps i) (const (listElt args i)))) )
   then
    (=
      (call P env args)
      (apply P env cmps) ) )
  (definition call) )
(assert C9
  (=
    (run cmp u)
    (exist resource 
      (and
        (DONE? (step resource cmp))
        (= (result (step resource cmp)) u)) ) )
  (definition run) )
(assert unicity
  (if 
    (= (and (run cmp u) (run cmp v)) 
   then
    (= u v) ))
  lemma)
(assert E1 
  [labables] <=> union[[program],[args],[computation], ...]
  axiom)
(assert E2
  [environment] < finiteMap1[[labable],[label]]  
  axiom)

More later

; Fsym - the sorts
[Fsignature]

[branch] <=> Pair[[label],[type]]
[tree-type] <=> TreeType[branch] where (Disjoint (labels-of [branch]))

[tree-type] < [typeDef]

[TypeTree] < [sexp]


(declare [sortSym] 'SIMILIARITY-TYPE)



(deflare [sortSym] 'Wff)

(attach 'OBJ? #'OBJ?)
(attach 'SYMBOL? #'SYMBOL?)
(assert (Value #'= [bool+]))
(assert (Recognizer 'INTEGER?))

(assert (forall (p [program])  
          (iff (Recognizer p) (forall (o [obj]) (Typeof (Valueof (run p o)) [bool+]))) ) 

or
(declare [indVar] p [program])
(declare [indVar] o [obj])
(assert (forall p (iff (Rcognizer p) (forall o (Typeof (Valueof (run p o)) [bool+])))) )

------------------------------------

(declare [indVar] n [natnum])
(assert (forall n
  (iff (Even n) (and (not (= n 0) (= n 1) (if (= n 2) :true (Even (- n 2))))))) ) 
(defun even (n)
  (and (not (= n 0) (= n 1) (if (= n 2) :true (even (- n 2))))) )
(assert (Provable (Recognizer #'even)
(type [even] subtype [integer]
  (typedef [even] {n | Even(n) }) ) 


note:
 (attach Even even)
 (attach #'even even)
are implied???

Suppose [a] <=> { t1, ... , tn } and (ex ti [scaler])

Conservative-Extention(add-syntable([app],[a]))

 (iff (Conservative-Extension a2 a1)
   (forall (x1 a1) (x2 a2)
     (and
       (if Proves(a1,'(Subtype(x1,x2))) then Proves(a2,'(Subtype(x1,x2))) ) and
       (if Consequence(a1,wff) then Consequence(a2,wff)) )

 (iff (Provable(wff,app)
   (and 
     (ex wff [wff])
     (Consequence(wff,facts(app)))


 )

Lsys0

; Ltyp

[term]
[awff]
[wff]