Language and Rules of Predicate Calculus

Description

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₁, .., X_n be predicate variables. Then R + "(" + X₁ + "," + .. + 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
  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)"

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

add proposition

modus ponens

replace proposition variable

replace predicate variable

rename bound subject variable

rename free subject variable

generalize a formula

particularization

use abbreviation

reverse abbreviation