FormalSystems

A Python implementation of Douglas Hofstadter formal systems

View the Project on GitHub alexprengere/FormalSystems

FormalSystems

This is a Python implementation of Douglas Hofstadter formal systems, from his book Gödel, Escher, Bach: An Eternal Golden Braid (commonly GEB).

In fact, you may define your own formal systems using a quite simple syntax, close to free text. Examples for MIU, pg, fg and NDP formal systems from the book are implemented in directory definitions.

A main Python script gives you possibilities to play with the formal system, including:

Formal system definition

Examples

The MIU system may be define with:

axioms:
    - MI

rules:
    - x is .*, xI => xIU
    - x is .*, Mx => Mxx
    - x is .*, y is .*, xIIIy => xUy
    - x y  .* , xUUy => xy

The underlying syntax is YAML (see raw format). You can define one or several axioms, or even an infinite number of axioms using a schema, as in the pg formal system:

axioms:
    - x is -+, xp-gx-

rules:
    - x y z are -+, xpygz => xpy-gz-

Syntax

Axiom definitions should be formatted like this ([] means this is optional):

[def_1, [def_2, ...]] expr

Where:

The definitions are written using char [is] regexp or char1 char2 [are] regexp if different wildcards have the same definition. Note that you should use only one character for wildcard definition.

Rules for theorem production should be formatted like this:

[def_1, [def_2, ...]] cond_1 [and cond_2 [and ...]] => th_1 [and th_2 [and ...]]

Where:

Installation

Install with:

$ python setup.py install --user

A script should be put in ~/.local/bin, make sure this path is in your $PATH:

$ export PATH=$PATH:~/.local/bin

Tests

If installation is successful, run the tests with:

$ cd tests
$ python test_formalsystems.py -v

Main script

After installation, you should have the main script FormalSystemsMain.py deployed somewhere where you $PATH points to, under the name FormalSystems. If it is not the case, you can always execute the script directly, assuming the dependencies are properly installed (just pyyaml and LEPL).

Usage of the main script is fully documented in --help argument.

You may generate theorems step by step if the number of axioms is finite:

$ FormalSystems definitions/MIU.yaml --iteration 3 
> Finite number of axioms, using step algorithm

STEP 1: MI

P  (1) x is .*, xI => xIU                    for  MI                         gives  MIU
P  (2) x is .*, Mx => Mxx                    for  MI                         gives  MII
.  (3) x is .*, y is .*, xIIIy => xUy        for  MI                       
.  (4) x y  .* , xUUy => xy                  for  MI                       

STEP 2: MIU/MII

P  (1) x is .*, xI => xIU                    for  MII                        gives  MIIU
.  (1) x is .*, xI => xIU                    for  MIU                      
P  (2) x is .*, Mx => Mxx                    for  MII                        gives  MIIII
P  (2) x is .*, Mx => Mxx                    for  MIU                        gives  MIUIU
.  (3) x is .*, y is .*, xIIIy => xUy        for  MII                      
.  (3) x is .*, y is .*, xIIIy => xUy        for  MIU                      
.  (4) x y  .* , xUUy => xy                  for  MII                      
.  (4) x y  .* , xUUy => xy                  for  MIU                      

STEP 3: MIIU/MIIII/MIUIU

Or using a bucket where axioms are thrown and theorems computed iteratively if the number of axioms is infinite:

$ FormalSystems definitions/pg.yaml --iteration 4
> Infinite number of axioms, using bucket algorithm

[Adding -p-g-- to bucket]

=== BUCKET 1: -p-g--

P  (1) x y z are -+, xpygz => xpy-gz-        for  -p-g--                     gives  -p--g---
[Adding --p-g--- to bucket]

=== BUCKET 2: -p--g---/--p-g---

P  (1) x y z are -+, xpygz => xpy-gz-        for  -p--g---                   gives  -p---g----
P  (1) x y z are -+, xpygz => xpy-gz-        for  --p-g---                   gives  --p--g----
[Adding ---p-g---- to bucket]

=== BUCKET 3: -p---g----/--p--g----/---p-g----

P  (1) x y z are -+, xpygz => xpy-gz-        for  -p---g----                 gives  -p----g-----
P  (1) x y z are -+, xpygz => xpy-gz-        for  ---p-g----                 gives  ---p--g-----
P  (1) x y z are -+, xpygz => xpy-gz-        for  --p--g----                 gives  --p---g-----
[Adding ----p-g----- to bucket]

=== BUCKET 4: -p----g-----/---p--g-----/--p---g-----/----p-g-----

Options are available to display theorem derivation as well:

$ FormalSystems definitions/NDP.yaml --quiet --derivation P-----
> Infinite number of axioms, using bucket algorithm
> Rule with several parents, using recursivity

=== BUCKET 1: --NDP-
=== BUCKET 2: --NDP---/-SD--/P--
=== BUCKET 3: --NDP-----/---SD--/---NDP--
=== BUCKET 4: --NDP-------/---NDP-----/-----SD--/P---/---NDP-
=== BUCKET 5: --NDP---------/---NDP--------/---NDP----/-------SD--/-----SD---/-SD---/----NDP---
=== BUCKET 6: ---NDP-----------/----NDP-------/---NDP-------/--NDP-----------/---------SD--/----NDP-
=== BUCKET 7: ----NDP-----------/----NDP-----/---NDP----------/---NDP--------------/--NDP-------------/-----------SD--/-------SD---/-SD----/----NDP--
=== BUCKET 8: ----NDP---------/----NDP---------------/---NDP-------------/---NDP-----------------/--NDP---------------/----NDP------/-------------SD--/-------SD----/-----SD----/-----------SD---/-----NDP-
=== BUCKET 9: --NDP-----------------/-----NDP------/----NDP-------------/---NDP--------------------/---NDP----------------/----NDP----------/----NDP-------------------/---------------SD--/-SD-----/-------------SD---/-----------SD----/P-----/-----NDP--

=== Theorem P----- found, derivation:
[1 ]  Axiom                                                                     gives  --NDP-              
[2 ]  (1) x y are -+, xNDPy => xNDPxy           for  --NDP-                     gives  --NDP---            
[3 ]  Axiom                                                                     gives  ---NDP--            
[3 ]  (1) x y are -+, xNDPy => xNDPxy           for  --NDP---                   gives  --NDP-----          
[4 ]  Axiom                                                                     gives  ----NDP-            
[4 ]  (1) x y are -+, xNDPy => xNDPxy           for  ---NDP--                   gives  ---NDP-----         
[4 ]  (2) z is -+, --NDPz => zSD--              for  --NDP-----                 gives  -----SD--           
[5 ]  (1) x y are -+, xNDPy => xNDPxy           for  ----NDP-                   gives  ----NDP-----        
[5 ]  (3) x z are -+, zSDx and x-NDPz => zSDx-  for  -----SD-- and ---NDP-----  gives  -----SD---          
[6 ]  (3) x z are -+, zSDx and x-NDPz => zSDx-  for  -----SD--- and ----NDP-----  gives  -----SD----         
[7 ]  (4) z is -+, z-SDz => Pz-                 for  -----SD----                gives  P-----