Lemmon Proof System

Chris Holland

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.

Preface

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:

{1, 2, 3}.

Order and repetition are irrelevant.

{1, 2, 3} = {2, 1, 3} = {1, 2, 2, 1, 3}

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.

Primitive Rules

Once you work through the rule definitions and examples below, consult Tim Eshing’s inference rule handout or my Lemmon System quick reference.

Assumption (A)

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 (A)
Assumption Set	Line #	Formula	Annotation
{𝑎}	𝑛.	𝜙	A

Use this rule to add the premises of a sequent to your proof.

For example:

(P ∨ Q), (P → R), (Q → R) ⊢ R
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
⋮	⋮	⋮	⋮

Reiteration (R)

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 𝑚.

Reiteration
Assumption Set	Line #	Formula	Annotation
𝔸	𝑚.	𝜙	A
𝔸	𝑛.	𝜙	Reit 𝑚

For example:

⊢ P → P
Assumption Set	Line #	Formula	Annotation
1	1.	P	A for →I
➤1	2.	P	Reit 1
⋮	⋮	⋮	⋮

Conjunction Introduction (&I) / Conjunction (Conj)

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 𝑚.

Conjunction Introduction (&I)
Assumption Set	Line #	Formula	Annotation
𝔸	𝑙.	𝜙
𝔹	𝑚.	𝜓
𝔸 ∪ 𝔹	𝑛.	𝜙 & 𝜓	&I 𝑙, 𝑚

For example:

((P & Q) → R) ⊢ (P → (Q → R))
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
⋮	⋮	⋮	⋮

Conjunction Elimination (&E)

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 𝑚.

Conjunction Elimination (&E)
Assumption Set	Line #	Formula	Annotation
𝔸	𝑚.	𝜙 & 𝜓
𝔸	𝑛.	𝜙	&E 𝑚

Alternatively:

Assumption Set	Line #	Formula	Annotation
𝔸	𝑚.	𝜙 & 𝜓
𝔸	𝑛.	𝜓	&E 𝑚

For example:

(P & Q) ⊢ (Q & P)
Assumption Set	Line #	Formula	Annotation
1	1.	P & Q	A
➤1	2.	P	&E 1
➤1	3.	Q	&E 1
⋮	⋮	⋮	⋮

Disjunction Introduction (∨I) / Addition (Add)

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 𝑚.

Disjunction Introduction (∨I)
Assumption Set	Line #	Formula	Annotation
𝔸	𝑚.	𝜙
𝔸	𝑛.	𝜙 ∨ 𝜓	∨I 𝑚

Alternatively:

Assumption Set	Line #	Formula	Annotation
𝔸	𝑚.	𝜙
𝔸	𝑛.	𝜙 ∨ 𝜓	∨I 𝑚

For example:

¬(P ∨ Q) ⊢ (¬P & ¬Q)
Assumption Set	Line #	Formula	Annotation
1	1.	¬(P ∨ Q)	A
2	2.	P	A for ¬I
➤2	3.	P ∨ Q	∨I 2
⋮	⋮	⋮	⋮

Disjunction Elimination (∨E) / Disjunctive Syllogism (DS)

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 𝑚.

Disjunction Elimination (∨E)
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:

((P ∨ Q) ∨ R) ⊢ (P ∨ (Q ∨ R))
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:

(P & Q) ⊢ ¬(¬P ∨ ¬Q)
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.

Conditional Introduction (→I) / Conditional Proof (CP)

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 𝑚.

Conditional Introduction (→I)
Assumption Set	Line #	Formula	Annotation
{𝑎}	𝑙.	𝜙	A for →I
𝔸	𝑚.	𝜓
𝔸 − {𝑎}	𝑛.	𝜙 → 𝜓	→I^(𝑙) 𝑚

For example:

((P & Q) → R) ⊢ (P → (Q → R))
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, 5
➤1	7	P → (Q → R)	→I⁽²⁾ 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.

∅ ⊢ P → P
Assumption Set	Line #	Formula	Annotation
1	1.	P	A for →I
1	2.	P	Reit 1
∅	3.	P → P	→I⁽¹⁾ 2

Conditional Elimination (→E) / Modus ponens (MP)

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 𝑚.

Conditional Elimination (→E)
Assumption Set	Line #	Formula	Annotation
𝔸	𝑙.	𝜙	A
𝔹	𝑚.	𝜙 → 𝜓	A
𝔸 ∪ 𝔹	𝑛.	𝜓	→E 𝑙, 𝑚

For example:

P → Q, P ⊢ Q
Assumption Set	Line #	Formula	Annotation
1	1.	P → Q	A
2	2.	P	A
➤1, 2	3.	Q	→E 1, 2

Biconditional Introduction (↔︎I)

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 𝑚.

Biconditional Introduction (↔︎I)
Assumption Set	Line #	Formula	Annotation
𝔸	𝑙.	𝜙 → 𝜓	A
𝔹	𝑚.	𝜓 → 𝜙	A
𝔸 ∪ 𝔹	𝑛.	𝜙 ↔︎ 𝜓	↔︎I 𝑙, 𝑚

For example:

P → Q, Q → P ⊢ P ↔︎ Q
Assumption Set	Line #	Formula	Annotation
1	1.	P → Q	A
2	2.	Q → P	A
3	3.	P ↔︎ Q	↔︎I 1, 2

Biconditional Elimination (↔︎E)

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 𝑚.

Biconditional Elimination (↔︎E)
Assumption Set	Line #	Formula	Annotation
𝔸	𝑚.	𝜙 ↔︎ 𝜓
𝔸	𝑛.	𝜙 → 𝜓	↔︎E 𝑚

Alternatively:

Assumption Set	Line #	Formula	Annotation
𝔸	𝑚.	𝜙 ↔︎ 𝜓
𝔸	𝑛.	𝜓 → 𝜙	↔︎E 𝑚

For example:

P ↔︎ Q ⊢ P → Q
Assumption Set	Line #	Formula	Annotation
1	1.	P ↔︎ Q	A
1	2.	P → Q	↔︎E 1

Negation Introduction (¬I)

Given

a formula 𝜙 that was introduced as assumption 𝑎 on line 𝑘
a formula 𝜓 on line 𝑙 resting on assumption set 𝔸
the formula ¬𝜓 on line 𝑚 resting on assumption set 𝔹,

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 𝑘.

Negation Introduction (¬I)
Assumption Set	Line #	Formula	Annotation
{𝑎}	𝑘.	𝜙	A for ¬I
𝔸	𝑙.	𝜓
𝔹	𝑚.	¬𝜓
(𝔸 ∪ 𝔹) − {𝑎}	𝑛.	¬𝜙	¬I^(𝑎) 𝑙, 𝑚

