The Building of Mind
Putting it All Together
By Richard Weyharuch

Preface

This paper explains my ideas about building an artifact that can think. I have not used 'theory of mind' because its usually reserved for explainations of how the human mind works. I am more interested in the question of what are the properties an individul needs to have to understand the world it's in and to form sucessful communities with other individuals.

A little History

My search for answer to these questions started in the early 1970s and continues today. I received my Ph.D. in mathematical logic from the mathematics department of Stanford under Soloman Feferman and with the kind guidence of Jean van Heijenoort (who was at NYU) and Georg Kreisel (who was in the Stanford philosophy department) and may others. After that I took a job at the Stanford Aritifical Intelligence Laboratory {SAIL) where, under the leadership of John McCarthy, I learned about computers and the hopes of using computers to do AI. At the beginning I believed that my knowledge of formal logic would immediately translate into 'smart' programs satisfying John's dream of real AI.

My initial work was with Robin Milner on program verification using LCF, a program that allowed you to define a program, p, and then used the commands of LCF to construct proofs of theorems about p. Since the LCF command were 'sound' with respesct to the semantics of Dana Scott's 'Logic for Computable Functions', using LCF to construct proofs had the effect of also verifying the correctness of the proof of each theorem. LCF was the first 'proof checker' (now called 'proof assistants') and the grandfather of many type-theoretic proof assistents including LEAN.

At the same time McCarthy had tasked Whit Diffee (of encription fame) with building a proof checker for first order logic. They called it PCHECK. (Note: all remnants of PCHECK including code and documentation have disappeared.) When Milner left SAIL I proposed replacing PCHECK with FOL, a program that used the LCF architecture to build a first order logic proof checker and replace PCHECK.

My idea was to test FOL in two ways: could FOL check the proofs of the logic theorems of Principia Mathmatica by Whitehead and Russell (a logicians favorite); and to see if the homework questions of undergraduate mathematics and logic courses could be answered in FOL and if the answers were 'handed in' would they get good grades?

The first test went was complated but was complicated by simple but annoying differences. Ther second test was a failure. It revealed that although the formalizations of mathmatics made by logicians were unusable for two main reasons. Sophisticated encodings of ideas were made to make theorems and meta-theorems easier to state and prove. Meta theory was treated informally although it was understood that it formalization was 'straight forward' but tedious. More importantly both the syntax and semanics of logic had become dependent on set theory and was not friendly to computers. Many of the common practices of mathmaticians use meta-mathematical results without mention and although logicians have addressed these issues they are not even mentioned in math books that use them. e.g., statements about the properties of subgrouops cannot even be stated in the language of the elementary theory of groups no less proved.

A program that can take a course in algebra must be able to use these principles even if they haven't articulated or proved them.

To be fair, the use of set theory (even in the foundations of recursion theory) was done long before there were actual digital computers.

The good news is that the analysis of valid consequence made by logicians was amazingly good and can be understood and used without using infinite sets. This is the secret of the discussions below.

Note: To paraphrase an observation made by John McCarthy on many occasions, "It is not possible for a program to find a proof of a mathematical theorem if it can't recognize and manipulate them." This observation suggests that building a 'proof checker' before tackling a 'theorem prover' is a good idea.

New Interpretations of Old Ideas

One of the unfortunate consequences of the developnment of set theory was the discovery that when using set theory in the foundations of mathematics there is no need for non-empty sets to contain anything but other sets. This removed the need for mathmatical logicians to confront the issues of epistomology, ontology and metaphysics that occur if there are things that are not sets. To be crude mathematicakl foundations based on set theory doesn't need sets of dogs. Real thinkers and AI agrnts do!!!

Another problem with set theory is the existence of infinite sets. NEWFOL uses the idea of a recognizer as thr replacement for the idea of set membership. The recognizer of a 'set' is a program that given any object

returns TRUE for objects it knows are in the set
        FALSE for objects it knows are not in the set
        IDK if it can't decide

