Primitive Rules and Examples
July 23, 2023
Version 1.1.2
Created for the SLUโs 2023 Summer Logic Reading Group, this webpage is a supplement to Tim Eshingโs inference rule handout. I have also posted a quick reference here. It is a work in progress and will be updated periodically. Please submit corrections and suggestions via the Logic Reading Group Discord forum.
Click on a heading to expand the content. Click the heading again to fold the content. When you hover your cursor over a proof the line under the cursor will highlight. Click once to keep the line highlighted. Clicking on a highlighted line will clear all highlights. Use this feature to check annotations numbers.
This webpage provides instructions for using the Lemmon System. The instructions are written in English, but also employ several metavariable types. The following key may be helpful.
| Metavariable type | Represented by |
|---|---|
| Formula | lowercase italic Greek letters: ๐, ๐, ๐, and ๐ |
| Line number | lowercase italic letters: ๐, ๐, ๐, ๐, ๐, and ๐ |
| Assumption set | capital double stroke Roman letters: ๐ธ and ๐น |
| Assumption set member | lowercase italic letters: ๐, ๐, ๐, and ๐ |
I also make use of some set theoretical notation.
A set is an unordered collection of set member. The members of a set are represented by names. The set members of a Lemmon proof assumption set are typically named with arabic numbers. A Lemmon assumption set is written by listing names of it set members. The names are separated by commas and enclosed in curly brackets. For example:
Order and repetition are irrelevant.
I will use the lowercase italic letters ๐โ๐ as metavariables for assumption set members and the capital double stroke Roman letters ๐ธ and ๐น as metavariables for sets. This will allow me to state the Lemmon rules without referring to specific sets or set members. The Lemmon proof rules require two set operations: union and difference.
The union of two sets is represented by placing the sets in parenthesis and separating them with the symbol โโชโ.
({๐, ๐} โช {๐, ๐})
(๐ธ โช ๐น)The outer most parenthesis may be dropped for readability.
{๐, ๐} โช {๐, ๐}
๐ธ โช ๐นThe union of a set ๐ธ and a set ๐น includes every member of set ๐ธ and every member of set ๐น.
{1} โช {2} = {1, 2}
{1, 3} โช {2, 3, 4} = {1, 2, 3, 4}
{1, 2, 3} โช {3, 4} = {1, 2, 3, 4}The union operation is used by most Lemmon inference rules.
Next we have the difference operation. We represent the difference of two sets by placing them in parenthesis and separating them with the symbol โโชโ.
({๐, ๐} โ {๐, ๐})
(๐ธ โ ๐น)Again, the outer most parenthesis may be dropped for readability.
{๐, ๐} โ {๐, ๐}
๐ธ โ ๐นThe difference of a set ๐ธ and a set ๐น includes every member of ๐ธ that is not a member of ๐น.
{1, 2} โ {2} = {1}
{1, 3} โ {2, 3} = {1}
{1, 2, 3} โ {1, 2, 3, 4, 5} = {}In the last example the resulting set has no members. In place of {}, we can use the empty set symbol โโ โ.
The Lemmon proof system uses the difference operation to discharge assumptions. The Lemmon rules for conditional introduction, negation introduction, and indirect proof all use the difference operation.
Accurate set notation requires that we enclose set members in brackets; however, this convention is typically relaxed when writing the assumption set on a Lemon proof line.
Once you work through the rule definitions and examples below, consult Tim Eshingโs inference rule handout or my Lemmon System quick reference.
Add any formula ๐ to a new line ๐ and add a new assumption name ๐ to its assumption set (๐ should be the only element in the set). Annotate the line with โA.โ
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| {๐} | ๐. | ๐ | A |
Use this rule to add the premises of a sequent to your proof.
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| โค1 | 1. | PโโจโQ | A |
| โค2 | 2. | PโโโQ | A |
| โค3 | 3. | QโโโR | A |
| โฎ | โฎ | โฎ | โฎ |
You can also use this rule to introduce an assumption for โI or ยฌI. Note this in the annotation.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | PโโจโQ | A |
| 2 | 2. | PโโโQ | A |
| 3 | 3. | QโโโR | A |
| โค4 | 4. | ยฌR | A for ยฌI |
| โฎ | โฎ | โฎ | โฎ |
Reiterate any formula ๐ from a previous line ๐. The new line ๐ will use the same assumption set as line ๐. Annotate the line with โReitโ and cite line ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐ | A |
| ๐ธ | ๐. | ๐ | Reit ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | P | A for โI |
| โค1 | 2. | P | Reit 1 |
| โฎ | โฎ | โฎ | โฎ |
Given any formula ๐ on a line ๐ resting on assumption set ๐ธ and any formula ๐ on a line ๐ resting on assumption set ๐น, add ๐โ&โ๐ to a new line ๐. Line ๐ will rest on ๐ธ โช ๐น. Annotate the line with โ&Iโ and cite lines ๐ and ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐ | |
| ๐น | ๐. | ๐ | |
| ๐ธ โช ๐น | ๐. | ๐โ&โ๐ | &I ๐, ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1 | (Pโ&โQ)โโโR | A |
| 2 | 2 | P | A for โI |
| 3 | 3 | Q | A for โI |
| โค2, 3 | 4 | Pโ&โQ | &I 2, 3 |
| โฎ | โฎ | โฎ | โฎ |
Given a formula ๐โ&โ๐ on a line ๐, add either ๐ or ๐, to a new line ๐. Line ๐ will use the same assumption set as line ๐. Annotate the line with โ&Eโ and cite line ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐โ&โ๐ | |
| ๐ธ | ๐. | ๐ | &E ๐ |
Alternatively:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐โ&โ๐ | |
| ๐ธ | ๐. | ๐ | &E ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | Pโ&โQ | A |
| โค1 | 2. | P | &E 1 |
| โค1 | 3. | Q | &E 1 |
| โฎ | โฎ | โฎ | โฎ |
Given a formula ๐ on a line ๐, add ether ๐โโจโ๐ or ๐โโจโ๐ to a new line ๐. Line ๐ will use the same assumption set as line ๐. Annotate the line with โโจIโ and cite line ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐ | |
| ๐ธ | ๐. | ๐โโจโ๐ | โจI ๐ |
Alternatively:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐ | |
| ๐ธ | ๐. | ๐โโจโ๐ | โจI ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | ยฌ(PโโจโQ) | A |
| 2 | 2. | P | A for ยฌI |
| โค2 | 3. | PโโจโQ | โจI 2 |
| โฎ | โฎ | โฎ | โฎ |
Given a formula ๐โโจโ๐ on a line ๐ resting on assumption set ๐ธ and the denial of ๐ on a line ๐ resting on assumption set ๐น, add ๐ to a new line ๐. Alternatively, given a formula ๐โโจโ๐ on a line ๐ resting on assumption set ๐น and the denial of ๐ on a line ๐ resting on assumption set ๐น, add ๐ to a new line ๐. Line ๐ will rest on the assumption set ๐ธ โช ๐น. Annotate line ๐ with โโจEโ and cite lines ๐ and ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐โโจโ๐ | |
| ๐น | ๐. | ยฌ๐ | |
| ๐ธ โช ๐น | ๐. | ๐ | โจE ๐, ๐ |
Alternatively,
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐โโจโ๐ | |
| ๐น | ๐. | ยฌ๐ | |
| ๐ธ โช ๐น | ๐. | ๐ | โจE ๐, ๐ |
Since a negated formula ยฌ๐ has two denial, ๐ and ยฌยฌ๐, the rule also permits
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ยฌ๐โโจโ๐ | |
| ๐น | ๐. | ๐ | |
| ๐ธ โช ๐น | ๐. | ๐ | โจE ๐, ๐ |
and
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐โโจโยฌ๐ | |
| ๐น | ๐. | ๐ | |
| ๐ธ โช ๐น | ๐. | ๐ | โจE ๐, ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | (PโโจโQ)โโจโR | A |
| 2 | 2. | ยฌ(Pโโจโ(QโโจโR)) | A for ยฌI |
| โฎ | โฎ | โฎ | โฎ |
| 2 | 7. | ยฌR | &E 5 |
| 2 | 8. | ยฌP | &E 3 |
| โค1, 2 | 9. | PโโจโQ | โจE 1, 7 |
| โค1, 2 | 10. | Q | โจE 8, 9 |
| โฎ | โฎ | โฎ | โฎ |
Another example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | Pโ&โQ | A |
| 1 | 2. | P | &E 1 |
| 1 | 3. | Q | &E 1 |
| 4* | 4. | ยฌPโโจโยฌQ | A |
| โค1, 4 | 5. | ยฌQ | โจE 2, 4 |
| โฎ | โฎ | โฎ | โฎ |
*Note that the assumption name โ4โ was introduced on line 4. The new name could have been any name but โ1,โ since โ1โ has already been used. Some logicians prefer sequential names, which keeps track of the total number of assumptions in the proof. Tim and I prefer that name match the line number on which the assumption was introduced. This makes the assumption easier to located when it is time to discharge the assumption. Another option is to name assumptoins with lowercase letters. Assumption names are not line numbers, so the lowercase letters emphasize the distinction.
Given a formula ๐ that was introduced as assumption ๐ on line ๐ and a formula ๐ on line ๐ resting on the assumption set ๐ธ, add ๐โโโ๐ to a new line ๐. Line ๐ will rest on the assumption set ๐ธ โ {๐}. (This will โdischargeโ assumption ๐.) Annotate the line with โโIโ followed by the assumption name ๐ in parenthesis and cite line ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| {๐} | ๐. | ๐ | A for โI |
| ๐ธ | ๐. | ๐ | |
| ๐ธ โ {๐} | ๐. | ๐โโโ๐ | โI(๐) ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1 | (Pโ&โQ)โโโR | A |
| 2 | 2 | P | A for โI |
| 3 | 3 | Q | A for โI |
| 2, 3 | 4 | Pโ&โQ | &I 2, 3 |
| 1, 2, 3 | 5 | R | โE 1, 4 |
| โค1, 2 | 6 | QโโโR | โI(3) 3, 5 |
| โค1 | 7 | Pโโโ(QโโโR) | โI(2) 2, 6 |
If you discharge all the assumptions for a formula, place the empty set symbol โโ โ in the assumption set column for the new line. If a formula rest on the assumption set โ it is a theorem.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | P | A for โI |
| 1 | 2. | P | Reit 1 |
| โ | 3. | PโโโP | โI(1) 2 |
Given a formula ๐ on a line ๐ resting on assumption set ๐ธ and formula ๐โโโ๐ on a line ๐ resting on assumption set ๐น, add ๐ to a new line ๐. Line ๐ will rest on the assumption set ๐ธ โช ๐น. Annotate line ๐ with โโEโ and cite lines ๐ and ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐ | A |
| ๐น | ๐. | ๐โโโ๐ | A |
| ๐ธ โช ๐น | ๐. | ๐ | โE ๐, ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | PโโโQ | A |
| 2 | 2. | P | A |
| โค1, 2 | 3. | Q | โE 1, 2 |
Given a formula ๐โโโ๐ on a line ๐ resting on assumption set ๐ธ and a formula ๐โโโ๐ on a line ๐ resting on assumption set ๐น, add ๐โโ๏ธโ๐ to a new line ๐. Line ๐ will rest on ๐ธ โช ๐น. Annotate line ๐ with โโ๏ธIโ and cite lines ๐ and ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐โโโ๐ | A |
| ๐น | ๐. | ๐โโโ๐ | A |
| ๐ธ โช ๐น | ๐. | ๐โโ๏ธโ๐ | โ๏ธI ๐, ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | PโโโQ | A |
| 2 | 2. | QโโโP | A |
| 3 | 3. | Pโโ๏ธโQ | โ๏ธI 1, 2 |
Given a formula ๐โ๏ธ๐ on a line ๐, add ๐โโโ๐ or ๐โโโ๐ to a new line ๐. Line ๐ will rest on the same assumption set as ๐. Annotate line ๐ with โโ๏ธEโ and cite line ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐โโ๏ธโ๐ | |
| ๐ธ | ๐. | ๐โโโ๐ | โ๏ธE ๐ |
Alternatively:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ๐โโ๏ธโ๐ | |
| ๐ธ | ๐. | ๐โโโ๐ | โ๏ธE ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | Pโโ๏ธโQ | A |
| 1 | 2. | PโโโQ | โ๏ธE 1 |
Given
add ยฌ๐ to a new line ๐. Line ๐ will rest on all the assumptions from lines ๐ and ๐, except ๐ (i.e., (๐ธ โช ๐น) โ {๐}). (Again, this is called discharging an assumption.) Annotate the line with โโIโ followed by the assumption name ๐ in parenthesis and cite lines ๐ and ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| {๐} | ๐. | ๐ | A for ยฌI |
| ๐ธ | ๐. | ๐ | |
| ๐น | ๐. | ยฌ๐ | |
| (๐ธ โช ๐น) โ {๐} | ๐. | ยฌ๐ | ยฌI(๐) ๐, ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | PโโโQ | A |
| 2 | 2. | ยฌQ | A |
| 3 | 3. | P | A for ยฌI |
| 1, 3 | 4. | Q | โE 1, 3 |
| โค1, 2 | 5. | ยฌP | ยฌI(3) 2, 4 |
Another example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | PโโจโP | A |
| 2 | 2. | ยฌP | A for ยฌI |
| 1, 2 | 3. | P | โจE 1, 2 |
| โค1 | 4. | ยฌยฌP | ยฌI(2) 2, 3 |
| โฎ | โฎ | โฎ | โฎ |
Given a formula ยฌยฌ๐ on a line ๐ resting on assumption set ๐ธ, add ๐ to a line ๐. Line ๐ will rest assumption set ๐ธ. Annotate line ๐ with โยฌEโ and cite line ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| ๐ธ | ๐. | ยฌยฌ๐ | |
| ๐ธ | ๐. | ๐ | ยฌE ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | PโโจโP | A |
| 2 | 2. | ยฌP | A for ยฌI |
| 1, 2 | 3. | P | โจE 1, 2 |
| 1 | 4. | ยฌยฌP | ยฌI(2) 2, 3 |
| โค1 | 5. | P | ยฌE 4 |
Given
add ๐โs denial to a new line ๐. Line ๐ will rest on all the assumptions from lines ๐ and ๐, except ๐ (i.e., (๐ธ โช ๐น) โ {๐}). Annotate the line with โRAAโ or โIPโ followed by the assumption name ๐ in parenthesis and cite lines ๐ and ๐.
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| {๐} | ๐. | ๐ | A for RAA |
| ๐ธ | ๐. | ๐ | |
| ๐น | ๐. | ยฌ๐ | |
| (๐ธ โช ๐น) โ {๐} | ๐. | ยฌ๐ | RAA(๐) ๐, ๐ |
Alternatively:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| {๐} | ๐. | ยฌ๐ | A for RAA |
| ๐ธ | ๐. | ๐ | |
| ๐น | ๐. | ยฌ๐ | |
| (๐ธ โช ๐น) โ {๐} | ๐. | ๐ | RAA(๐) ๐, ๐ |
For example:
| Assumption Set | Line # | Formula | Annotation |
|---|---|---|---|
| 1 | 1. | PโโจโP | A |
| 2 | 2. | ยฌP | A for RAA |
| 1, 2 | 3. | P | โจE 1, 2 |
| โค1 | 4. | P | RAA(2) 2, 3 |
Since many of us learned logic using the Fitch Proof system, this section compares Lemmon and Fitch style proofs. Lemmon proofs use the primitive rules above. Fitch proofs use the rules from chapter 16 of forall๐ฅ: Calgary (Fall 2021+).
| 1 | 1. | ยฌPโโจโQ | A |
| 2 | 2. | P | A for โI |
| 1, 2 | 3. | Q | โจE 1, 2 |
| 1 | 4. | PโโโQ | โI(2) 2, 3 |
| 1ยฌPโโจโQ | |
| 2P | |
| 3Q | โจE 1, 2 |
| 4PโโโQ | โI 2โ3 |
| 1 | 1. | PโโจโQ | A |
| 2 | 2. | ยฌ(QโโจโP) | A for RAA |
| 3 | 3. | P | A for ยฌI |
| 3 | 4. | QโโจโP | โจI 3 |
| 2 | 5. | ยฌP | ยฌI(3) 2, 4 |
| 1, 2 | 6. | Q | โจE 1, 5 |
| 1, 2 | 7. | QโโจโP | โจI 6 |
| 1 | 8. | QโโจโP | RAA(2) 2, 7 |
| 1PโโจโQ | |
| 2P | |
| 3QโโจโP | โจI 2 |
| 4Q | |
| 5QโโจโP | โจI 4 |
| 6QโโจโP | โจE 1, 2โ3, 4โ5 |
| 1 | 1. | PโโจโP | A |
| 2 | 2. | ยฌP | A for RAA |
| 1, 2 | 3. | P | โจE 1, 2 |
| 1 | 4. | P | RAA(2) 2, 3 |
| 1PโโจโP | |
| 2P | |
| 3P | Reit 2 |
| 4PโโจโP | โจE 1, 2โ3, 2โ3 |
| 1 | 1. | ยฌ(Pโ&โQ) | A |
| 2 | 2. | P | A for ยฌI |
| 3 | 3. | Q | A for ยฌI |
| 2, 3 | 4. | Pโ&โQ | &I 2, 3 |
| 1, 3 | 5. | ยฌQ | ยฌE(2) 1, 4 |
| 1 | 6. | ยฌP | ยฌE(3) 3, 5 |
| 1 | 7. | ยฌPโโจโยฌQ | โจI 6 |
| 1ยฌ(Pโ&โQ) | |
| 2P | |
| 3Q | |
| 4Pโ&โQ | &I 2, 3 |
| 5โฅ | ยฌE 1, 4 |
| 6ยฌQ | ยฌI 3โ6 |
| 7โฅ | ยฌE 3, 6 |
| 8ยฌP | IP 2โ7 |
| 9ยฌPโโจโยฌQ | โจI 8 |
| 1 | 1. | ยฌ(ยฌPโ&โยฌQ) | A |
| 2 | 2. | ยฌ(PโโจโQ) | A for RAA |
| 3 | 3. | P | A for ยฌI |
| 3 | 4. | PโโจโQ | โจI 3 |
| 2 | 5. | ยฌP | ยฌI(3) 2, 4 |
| 6 | 6. | Q | A for RAA |
| 6 | 7. | PโโจโQ | โจI 6 |
| 2 | 8. | ยฌQ | ยฌI(6) 2, 7 |
| 2 | 10. | ยฌPโ&โยฌQ | &I 5, 8 |
| 1 | 12. | PโโจโQ | RAA(2) 1, 10 |
| 1ยฌ(ยฌPโ&โยฌQ) | |
| 2ยฌ(PโโจโQ) | |
| 3P | |
| 4PโโจโQ | โจI 3 |
| 5โฅ | ยฌE 2, 4 |
| 6ยฌP | ยฌI 3โ5 |
| 7Q | |
| 8PโโจโQ | โจI 7 |
| 9โฅ | ยฌE 2, 8 |
| 10ยฌQ | ยฌI 7โ9 |
| 11ยฌPโ&โยฌQ | &I 6, 10 |
| 12โฅ | ยฌE 1, 11 |
| 13PโโจโQ | IP 2โ12 |
| 1 | 1. | PโโจโQ | A |
| 2 | 2. | PโโโR | A |
| 3 | 3. | QโโโS | A |
| 4 | 4. | ยฌ(RโโจโS) | A for RAA |
| 5 | 5. | P | A for ยฌI |
| 2, 5 | 6. | R | โE 2, 5 |
| 2, 5 | 7. | RโโจโS | โจI 6 |
| 2, 4 | 8. | ยฌP | ยฌI(5) 4, 7 |
| 1, 2, 4 | 9. | Q | โจE 1, 8 |
| 1, 2, 3, 4 | 10. | S | โE 3, 9 |
| 1, 2, 3, 4 | 11. | RโโจโS | โจI 10 |
| 1, 2, 3 | 12. | RโโจโS | RAA(4) 4, 11 |
| 1PโโจโQ | |
| 2PโโโR | |
| 3QโโโS | |
| 4P | |
| 5R | โE 2, 4 |
| 6RโโจโS | โจI 5 |
| 7Q | |
| 8S | โE 3, 7 |
| 9RโโจโS | โจI 8 |
| 10RโโจโS | โจE 1, 4โ6, 7โ8 |
| 1 | 1. | Pโโ๏ธโQ | A |
| 1 | 2. | PโโโQ | โ๏ธE 1 |
| 1 | 3. | QโโโP | โ๏ธE 1 |
| 1 | 4. | Qโโ๏ธโP | โ๏ธI 2, 3 |
| 1Pโโ๏ธโQ | |
| 2P | |
| 3Q | โ๏ธE 1 |
| 4Q | |
| 5P | โ๏ธE 1 |
| 6Qโโ๏ธโP | โ๏ธI 2โ3, 4โ5 |
| 1 | 1. | (PโโจโQ)โ&โ(PโโจโR) | A |
| 1 | 2. | PโโจโQ | &E 1 |
| 1 | 3. | PโโจโR | &E 1 |
| 4 | 4. | ยฌ(Pโโจโ(Qโ&โR)) | A for RAA |
| 5 | 5. | P | A for ยฌI |
| 5 | 6. | Pโโจโ(Qโ&โR) | โจI 5 |
| 4 | 7. | ยฌP | ยฌI(5) 4, 6 |
| 1, 4 | 8. | Q | โจE 2, 7 |
| 1, 4 | 9. | R | โจE 3, 7 |
| 1, 4 | 10. | Qโ&โR | &I 8, 9 |
| 1, 4 | 11. | Pโโจโ(Qโ&โR) | โจI 10 |
| 1 | 12. | Pโโจโ(Qโ&โR) | RAA(4) 4, 11 |
| 1(PโโจโQ)โ&โ(PโโจโR) | |
| 2PโโจโQ | &E 1 |
| 3PโโจโR | &E 1 |
| 4ยฌ(Pโโจโ(Qโ&โR)) | |
| 5P | |
| 6Pโโจโ(Qโ&โR) | โจI 5 |
| 7โฅ | ยฌE 4, 6 |
| 8Q | X 7 |
| 9R | X 7 |
| 10Q | |
| 11Q | Reit 10 |
| 12Q | โจE 2, 5โ8, 10โ11 |
| 13R | |
| 14R | Reit 13 |
| 15R | โจE 3, 5โ9, 13โ14 |
| 16Qโ&โR | &I 12, 15 |
| 17Pโโจโ(Qโ&โR) | โจI 16 |
| 18โฅ | ยฌE 4, 17 |
| 19Pโโจโ(Qโ&โR) | IP 4โ18 |