## Rules for System II

1/14/07 *under construction*

## Terms, constants, variables, propositions, and predicates

<term letter> ::= any member of ['a'..'z']

<atomic term> ::= <term letter>

<term> ::= <term letter> | <term letter> ( <term>... <term> )(*the list of terms within the brackets must have at least one member*)

<constant> ::= any member of ['a'..'t']

<variable> ::= any member of ['u'..'z']

<predicate letter> ::= any member of ['A'..'Z']

<proposition> ::= <predicate letter>

<predicate> ::= <predicate letter> <term 1>... <term n>

So, for example:- f, x, and z are all terms; b, j, and f are all constants (and terms); u, w, and z are variables (and terms); H is a proposition; Rxy, and Gfx are predicates. And f(, K(fg) and Jf)g are none of these.

In any of its non-elementary configurations, Deriver permits functional terms, in which case f(a), g(bc), f(g(d)) are all terms and Rf(x)g(y) is a predicate.

## Well formed formulas

There is the notion of a well-formed formula or <wff> .

<wff> ::=

<proposition>

| <predicate>

| <term1> = <term2>

| (<wff>)

| ∼<wff>

| <wff1> . <wff2>

| <wff1> ∨<wff2>

| <wff1> ⊃ <wff2>

| <wff1> ≡<wff2>

| (<variable>) <wff>

| (∃<variable>) <wff>

For example, P, Pa, Qbv, (x)Hxy are all well-formed formulas and so too are a=b and (∃x)(x=d).

Brackets are used to clarify or disambiguate expressions (much as they are in mathematics).

## Scope, Bound, Free, Free for

If <scope> is any well-formed formula then (∃<variable>)<scope> is the existential quantification of <scope> using <variable> and (<variable>)<scope> is the universal quantification of <scope> using <variable>. In each case the <scope> is the scope of the quantification.

A quantifier binds all occurrences of its <variable> in its scope. An occurrence of a variable which is not bound is called free. So, in (∀x)(Fx)⊃Gx the occurrence of x immediately after F is bound whereas the occurrence of x immediately after G is free; but in the formula (∀x)(Fx⊃Gx) both occurrences are bound.

Substitutions are on occasions made of one term for free occurrences of another. The notation <wff>[<newterm>/<oldterm>] means the formula <wff> with <newterm> substituted for the free occurrences of <oldterm> throughout. The notation <wff>[<newterm>/<oldterm> any occurrences ] means the formula <wff> with <newterm> substituted for zero of more of the free occurrences of <oldterm>.

A hazard with substitutions is capturing. This, for example, is where you wish to substitute an x for a free y but the free y is within the scope of a quantifier using the variable x; so were the substitution to be made the formerly free y becomes a bound x. (For example if you put x for y in (∀x)(Fxy) you get (∀x)(Fxx) and there is capture). This is to be avoided.

Hence...

Any term occurs within itself.

A variable x is free for substitution by term t in formula F iff there is no free occurrence of x in F within the scope of a quantifier whose variable of quantification occurs in t (alternatively t is free for substitution for x in F). The terminology here is awkard. A better variant is to say that a substitution is legitimate (iff it avoids capture).

## The Rules

[Most configurations of Deriver do not make all these rules available at once.]

### The Rule Modus Ponens (MP)

Two lines need to be selected: one with the form (<if-formula⊃<then-formula>), and the other with the form <if-formula>. Then choosing MP will add the <then-formula> as the next line.

### The Rule Modus Tollens (MT)

Two lines need to be selected: one with the form (<if-formula⊃<then-formula>), and the other with the form ~<then-formula>. Then choosing MP will add ~<if-formula> as the next line.

### The Rule of Hypothetical Syllogism (HS)

This requires the selection of two lines: the formula of one must be (<if-clause>⊃<then-clause>) and the other must be the (<then-clause>⊃<then-clause2>) of the first. The Rule will then add the <if-clause>⊃<then-clause2>.

### The Rule of Disjunction Syllogism (DS)

