Rules for System I

Rules for System 1

11/15/06

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'..'l']
<variable> ::= any member of ['m'..'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); n, 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

We can state the rules of derivation in terms of the line that is to be added and the lines already in the derivation; these rules will normally make reference to assumptions of lines, the formulas that appear on the lines, and the justification that is to appear.

The rules will be expressed using notation like

n. <assumptions> <formula> <justification>

The first item is the line number, the second the assumptions of that line, the third the formula of the line, and the last the justification of the line

The Rule of Assumption Ass (sometimes called Trivial Inference TI)

A line of the form

<next line number> <existing assumptions + formula> <formula> 'Ass'

may be added to a derivation.

Implementation of Ass

A derivation starts with each of the standing assumptions written out as an opening line-- each justified by Ass. The standing assumptions run through the entire derivation and cannot be changed. Each use of Ass forces the adoption of a new assumption. If an earlier use of Ass has led to the adoption of a new assumption, over and above the standing assumptions, then Ass permits the dropping of the last assumption. This allows for the more complex forms of derivation needed for, as an example, ∨E.

The Rule of the Introduction of Negation ~I

(Version 1) If a derivation contains a line of the form

n. <assumptions1+ distinguished assumption> Absurd <any justification>

then a line of the form

<next line number> <assumptions1 + assumptions2 + optional further assumptions> ∼<distinguished assumption> 'n ~I'

may be added to the derivation.

With the implementation of Rules like this one, <assumptions1> and <assumptions2> will normally be the same, and there will be no <optional further assumptions>. So the Rule might have been written:-

If a derivation contains a line of the form

n. <assumptions1+ distinguished assumption> Absurd <any justification>

then a line of the form

<next line number> <assumptions1> ∼<distinguished assumption> 'n,k ~I'

may be added to the derivation.

Implementation of ∼I (Version 1)

A new assumption <assumption> needs to be added using Ass. A sub-proof is started aimed at obtaining the propositional constant Absurd. Then the selection of Absurd, and choosing ~I will cause the dropping of the last new assumption and addition of the negation of that assumption as the next line ∼<assumption>.

(Version 2) If a derivation contains a line of the form

n. <assumptions1+ distinguished assumption> <formula> <any justification>

and a line of the form

k. <assumptions1+ distinguished assumption> ∼<<formula> <any justification>

then a line of the form

<next line number> <assumptions1 + assumptions2 + optional further assumptions> ~<distinguished assumption> 'n,k ~I'

may be added to the derivation.

Implementation of ∼I (Version 2)

A new assumption <assumption> needs to be added using Ass. A sub-proof is started aimed at obtaining two separate formulas, with one of which being the negation of the other. Then the selection of two formulas, one being the negation of the other, and choosing ∼I will cause the dropping of the last new assumption and addition of the negation of that assumption as the next line ∼I<assumption>.

The Rule of the Elimination of Negation ∼E

If a derivation contains a line of the form

n. <assumptions> ∼∼<formula> <any justification>

a line of the form

<next line number> <assumptions + optional further assumptions> <formula> 'n ∼E'

may be added to the derivation.

Implementation of ∼E

∼E removes both negations from a selected double negation ∼∼<formula> to add <formula>.

The Rule of Introduction of Conjunction ∧I

If a derivation contains a line of the form

n. <assumptions1> <formula1> <any justification>

and a line of the form

k. <assumptions2> <formula2> <any justification>

then a line of the form

<next line number> <assumptions1 + assumptions2 + optional further assumptions> <formula1>∧<formula2> 'n,k ∧I'

may be added to the derivation.

Implementation of ∧I

Select two formulas <firstformula> and <secondformula> then ∧I adds <firstformula>∧<secondformula>. You will be asked to choose whether the first formula is to go on the left or on the right.

The Rule of Elimination of Conjunction ∧E

If a derivation contains a line of the form

n. <assumptions> <formula1>∧<formula2> <any justification>

then a line either of the form

<next line number> <assumptions> <formula1> 'n ∧E'

or of the form

<next line number> <assumptions> <formula2> 'n ∧E'

may be added to the derivation.

Implementation of ∧E

Select a formula <firstformula>∧<secondformula> then ∧E adds either <firstformula> or <secondformula>. You will be asked to choose whether you would like the <firstformula> or the <secondformula>.

The Rule of Introduction of Disjunction ∨I

If a derivation contains a line of the form

n. <assumptions> <formula> <any justification>

then a line of the form

<next line number> <assumptions> <formula>∨<new formula> 'n ∨I'

or a line of the form

<next line number> <assumptions> <new formula>∨<formula> 'n ∨I'

may be added to the derivation.

Implementation of ∨I

Select a formula <formula> then ∨I adds <formula>∨<new formula> or <new formula>∨<formula>. You will be asked to choose whether the selected formula is to go on the left or on the right.

The Rule of Elimination of Disjunction ∨E

If a derivation contains a line of the form

n. <assumptions> <left formula>∨<right formula> <any justification>

and a line of the form

k. <assumptions+left formula> <conclusion formula> <any justification>

and a line of the form

r. <assumptions+right formula> <conclusion formula> <any justification>

then a line of the form

<next line number> <assumptions> <conclusion formula> 'n,k,r ∨E'

may be added to the derivation.

Implementation of ∨E

This rule operates with a line with an 'Or' formula (<left formula>∨<right formula>) and two subproofs, one from the additional assumption of the <left formula> to the <conclusion> and the other from the additional assumption of the <right formula> to the <conclusion>.

Select an 'Or' formula (<left formula>∨<right formula>) and two subproofs (a subproof is selected by selecting its last line), one from the additional assumption of the <left formula> to the <conclusion> and the other from the <right formula> to the <conclusion>. Then ∨E adds <conclusion>.

The Rule of Introduction of the Conditional ⊃I

If a derivation contains a line of the form

n. <assumptions + if-assumption> <then-formula> <any justification>

then a line of the form

<next line number> <assumptions> (<if-assumption>⊃<then-formula>)'n ⊃I'

may be added to the derivation.

Implementation of ⊃I

A new assumption <if-assumption> needs to be added using Ass, and a sub-proof started. The sub-proof should run to the desired <then-formula>. Then the selection of the (last line of) the sub-proof, i.e. the <then-formula>, and choosing ⊃I will cause the sub-proof to be ended, the <if-assumption> to be dropped, and addition of (<if-assumption>⊃<then-formula>)' as the next line.

The Rule of Elimination of the Conditional ⊃E

If a derivation contains a line of the form

n. <assumptions1> (<if-formula⊃<then-formula>) <any justification>

and a line of the form

k. <assumptions2> <if-formula> <any justification>

then a line of the form

<next line number> <assumptions1 + assumptions2 > <then-formula> 'n,k ⊃E'

may be added to the derivation.

Implementation of ⊃E

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

The Rule of Introduction of the BiConditional ≡I

If a derivation contains a line of the form

n. <assumptions + left-formula> <right-formula> <any justification>

and a line of the form

k. <assumptions + right-formula> <left-formula> <any justification>

then a line of the form

<next line number> <assumptions> (<left-formula>≡<right-formula>)'n,k ≡I'

may be added to the derivation.

Implementation of ≡I

A new assumption <left-formula> needs to be added using Ass, and a sub-proof started. The sub-proof should run to the desired <right-formula>. Then a new assumption <right-formula> needs to be added using Ass, and a second sub-proof started. When this second sub-proof starts, the 'Drop last' button should be used on the Ass rule to drop the previous new assumption (ie <left-formula>). The second sub-proof should run to the desired <left-formula>.Then the selection of the (last line of) the two sub-proofs, i.e. the <right-formula> on the last line of the closed first sub-proof and the <left-formula> on the last line of the open second sub-proof, and choosing ≡I will cause the second sub-proof to be ended, and addition of (<left-formula>≡<right-formula>)' as the next line.

The Rule of Elimination of the BiConditional ≡E

If a derivation contains a line of the form

n. <assumptions> <left-formula>≡<right-formula> <any justification>

then a line either of the form

<next line number> <assumptions> <left-formula>⊃<right-formula> 'n ≡E'

or of the form

<next line number> <assumptions> <right-formula>⊃<left-formula> 'n ≡E'

may be added to the derivation.

Implementation of ≡I

Select a formula <firstformula> ≡<secondformula> then ≡E adds either <left-formula>⊃<right-formula> or <right-formula>⊃<left-formula>. You will be asked to choose which one you would like.

The Rule of Introduction of the Universal Quantifier, Universal Generalization UG

If a derivation contains a line of the form

n. <assumptions> <formula><any justification>

and

the variable <variable> is not free in any of the <assumptions> of line n

then a line of the form

<next line number> <assumptions> (∀<variable>)<formula> 'n UG'

may be added to the derivation.

Implementation of UG

Select a <formula> and press UG. You will be asked for the <variable> you wish to use. Then the Rule will check whether the <variable> is free in any of the assumptions of the selected <formula>. If it is not, then (∀<variable>)<formula> will be added.

The Rule of Elimination of the Universal Quantifier, Universal Instantiation UI

If a derivation contains a line of the form

n. <assumptions> (∀<variable>)<formula> <any justification>

and

the variable of quantification <variable> is free for the term <term> in the scope <formula>

then a line of the form

<next line number> <assumptions> <formula[<term>/<variable>]> 'n UI'

may be added to the derivation.

Implementation of UI

Select a formula with the form (∀<variable>)<formula> and press UI.  You will be asked for the <term> that you wish to have as the instantiation of <variable>. Then the Rule will check whether the proposed substitution of the <term> for the <variable> leads to the capturing of the <term> by another quantifier.  If it does not and the <variable> is free for the <term> in the <formula>, then <formula[<term>/<variable>]> is added.

The Rule of Introduction of the Existential Quantifier, Existential Generalization EG

If a derivation contains a line of the form

n. <assumptions> <formula><any justification>

and

the formula contains zero or more occurrences of the term <term> which are free for the variable <variable> ie substituting that variable for the term does not lead to capturing of the variable by a quantifier

then a line of the form

<next line number> <assumptions> (∃<variable>)(<formula>[<variable>/<term> zero or more occurrences where <term> is free for <variable>]) 'n EG'

may be added to the derivation.

Implementation of EG

Select any <formula> and press EG. You will be asked which <term> you wish to generalize on and which <variable> you wish to generalize with. The <formula> may contain zero occurrences of the <term> or it may contain some occurrences. For each occurrence you will be asked whether you wish to generalize on that occurrence. The resulting <scope> for the existential quantifier will be displayed to allow you to check or revise your choice. Then the Rule will check whether the proposed generalization of the <term> to the <variable> leads to the capturing of the <variable> by another quantifier.  If it does not and the <variable> is free for the <term> in the <scope> then (∃<variable>)<scope> is added.

The Rule of Elimination of the Existential Quantifier, Existential Instantiation EI

If a derivation contains a line of the form

n. <assumptions> (∃<variable>)(<scope>) <any justification>

and a line of the form

k. <assumptions+ <scope>> <formula> <any justification>

and

the variable <variable> is not free in any of the <assumptions> of line n and it is not free in the formula <formula>

then a line of the form

<next line number> <assumptions> <formula> 'k EI'

may be added to the derivation.

Implementation of EI

You have to have in mind here some existential formula (∃<variable>)<scope> that you are going to instantiate. First use Ass to adopt <scope> as a new assumption and derive the <formula> you want as the existential instantiation as the last line of an open sub-proof or sub-derivation. Then select the existential formula (∃<variable>)<scope> and the last line <formula> and press EI. The Rule will check whether <variable> is free in the assumptions of the existential formula, it will check whether <variable> is free in the assumptions of the intended instantiation <formula> (sadly, this is complicated, but the assumptions in question are the assumptions of the last line <formula> minus the assumption <scope>, which is the new assumption of the sub-proof), and it will check whether <variable> is free in <formula>.   The conditions satisfied, the Rule will drop the extra assumption of the sub-derivation and add <formula> as the new line.

The Rule of Repeat R

If a derivation contains a line of the form

n. <assumptions> <formula> <any justification>

a line of the form

<next line number> <assumptions + optional further assumptions> <formula> 'n R'

may be added to the derivation.

Note: Repeat is often used, but suppressed, in the implementation of other rules. For example, if the User is working on a sub-proof, based on <assumptions + optional further assumptions>, and uses ∧E on a formula which occurs earlier in the proof, based just on <assumptions>, then ∧E will add one of the conjuncts directly as the next line, based on <assumptions + optional further assumptions>.

Implementation of R

R repeats any selected line. The repeated line can have more assumptions than the original selection (but it cannot have less), so in effect the rule can add assumptions to the original line.

The Rule of Introduction of Absurdity AbsI

If a derivation contains a line of the form

n. <assumptions1> <formula> <any justification>

and a line of the form

k. <assumptions2> ~<formula> <any justification>

then a line of the form

<next line number> <assumptions1 + assumptions2 + optional further assumptions> Absurd 'n,k AbsI'

may be added to the derivation.

Implementation of AbsI

Two lines need to be selected (click on one, command click on the second). The formula on one of these selected lines must be the negation of the formula on the other selected line (ie one is ~<formula> and the other is <formula>). The rule will add the propositional constant Absurd.

The Rule of Theorem

A line of the form

<next line number> <assumptions> <formula> '<Your annotation>'

may be added to a derivation.

Implementation of Theorem

This 'rule' allows you to add any theorem you wish as a line of the proof. You will be asked what the theorem is, and how you would like the line annotated.

Rule Identity Introduction II

A line of the form

<next line number> <any assumptions> <term1>=<term2> 'II'

may be added to the derivation, where <term1> and <term2> are any two same or different terms.

This adds <term1>=<term2> for any term.

Rule Identity Elimination IE

This covers two cases.

If a derivation contains a line of the form

n. <assumptions1> <Predicate><term1><term2>..<termn> <any justification>

and a line of the form

k. <assumptions2> <term1>=<term2> <any justification>

then a line of the form

<next line number> <assumptions1 + assumptions2 <<Predicate><term1/term2><term2/term1>..<termn> 'n,k IE'

may be added to the derivation.

This notation is intended to mean:- 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).

The second case is that where the Predicate line is itself an identity statement> ie 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).

Implementation of IE

Select two formulas, one of which is an identity <term1>=<term2> and the other is an atomic formula (ie either a Predicate applied to some terms, or another identity statement) and where the second formula contains some occurrences of <term1> or <term2>. The rule will ask you about which occurrences you want to substitute for.