for questions or link request: module admin

Language and rule definition of predicate calculus

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

Description

This html file is part of the project "Principia Mathematica 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 manipulating 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.
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'.
With quantifier we denote the strings "$" and """ .
We call proposition variables all strings that look like "P", "Q", "A", "B", "C", "D" or "P" + number.
All strings of the form "x", "y", "z", "u", "v", "w", "r", "s", "t", "a", "b", "c", "d" or "x" + number are called subject variables.
With predicate variable we denote strings that look like "R", "F", "G", "H", "I", "J" or "R" + number.

We call any of the following strings atomic formula:

proposition variables

let R be a predicate variable, n a natural number (>0) and let X₁, .., X_n be a 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, iff it is 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 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 q if it is a formula (and the next symbol is no digit).

The following strings are examples for formulas. (White space is ignored.)

"(P Ù (Q Ù P))"

"(P Þ (P Ú Q))"

"((ØP Ú P) Þ (P Ú ØP))"

"(P(y) Þ $ x (P(x)))"

The following strings are no formulas:

"(P Ù Q Ù P)"

"(P(x) Þ $ x (P(x)))"

After the basic language definitions we could now take a look at the deduction rules. Deduction rules enable us to deduct 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 achive 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 sentence

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 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 occurences 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 + "(" + X₁ + ",".. + X_m + ")" with m different subject variables X₁,.. ,X_m. These subject variables must occur free in p. All other free variables of p must not occur bound in q, and all bound variables of p don't don't even occur in q. Now any occurence of R + "(" + Y₁ + ",".. + Y_m + ")" with subject variables Y₁,.. ,Y_m is replaced by the resulting formula of replacing X₁,.. ,X_m by Y₁,.. ,Y_m. 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	occurence 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 occurence of a qantifier followed by X and a part formula in brackets 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 leads to a new proof line.

generalize a formula

parameters:

n	proof line number
m	occurence 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	occurence number

Let q be the formula in proof line n. Then the m-th occurence 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	occurence number

Let q be the formula in proof line n. Then the m-th occurence in q that matches the long form of referenced abbreviation is replaced by its short form. If the resulting string is a formula it is allowed to extend the proof lines with it.