This requires the selection of two lines: the formula of one must be <left>∨<right> and the other must be the ~<left> of the first. The Rule will then add the <right>.

### The Rule of Constructive Dilemma (CD)

This requires the selection of two lines: the formula of one must be (<if-clause>⊃<then-clause>).(<if-clause2>⊃<then-clause2>) and the other must be the <if-clause>∨<if-clause2> of the first. The Rule will then add the <then-clause1>∨<then-clause2>.

### The Rule of Destructive Dilemma (DD)

This requires the selection of two lines: the formula of one must be (<if-clause>⊃<then-clause>).(<if-clause2>⊃<then-clause2>) and the other must be the ~<then-clause1>∨~<then-clause2> of the first. The Rule will then add the ~<if-clause>∨~<if-clause2>.

### The Rule of Simplification (Simp)

Select a line <leftformula>.<rightformula> then Simplification adds its left conjunct <leftformula>.

### The Rule of Conjunction (Conj)

Select two lines <firstformula> and <secondformula> then Conjunction adds <firstformula>.<secondformula>. You will be asked to choose whether the new formula is to go on the left or on the right.

### The Rule of Addition (Add)

Select a <formula> then Addtion will ask you to input a <newformula> and then add <formula>∨<newformula>.

### The Rule of Assumption (Ass)

Assumption will ask you to input a <newformula> and then will start a sub-proof adding <newformula> as the opening line.

### The Rule of Conditional Proof (CP)

Select a <formula> which is the last line of a open sub-proof starting from <newformula> then Conditional Proof closes the sub-proof and adds <newformula> ⊃ <formula> as the next line.

### The Rule of Universal Instantiation (UI)

Select a (<variable>)<scope> , where <scope> contains at least one free occurrence of <variable> then Universal Instantiation will ask you for the <term> that you want as an instance and will add <scope>[<term>/<variable>] provided the <variable> is free for the <term> in the <scope>.

### The Rule of Universal Generalization (UG)

Select a formula <scope>[<variable2>/<variable>] then Universal Generalization will add (<variable>)<scope>, provided <scope>[<variable2>/<variable>] contains no free variable introduced by Existential Instantiaition, and <variable2> does not occur free in any assumption within whose range <wff>[<variable2>/<variable>] lies.

### The Rule of Existential Instantiation (EI)

Select a formula (∃<variable>)<scope> then EI will choose a <variable2>, which is not free in an earlier line, and add <scope>[<variable2>/<variable>].

### The Rule of Existential Generalization (EG)

Select a <scope>[<term>/<variable>] where <scope> contains at least one free occurrence of <variable> then EG will ask you for the <term>, for the <variable>, and for your choice of occurrences of <term> that you wish to generalize on. It will add add (∃<variable>)<scope> provided the <variable> is free for the <term> in the <scope>.

### The Rule of Identity 1 (Id1)

This covers two cases. Given any n-place predicate, say <Predicate><term1><term2>..<termn>, and an identity statement <term1>=<term2>, this permits the replacement of any occurrence of <term1> in <Predicate><term1><term2>..<termn> by <term2> and any occurrence of <term2> in <Predicate><term1><term2>..<termn> by <term1> (you will be asked which occurrences you wish to replace). Or given an identity statement, say <term3>=<term4>, and an identity statement <term1>=<term2>, this permits the replacement of any occurrence of <term1> in <term3>=<term4> by <term2> and any occurrence of <term2> in <term3>=<term4> by <term1> (you will be asked which occurrences you wish to replace).

### The Rule of Identity 2 (Id2)

Select a <wff1> and <wff2> then Id2 will ask you for the two terms <nu-term> and <mu-term> that you are interested in, and if ~<wff1> is <wff2>[nu-term/mu-term] it will add ~(<nu-term> = <mu-term>).

### Rule of Theorem (T)

If you know of some <formula> which you are willing to guarantee is a theorem, the Rule Theorem will add it.

### Rewrite Rules

These Rules permit the replacement or rewriting of either an entire formula or a subformula of a formula. There are many such Rules, what they do is explained in the Rewrite Rules documentation.