Let φ, ψ, χ stand for well formed formulas, and let m, n, o stand for available line numbers in a derivation.

&I - Conjunction Introduction

Application: If φ is on line m, and ψ on line n, then you may infer ⌜(φ & ψ)⌝ by citing ⌜&I, m, n⌝ as justification.

Justification: ⌜(φ & ψ)⌝ is true if and only if φ is true and ψ is true. As such, if φ is true and ψ is true then ⌜(φ & ψ)⌝ is true.

Natural Language Example: If we have established that 'It is raining' and 'I have an umbrella', we can infer that 'It is raining and I have an umbrella'.

&E - Conjunction Elimination

Application: If ⌜(φ & ψ)⌝ is on line m, then you may either infer φ by citing ⌜&E, m⌝ as justification or infer ψ by citing ⌜&E, m⌝ as justification.

Justification: ⌜(φ & ψ)⌝ is true if and only if φ is true and ψ is true. As such, if ⌜(φ & ψ)⌝ is true, then φ is true and ψ is true individually.

Natural Language Example: If we know that 'It is raining and I have an umbrella', we can infer that 'It is raining' and also that 'I have an umbrella'.

∨I - Disjunction Introduction

Application: If φ is on line m, then you may either infer ⌜(φ ∨ ψ)⌝ by citing ⌜∨I, m⌝ as justification or infer ⌜(ψ ∨ φ)⌝ by citing ⌜∨I, m⌝ as justification.

Justification: ⌜(φ ∨ ψ)⌝ is true if either φ is true or ψ is true (or both). As such, if φ is true, then ⌜(φ ∨ ψ)⌝ and⌜(ψ ∨ φ)⌝ is true regardless of the truth value of ψ.

Natural Language Example: If we have established that 'It is raining', we can infer that 'It is raining or the sun is shining'.

∨E - Disjunction Elimination

Application: If ⌜(φ ∨ ψ)⌝ is on line m, and ~φ is on line n, then you may infer ψ by citing ⌜∨E, m, n⌝ AND if ⌜(φ ∨ ψ)⌝ is on line m, and ~ψ is on line n, then you may infer φ by citing ⌜∨E, m, n⌝ .

Justification: ⌜(φ ∨ ψ)⌝ is true if either φ is true or ψ is true (or both). If we know one of these disjuncts to be false, the other must be true in order for the initial disjunction to hold. Thinking of 'or' statements as claiming that at least one of the disjuncts is true helps with reasoning this out.

Natural Language Example: If we know that 'It is raining or it is sunny', and we establish that 'It is not raining', then we can infer that 'It is sunny'.

⟶I - Conditional Introduction

Application: If φ is assumed on line m, and upon making that assumption, you can infer ψ on some line n within the sub-proof opened on line m, then you may discharge the assumption on line m, close the sub-proof from lines m-n, and infer ⌜(φ ⟶ ψ)⌝ on some line m by citing ⌜⟶I, m-n⌝.

Justification: If we assume that φ is true and upon making that assumption we can establish that ψ is true, then we know that ⌜(φ ⟶ ψ)⌝ is true since ⌜(φ ⟶ ψ)⌝ is true if φ is true and ψ is true.

Natural Language Example: Suppose, I average at least an 86% across the remaining assignments [opening assumption]. In this case, I would end up with at least a 91% average for all the assignments in this class. In this case, I’d get at least an A- in this course. So, if I get at least an 86% average across the remaining assignments, then I will get at least an A- in this course [discharging the assumption].

⟶E - Conditional Elimination

Application: If ⌜(φ ⟶ ψ)⌝ is on line m and φ is on line n, then you may infer ψ by citing ⌜⟶E, m, n⌝ as justification.

Justification: ⌜(φ ⟶ ψ)⌝ is true if and only if either φ is false or ψ is true. As such, if ⌜(φ ⟶ ψ)⌝ is true and φ is true (i.e. φ is not false), then we know that ψ is true.

Natural Language Example: If we know that “If it is raining, then I have an umbrella” is true and we know that “it is raining” is true, then we know that “I have an umbrella” is true.

⟷I - Biconditional Introduction

Application: If ⌜(φ ⟶ ψ)⌝ is on line m and ⌜(ψ ⟶ φ)⌝ is on line n, then you may infer ⌜(φ ⟷ ψ)⌝ by citing ⌜⟷I, m, n⌝.