For example:

(P → Q), ¬Q ⊢ ¬P
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⁽³⁾ 2, 4

Another example:

(P ∨ P) ⊢ P
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, 3
⋮	⋮	⋮	⋮

Negation Elimination (¬E)

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 𝑚.

Negation Elimination (¬E)
Assumption Set	Line #	Formula	Annotation
𝔸	𝑚.	¬¬𝜙
𝔸	𝑛.	𝜙	¬E 𝑛

For example:

(P ∨ P) ⊢ P
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, 3
➤1	5.	P	¬E 4

Reductio ad absurdum (RAA) / Indirect Proof (IP)

Given

a formula 𝜙 that was introduced as assumption 𝑎 on line 𝑘
a formula 𝜓 on line 𝑙 resting on assumption set 𝔸
the formula ¬𝜓 on line 𝑚 resting on assumption set 𝔹,

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 𝑘.

*Reductio ad absurdum* (RAA) / Indirect Proof (IP)
Assumption Set	Line #	Formula	Annotation
{𝑎}	𝑘.	𝜙	A for RAA
𝔸	𝑙.	𝜓
𝔹	𝑚.	¬𝜓
(𝔸 ∪ 𝔹) − {𝑎}	𝑛.	¬𝜙	RAA^(𝑎) 𝑙, 𝑚

Alternatively:

Assumption Set	Line #	Formula	Annotation
{𝑎}	𝑘.	¬𝜙	A for RAA
𝔸	𝑙.	𝜓
𝔹	𝑚.	¬𝜓
(𝔸 ∪ 𝔹) − {𝑎}	𝑛.	𝜙	RAA^(𝑎) 𝑙, 𝑚

For example:

(P ∨ P) ⊢ P
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, 3

Derived Rule Proofs

Since many of us learned logic using the Fitch Proof system, I’ve included both Lemmon and Fitch style proofs for each derived rule. Lemmon proofs use the primitive rules above. Fitch proofs use the rules from chapter 16 of forall𝑥: Calgary (Fall 2021+). Compare the proofs to better understand each system.

Double Negation (DN)

Lemmon

¬¬P ⊢ P
Assumption Set	Line #	Formula	Annotation
1	1.	¬¬P	A
1	2.	P	¬E 1

P ⊢ ¬¬P
Assumption Set	Line #	Formula	Annotation
1	1.	P	A
2	2.	¬P	A
1	3.	¬¬P	¬I⁽²⁾ 1, 2

Fitch

¬¬P ⊢ P
1¬¬P
2¬P
3⊥	¬E 1, 2
4P	IP 2–3

P ⊢ ¬¬P
1P
2¬P
3⊥	¬E 1, 2
4¬¬P	¬I 2–3

Redundancy (Re)

Lemmon

(P & P) ⊢ P
Assumption Set	Line #	Formula	Annotation
1	1.	P & P	A
1	2.	P	&E

P ⊢ (P & P)
Assumption Set	Line #	Formula	Annotation
1	1.	P	A
1	2.	P & P	&I 1, 1

(P ∨ P) ⊢ P
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, 3

P ⊢ (P ∨ P)
Assumption Set	Line #	Formula	Annotation
1	1.	P	A
1	2.	P ∨ P	∨I 1

Fitch

(P & P) ⊢ P
1P & P
2P	&E 1

P ⊢ (P & P)
1P
3P & P	&I 1, 1

(P ∨ P) ⊢ P
1P ∨ P
2P
3P	Reit 2
4P ∨ P	∨E 1, 2–3, 2–3

P ⊢ (P ∨ P)
1P
2P ∨ P	∨I 1

Commutativity (Comm)

Lemmon

(P & Q) ⊢ (Q & P)
Assumption Set	Line #	Formula	Annotation
1	1.	P & Q	A
1	2.	P	&E 1
1	3.	Q	&E 1
1	4.	Q & P	&I 2, 3

(Q & P) ⊢ (P & Q)
Assumption Set	Line #	Formula	Annotation
1	1.	Q & P	A
1	2.	Q	&E 1
1	3.	P	&E 1
1	4.	P & Q	&I 2, 3

(P ∨ Q) ⊢ (Q ∨ P)
Assumption Set	Line #	Formula	Annotation
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⁽³⁾ 2, 4
1, 2	6.	Q	∨E 1, 5
1, 2	7.	Q ∨ P	∨I 6
1	8.	Q ∨ P	RAA⁽²⁾ 2, 7

(Q ∨ P) ⊢ (P ∨ Q)
Assumption Set	Line #	Formula	Annotation
1	1.	Q ∨ P	A
2	2.	¬(P ∨ Q)	A for RAA
3	3.	P	A for ¬I
3	4.	P ∨ Q	∨I 3
2	5.	¬P	¬I⁽³⁾ 2, 4
1, 2	6.	Q	∨E 1, 5
1, 2	7.	P ∨ Q	∨I 6
1	8.	P ∨ Q	RAA⁽²⁾ 2, 7

(P ↔︎ Q) ⊢ (Q ↔︎ P)
Assumption Set	Line #	Formula	Annotation
1	1.	P ↔︎ Q	A
1	2.	P → Q	↔︎E 1
1	3.	Q → P	↔︎E 1
1	4.	Q ↔︎ P	↔︎I 2, 3

(Q ↔︎ P) ⊢ (P ↔︎ Q)
Assumption Set	Line #	Formula	Annotation
1	1.	Q ↔︎ P	A
1	2.	Q → P	↔︎E 1
1	3.	P → Q	↔︎E 1
1	4.	P ↔︎ Q	↔︎I 2, 3

Fitch

(P & Q) ⊢ (Q & P)
1P & Q
2P	&E 1
3Q	&E 1
4Q & P	&I 2, 3

(Q & P) ⊢ (P & Q)
1Q & P
2Q	&E 1
3P	&E 1
4P & Q	&I 2, 3

(P ∨ Q) ⊢ (Q ∨ P)
1P ∨ Q
2P
3Q ∨ P	∨I 2
4Q
5Q ∨ P	∨I 4
6Q ∨ P	∨E 1, 2–3, 4–5

(Q ∨ P) ⊢ (P ∨ Q)
1Q ∨ P
2Q
3P ∨ Q	∨I 2
4P
5P ∨ Q	vI 5
6P ∨ Q	∨E 1, 2–3, 4–5

