HOME


NEWFOL: the Logic
Building and Manipulating NEWFOL [context]s

Version 3.001 2020-04-22
Version 2.001 2015-08-23
Version 0.001 2013-08-12

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.

Table of contents


Preface

This document describes NEWFOL, a collection of ideas for formalizing knowledge about arbitrary subjects that is can be embedded in modern computer applications. The fact that it can be implemented in a computer, means that it can mention 'infinite' structures, but its own structures must representable in the memory of a computer, i.e., they must be finite.

NEWFOL is, in fact, the result of a careful analysis of the computational content of traditional classical logic. In addition, two pragmatic principles were important to its design: one, to be able to formalize any subject—mathematics is a somewhat exotic technical subject (what about cows?); and two, that its ability to reason should include arguments made in ordinary human situations/conversation.

Based on the ideas presented in this paper, IBUKI has built a computer system also called NEWFOL like its predecessors the first of which was called FOL built in 1974, updated to use IBML (the IBUKI Modeling Language) for data and SEUS (a programming language) implemented as a computation system. Although the original FOL was described as a 'proof checker' (or in modern usage a 'proof assistnt') it was, in fact, an interactive program where proofs were developed through conversation. Deductions were generated by suggesting to the system what rules to apply to already agreed upon facts or suggesting new assumptions or suggesting a possible conclusion that might be justifiable on the basis of what was already known and it could learn new methods by either talking to a 'user' or reading about them. This document does not discuss the language used in this conversation, but does mention some algorithms tht would be useful in a computer based 'thinking artifact' to manipulate the 'mental models' it needs for reasoning.

This document discusses the details of NEWFOL contexts. Each context contain a first order language, operations to recognize an extended notion of well-formed formula, [wff]s, the creation and use of simulation structures (the finite structures NEWFOL contexts use as a replacement for model) and a finite list of facts, that, in addition to containing a wff that is by definition 'true' in a context, includes the reason (its justification) that it is accetable/true in the context. The tools also include rules of inference (maps on [context]s) and other programs for handling more than one context at a time (including reflection principles).

NEWFOL speaks to three audiences:

For logicians and philosopher: NEWFOL is a new way of thinking about how to describe ideas and shows how to replace the infinitary notions implicit of set theory with finitary/computational ones using an information centric semantics. For logicians This bridges the notions of classical logic, Hilbert's ideas on finitism and Brouwer's notions of intuitionism by introducing a finitist understanding of full classical logic. This is not just the isolating of the finitist parts of classical semantics but presents an alterative explanation of full classical reasoning that is constructively acceptable.

For academic computer science and AI researchers: NEWFOL describes an architecture and framework for building autonomous computer thinkers. Currently, NEWFOL languages are close to formal first order languages, but there is nothing in its semantics that requires this. Natural languages, e.g., English, could be used to communicate with a NEWFOL system. These system will 'go' to the library and acquire its knowledge rather than rely on developers or statistics to learn things. NEWFOL addresses the core of the original goals of AI. We do not call NEWFOL a cognative architecture because it makes no claims to say anything about how biological brains work. What it does claim is that it can understandably facilitate the construction of practical physical systems whose functional capabilities exceed current AI systems functionality by a lot.

For computer systems application design: NEWFOL proposes a way of building computer systems that can organize and retrieve data (perhaps using current database and deep learning programs) but can also use its knowledge to think about the data and draw conclusions that were not anticipated by the system designers. Today, every organization that has digital content needs this kind of examination.

Introduction

A major thrust in western thought has been the idea that the world we live in is an understandable place and the goal of modern science is to understand what exactly is in our world and how it works. In western society this idea has been reinforced by the idea that God has a perfect and accutate understanding of the world (so such an undertanding exists) and that coming to know this external universal knowledge is benefitial.

I have come to believe that the idea of 'truth' outside of an individual may exist but that an inividul's knowledge lies completly inside its boundry and the relevant question is: what is in the mind of an individual that allows it to know something and how does an individual come to know about their their world, i.e., what is real. NEWFOL is my answer to these questions.