Justification: ⌜(φ ⟷ ψ)⌝ is logically equivalent to ⌜((φ ⟶ ψ) & (ψ ⟶ φ))⌝ and ⌜((φ ⟶ ψ) & (ψ ⟶ φ))⌝ follows from ⌜(φ ⟶ ψ)⌝ and ⌜(ψ ⟶ φ)⌝. As such, ⌜(φ ⟷ ψ)⌝ can be inferred from ⌜(φ ⟶ ψ)⌝ and ⌜(ψ ⟶ φ)⌝.

Natural Language Example: Consider the sentence “it is raining if and only if I have an umbrella”. This biconditional sentence is just a conjunction of the conditional sentences “it is raining if I have an umbrella” and “it is raining only if I have an umbrella”. Putting these conditionals into a more logically perspicuous form gives us: “if I have an umbrella, then it is raining” and “if it is raining, then I have an umbrella” (respectively). So, if we know that the sentences “if I have an umbrella, it is raining” and “if it is raining, then I have an umbrella” are both true, then we also know that the sentence “it is raining if and only if I have an umbrella” is true.

⟷E - Biconditional Elimination (v.1)

Application: If ⌜(φ⟷ ψ)⌝ is on line m and φ is on line n, then you may infer ψ by citing ⌜⟷E, m, n⌝. Also, if ⌜(φ⟷ ψ)⌝ is on line m and ψ is on line n, then you may infer φ by citing ⌜⟷E, m, n⌝.

Justification: ⌜(φ⟷ ψ)⌝ is true if and only if either both φ and ψ true or both φ and ψ false. Thus, if we know that ⌜(φ⟷ ψ)⌝ is true and we know that φ is true, then we also know that ψ is true. Similarly, if we know that ⌜(φ⟷ ψ)⌝ and we know that ψ is true, then we also know that φ is true.

Natural Language Example: If we know that “I have an umbrella if and only if it is raining” is true and we know that “I have an umbrella” is true, then we can infer that “it is raining” is true.

~I - Negation Introduction

Application: If φ is assumed on line m, and upon making that assumption, you infer ⌜ψ & ~ψ⌝ on line n within the sub-proof opened on line m, then you may discharge the assumption on line m, close the sub-proof from lines m-n, and infer ⌜~φ⌝ by citing ⌜~I, m-n⌝.

Justification: If we assume that φ is true and upon making that assumption we can infer a sentence ψ and its negation ⌜~ψ⌝, then we know that our assumption φ cannot be true since it is not possible for both a sentence and its negation to be true at the same time. Thus, we know that ⌜~φ⌝ is true.

Natural Language Example: Suppose that we assume that “there is a largest positive integer” is true. Let’s call this largest positive integer “k”. If it is true that k is the largest positive integer, then we know that “there is a positive integer larger than k” is false. However, there is a positive integer larger than k, namely, k+1. Since this is the case, then we also know that “there is a positive integer larger than k” is true. Given that upon making the assumption that “there is a largest positive integer” is true, we are able to infer that “there is some positive integer larger than k” is true and we are able to infer that “there is some positive integer larger than k” is false, then we know that “there is a largest positive integer” must be false since if it were true, it would lead to a contradiction.

~E - Negation Elimination

Application: If ⌜~φ⌝ is assumed on line m, and upon making that assumption, you infer ⌜ψ & ~ψ⌝ on line n within the sub-proof opened on line m, then you may discharge the assumption on line m, close the sub-proof from lines m-n, and infer φ by citing ⌜~E, m-n⌝.

Justification: If we assume that ⌜~φ⌝ is true and upon making that assumption we can infer a sentence ψ and its negation ⌜~ψ⌝, then we know that our assumption ⌜~φ⌝ cannot be true since it is not possible for both a sentence and its negation to be true at the same time. Thus, we know that φ is true.

Natural Language Example: Suppose that we assume that “it is not the case that either Jordan is married or Jordan is not married” is true. Since this is true, then “either Jordan is married or Jordan is not married” is false. But, “either Jordan is married or Jordan is not married” must be true since someone is either married or they aren’t—there aren’t any other options and everyone has to be one or the other. Thus, upon making our assumption, we are able to establish that “either Jordan is married or Jordan is not married” is true (given the reasoning in the previous sentence) and that “either Jordan is married or Jordan is not married” is false (given our assumption). Thus, we know “it is not the case that either Jordan is married or Jordan is not married” must be false (i.e., that “either Jordan is married or Jordan is not married” must be true) since if “it is not the case that either Jordan is married or Jordan is not married” were true, it would lead to a contradiction.