(P ↔︎ Q) ⊢ (Q ↔︎ P)
1P ↔︎ Q
2P
3Q	↔︎E 1
4Q
5P	↔︎E 1
6Q ↔︎ P	↔︎I 2–3, 4–5

(Q ↔︎ P) ⊢ (P ↔︎ Q)
1Q ↔︎ P
2Q
3P	↔︎E 1
4P
5Q	↔︎E 1
6P ↔︎ Q	↔︎I 2–3, 4–5

Associativity (Assoc)

Lemmon

(P & (Q & R)) ⊢ ((P & Q) & R)
Assumption Set	Line #	Formula	Annotation
1	1.	P & (Q & R)	A
1	2.	P	&E 1
1	3.	Q & R	&E 1
1	4.	Q	&E 3
1	5.	R	&E 3
1	6.	P & Q	&I 2, 4
1	7.	(P & Q) & R	&I 5, 6

((P & Q) & R) ⊢ (P & (Q & R))
Assumption Set	Line #	Formula	Annotation
1	1.	(P & Q) & R	A
1	2.	P & Q	&E 1
1	3.	R	&E 1
1	4.	P	&E 2
1	5.	Q	&E 2
1	6.	Q & R	&I 3, 5
1	7.	P & (Q & R)	&I 4, 6

(P ∨ (Q ∨ R)) ⊢ ((P ∨ Q) ∨ R)
Assumption Set	Line #	Formula	Annotation
1	1.	P ∨ (Q ∨ R)	A
2	2.	¬((P ∨ Q) ∨ R)	A for RAA
3	3.	¬R	A for RAA
4	4.	¬P	A for RAA
1, 4	5.	Q ∨ R	∨E 1, 4
1, 3, 4	6.	Q	∨E 3, 5
1, 3, 4	7.	P ∨ Q	∨I 6
1, 3, 4	8.	(P ∨ Q) ∨ R	∨I 7
1, 2, 3	9.	P	RAA⁽⁴⁾ 2, 8
1, 2, 3	10.	P ∨ Q	∨I 9
1, 2, 3	11.	(P ∨ Q) ∨ R	∨I 10
1, 2	12.	R	RAA⁽³⁾ 2, 11
1, 2	13.	(P ∨ Q) ∨ R	∨I 12
1	14.	(P ∨ Q) ∨ R	RAA⁽²⁾ 2, 13

((P ∨ Q) ∨ R) ⊢ (P ∨ (Q ∨ R))
Assumption Set	Line #	Formula	Annotation
1	1.	(P ∨ Q) ∨ R	A
2	2.	¬(P ∨ (Q ∨ R))	A for RAA
3	3.	¬P	A for RAA
4	4.	¬R	A for RAA
1, 4	5.	P ∨ Q	∨E 1, 4
1, 3, 4	6.	Q	∨E 3, 5
1, 3, 4	7.	Q ∨ R	∨I 6
1, 3, 4	8.	P ∨ (Q ∨ R)	∨I 7
1, 2, 3	9.	R	RAA⁽⁴⁾ 2, 8
1, 2, 3	10.	Q ∨ R	∨I 9
1, 2, 3	11.	P ∨ (Q ∨ R)	∨I 10
1, 2	12.	P	RAA⁽³⁾ 2, 11
1, 2	13.	P ∨ (Q ∨ R)	∨I 12
1	14.	P ∨ (Q ∨ R)	RAA⁽²⁾ 2, 13

Fitch

((P & Q) & R) ⊢ (P & (Q & R))
1P & (Q & R)
2P	&E 1
3Q & R	&E 1
4Q	&E 3
5R	&E 3
6P & Q	&I 2, 4
7(P & Q) & R	&I 5, 6

(P & (Q & R)) ⊢ ((P & Q) & R)
1(P & Q) & R
2P & Q	&E 1
3R	&E 1
4P	&E 2
5Q	&E 2
6Q & R	&I 3, 5
7P & (Q & R) &I 4, 6

(P ∨ (Q ∨ R)) ⊢ ((P ∨ Q) ∨ R)
1P ∨ (Q ∨ R)
2P
3P ∨ Q	∨I 2
4(P ∨ Q) ∨ R	∨I 3

5Q ∨ R
6Q
7P ∨ Q	∨I 6
8(P ∨ Q) ∨ R	∨I 7

9R
10(P ∨ Q) ∨ R	∨I 9
11(P ∨ Q) ∨ R	∨E 5, 6–8, 9–10
12(P ∨ Q) ∨ R	∨E 1, 2–4, 5–11

((P ∨ Q) ∨ R) ⊢ (P ∨ (Q ∨ R))
1(P ∨ Q) ∨ R
2P ∨ Q
3P
4P ∨ (Q ∨ R)	∨I 3
5Q
6Q ∨ R	∨I 5
7P ∨ (Q ∨ R)	∨I 6
8P ∨ (Q ∨ R)	∨E 2, 3–4, 5–7
9R
10Q ∨ R	∨I 9
11P ∨ (Q ∨ R)	∨I 10
12P ∨ (Q ∨ R)	∨E 1, 2–8, 9–11

Distribution (Dist)

Lemmon

(P & (Q ∨ R)) ⊢ ((P & Q) ∨ (P & R))
Assumption Set	Line #	Formula	Annotation
1	1.	P & (Q ∨ R)	A
1	2.	P	&E 1
1	3.	Q ∨ R	&E 2
4	4.	¬((P & Q) ∨ (P & R))	A for RAA
5	5.	¬(P & Q)	A for RAA
6	6.	Q	A for ¬I
1, 6	7.	P & Q	&I 2, 6
1, 5	8.	¬Q	¬I⁽⁵⁾ 5, 7
1, 5	9.	R	∨E 3, 8
1, 5	10.	P & R	&I 2, 9
1, 5	11.	(P & Q) ∨ (P & R)	∨I 10
1, 4	12.	P & Q	¬I⁽⁵⁾ 4, 11
1, 4	13.	(P & Q) ∨ (P & R)	∨I 12
1	14.	(P & Q) ∨ (P & R)	¬I⁽⁴⁾ 4, 13

((P & Q) ∨ (P & R)) ⊢ (P & (Q ∨ R))
Assumption Set	Line #	Formula	Annotation
1	1.	(P & Q) ∨ (P & R)	A
2	2.	¬(P & (Q ∨ R))	A for RAA
3	3.	¬(P & Q)	A for RAA
1, 3	4.	P & R	∨E 1, 3
1, 3	5.	P	&E 4
1, 3	6.	R	&E 4
1, 3	7.	Q ∨ R	∨I 6
1, 3	8.	P & (Q ∨ R)	&I 5, 7
1, 2	9.	P & (Q ∨ R)	RAA⁽³⁾ 2, 8
1	10.	P & (Q ∨ R)	RAA⁽²⁾ 2, 9

