HOME

A Summary of FOL Notions

Version 0.001 2020-04-15

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 a brief summary of the features and notions of FOL and how they differ from the usual formalization of first order logic.

A Little History

The design was driven by two considerations: actual computer hardware can only 'contain' finite data structures; and the activity of proving theorems, in practice, differed substantially from the accepted formalizations of logicians (for more details see FOL History).

The Ideas

Language

An FOL language replaced the usual definition of a first order language as an infinite set of symbols with: 1) a finite description of a many-sorted first order language with equality and function symbols; and, 2) recognizers (programs) for sentences (i.e., 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.

Simulation Structure

FOL replaced the logicians notion of model with that of simulation structure, a finite structure containing computer data as elements of the 'domain' and programs (as data) to represent 'functions' and 'relations'.

Language/Simulation Structure Pairs

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 replace the use of model theory and the logical notion of interpretation was implemented as computer program. The definitions of satisfaction and consistency follow in the usual way.

Context

An FOL context added a finite collection of facts to an L/S pair, replacing the logician's notion of theory with a finite structure. Context is the central notion of FOL and multiple independent contexts were definable at the same time and single context reasoning was adjusted to deal with multi-context systems, a phrase later coined by Fausto Guinchiglia.

Using FOL Contexts

Each context excapulated a self contained 'theory' of the things in it simulation structure.

Rules of Inference

In a critical departure from tradition, rules of inference were defined as satisfaction preserving (rather than validity preserving) maps on contexts. This implicitly assumes more than one context,

-------------------------------------------------------------------------------
Aside (logic)

Operationally this is reminiscent of Brower's creating subject but it
fails to obey Kreisel's axioms because it allows things like 'forgetting' and
'changing one's mind', both of which occur frequently in ordinary reasoning.
We believe Brower's idea of 'reasoning' as an ongoing mental activity is
exactly right but we are interested in making an actual 'reasoner' who we 
want to be able to make and correct their mistakes and can 'forget' things
that later prove uninteresting. If you think of the process of reasoning as
a sequence of steps, each of which might be call a 'rule of inference' then
FOL rules of inference allow for these behaviors whereas validity perserving
rules do not. we think this makes for a more realistic 'creating subject'
than Brower/Kreisel. 

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

Logicians implicitly recognize the importace of satisfaction preserving operations whenever they use a conservation extension result, each of which implicitly define a satisfaction preserving map on theories. The introduction of a new symbol into a language is done all the time both in logic papers and in computer implementation of logics. The question that's not asked is: since this operation is not validity preserving, what principle is being used when doing it? The FOL answer is that its accceptabe because adding a new symbol to the language of an FOL context is a proper FOL rule of inference.

As all validity preserving maps on sets of WFFs are also satisfaction preserving maps, FOL did deduction using the natural deduction rules of Prawitz implemented as FOL rules of inference.

Multiple Contexts

A simple need for multiple contexts is implicit in the definition of 'rule of inference'. We expect that the result of applying a rule to a context results in a different context. This woyld be the case if we were reasoning about a single subject. A slightly complex case is where we use this technique to reason about multiple subjects—baseball, cooking, ... .

The more interesting case is where contexts are related in some way. deductions using Prawitz;s natural deduction was extended to allow dependencies to occur among 'thoery' of something Each context excapulate1 a single 'thoery' of somethinge to This extension included the ability of a conclusion in on context to d

Meta-Theory

A reserved context, called META, was used to formalize the notion of contexts. The 'recognizers' for sentences mentioned above are in the simulation of META as well as a sort called 'CONTEXT'. Using an individual constant of sort 'CONTEXT', semantic attachment allowed FOL to 'name' a context data structure, making metatheory just a normal part of FOLs multi-context reasoning capability. By adding reflection principles (simple soundness statements relating any context to META), as a kind of multi-context reasoning and because our implementation environment allowed FOL to create 'rational' ('circular' but finite) structures, FOL was able to give examples of META using reflection principles to reason about itself, showing how to eliminate the 'infinite' tower of meta-theories implicit in the usual formalization of metatheory given by logicians.

Use cases

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, ... . Although essentially the same, we give five docs here because each has its own strengths and they 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.