


HOME

Logic, Computation and Philosohy

Version 0.008 2024-01-12
Version 0.007 2020-03-31
Version 0.006 2019-06-06
Version 0.001 2014-03-19

Editors:: Richard Weyhrauch (IBUKI)

Note:

This is an internal IBUKI document and not available for general distribution. The information in this document (and its companion documents) is the confidential proprietary property of IBUKI. It contains trade secret, published and unpublished components. These documents and the IBUKI systems (appearing under various names) has been developed over a substantial period of time at IBUKI's expense.

Introduction

This note outlines the basic ideas of logic, computation and philosophy that I have found useful in my understanding of 'how thought can happen' without reference to what is being thought about. It is not an expositition or review of history, but, contains my interpetation of existing notions. It is wide reaching and I take responsibility for any misrepresentation of anyone's ideas. The observations here my take on various notions as they apply to my thoughts on 'the building of mind' and what I now call AI agents.

My goal is very general. I want to build an AI agent out of physical hardware including computers. Thus the 'mind' of my 'thinker/AI agent' must also be builtable out some combination of physical devices and structures that can be made in the memory of computer. My starting point is the notion of a formal system and the analysis of how formal systems have been used by logicians to explain thought.

I start with logic because I believe that the analysis of logicians of how and why formal systems are the good tools for describing understanding is compelling and has been under appreciated by AI researchers. As a result opportunity to leverage that work has largely been lost. That being said, the methods of logicians fall short (for my purposes) in at least two ways: the logicians tools for explaination is limited to text and the technical success of set theory and its reliance on infinite sets to explain 'meaning' has largely had the effect of overrunning other altrnatives.

-------------------------------------------------------------------------------
I full well know that 'category theory' has many adherents as an alternative
to set theory, but my remarks below will be equally applicably to these 
theories as my ideas will suggest scrapping the notion of 'theory' itself.
-------------------------------------------------------------------------------

In the first section we list the relavant first order notions of logic. We restrict ourselves to first order notions because: 1) they are necessary; and, 2) perhaps less obviously, with careful formulation we believe that they are all that's needed (i.e., they're sufficient).

The second section deals with how the logical notions enumerated in part one can be reinterpreted in light of my goals and my understanding of modern computers. This is not to ignore the notions of logic, but to ask how the results of logicians, like Skolem or Hilbert or Gödel, should be seen now that actual computers are commonplace and we know how they work not just theories about computability, i.e., recursion theory. For the most part, the logicians notion of theory and computation predate the existence of modern computers and the ideas of programming languages. My goal is to build an AI agent. Section two inroduces my ideas about how to interpret and use the notions of logic with computational and information centric ideas. The most radical result of this work is a view of 'thought' that lies somewhere between nominalism and ultra-finitistism and whose foundation is information and computation not set theory.

Section two reviews some notions of computation. Because the understanding of both the proof theories and the model theories of traditional logic are grounde in an understanding of the infinite sets the goal here is to show how these abstract ad infinitary ideas can be rethought to be realizable as 'data' in the 'head' of an AI agent.

Many issues discussed by philosophers center on questions of how our understanding of the world works. These are the same issues that will confront an AI agent. Section three explains how these issues inform me about how an understanding of the 'real' world can be developed at all.

This is followed by a bibliography of both introductory and advanced reading.

Logic: First Order Notions

The notions of logic described in this section are basic ideas of logic taught in an introductory course that describes first order logic and its semantics. It is these notions that we intend rethink using finitist information theoretic ideas in a system called NEWFOL.

The Notion of a Theory

The notion of theory usually refers to a set of formulas that are closed under deduction, i.e., 'deductively closed'. To make sense of this description we need to also understand several other notions. The notion of a 'language', specified a collection of symbols and which expresssions, built using these symbols are well-formed, i.e., well-formed formulas or [wff]s. The notion of a 'model' that decribes a non-empty collection of objects that the theory is about; an 'interpretation' which assigns members of a model to the symbols of a language. An interpretation, i.e., a map between the symbols of a language and a model that asssigns a truth value to each [wff].