(P ∨ (Q & R)) ⊢ ((P ∨ Q) & (P ∨ R))
Assumption Set	Line #	Formula	Annotation
1	1.	P ∨ (Q & R)	A
2	2.	¬((P ∨ Q) & (P ∨ R))	A for RAA
3	3.	P	A for ¬I
3	4.	P ∨ Q	∨I 3
3	5.	P ∨ R	∨I 3
3	6.	(P ∨ Q) & (P ∨ R)	&I 4, 5
2	7.	¬P	¬I⁽³⁾ 2, 6
1, 2	8.	Q & R	∨E 1, 7
1, 2	9.	Q	&E 8
1, 2	10.	R	&E 8
1, 2	11.	P ∨ Q	∨I 9
1, 2	12.	P ∨ R	∨I 10
1, 2	13.	(P ∨ Q) & (P ∨ R)	&I 11, 12
1	14.	(P ∨ Q) & (P ∨ R)	RAA⁽²⁾ 2, 13

((P ∨ Q) & (P ∨ R)) ⊢ (P ∨ (Q & R))
Assumption Set	Line #	Formula	Annotation
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⁽⁵⁾ 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, 11

Fitch

(P & (Q ∨ R)) ⊢ ((P & Q) ∨ (P & R))
1P & (Q ∨ R)
2P	&E 1
3Q ∨ R	&E 1
4Q
5P & Q	&I 2, 4
6(P & Q) ∨ (P & R)	∨I 5
7R
8P & R	&I 2, 7
9(P & Q) ∨ (P & R)	∨I 8
10(P & Q) ∨ (P & R)	vE 3, 4–6, 7–9

((P & Q) ∨ (P & R)) ⊢ (P & (Q ∨ R))
1(P & Q) ∨ (P & R)
2P & Q
3P	&E 2
4Q	&E 2
5Q ∨ R	∨I 4
6P & (Q ∨ R)	&I 3, 5
7P & R
8P	&E 7
9R	&E 7
10Q ∨ R	∨I 9
11P & (Q ∨ R)	&I 8, 10
12P & (Q ∨ R)	∨I 1, 2–6, 7–11

(P ∨ (Q & R)) ⊢ ((P ∨ Q) & (P ∨ R))
1P ∨ (Q & R)
2P
3P ∨ Q	∨I 2
4P ∨ R	∨I 2
5(P ∨ Q) & (P ∨ R)	&I 3, 4
6Q & R
7Q	&E 6
8R	&E 6
9P ∨ Q	∨I 7
10P ∨ R	∨I 8
11(P ∨ Q) & (P ∨ R)	&I 9, 10
12(P ∨ Q) & (P ∨ R)	∨I 1, 2–5, 6–12

((P ∨ Q) & (P ∨ R)) ⊢ (P ∨ (Q & R))
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

DeMorgan’s Theorem (DM)

Lemmon

¬(P & Q) ⊢ (¬P ∨ ¬Q)
Assumption Set	Line #	Formula	Annotation
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⁽²⁾ 1, 4
1	6.	¬P	¬E⁽³⁾ 3, 5
1	7.	¬P ∨ ¬Q	∨I 6

(¬P ∨ ¬Q) ⊢ ¬(P & Q)
Assumption Set	Line #	Formula	Annotation
1	1.	¬P ∨ ¬Q	A
2	2.	P & Q	A for ¬I
2	3.	P	&E 2
2	4.	Q	&E 2
1, 2	5.	¬Q	∨E 1, 3
1	6.	¬(P & Q)	¬I⁽²⁾ 4, 5

¬(P ∨ Q) ⊢ (¬P & ¬Q)
Assumption Set	Line #	Formula	Annotation
1	1.	¬(P ∨ Q)	A
2	2.	P	A for ¬I
2	3.	P ∨ Q	∨I 2
1	4.	¬P	¬I⁽²⁾ 1, 3
5	5.	Q	A for ¬I
5	6.	P ∨ Q	∨I 5
1	7.	¬Q	¬I⁽⁵⁾ 1, 6
1	8.	¬P & ¬Q	&I 4, 7

(¬P & ¬Q) ⊢ ¬(P ∨ Q)
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 for ¬I
1, 4	5.	Q	∨E 2, 4
1	6.	¬(P ∨ Q)	¬I⁽⁴⁾ 3, 5

(P ∨ Q) ⊢ ¬(¬P & ¬Q)
Assumption Set	Line #	Formula	Annotation
1	1.	P ∨ Q	A
2	2.	¬P & ¬Q	A for ¬I
2	3.	¬P	&E 2
2	4.	¬Q	&E 2
1, 2	5.	P	∨E 1, 4
1	6.	¬(¬P & ¬Q)	¬I⁽²⁾ 3, 5

¬(¬P & ¬Q) ⊢ (P ∨ Q)
Assumption Set	Line #	Formula	Annotation
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⁽³⁾ 2, 4
6	6.	Q	A for RAA
6	7.	P ∨ Q	∨I 6
2	8.	¬Q	¬I⁽⁶⁾ 2, 7
2	10.	¬P & ¬Q	&I 5, 8
1	12.	P ∨ Q	RAA⁽²⁾ 1, 10

(P & Q) ⊢ ¬(¬P ∨ ¬Q)
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
1	6.	¬(¬P ∨ ¬Q)	¬I⁽⁴⁾ 3, 5

¬(¬P ∨ ¬Q) ⊢ (P & Q)
Assumption Set	Line #	Formula	Annotation
1	1.	¬(¬P ∨ ¬Q)	A
2	2.	¬P	A for RAA
2	3.	¬P ∨ ¬Q	∨I 2
1	4.	P	RAA⁽²⁾ 1, 3
5	5.	¬Q	A for RAA
5	6.	¬P ∨ ¬Q	∨I 5
1	7.	Q	RAA⁽⁵⁾ 1, 6
1	8.	P & Q	&I 4, 7

Fitch

¬(P & Q) ⊢ (¬P ∨ ¬Q)
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

(¬P ∨ ¬Q) ⊢ ¬(P & Q)
1(¬P ∨ ¬Q)
2(P & Q)
3P	&E 2
4Q	&E 2
5¬Q	∨E 1, 3
7⊥	¬E
8¬(P & Q)	IP 2–7

