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 t6he 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
This 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 claaed '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 completed 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 unuable 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 semanyics 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 address these issues they are
not mentioned in even math books that use them. e.g. statements about the
properties of subgrouops cannot even bae stated in the language of the
elementary theory of groups.
A program that can take a course in Aalgebra must be able to use these
principles even if they haven't proved them.
To be fair the use of set theory (even in the foundations of recursion
theory) was set long before there were actual digital computers.
The good news is that the analysis of logicians was amazingly good and
can be understood and used without using infinite set6s. 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 one." This observation suggests
that building a 'proof checker' before taclkling a 'theorem prover' is a good
idea.
Format and Structure
One of the properties of this book is that it is not linearly arranged as
is usual. What replaces the usual linear organization is a set of links to
notes that serve as reusable but self-contained texts that are linked at
the relevant places in the text. 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 notes are
given names and appear in the text deliniated by square brackets '[name]',
which includes a link to the topic called 'name'.
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, correlate it with the text in the original
language.
In addition we maintain pointers to specialized vocabularies and
information about both 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 Amazon when they are
books in copyright or JSTOR if then are in copyright journal articles)
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.
One of the unfortunate consequences of the sevelopnment of set thepry
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 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 cant decide
This is NOT a three valued logic!!! the object os either in the set or not.
i.e., the logic is two valued but the recognizer may not be able to figue out
it value so 'I don't know' is returned.
The notion of a recognizer is implicit in Skolem 1928 where he proposes
that the meaning of a universally quantified formula where the quantifier
ranges over S is TRUE for any object that can be determined to be an S (not
TRUE for all things that are in S). 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
wether I add a to b or whether I add b to a.' This interpretation of
quantifers makes no ontological commitment to the existence of the infinite
set of natural numbers. It simple means that if I'm given two of them the I
can add them in any order leaving mute hoe 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. This book is not a survey of such
ideas. The first part of this book 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
- Logic and Written Language
- Medieval Logic
- Nineteenth Century Logic
- Logic from Frege to Godel
- Contemporary Theories
- Computer Science 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
| 