Rules for the 'Default' System
9/25/19
Propositions
<proposition> ::= any member of ['A'..'Z']
So, for example:- A, M, and Z are all propositions.
Well formed formulas
There is the notion of a well-formed formula or <wff> .
<wff> ::=
<proposition>
| (<wff>)
| ∼<wff>
| <wff1> & <wff2>
| <wff1> ∨ <wff2>
| <wff1> → <wff2>
| <wff1> ≡ <wff2>
For example, P, P&Q, A→(B→C) are all well-formed formulas.
Brackets are used to clarify or disambiguate expressions (much as they are in mathematics).
The Rules
The Rules are presented as Introduction and Elimination (Intelim) Rules— each of the logical connectives has a rule for introducing it and a rule for eliminating it (and there are some other rules to fill out the infrastructure).
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 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.