¬(P ∨ Q) ⊢ (¬P & ¬Q)
1¬(P ∨ Q)
2P
3P ∨ Q	∨I 2
4⊥	¬E 1, 3
5¬P	¬I 2–4
6Q
7P ∨ Q	∨I 2
8⊥	¬E 1, 7
9¬Q	¬I 6–8
10¬P & ¬Q	&I 5, 9

(¬P & ¬Q) ⊢ ¬(P ∨ Q)
1¬P & ¬Q
2¬P	&E 1
3¬Q	&E 1
4P ∨ Q
5Q	∨E 2, 4
6⊥	¬E 3, 5
7¬(P ∨ Q)	¬I 4–6

(P ∨ Q) ⊢ ¬(¬P & ¬Q)
1P ∨ Q
2¬P & ¬Q
3¬P	&E 2
4¬Q	&E 2
5P	∨E 1, 4
6⊥	¬E 3, 5
7¬(¬P & ¬Q)	IP 2–6

¬(¬P & ¬Q) ⊢ (P ∨ Q)
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

(P & Q) ⊢ ¬(¬P ∨ ¬Q)
1P & Q
2P	&E 1
3Q	&E 1
4¬P ∨ ¬Q
5¬Q	∨E 2, 4
6⊥	¬E 3, 5
7¬(¬P ∨ ¬Q)	¬I 4–6

¬(¬P ∨ ¬Q) ⊢ (P & Q)
1¬(¬P ∨ ¬Q)
2¬P
3¬P ∨ ¬Q	∨I 2
4⊥	¬E 1, 3
5P	IP 2–4
6¬Q
7¬P ∨ ¬Q	∨I 6
8⊥	¬E 1, 7
9Q	IP 6–8
10P & Q	&I 5, 9

Def. of Conditional (→^df)

Lemmon

(¬P ∨ Q) ⊢ (P → Q)
Assumption Set	Line #	Formula	Annotation
1	1.	¬P ∨ Q	A
2	2.	P	A for →I
1, 2	3.	Q	∨E 1, 2
1	4.	P → Q	→I⁽²⁾ 2, 3

(P → Q) ⊢ (¬P ∨ Q)
Assumption Set	Line #	Formula	Annotation
1	1.	P → Q	A
2	2.	¬(¬P ∨ Q)	A for RAA
3	3.	P	A for ¬I
1, 3	4.	Q	→E 1, 3
1, 3	5.	¬P ∨ Q	∨I 4
1, 2	6.	¬P	¬I⁽³⁾ 2, 5
1, 2	7.	¬P ∨ Q	∨I 6
1	8.	¬P ∨ Q	RAA⁽²⁾ 2, 7

(P ∨ Q) ⊢ (¬P → Q)
Assumption Set	Line #	Formula	Annotation
1	1.	P ∨ Q	A
2	2.	¬P	A for →I
1, 2	3.	Q	∨E 1
1	4.	¬P → Q	→I⁽²⁾ 2, 3

(¬P → Q) ⊢ (P ∨ Q)
Assumption Set	Line #	Formula	Annotation
1	1.	¬P → Q	A
2	2.	¬(P ∨ Q)	A for ¬I
3	3.	¬P	A for RAA
1, 3	4.	Q	→E 1, 3
1, 3	5.	P ∨ Q	∨I 4
1, 2	6.	P	RAA⁽³⁾ 2, 5
1, 2	7.	P ∨ Q	∨I 6
1	8.	P ∨ Q	¬I⁽²⁾ 2, 7

(P ∨ Q) ⊢ (¬Q → P)
Assumption Set	Line #	Formula	Annotation
1	1.	P ∨ Q	A
2	2.	¬Q	A for →I
1, 2	3.	P	∨E 1, 2
1	4.	¬Q → P	→I⁽²⁾ 2, 3

(¬Q → P) ⊢ (P ∨ Q)
Assumption Set	Line #	Formula	Annotation
1	1.	¬Q → P	A
2	2.	¬(P ∨ Q)	A for RAA
3	3.	¬Q	A for RAA
1, 3	4.	P	→E 1, 3
1, 3	5.	P ∨ Q	∨I 4
1, 2	6.	Q	RAA^(3) 2, 5
1, 4	7.	P ∨ Q	∨I 6
1	8.	P ∨ Q	RAA⁽²⁾ 2, 7

Fitch

(¬P ∨ Q) ⊢ (P → Q)
1¬P ∨ Q
2P
3Q	∨E 1, 2
4P → Q	→I 2–3

(P → Q) ⊢ (¬P ∨ Q)
1P → Q
2¬(¬P ∨ Q)
3P
4Q	→E 1, 3
5¬P ∨ Q	∨I 4
6⊥	¬E 2, 5
7¬P	IP 3–6
8¬P ∨ Q	∨I 7
9⊥	¬E 2, 8
10¬P ∨ Q	IP 2–6

(P ∨ Q) ⊢ (¬P → Q)
1P ∨ Q
2¬P
3Q	∨E 1, 2
4¬P → Q	→I 2–3

(¬P → Q) ⊢ (P ∨ Q)
1¬P → Q
2¬(P ∨ Q)
3¬P
4Q	→E 1, 3
5P ∨ Q	∨I 4
6⊥	¬E 2, 5
7P	IP 3–6
8P ∨ Q	∨I 7
9⊥	¬E 2, 8
10P ∨ Q	IP 2–9

(P ∨ Q) ⊢ (¬Q → P)
1P ∨ Q
2¬Q
3P	∨E 1, 2
4¬Q → P	→I 2–3

(¬Q → P) ⊢ (P ∨ Q)
1¬Q → P
2¬(P ∨ Q)
3¬Q
4P	→E 1, 3
5P ∨ Q	∨I 4
6⊥	¬E 2, 5
7Q	IP 3–6
8P ∨ Q	∨I 7
9⊥	¬E 2, 8
10P ∨ Q	IP 2–9

True Consequent (TC)

Lemmon

Q ⊢ (P → Q)
Assumption Set	Line #	Formula	Annotation
1	1.	Q	A
2	2.	P	A for →I
1	3.	P → Q	→I⁽²⁾ 1, 2

Fitch

Q ⊢ (P → Q)
1Q
2P
3Q	Reit 1
4P → Q	→I 2–3

False Antecedent (FA)

Lemmon

¬P ⊢ (P → Q)
Assumption Set	Line #	Formula	Annotation
1	1.	¬P	A
2	2.	P	A for →I
3	3.	¬Q	A for RAA
1, 2	4.	Q	RAA⁽³⁾ 1, 2
1	5	P → Q	→I⁽²⁾ 4

Fitch

1¬P
2P
3⊥	¬E 1, 2
4Q	X 3

