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.