# 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:

• axiom schema support (iteration, decision procedure)
• theorem step by step generation (using different algorithms)
• theorem derivation

## 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:

• `def_i` is an optional definition of wildcard, using a regular expression, for example:

• ".*" may be anything including the empty string
• "-+" is a string composed of "-"

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.

• `expr` is the axiom expression

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:

• `def_i` is the same as before
• `cond_i` is a required theorem, in order to produce new theorems (separated by and if several conditions)
• `th_i` is a produced theorems with the rule

## 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

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

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

=== 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----

=== 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-----

=== 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-----```