Impossible Antecedent (IA)

Lemmon

(P → Q), (P → ¬Q) ⊢ ¬P
Assumption Set	Line #	Formula	Annotation
1	1.	P → Q	A
2	2.	P → ¬Q	A
3	3.	P	A for ¬I
1, 3	4.	Q	→E 1, 3
2, 3	5.	¬Q	→E 2, 3
1, 2	6.	¬P	¬I⁽³⁾ 4, 5

Fitch

(P → Q), (P → ¬Q) ⊢ ¬P
1P → Q
2P → ¬Q
3P
4Q	→E 1, 3
5¬Q	→E 2, 3
6⊥	¬E 4, 5
7¬P	¬I 3–6

Hypothetical Syllogism (HS)

Lemmon

(P → Q), (Q → R) ⊢ (P → R)
Assumption Set	Line #	Formula	Annotation
1	1.	P → Q	A
2	2.	Q → R	A
3	3.	P	A for →I
1, 3	4.	Q	→E 1, 3
1, 2, 3	5.	R	→E 2, 4
1, 2	6.	P → R	→I⁽³⁾ 3, 5

Fitch

1P → Q
2Q → R
3P
4Q	→E 1, 3
5R	→E 2, 4
6P → R	→I 3–5

Negated Conditional (¬→)

Lemmon

¬(P → Q) ⊢ (P & ¬Q)
Assumption Set	Line #	Formula	Annotation
1	1.	¬(P → Q)	A
2	2.	¬(P & ¬Q)	A for RAA
3	3.	P	A for →I
4	4.	¬Q	A for ¬I
3, 4	5.	P & ¬Q	&I 3, 4
2, 3	6.	Q	RAA⁽⁴⁾ 2, 5
2	7.	P → Q	→I⁽³⁾ 3, 6
1	8.	P & ¬Q	RAA⁽²⁾ 1, 7

(P & ¬Q) ⊢ ¬(P → Q)
Assumption Set	Line #	Formula	Annotation
1	1.	P & ¬Q	A
1	2.	P	&E 1
1	3.	¬Q	&E 1
2	4.	P → Q	A for ¬I
1, 2	5.	Q	→E 2, 4
1	6.	¬(P → Q)	¬I⁽⁴⁾ 3, 5

Fitch

¬(P → Q) ⊢ (P & ¬Q)
1¬(P → Q)
2¬(P & ¬Q)
3P
4¬Q
5P & ¬Q	&I 3, 4
6⊥	¬E 2, 5
7Q	IP 4–6
8P → Q	→I 3–7
9⊥	¬E 1, 8
10P & ¬Q	IP 2–9

(P & ¬Q) ⊢ ¬(P → Q)
1P & ¬Q
2P	&E 1
3¬Q	&E 1
4P → Q
5Q	→E 2, 4
6⊥	¬E 3, 5
7¬(P → Q)	IP 4–6

Negated Biconditional (¬↔︎)

Lemmon

¬(P ↔︎ Q) ⊢ ((P & ¬Q) ∨ (¬P & Q))
Assumption Set	Line #	Formula	Annotation
1	1.	¬(P ↔︎ Q)	A
2	2.	¬((P & ¬Q) ∨ (¬P & Q))	A for RAA
3	3.	¬(P & ¬Q)	A for RAA
2, 3	4.	¬P & Q	∨E 2, 3
2, 3	5.	Q	&E 4
7	6.	P	A for →I
2, 3	7.	P → Q	→I⁽⁶⁾ 5, 6
8	8.	¬(¬P & Q)	A for RAA
2, 8	9.	P & ¬Q	∨E 2, 8
2, 8	10.	P	&E 9
13	11.	Q	A for →I
2, 8	12.	Q → P	→I⁽¹¹⁾ 10, 11
2, 3, 8	13.	P ↔︎ Q	↔︎I 7, 12
1, 2, 3	14.	¬P & Q	RAA⁽⁸⁾ 1, 13
1, 2, 3	15.	P & ¬Q	∨E 2, 14
1, 2	16.	P & ¬Q	RAA⁽³⁾ 3, 15
1, 2	17.	(P & ¬Q) ∨ (¬P & Q)	∨I 16
1	18.	(P & ¬Q) ∨ (¬P & Q)	RAA⁽²⁾ 2, 17

((P & ¬Q) ∨ (¬P & Q)) ⊢ ¬(P ↔︎ Q)
Assumption Set	Line #	Formula	Annotation
1	1.	((P & ¬Q) ∨ (¬P & Q))	A
2	2.	P ↔︎ Q	A for ¬I
2	3.	(P → Q) & (Q → P)	↔︎E 2
2	4.	P → Q	&E 3
2	5.	Q → P	&E 3
6	6.	P & ¬Q	A for ¬I
6	7.	P	&E 6
6	8.	¬Q	&E 6
2, 6	9.	Q	↔︎E 4, 7
2	10.	¬(P & ¬Q)	¬I⁽⁶⁾ 8, 9
1, 2	11.	¬P & Q	∨E 1, 10
1, 2	12.	¬P	&E 11
1, 2	13.	Q	&E 11
1, 2	14.	P	↔︎E 5, 13
2	15.	¬(P ↔︎ Q)	¬I⁽²⁾ 12, 14

Fitch

¬(P ↔︎ Q) ⊢ ((P & ¬Q) ∨ (¬P & Q))
1¬(P ↔︎ Q)
2¬((P & ¬Q) ∨ (¬P & Q))
3¬(P & ¬Q)
4¬(¬P & Q)
5P
6¬Q
7P & ¬Q	&I 5, 6
8⊥	¬E 3, 7
9Q	IP 6–8
10Q
11¬P
12¬P & Q	&I 10, 11
13⊥	¬E 4, 12
14P	IP 11, 13
15P ↔︎ Q	↔︎I 5–9, 10–14
16⊥	¬E 1, 15
17¬P & Q	IP 4–16
18(P & ¬Q) ∨ (¬P & Q)	∨I 17
19⊥	¬E 2, 18
20P & ¬Q	IP 3–19
21(P & ¬Q) ∨ (¬P & Q)	∨I 20
22⊥	¬E 2, 21
23(P & ¬Q) ∨ (¬P & Q)	IP 2–22

((P & ¬Q) ∨ (¬P & Q)) ⊢ ¬(P ↔︎ Q)
1((P & ¬Q) ∨ (¬P & Q))
2P ↔︎ Q
3P & ¬Q
4P	&E 3
5¬Q	&E 3
6Q	↔︎E 2, 4
7⊥	¬E 5, 6
8¬(P & ¬Q)	IP 3–7
9¬P & Q	∨E 1, 8
10¬P	&E 9
11Q	&E 9
12P	↔︎E 2, 11
13⊥	¬E 10, 12
14¬(P ↔︎ Q)	IP 2–13

