for questions or link request: module admin

# Language and Rules of Predicate Calculus

name: rules, rule version: 1.00.00, author: Michael Meyling

## Description

This html file is part of the project "Hilbert II". See project homepage. Here we introduce the formal language and the deduction rules. This is done in an informal way. Important theorems (e.g.: universal decomposition, and any proofs) are left out.

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 X1, .., Xn be predicate variables. Then R + "(" + X1 + "," + .. + Xn + ")" 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
  A subject variable is free or bound if it is free or bound in p or q.
- 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)"

The following strings are not formulas:

- "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.

## add axiom

parameters:

label | reference name for an axiom

This rule adds the (by label) referenced axiom as a new proof line.

## add proposition

parameters:

label | reference name for a proposition

This rule adds an already proved proposition to the proof lines.

## modus ponens

parameters:

n | proof line number
m | proof line number

Let p be the formula in proof line number n and if the proof line m has the form "(" + p + "→" + q + ")" (q must be a formula), then q could be added to the proof lines.

## replace proposition variable

parameters:

A | proposition variable
p | formula
n | proof line number

Let q be the formula in proof line n. If q has the proposition variable A as a part formula and the free variables of p are different from the bound variables of q and the resulting string u of replacing all occurrences of A by p is a formula then u could be added as a new proof line.

## replace predicate variable

parameters:

A | atomic formula with predicate variable
p | formula
n | proof line number

Let q be the formula in proof line n. Let A be equal to R + "(" + X1 + ",".. + Xm + ")" with m different subject variables X1,.. ,Xm. These subject variables must occur free in p. All other free variables of p must not occur bound in q, and no bound variables of p occur in q. Now any occurrence of R + "(" + Y1 + ",".. + Ym + ")" with subject variables Y1,.. ,Ym in q is replaced by the formula that results from replacing X1,.. ,Xm by Y1,.. ,Ym in p. If this string u is a formula the proof lines could be extended with u.

## rename bound subject variable

parameters:

X | subject variable
Y | subject variable
n | proof line number
m | occurrence number

Let q be the formula in proof line n. Y must not be a free variable of q. By replacing X by Y in the m-th occurrence of a quantifier followed immediately by X and a part formula in parentheses we get a new string that could be added as a new proof line if it is a formula.

## rename free subject variable

parameters:

X | subject variable
Y | subject variable
n | proof line number

Let q be the formula in proof line n. If X is free in q replacing X by Y in q could be added as a new proof line.

## generalize a formula

parameters:

n | proof line number
m | occurrence number

If the n-th proof line is equal to "(" + p + "→" + q + ")" with formulas p, q and X is not free in p but free in q then "(" + p + "→(∀"" + X + "(" + q + "))" could be written as a new proof line.

## particularization

parameters:

X | subject variable
n | proof line number

If the n-th proof line is equal to "(" + p + "→" + q + ")" with formulas p, q and X is not free in q but free in p then "((∃" + X + "(" + p + ")→" + q + ")" could be written as a new proof line.

## use abbreviation

parameters:

label | reference name for an abbreviation
n | proof line number
m | occurrence number

Let q be the formula in proof line n. Then the m-th occurrence in q that matches the short form of the referenced abbreviation is replaced by its long form. If the resulting string is a formula it could be added as a new proof line.

## reverse abbreviation

parameters:

label | reference name for an abbreviation
n | proof line number
m | occurrence number

Let q be the formula in proof line n. Then the m-th occurrence in q that matches the long form of referenced abbreviation is replaced by its short form. If the resulting string is a formula it could be added as a new proof line.