This document describes the syntax and semantics of NEWFOL. NEWFOL uses IBML types as objects, programs instead of sets in models and what we call 'information theoretic' semantics to determine the truth of sentences. The most important notion of NEWFOL is the reification of context using IBML [context]s. NEWFOL [context]s are finite data structures, defined as IBML types, that replace traditional theories and their model theories with structures that can be implemented on modern computers. Some of the differences are iscussed in appendix A.

NEWFOL ideas can be used in applications that want to incorporate models of the world and use 'theories' to reason about these models. The NEWFOL system, built by IBUKI, implements these structures for use on modern computers and allows you to build an artifact that can think.

Basic NEWFOL Notions

A corollary of my belief that all knowledge is local to an individual is that any object that knows something has some internal structure that 'holds' that knowledge. A further corollary is that if an individual occupies a finite space then its knowledge structures must be finite.

NEWFOL [context]s are a practical solution to the problem of what to use as knowldge structures when building something that can know.

NEWFOL operations on [context]s are a practical solution to the problem of what to use when building something that can think.

A Context

A Language

A NEWFOL language consists of two parts; its vocabulary and its grammer.

The vocabulary is a finite collection of words that can be used to form sentences of the context. The IBML type of the vocabulary of a [context] is a [lexicon].

There are two kinds of expressions names, which in logic are called terms, and sentences, which in logic are called formulas. The grammer of a language describes which expressions are well-formed expressions of the language. Names are modeled as [trm]s (as we us th type [term] for something else) and sentences as [wff]s or well-formed formulas following the practice of logicians.

A Derivation

A derivation (the following description of which is almost verbatim from [Prawitz11965] begins by inferring a consequence from some [assumption] or [axiom] by means of one of the rules listed below. We indicate this bywriting the formulas assumed on a horizontal line and the formula infered immediately below the line. Applying several rules thus can be thought of as a tree wiich we call a derivation.

As an example suppose we want to derive (IMPLIES A (AND B C)) from the assumption (AND (IMPLIES A B) (IMPLIES A C)). We proceed as follows: 

     (AND (IMPLIES A B) (IMPLIES A C))       (AND (IMPLIES A B) (IMPLIES A C))
     ---------------------------------       ---------------------------------
A          (IMPLIES A B)                A         (IMPLIES A C)
------------------------                -----------------------       
            B                                      C
            ----------------------------------------
                          (AND B C)

This derivation contains four assumptions: two of the form 

(AND (IMPLIES A B) (IMPLIES A C))

that occur on the first line. And two of the form 

A

That occur as the first and third formulas on the second line.

Each formula in the tree is said to be derived from the ones above. If we restrict our attention to a particular formula then it is said to be the end formula or conclusion of the subtree above it in the derivation. The set of formulas that are at the leafs of the subtree (i.e., the ones not under a horizontal line) are called the [assumption]s of that derivation. We say that the endf ormula depends on these [assuption]s. In the derivation above we say that (AND B C) is derived from the assumptions 

A and (AND (IMPLIES A B) (IMPLIES A c))

and in this derivation (AND B C) depends on the occurences of these [assumption]s.

The Language of a [context]

NEWFOL recognizes [folsym]s as those [symbol]s that are usable in the [language] of a [context]. The general noction of a NEWFOL [lexicon] is a list of [folsym]s, each with an associated syntyps and in the cas of [applsym]s an arity, a [natnum] tGiven a list of [folsym]s, NEWFOL [expression]s as follows:

The [language] of a NEWFOL [context] contains two parts: a [lexicon]; and a grammar for specifying well-formed [expression]s of the [language]. This grammar is shared by all [context]s.

All NEWFOL [context]s have the same logical constants

  • sentential constants [sentconst]s: FALSE TRUE
  • propositional connnectives [propconn]s:
    NOT AND OR IMPLIES WFFIF TRMIF IFF
  • quantifiers [quant]s: FORALL EXISTS

[context]s are distinguished by their non-logical symbols.

  1. Individual Symbols
    • individual constants [indconst]s
    • individual parameters [indpar]s
    • individual variables [indvar]s
  2. Function Symbols
    • function constants [funconst]s
    • function parameters [funpar]s
  3. Relation Symbols
    • relation constants [relconst]s
    • relation parameters [relpar]s
    • Predicate Symbols
      • predicate constanst [predconst]s
        • sort symbols [sortsym]s
      • predicate parameters [predpar]s

This differs from the usual definition of a first order language with the the intriduction of TRMIF, WFFIF and the introduction of [sort]s. Not all [expression]s are the terms, [trm]s and the sentences, by tradition called well-formed formulas, [wff]s of the language.

Symbols of the Language

Declare

Expressions of the Language

An expression of the language is an x

Expression Paths [EXP-PATH]

The Simulation Structure of a [contect]

The Facts of a [contect]

Constructor 

  (|fact-mak [fast-name] [wff] [justification] [assumptions])
     ==> [fact]                                                   [function]

Selectors 

  (|fact-get-name [fast]) ==> [fact-name]                        [function]
  (|fact-get-wff [fast]) ==> [wff]                        [function]
  (|fact-get-justification [fast]) ==> [justification            [function]
  (|fact-get-wff [assumtios) ==> [fact-name-list]                [function]

Rules of Inference as Opreations on [context]s

Facts va conclusions

Assumptions and Axioms

Propositional Logic

Conjunction: 
  (|and-i| [fast-list]) ==> [conclusion]                        [function]

  (|and-e [fact] ast-list]) ==> [conclusion]                   [function]

  (|or-i| [fast-list]) ==> [conclusion]                        [function]

  (|or-e [fact] ast-list]) ==> [conclusion]                   [function]

  (|not-i| [fast-list]) ==> [conclusion]                        [function]

  (|not-e [fact] ast-list]) ==> [conclusion]                   [function]

  (|implies-i| [fast-list]) ==> [conclusion]                        [function]

  (|implies-e [fact] ast-list]) ==> [conclusion]                   [function]

  (|iff-i| [fast-list]) ==> [conclusion]                        [function]

  (|iff-e [fact] ast-list]) ==> [conclusion]                   [function]

