HOME

FOL History

Version 0.001 2020-04-16

Author:

Richard Weyhrauch (IBUKI)

Note:

This is an original 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.

Abstract

This is my story of how various notions found their way into the original FOL systems. It is important to realize that these ideas were not the result of my thinking about how to represent proofs. I started by implementing a system that could be told a first order language and would accept 'axioms' and could make deductions if given the premises and told what rule to apply. The structure of the program was like the LCF program of Robin Milnor except that it understood first order expressions and used natural deduction as described by Prawitz.

The reason I wrote, and why you should read, this 'history' is that it illustrates how looking at 'real' proofs informed the feature set of FOL and it describes the changes in my perspective abhout what such a system should do.

Preface

For me, this work started because John McCarthy observed that it was not possible to write a computer program to find a proof for a theorem if it couldn't even 'be told'/represent the proof at all. This led to the idea of a 'proof checker' which would accept a 'proof' input by hand. The FOL program was, at first, a contribution this idea. The implementation of FOL was driven, in part, by my belief that first order notions are essential to reasoning and therefore any attempt to build a program to understand proofs must, at a minimum, incorporate first order ideas.

When I first worked at the Stanford Artificial Intelligence Lab (1972) I worked with Robin Milner on the LCF project. LCF stood for the 'Logic of Computable Functions', as described by Dana Scott. The idea of the project was to write a program that could be used to develop and record proof about 'computable functions' in the service of proving useful properties of computer programs (e.g., 'correctness' - did a program meet its spec?). The importance of this work to the future FOL project is that it produced an architectural framework for any 'proof checker', the logic of computable functions in the LCF project case. I realized that the structure of the LCF program could be used to build a 'proof checker' for first order logic.

This was not the first attempt to build such a tool at the AI Lab. Whit Diffie, of encription fame, had developed (as envisioned by John McCarthy) PCHECK, a first order 'proof checker' based on the Hilbert style of prooof representation. On the other hand, for FOL I chose the natural deduction system of Prawitz. This better matched the LCF paradigm. It was called 'natural' deduction because it seemed to better follow the patterns of ordinary human reasoning.

The FOL project was greatly faciliated by the SAIL keyboard, desktop displays, printers and software environment that had all the logical symbols available in the early 1970s, before digital typography. That's the good news. The bad news, for me, was that readers of the early FOL papers didn't realize that they contained actual FOL computer output and thought that the examples were fabricated. This misunderstanding made it into the published version of the 'Prolegamena' paper in the AI journal which re-typeset the computer output using traditional mathematical typography, further confusing the issue. Naive me didn't realize this until many years later.

Onward

I first implemented a straightforward system that allowed the definition of a first order language and to use the Prawitz natural deduction rules to make proofs from assumptions. When this system was functional, as a test, I set myself two tasks: 1) use FOL to prove all the theorems in the 'Principia Mathematica' of Whitehead and Russell; and 2) since mathematics was, according to logicians, was among the most 'formalized' subjects, to see if FOL was able to create proofs and produce output that was acceptable to hand in to teachers as homework typically assigned in undergraduate mathematics courses.

The first task was mechanical and I didn't actually finish it, but the second one is really the reason for my writing this 'history'. It immediately showed the hugh gap between the formalisms I had learned as a PhD student in mathematics/logic and the world of actual universe of real problem solving activity. Of course, it was always possible to restate ordinary reasoning as deductions/proofs in the familiar formalisms, but the reformulations were unsatisfactory to me because they weren't what people actually did or even what professional mathematicians/logicians wrote down in academic journals.

Math Homework

This note describes how the features of the original FOL system grew out of my goal to build a system that could read and print proofs as might be encountered in the homework assignments in a math course and then use the output to hand in the assignment and get it graded. The goal was first to simply have a person type in the assignment questions and their answers (a homework assistent). It did not have to solve the homework problem (theorem proving was to come later), it simply had to accept the problem and be told the answer.

First Order Logic revisited

Computers can only hold a finite amount of data. This fundemental (although obvious) observation turned out to be one of the main reasons that implementation of the FOL system needed to rethink how the logicians use of the infinite structures afforded by set theory couls be reformulated to be useful in a computer environment.

An FOL language. Here was the first challenge. In most formulations of logical formalisms logicians imagined they had a 'infinite' collection of symbols available for use in building languages. FOL replaced the usual definition of a first order language with a finite description of a many-sorted first order language plus recognizers for sentences (ie WFFs). The introduction of a partial order on sorts (now called order sorted logic) had the effect of removing a dependency on set theory to reason about the hierarchical nature of things and made proofs more natural. At the time, it was realized that reasoning about sorts could be carried out in a fragment of monadic predicate calculus and was thus decidable. I don't think this was written down anywhere. FOL replaced the logicians notion of model with simulation structures, a finite structure containing computer data as elements of the 'domain' and programs (as data) to represent 'functions' and 'relations'.

The connection between a language and a simulation structure was called semantic attachment and FOL introduced the notion of a Language/Simulation air (L/S pair). These finite structures replaced model theory. Since all these notions had representations as finite data structures, the logical notion of interpretation was implemented as computer program. This allows the definition of satisfaction to be made in the usual way.

By adding a finite collection of 'facts' to an L/S pair, FOL implemented a finite realization of the notion of theory (which FOL called a context). In a critical departure from tradition, rules of inference were defined as satisfaction preserving (rather than validity preserving) maps on contexts. This is reminiscent of Brower's creating subject it fails to obey Kreisel's axioms because it allows 'forgetting and 'changing one's mind', both of which are properties of ordinary reasoning. The recognization of the importance of this idea is use of conservation extension results each of which implicitly define a satisfaction preserving map on theories. All validity preserving maps on sets of WFFs are also satisfaction preserving map on contexts. FOL implemented Prawitz's natural deduction rules in this way.

Since the language of one context can 'name' something of sort context, FOL used semantic attachment to interpret such a 'name' as a data structure for a context making multi-context hierarchical reasoning and metatheory available 'for free'. By adding 'reflection' principles (simple soundness statements about multi-context systems) and because our implementation language allowed us to create 'rational' ('circular' but finite) structures, FOL was able to gave examples of how to eliminate the 'infinite' tower of meta-theories by allowing a context to name and therefore reason about 'itself'.

We (and many many others) published the use of FOL contexts to show how, using first order ideas (without the introduction of 'new' logics), can do modal reasoning, reasoning about time without indexicals, metatheory, default reasoning, non-monotonic logic, circumscription, jumping to conclusions, ... . There are five Original FOL Documents, each with its own strengths and which show the evolution of ideas. There are many dozens of published docs describing FOLs many uses. Note that the examples appearing in the first four reports are actual computer output. The AI lab printers had all the ususl logical symbols on them long before digital typography.