www.qedeq.org

 Hilbert II

English   Deutsch
Hilbert II bei SourceForge
Einführung
News
Mathematik
QEDEQ
Planung
Download
Glossar
Entwicklung
Prototyp
Installation
Anleitung
Aussagenlogik
Prädikatenlogik
QEDEQ
Modul
Formel
QEDEQ Text
Fehler
Links
Kontakt
Sitemap
Prototyp / PMII QEDEQ-Modul / Formel

Here is an first attempt to formalize a formula in the QEDEQ language:

ALPHABET := {'A', 'B', 'C', .., '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-tuple) is a neutral element of this operation.
(ALPHABET, +) has the algebraic structure of an monoid
    (half group with neutral element e (the 0-tuple))
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). Analogous 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 "sub word" 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 occurrence, the number of these occurrences
    could be 0 (one argument, postfix notation)
    A* := {e, a, aa, aaa, aaaa, ... with a from A}
"[" "]" stand for an optional occurrence (one argument, pre- and
    postfix notation)
    [A] := {e} union A

NDIGIT := '1'|'2'|'3'|'4'|'5'|'6'|'7'|'8'|'9'
DIGIT := '0'| NDIGIT
NUMBER := NDIGIT DIGIT*
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
ATOMIC_FORMULA to a subset of SUBJECT_VARIABLE:

free(ATOMIC_FORMULA) -> SUBJECT_VARIABLE

Let F be in PRIME_FORMULA:
free(F) := {S | S is sub word of F and S is in
  SUBJECT_VARIABLE}
bound(F) := {}

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

1. every ATOMIC_FORMULA is a 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(X), then the following words are also in FORMULA:
   'FORALL(' x ',' f ')'
   'EXISTS(' x ',' f ')'
  Let h be one of these new formula, then we define:
  free(h) := free(f) minus {x}
  bound(h) := bound(f) union {x}


update 1970-01-01 01:00:00+0100