Principia Mathematica II

Subject: QEDEQ Formula and Proof Methods Description
Date:    2003-11-24
***********************************************************************

Prototype Warning
=================
This program suite is only a working prototype for the main project
*Hilbert II*. It concentrates on the basic logic foundation of 
mathematics. The software design of the main implementation will be 
highly different. The following information is only appropriate for 
this prototype. Look at 
 http://www.qedeq.org/
 http://sourceforge.net/projects/pmii/
to get the latest source code and information.


Description
===========
This document describes the main elements of the QEDEQ language: a
formula and proof methods.


Basic Definitions and Operators of the Meta Language
====================================================
The following definitions should fix the notation.

ALPHABET := {'A', 'B', 'C', .., 'Z', 'a', 'b', ..., 'z',
  '0', '1', '2', ..,'9', '(', ')', '_', '.', '"'} 

WORDS := { (a_1, a_2, a_3, ..., a_n) in ALPHABET^n, with n a natural
    Number or 0}
+ : WORDS -> WORDS
 (a_1, ..., a_n), (b_1, ..., b_m) :-> (a_1, ..., a_n, b_1, ..., b_m)
the "empty word" (0-tupel) is a neutral element of this operation.

(ALPHABET, +) has the algebraic structure of an monoid
    (half group with neutral element e (the 0-tupel))
as usual, the operation + is extended to work on the
potence set of words (if A subset of WORDS, B subset of WORDS,
then A + B := { a + b | a in A, b in B})
For a shorter writing we write "a + B" iff we mean "{a} + B" (with
a element from WORDS and B a subset from WORDS). Analougous we
write "A + b" iff we mean "A + {b}" (with A a subset from WORDS and
b element from WORDS).
Also for a shorter writing "(", ",", ")" (from tuples) and "+" are 
never written. E.g.: "abc" stands for "(a) + (b) + (c)" and
"AB" for "A + B" (with a, b, c elements from ALPHABET and A, B
subsets or elements from WORDS).
We say A is a "subword" of B, iff there are elements U, V of WORDS
so that B = UAV.

operators on sets of WORDS:
"|" stands for an union (operator has minimal 2 arguments, 
    infix notation)
    A | B := {a element of A or element from B}
"*" stands for an repeated occurence, the number of these occurences 
    could be 0 (one argument, postfix notation)
    A* := {e, a, aa, aaa, aaaa, ... with a from A}
"[" "]" stand for an optional occurence (one argument, pre- and 
    postfix notation)
    [A] := {e} union A


Numbers, Strings, Formulas and free Variables
=============================================

NDIGIT := '1'|'2'|'3'|'4'|'5'|'6'|'7'|'8'|'9'

DIGIT := '0'| NDIGIT

NUMBER := NDIGIT DIGIT*

STRING := '"' (ALBHABET minus {'"'})* '"'

SUBJECT_VARIABLE := 'VAR(' NUMBER ')'

PREDICATE_VARIABLE := 
  'PREDVAR(' NUMBER ',(' SUBJECT_VARIABLE (',' SUBJECT_VARIABLE)* '))'

PROPOSITION_VARIABLE := 'PROP(' NUMBER ')'

ATOMIC_FORMULA := PREDICATE_VARIABLE | PROPOSITION_VARIABLE


We define a function "free" and a function "bound" that maps every 
element of ATOMIC_FORMULA to a subset of SUBJECT_VARIABLE:
free(ATOMIC_FORMULA) -> SUBJECT_VARIABLE
Let F be in ATOMIC_FORMULA:
free(F) := {S | S is subword of F and S is in 
  SUBJECT_VARIABLE}
bound(F) := {}

now we recursivly define the subset of WORDS "FORMULA" and extend 
the domains of "free" and "bound":

1. every element of ATOMIC_FORMULA is also in FORMULA
2. if F is in FORMULA, then
   'NOT(' F ')' is also in FORMULA and we define
   free('NOT(' F ')') := free(F)
   bound('NOT(' F ')') := bound(F)
3. if F and G are in FORMULA, free(F) and bound(G) have an empty 
   intersection, bound(F) and free(G) have an empty intersection, 
   then the following words are also in FORMULA:
   'AND(' F ',' G ')'
   'OR(' F ',' G ')'
   'IMPL(' F ',' G ')'
   'EQUI(' F ',' G ')'
   Let H be one of these new elements, then we define:
   free(H) := free(H) union free(G)
   bound(H) := bound(H) union bound(G)
4. if F is in FORMULA, and X is in SUBJECT_VARIABLE with X in 
   free(F), then the following words are also in FORMULA:
   'FORALL(' X ',' F ')'
   'EXISTS(' X ',' F ')'
  Let H be one of these new element, then we define:
  free(H) := free(F) minus {X}
  bound(H) := bound(F) union {X}


Proof Methods
=============

// TODO expand this paragraph

LINK := 'LINK(' STRING ')'

modus_ponens := 'MODUSPONENS(line1 ',' line2 ')'

Where line1 and line 2 are elements of NUMBER.  The referenced proof 
line line2 must be an implication which has as first argument 
a formula equal to the referenced proof line line1.

add_axiom := 'ADDAXIOM(' LINK ')'

Where "line" is an element of NUMBER, "definition" is an element of 
LINK and "occurrence" is an element of NUMBER we define:
use_abbreviation 
  := 'USEABBREVIATION(' line ',' definition ',' occurrence ')'
reverse_abbreviation 
  := 'REVERSEABBREVIATION(' line ',' definition ',' occurrence ')'

Where "line" is an, element of NUMBER, "var" is an element of 
PROPOSITION_VARIABLE and "replacement" is an element of FORMULA 
we define:
replace_proposition_variable
  := 'REPLACEPROP(' line ',' var ',' replacement ')'
    The set of free variables of the formula and
    the set of bound variables of the proof line formula
    must be disjunct. The set of bound variables
    of the formula and the free variables of the
    proof line must be disjunct too.
    If the proposition variable var is in reach of an
    quantor with subject variable x, this
    subject variable must not occur in the
    replacement formula.

'ADDSENTENCE(' add theorem

'REPLACEPREDICATE(' replace predicate variable
'RENAMEFREEVARIABLE(' rename free subject variable
'RENAMEBOUNDVARIABLE(' rename bound subject variable 
'GENERALIZATION(' generalization
'PARTICULARIZATION(' particularization