Date: Feb 9, 2013 9:09 PM
Author: Graham Cooper
Subject: VENN DIAGRAM  of  FORMAL SYSTEM TYPES


|-------------STRINGS----------|
|
| abc^*z qed
|
|
| /--------WFF---------\
| /
| / PARADOXES X=~X
| / FALSE FORMULA ~X=X
| /
| |
| | /---THEOREMS-----\
| | /
| | | BT(S(0),0)
| | |
| | | ------------\
| | | / THEOREMS
| | | | STARTING
| | | | WITH NOT
| | | |
| | | | ~(BT(0,X)
| | | \------------/
| | |
| | \
| | \-----------------/
| \
| \
| \
| \--------------------/
|
|
|-----------------------------|


WFF C STRINGS
THEOREMCS C WFF
THEOREMS starting with NOT(....) C THEOREMS


----

A SET type can also be useful in programming
to instantiate "russell" into X in X~eX


----

Godel's Proof does not use this model.

Can anyone figure out why?


Herc
--
www.BLoCKPROLOG.com