Appendix 1

  1. NEWFOL is a many-sorted version of first order logic. Many formulizations of many-sorted logic follow [WANG1940] where the models of such thories contained disjoint domains, one for each sort. Instead NEWFOL [context]s explicitly designate a subset of its monadic predicate symbols to be [sort]s. The meaning of these predicates relative to a model is given in the ordinary way and they naturally organized into a hierarchy by inclusion. That is, in the metatheory we define 
      (IFF-DEF
    (MOREGENERAL C S1 S2)
    (CONSEQUENCE C '(FORALL (OBJ) (IMPIES (S2 OBJ) (S1 OBJ)))) )

    The resulting partial order on [sort]s is thus accmplished without using set theory or its comprehension axioms.

    We also allow the variables in quantifier foe=rmulas to be restricted to particular [sort]s with the quantifier rules suitably modified. The correctness of the modifications requires the implicit axiom 

      (EXIST (obj) (SORT? obj))

    When appropriate we attach each [sort] to an IBML type and the notion of many-sorted logic is extended to use the partial order determined by the subtype relation on IBML types. This partial order on sorts was part of the original FOL where sorts were declared to be particular monadic predicate constance and the partial order was given by certain axioms (see ...).

  2. Conditional expressions are allowed when forming both [term]s and [wff]s. The notion of interpretation is extended to these expressions. Of course this introduces a mutual recursion between the value of a [term] in a model and the truth value of a [wff] but since we have andoned reductionist foundations this is fine.
  3. first order axiom schemas containing both predicate and function parameters are allowed.
  4. NEWFOL xontexts are finite structures. Like the 'creating subject', at any time a context only contains a finite number of 'theorems', which we call [fact]s. [fact]s are not simply [wff]s of the language of the context bur come with additional information. Most important is that each [fact] 'in' a [context] comes with a [justification]. Its [justification] gives the 'reason' why the wff] of the [fact] is 'acceptable' in the [context]. In ordinary natural deduction each end formula (i.e., the concluded [wff]) has associated with it a deduction tree with lsbeled assumptions (its [justification]). This makes it clear how a [wff] that appears in a deduction the justification tree as the end formula of a 'sub-derivation' that being the end formula of a derivation is not enough to characterixe the [wff] as a fact]. In AI people are now talking about assumption based reasoning but still don't appreciate the work of Prawitz on natural deduction.
  5. NEWFOL thinks of rules of inference not as generating deductions but as maps from [context]s to [contect]s. We formalize this in the non-elementary theory of [context]s and FOL only requires a rule of inference to be satisfaction preserving. FOL also seperates the act of making a conclusion from a [context] from the act of adding s conclusion to the [facts] of a [context]. Thus ideas that are generally left unformalized (like lagugage enlargement, subsidiary deduction rules, (if fact every conservative extensions suggest a new satisfaction preserving rule) ans even forgettlng are easily formulated as satisfaction preserving maps on [context]s and and like Brouwer's 'creating subject' FOL formalizes the idea we can learn new things. Unlike the 'creating subject' we can also change our mind and even forget things. In this way we model thinking in a way that has the finite approach of the 'creating subject' but at the same time accounts for changing ideas with the acquisition of new insights.
  6. NEWFOL provided some helpful rules like purely propositional deductions and some other decision procedures that are available in a single 'step'. From the conversational perspective you could ask FOL if some [wff] followed tautologically from what was previously discussed and FOL would attempt to varify whether thst was the case. The introduction of meta reasoning allowed the definition of new subsidiary deduction rules and reflection allowed the new rules to be used.

    This is a departure from the normal formulation of theory as being deductively closed.

  7. a 'partial' model, which we called a simulation structure in the original FOL, can be built using SEUS data and functions as the 'meanings' of an FOL language. FOL can use this 'model' to determine the 'meaning' of an FOL expressions. This form of deduction simply 'looks' in the 'model'.
  8. NEWFOL knows enough metamathematics to be able to understand and use subsidiary deductior rules allowing the introduction of as many metamathematical operators as you like.

Like the 'creating subject', FOL increases its knowledge over time and can have more and more knowedgable conversations as it discovers more facts about its mental models of things allowing it to reason about its knowledge.

The natural deduction rules used by NEWFOL are closely related to the system of first order predicate calculus described in Prawitz[1965].

The properties of this extension of ordinary logic together with with detailed examples appear in Weyhrauch[1979]. Prawitz distinguishes between individual variables and individual parameters. In NEWFOL individual variables may appear both free and bound in [wff]s. As in Prawitz individual parameters must always appear free.

Natural numbers are automatically declared individual constants of sort NATNUM. This is one of the few defaults in NEWFOL. The only kind of numbers understood by NEWFOL are are natural numbers, i.e. non-negative integers. -3 should be thought of not as an individual constant, but rather as the prefix operator - applied to the individual constant 3.

A user may specify that binary predicate and operation symbols are to be used as infixes. The declaration of a unary application symbol to be prefix makes the parentheses around its argument optional.

The number of arguments of an application term is called its arity.

NEWFOL always considers two [wff]s to be equal if they can both be changed into the same [wff] by making allowable changes of bound variables. Thus, for example, the TAUT rule will accept (forall x (P x)) imp (FORALL y (P y)) as a tautology if x and y are of the]\ same sort.

NEWFOL uses conditional expressions for both [wff]s and [trm]s. Conditional expressions are not used in standard descriptions of predicate calculus because they complicate the definition of satisfaction by making the value of a [trm] and the truth value of a [wff] mutually recursive. Hilbert and Bernays[l934] proved that these additions were a conservative extensions of ordinary predicate calculus so, in some sense, they are not needed. McCarthy[1963] stressed, however, that the increased naturalness when using conditional expressions to describe functions, is more than adequate compensation for the additional complexit

The [language] of a [context]

The [language] of a NEWFOL [context] consists of: a [lexicon] specifying the words of the [language] and their syntatic properties; and, a grammar that specifying the sentences of the [language] uniformally in the [lexicon]. This means that there is an algorithm that takes a [lexicon] and an expression as its arguments and determines whether or not the expression is a sentence of the [language]. All NEWFOL [context]s share this grammar and the combination of a [lexicon] and this algorithm can be repersented in a computer.

Quantification Rules

  • Mental Images/Models
  • Social Remark