The use of IDK (I don't kbnow) here does not mean that NEWFOL is a three valued logic!!! the object is either in the set or not. i.e., the logic is two valued but the recognizer may not be able to figure it out it and so the recognizer return the answer 'I don't know' admitting its lack of sucess at determining membership. \\returned.

The notion of a recognizer is implicit in [skolem1928xxx] where he proposes that a formula universally quantified over natural numbers is TRUE for any object that can be determined to be a natural number. (not that it is TRUE for all natural numbers). So in arithmetic

∀a b.(a+b=b+a)

means 'if I am given two natural numbers a and b I get the same answer whether I add a to b or add b to a.' This interpretation of quantifers makes no ontological commitment to the existence of the infinite set of natural numbers. It simply means that if I'm given two of natural numbers I can add them in either order leaving mute how I know they are natural numbers, NEWFOL introduced recognizers because it couldn't put the 'set of natural numbers' into a computer memory but the effect is the same. In NEWFOL all quantifiers range over IBML types and all types have recognizers so this interpretation of quantifiers follows naturally.

Introduction

This work is about: what is in a mind? This is a question that has been asked from the times of the ancient Greeks. to review these discussions but to describe NEWFOL, a system that addresses this problem by describing how to make a program that has an understandinfg of real world objects, and through conversion can communicate with people about then and learn new things about the world through conversation. The first part of this document sets the stage for making a specific proposal about exactly how to build such a mind. The issues that have been written about in the 'far' past are important because, even though they are sometimes eclipsed by current technically significant results, the issues addressed still have teeth and are relevent to our goal. The people who have grappled with our subject were serious thinkers and we need to understand what they were thinking. This is additionally complicated by the fact that much of the work that predates the 20th century was not written in English but at first in Greek or Latin and later French, Italian or German. Unfortunately this leaves many of todays American scholars completely in the dark about these older ideas. We are lucky that there are still scholars who are willing and able to look at these works in their original languages and to both translate them and to write expository articles on their content.

Some major areas of interest are:

• Mental Language
  • Child Development
• Logic and Written Language
  • Medieval Logic
  • Nineteenth Century Logic
  • Logic from Frege to Godel
  • Contemporary Theories
• Computers and AI

What is Real

'Tell me one last thing,' said Harry. 'Is this real? Or has this been
happening inside my head?’ 

Dumbledore beamed at him, and his voice sounded loud and strong in Harry's
ears even though the bright mist was descending again, obscuring his figure. 

'Of course it is happening inside your head, Harry, but why on earth should
that mean that it is not real?'

J.K. Rowling
Harry Potter and the Deathly Hollows
Chapter 35 - King's Cross - the last three paragraphs

Or more scholarly

We are what we think
All that we are arises with our thoughts
With our thoughts we make the world
              The Dhammapada (words of the Buddha)

What is truth?
             John XVIII, 38 {Pontius Pilate to Jesus}


"What is truth?" (John VXIII, 18)
             Saul Kripke (Outline of a theory of truth)

Mental Language

Child Developmene

Logic and Written Language

Medieval Logic

Nineteenth Century Logic

Logic from Frege to Godel

Contemporary Theories

Computer Science and AI

Vocabulary

Format and Structure

The natural semantics of the concepts in this document are mutually recusrsive so a traditional hierarchical presentation seems forced. The choice of HTML as the media allows us to organize the descriptions in small semantically coherent chunks where a reader can move to related material with a simple click. This is not practical in a printed document where the related material might be dozens of pages away and the time spent navigating around the document unreasonable.

This arrangement allows a reader to choose where and when to access details about many topics whose inclusion in situ would be distracting to the flow of ideas. These links are given names and appear in the text deliniated by square brackets '[name]', which can be clicked on to move to the topic named.

Quotes, unless long, are usually found in the text itself but their bibliographic references are linked to the text and if the text is a translation we, if possible, link it with the text in the original language.

We also sometimes add pointers into specialized vocabularies and information about topics, works and people mentioned in the text. The pages pointed to by these links are provided by IBUKI who has made its data base available for this work. In addition, there are pointers to a web site that IBUKI maintains with pointer either to sources on the web or where they can be purchased (usually from Amazon when they are books in copyright or JSTOR if they are journal articles still subject to copyright.)

At the moment this site is produced by hand and serves as an example of a new kind of publication. Speculum Mundi Press (an imprint of IBUKI) has the technology for generating this site and associated eBooks.