Conditional Contraposition (Con)

Lemmon

(P → Q) ⊢ (¬Q → ¬P)
Assumption Set	Line #	Formula	Annotation
1	1.	P → Q	A
2	2.	¬Q	A for →I
3	3.	P	A for ¬I
1, 3	4.	Q	→E 1, 3
1, 2	5.	¬P	¬I⁽³⁾ 2, 4
1	6.	¬Q → ¬P	→I⁽²⁾ 2, 5

(¬Q → ¬P) ⊢ (P → Q)
Assumption Set	Line #	Formula	Annotation
1	1.	¬Q → ¬P	A
2	2.	P	A for →I
3	3.	¬Q	A for RAA
1, 3	4.	¬P	→E 1, 3
1, 2	5.	Q	RAA⁽³⁾ 2, 4
1	6.	P → Q	→I⁽²⁾ 2, 5

Fitch

(P → Q) ⊢ (¬Q → ¬P)
1P → Q
2¬Q
3P
4Q	→E 1, 3
5⊥	¬E 2, 4
6¬P	¬I 3–5
7¬Q → ¬P	→I 2–6

(¬Q → ¬P) ⊢ (P → Q)
1¬Q → ¬P
2P
3¬Q
4¬P	→E 1, 3
5⊥	¬E 2, 4
6Q	IP 3–5
7P → Q	→I 2–6

Biconditional Contraposition (BiCon)

Lemmon

(P ↔︎ Q) ⊢ (¬Q ↔︎ ¬P)
Assumption Set	Line #	Formula	Annotation
1	1.	P ↔︎ Q	A
1	2.	P → Q	↔︎E 1
1	3.	Q → P	↔︎E 1
4	4.	¬Q	A for →I
5	5.	P	A for ¬I
1, 5	6.	Q	→E 2, 5
1, 4	7.	¬P	¬I⁽⁵⁾ 4, 6
1	8.	¬Q → ¬P	→I⁽⁴⁾ 4, 7
9	9.	¬P	A for →I
10	10.	Q	A for ¬I
1, 10	11.	P	→E 3, 10
1, 9	12.	¬Q	¬I⁽¹⁰⁾ 9, 11
1	13.	¬P → ¬Q	→I⁽⁹⁾ 9, 12
1	14.	¬Q ↔︎ ¬P	↔︎I 8, 13

(¬Q ↔︎ ¬P) ⊢ (P ↔︎ Q)
Assumption Set	Line #	Formula	Annotation
1	1.	¬Q ↔︎ ¬P	A
1	2.	¬Q → ¬P	↔︎E 1
1	3.	¬P → ¬Q	↔︎E 1
4	4.	P	A for →I
5	5.	¬Q	A for RAA
1, 5	6.	¬P	→E 2, 5
1, 4	7.	Q	RAA⁽⁵⁾ 4, 6
1	8.	P → Q	→I⁽⁴⁾ 4, 7
9	9.	Q	A for →I
10	10.	¬P	A for RAA
1, 10	11.	¬Q	→E 3, 10
1, 9	12.	P	¬I⁽¹⁰⁾ 9, 11
1	13.	Q → P	→I⁽⁹⁾ 9, 12
1	14.	P ↔︎ Q	↔︎I 8, 13

Fitch

(P ↔︎ Q) ⊢ (¬Q ↔︎ ¬P)
1P ↔︎ Q
2¬Q
3P
4Q	↔︎E 1, 3
5⊥	¬E 2, 4
6¬P	¬I 3–5
7¬P
8Q
9P	↔︎E 1, 8
10⊥	¬E 7, 9
11¬Q	¬I 8–10
12¬Q ↔︎ ¬P	↔︎I 2–6, 7–11

(¬Q ↔︎ ¬P) ⊢ (P ↔︎ Q)
1¬Q ↔︎ ¬P
2P
3¬Q
4¬P	↔︎E 1, 3
5⊥	¬E 2, 4
6Q	IP 3–5
7Q
8¬P
9¬Q	↔︎E 1, 8
10⊥	¬E 7, 9
11P	¬I 8–10
12P ↔︎ Q	↔︎I 2–6, 7–11

Modus Tollens (MT)

Lemmon

(P → Q), ¬Q ⊢ ¬P
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⁽³⁾ 2, 4

(¬P → Q), ¬Q ⊢ P
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	RAA⁽³⁾ 2, 4

(P → ¬Q), Q ⊢ ¬P
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⁽³⁾ 2, 4

(¬P → ¬Q), Q ⊢ P
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	RAA⁽³⁾ 2, 4

Fitch

(P → Q), ¬Q ⊢ ¬P
1P → Q
2¬Q
3P
4Q	→E 1, 3
5⊥	¬E 2, 4
6¬P	IP 3–5

(¬P → Q), ¬Q ⊢ P
1¬P → Q
2¬Q
3¬P
4Q	→E 1, 3
5⊥	¬E 2, 4
6P	IP 3–5

(P → ¬Q), Q ⊢ ¬P
1P → ¬Q
2Q
3P
4¬Q	→E 1, 3
5⊥	¬E 2, 4
6¬P	IP 3–5

(¬P → ¬Q), Q ⊢ P
1¬P → ¬Q
2Q
3¬P
4¬Q	→E 1, 3
5⊥	¬E 2, 4
6P	IP 3–5

Biconditional Ponens (BP)

Lemmon

(P ↔︎ Q), P ⊢ Q
Assumption Set	Line #	Formula	Annotation
1	1.	P ↔︎ Q	A
2	2.	P	A
1, 2	3.	P → Q	↔︎E 1, 2
1, 2	4.	Q	→E 2, 3

(P ↔︎ Q), Q ⊢ P
Assumption Set	Line #	Formula	Annotation
1	1.	P ↔︎ Q	A
2	2.	Q	A
1, 2	3.	Q → P	↔︎E 1, 2
1, 2	4.	P	→E 2, 3

Fitch

(P ↔︎ Q), P ⊢ Q
1P ↔︎ Q
2P
3Q	↔︎E 1, 2

(P ↔︎ Q), Q ⊢ P
1P ↔︎ Q
2Q
3P	↔︎E 1, 2

Biconditional Tollens (BT)

Lemmon

