for questions or link request: module admin

All we will do is manipulate symbols. We build symbol strings and use certain simple rules to get new symbol strings. So by starting with a few basic strings we create a whole universe of derived symbol strings. It turns out that these strings could be interpreted as a view to the incredible world of mathematics.

See derived theorems of propositional calculus and derived theorems of predicate calculus

The following **symbols** are used: '∧', '∨', '→', '↔', '¬', '∃', '∀',
'x', 'y', 'z', 'u', 'v', 'w', 'r', 's', 't', 'a', 'b', 'c', 'd', 'P', 'Q', 'A', 'B', 'C', 'D', 'R', 'F', 'G', 'H', 'I', 'J', '0' , '1', '2', '3', '4', '5', '6', '7', '8', '9', '(' , ')', ',' .

Now we build **strings** made of these symbols. Strings are finite sequences of symbols. The length of a string is the length of the sequence. In this article whitespace of strings is ignored. Strings could be concatenated using the operator "+".

We call **number** all (nonempty) strings that are entirely made of '0', '1', '2', '3', '4', '5', '6', '7', '8', '9' but don't start with '0'.

We call **quantifier** the strings "∃" and "∀".

We call **proposition variables** all strings that look like "P", "Q", "A", "B", "C", "D" or "P" + *number*.

We call **subject variables** all strings of the form "x", "y", "z", "u", "v", "w", "r", "s", "t", "a", "b", "c", "d" or "x" + *number*.

We call **predicate variables** all strings that look like "R", "F", "G", "H", "I", "J" or "R" + *number*.

We call any of the following strings **atomic formulas**:

- proposition variables
- Let R be a predicate variable, n a natural number (>0) and let X
_{1}, .., X_{n}be predicate variables. Then R + "(" + X_{1}+ "," + .. + X_{n}+ ")" is an atomic formula and n is called the**argument number**of that predicate variable

Now we define recursively **formulas** and the relations **free** and **bound** for these
strings:

- Every atomic formula p is a formula. A subject variable is free in p, if it is needed to construct p; no subject variable is bound in p.
- Let p and q be formulas. If there is no subject variable free in p and bound in q, and no subject variable free in q and bound in p, then the following strings are
also formulas:
- "(" + p + "∧" + q + ")"
- "(" + p + "∨" + q + ")"
- "(" + p + "→" + q + ")"
- "(" + p + "↔" + q + ")"
- "¬" + p

- For every subject variable X that is free in p, and any quantifier A the string A + X + "(" + p + ")" is a formula. Except X every free subject variable from p stays free, X is now bound.

Let p be a string that is a formula and let q be a substring of p. q is called a **part formula** of p if it is a formula (and
the next symbol is not a digit).

For an easier writing we omit leading and closing parentheses of the outermost formula.

The following strings are examples of *formulas*. (Whitespace is ignored.)

- "P ∧ (Q ∧ P)"
- "P → (P ∨ Q)"
- "(¬P ∨P) → (P ∨ ¬P)"
- "R(y) → ∃x R(x)"

- "P ∧Q ∧ P"
- "R(x) → ∃x R(x)"

After the basic language definitions we could now take a look at the deduction rules. Deduction rules enable us to deduce new formulas from a basic set of formulas
called **axioms**. We also have a list of **abbreviations** for certain operators. To prove a **proposition** we use rules to get a sequence of formulas: the
**proof lines**. We use a deduction rule on our axioms, abbreviations, already proved sentences and proof lines to achieve a new proof line. The proof is finished if the last proof line
is identical to the proposition.

label |
reference name for an axiom |

label |
reference name for a proposition |

n |
proof line number |

m |
proof line number |

A |
proposition variable |

p |
formula |

n |
proof line number |

A |
atomic formula with predicate variable |

p |
formula |

n |
proof line number |

X |
subject variable |

Y |
subject variable |

n |
proof line number |

m |
occurrence number |

X |
subject variable |

Y |
subject variable |

n |
proof line number |

n |
proof line number |

m |
occurrence number |

X |
subject variable |

n |
proof line number |

label |
reference name for an abbreviation |

n |
proof line number |

m |
occurrence number |

label |
reference name for an abbreviation |

n |
proof line number |

m |
occurrence number |