theory, satisfiable, consistent, consequence, validity

   A wff is true in a model if its interpretation is true (in the model)
   A wff is 'satisfiable' if this exists a model in which it is true
   A wff is 'valid' if it is true in all models (eg (implies A A)
   A collection of wffs is 'consistent' if there is at least one model in which
     all its formulas are true
 
   The semantic notion of 'consequence' is
     A wff  'is a consequence of' a collection of wffs, WFFS
       if whenever all the wffs in WFFS are true in a model then so is wff
     A 'rule of inference' is a map from collections of wffs to a wff
       (or in some formulations collections of wffs) where, if all the 
       arguments of the map are true in a model then so is the wff.
     A 'valid rule of inference' is a rule that has the property that it maps 
       collections of valid wffs onto a valid wff.
     A set of 'rules of inference is called 'complete' if all valid wffs are 
       the consequence if some collection of valid ri=ules of inference.

The Notion of a First Order Language

Symbols

One way of defining a first order language is to specify a finite collection of individual symbols, function symbols, relation symbols; and appropriately constants and parameters for each. The language may also contain variable symbols ranging over individuals, but it is first order because there are no variable symbols ranging over functions or relations.

Terms and Wffs

First order logic defines two kinds of expressions: terms, [trm]s, for naming objects and well formed formulas, [wff]s, for describing sentences about those objects. [wff]s and [trm]s are syntactic objects, i.e., [text].

The definition [trm] and [wff] can be defined uniformly in a First order language which specifies a finite number of individual symbols, function symbols, relation symbols; constants, variables, and parameters. The logical symbols (like 'and' and 'or') are common to all NEWFOL contexts.

Logicians have described various algorithms for determining if an expression is a [wff] or a [trm]. We call programs that implement algorithms that tell if a data structure is of a particular [sort] a recognizer. Even though we have such a recognizer (which, as a program, is itself a finite thing) and even though the collection of symbols in the language is finite, the collections of 'recognizable' [trm]s and [wff]s is unbounded.

Summary

NEWFOL writes them using s-expressions, [sexp]s, a la LISP and use their associated data structures (called m-expressions in Lisp 1.5) when building computer systems.

In the following when we use the word language we mean the first order language of some NEWFOL [context].

Finitization

      The collection of examples of [wff]s in a NEWFOL language is 'infinite'
      BUT we replace this 'set' (in the context Meta) by a [sort] predicate,
      WFF?, and attach it to a program (implementing the logicians algorithm)
      that takes an [object] and returns True or False depending
      if the [object] is a [wff] or not. This algorithm is 'uniform' in the 
      [fol-language]. By definition, [fol-language]s only contain a finite 
      number of symbols an the language of NEWFOL is finitely determined by
      a finite collection of [symbol]s and a finite collection of recognizers.

      For example, in the NEWFOL [context] Meta we attach the SEUS program
      #'WFF?, the recognizer for [wff]s, to the [sortsym] WFF?.  #'WFF?
      implements a primitive recursive function

      We implement a NEWFOL language as a finite collection of [symbol]s and,
      as described above, a collection of recognizers (programs) that take
      as arguments an object (a data structure) and a NEWFOL language (ie
      another finite structure) that determine the [sort] of the object.
      Since all our [object]s are IBML types the existence of such a program
      is guaranteed by the semantics of the IBML type system.

      The idea of a recognizer is a program that tells you (for any [object])
      if it is 'recognized' to be of a particular type. In the implementation
      of NEWFOL recognizers will be written in SEUS (implemented as a
      restartable computation system) and by convention: if [name] is a 
      [type-name] then: |name| is a lexical (term as spoken not logical)
      expression; '[name]' is the symbol that names the type in any NEWFOL
      [context] mentioning it; 'NAME?' is the [sortsym] that name's the
      recognizer of that [sort]. Like LISP use #'name as the read/print
      name for the recognizer in SEUS, which is the attachment of the 
      [sortsym] NAME?  '[name]' gets attached to the type tree for the
      type and NAME? is attached to #'NAME.

      This is actually simple in practice but probably needs an example to 
      be better understood.

The strategy here, to reformulate the ideas of logic as finite structures is one of the important techniques used to remove the infinitary aspects of reasoning systems. This idea has its origin in Skolem's interpretation of arithmetic in the 1928 paper where he informally uses the idea of recognizer rather than set.

In the NEWFOL system we extend the usual language of first logic by introducing a subset of predicate symbols called [sort]s. Each [sortsym] in the language is a predicate symbol with one argument that is used to name the predicate that reconizes things of that [sort]. We also allow the use of individual variable and parameter symbols whose domain is restricted to only include [object]s of that [sort]. In order to assure that the semantics remain first order and that the 'relatativised' quanterfier rules are sound we require that there is at least on thing of that [sort]. This corresponds to the fact that in normal semantics of first order theories, the domain of a model must be non-empty. This means that the declaration of a [sort] in NEWFOL requires that

      (exists x (SORT? x))

is a consequence of the context.

Since all [object]s in a NEWFOL simulation structures are IBML types, each [sort] corresponds to a type and the recognizer for that type is the natural attachment to its [sortsym]. By convention: if we have a type named [name] then its crresponding [sortsym] is NAME? and its recognizer is DEFLAMed to be NAME? and any FOL context that has 'NAME?' in its language has the program #'NAME? attached to it.

Since the interpretation of a [sort] is a [type] the partial order on [sort]s must correlate with the subtype relation on [type]. So we have

      (implies
        (and (more-general s1 s2) (isin t1 s1) (isin t2 s2))
        (subtype (attachment-of t1) (attachment-of t2))

in the elementary theory of some context.

The Notion of Model

  Model.  A collection of things usually defined in 'set theory.
 
Finitization
   Simulation structure 
   where 'individual constants are also attached to functions
     allowing us to define boundaries, sensors and effectors
 
 
Logical notion
Interpretation of a formula in a model
 
 
Finitization

A program for evaluating an expression WRT a simulation structure

Since programs are restartable and simulation structures do no always know
the answers we alter the interpretation 'function' of logic to be a
restartable computation where we introduce the value IDK (I don't know)
which is returned whenever 1) the computation is not DONE? or 2) if the
simulation structure simply 'doesn't know'. In fact, in a context without
any attachments (i.e., having the 'empty' simulation structure) the 
interpreter will always return IDK, so a term always has an interpretation
in a context, but it may be 'I don't know'!!! a formalization of ignorance
(problematic for philosophy) ditto for wffs.  It may seem at first that IDK
introduces a third truth value. Our interpretatoion is rather different. We
imagine that all terms have values and all wffs are either True or False BUT
in some contexts (with limited computing resources) we may not be able to
tell. In fact interpretation could produce IDK sometimes and a value others.
A property of contexts without hardware attachments, however, is that if
it ever returns a value that is not IDK the it must always return this value.
This 'partialness' is a unique property of NEWFOL.
 
SIMPLIFY is a very cleaver operation in FOL. It is called SIMPLIFY because if
you give it an expression in a context it tries to return a 'simpler'
expression. Of course simplicity is in the eye of the beholder but in simple
cases it means replacing terms with constants and producing propositionally
simpler wffs if it can. eg
  3+4 ==> 7  or 
  2<3 ==> true (with their standard meanings in arithmetic)
   
In the wristwatch case if we asked it "What time is it?" after we declared the
symbol 'now' but before we did the Hardware attachment SIMPLIFY would have
returned the wff "now = now" meaning that it didn't really have a meaning of
'now' so that was the best it could do. I gave the result after making
the attachment (with the correct reptype) so it not only could find an answer
but also could say the answer in the language of the context. This is a subtle
point. When we ask for the value of 'now' in the SS (simulation structure) it
could correctly have computed its value, but the language may not have had a
name for it. In the case of numbers this is additionally confusing because we
generally use '6' both for mentioning the number 6 and the numeral |6|.  For
integers FOL knew about this and if a number was returned as the value of an
attachment and the context 'knew about' arithmetic the if it already had (in
its language) a numeral for this number it used it and if it didn't it
silently made one and used that!!!! If we used roman numerals so our context
used |vi| to 'name' the number 6 it might be less confusing but less 'normal'.
The use of the same 'word' in natural language to mention an object and its
name has confused linguists and AI persons. Here we win because in our mental
model of arithmetic numerals are part of the language and numbers are in the
SS. Since we separate the mental images of our thinker from the sentences it
would use to describe its mental images we can have our cake and eat it too!!!
I daon't think anyone else does this
 

Logical notion:
  Theory. satisfiable consistent,  consequence, validity
   A wff is true in a model if its interpretation is true (in the model)
   A wff is 'satisfiable' if this exists a model in which it is true
   A wff is 'valid' if it is true in all models (eg (implies A A)
   A collection of wffs is 'consistent' if there is at least one model in which
     all its formulas are true
 
   The semantic notion of 'consequence' is
     A wff  'is a consequence of' a collection of wffs, WFFS
       if whenever all the wffs in WFFS are true in a model then so is wff
   A 'rule of inference' is a map from collections of wffs to a wff
     (or in some formulations collections of wffs) where, if all the 
     arguments of the map are true in a model then so is the wff.
   A 'valid rule of inference' is a rule that has the property that it maps 
     collections of valid wffs onto a valid wff.
   A set of 'rules of inference is called 'complete' if all valid wffs are 
     the consequence if some collection of valid ri=ules of inference.
 
       
Finitazation
   An FOL context is the finite realization of a theory
 
 
Logical notion
  consequence, rule of inference - validity and satisfaction
 
Finitization
  FOL a rule of inference is a satisfaction preserving operation on
  [fol-context]s

Computation

Side effects - IO

state

error hndling

restartable

resource bounded

m-expressions VS s-expressions
or programs vs data

programs as data

Interactive Computing

Building structure - updating

'pointers' - sharing vs not

interning

Computation Systems

Philospphy

Universals

Catagories

Plato
Martius Cappella
St.Augystine - Boethius
Oakham - nominalism
Hamilton
Frege
Russell
Skolem
Godel

References - Compution

Turing

Kleene

Landin

Scheme

RUM

computation systems

References - Philosophy

Aristotle

St. Augustine

Bothius

References - Logic