(P ↔︎ Q), ¬Q ⊢ ¬P
Assumption Set	Line #	Formula	Annotation
1	1.	P ↔︎ Q	A
2	2.	¬Q	A
1	3.	P → Q	↔︎E 1
4	4.	P	A for RAA
1, 4	5.	Q	→E 3, 4
1, 2	6.	¬P	RAA⁽⁴⁾ 2, 5

(P ↔︎ Q), ¬P ⊢ ¬Q
Assumption Set	Line #	Formula	Annotation
1	1.	P ↔︎ Q	A
2	2.	¬P	A
1	3.	Q → P	↔︎E 1
4	4.	Q	A for RAA
1, 4	5.	P	→E 3, 4
1, 2	6.	¬Q	RAA⁽⁴⁾ 2, 5

Fitch

(P ↔︎ Q), ¬Q ⊢ ¬P
1P ↔︎ Q
2¬Q
3P
4Q	↔︎E 1
5⊥	¬E 2, 5
6¬P	IP 3–5

(P ↔︎ Q), ¬P ⊢ ¬Q
1P ↔︎ Q
2¬P
3Q
4P	↔︎E 1
5⊥	¬E 2, 5
6¬Q	IP 3–5

Import (Imp)

Lemmon

(P → (Q → R)) ⊢ ((P & Q) → R)
Assumption Set	Line #	Formula	Annotation
1	1	P → (Q → R)	A
2	2	P & Q	A for →I
2	3	P	&E 2
2	4	Q	&E 2
1, 2	5	Q → R	→E 1, 3
1, 2	6	R	→E 4, 5
1	7	(P & Q) → R	→I⁽²⁾ 2, 6

Fitch

(P → (Q → R)) ⊢ ((P & Q) → R)
1P → (Q → R)
2P & Q
3P	&E 2
4Q	&E 2
5Q → R	→E 1, 3
6R	→E 4, 5
7(P & Q) → R	→I 2–6

Export (Exp)

Lemmon

((P & Q) → R) ⊢ (P → (Q → R))
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, 5
1	7	P → (Q → R)	→I⁽²⁾ 2, 6

Fitch

((P & Q) → R) ⊢ (P → (Q → R))
1(P & Q) → R
2P
3Q
4P & Q	&I 2, 3
5R	→E 1, 4
6Q → R	→I 3–5
7P → (Q → R)	→I 2–6

Special Dilemma (SpecD)

Lemmon

(P → Q), (¬P → Q) ⊢ Q
Assumption Set	Line #	Formula	Annotation
1	1.	P → Q	A
2	2.	¬P → Q	A
3	3.	¬Q	A for RAA
4	4.	P	A for ¬I
1, 4	5.	Q	→E 1, 4
1, 3	6.	¬P	¬I⁽⁴⁾ 3, 5
1, 2, 3	7.	Q	→E 2, 6
1, 2	8.	Q	IP⁽³⁾ 3, 7

Fitch

(P → Q), (¬P → Q) ⊢ Q
1P → Q
2¬P → Q
3¬Q
4P
5Q	→E 1, 4
6⊥	¬E 3, 5
7¬P	¬I 4–6
8Q	→E 2, 7
9⊥	¬E 3, 8
10Q	IP 3–9

Simple Dilemma (SD)

Lemmon

(P ∨ Q), (P → R), (Q → R) ⊢ R
Assumption Set	Line #	Formula	Annotation
1	1.	P ∨ Q	A
2	2.	P → R	A
3	3.	Q → R	A
4	4.	¬R	A for RAA
5	5.	P	A for ¬I
2, 5	6.	R	→E 2, 5
2, 4	7.	¬P	¬I⁽⁵⁾ 4, 6
1, 2, 4	8.	Q	∨E 1, 7
1, 2, 3, 4	9.	R	→E 3, 8
1, 2, 3	10.	R	RAA⁽⁴⁾ 4, 9

Fitch

1P ∨ Q
2 P → R
3Q → R
4P
5R	→E 2, 4
6Q
7R	→E 3, 6
8R	∨E 1, 4–5 6–7

Complex Dilemma (CD)

Lemmon

(P ∨ Q), (P → R), (Q → S) ⊢ (R ∨ S)
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⁽⁵⁾ 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, 11

Fitch

(P ∨ Q), (P → R), (Q → S) ⊢ (R ∨ S)
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

Ex Falso Quodlibet (EFQ)

Lemmon

P, ¬P ⊢ Q
Assumption Set	Line #	Formula	Annotation
1	1.	P	A
2	2.	¬P	A
1	3.	P ∨ Q	∨I 1
1, 2	4.	Q	∨E 2, 3

Fitch

P, ¬P ⊢ Q
1P
2¬P
3⊥	¬E 1, 2
4Q	X 3

Preface

Primitive Rules

Assumption (A)

Reiteration (R)

Conjunction Introduction (&I) / Conjunction (Conj)

Conjunction Elimination (&E)

Disjunction Introduction (∨I) / Addition (Add)

Disjunction Elimination (∨E) / Disjunctive Syllogism (DS)

Conditional Introduction (→I) / Conditional Proof (CP)

Conditional Elimination (→E) / Modus ponens (MP)

Biconditional Introduction (↔︎I)

Biconditional Elimination (↔︎E)

Negation Introduction (¬I)

Negation Elimination (¬E)

Reductio ad absurdum (RAA) / Indirect Proof (IP)

Derived Rule Proofs

Double Negation (DN)

Lemmon

Fitch

Redundancy (Re)

Lemmon

Fitch

Commutativity (Comm)

Lemmon

Fitch

Associativity (Assoc)

Lemmon

Fitch

Distribution (Dist)

Lemmon

Fitch

DeMorgan’s Theorem (DM)

Lemmon

Fitch

Def. of Conditional (→df)

Lemmon

Fitch

True Consequent (TC)

Lemmon

Fitch

False Antecedent (FA)

Lemmon

Fitch

Impossible Antecedent (IA)

Lemmon

Fitch

Hypothetical Syllogism (HS)

Lemmon

Fitch

Negated Conditional (¬→)

Lemmon

Fitch

Negated Biconditional (¬↔︎)

Lemmon

Fitch

Conditional Contraposition (Con)

Lemmon

Fitch

Biconditional Contraposition (BiCon)

Lemmon

Fitch

Modus Tollens (MT)

Lemmon

Fitch

Biconditional Ponens (BP)

Lemmon

Fitch

Biconditional Tollens (BT)

Lemmon

Fitch

Import (Imp)

Lemmon

Fitch

Export (Exp)

Lemmon

Fitch

Special Dilemma (SpecD)

Lemmon

Fitch

Simple Dilemma (SD)

Def. of Conditional (→^df)