6. PROPOSITIONAL CALCULUS
Outline
James Fieser, UT Martin
updated 10/29/2025
Propositional calculus builds upon propositional logic, and it involves a collection of inference rules that are used to produce proofs of valid argument forms. This chapter discusses four groups of inference rules. Many of these rules go by two separate names, following two separate conventions. First, there are traditional rule names, some of which were devised by medieval logicians (e.g., modus ponens, modus tollens), and others by nineteenth and twentieth century logicians (e.g., double negation, simplification). Second, there is an organizational system devised by logician Gerhard Gentzen in the 1930s, which devised ten rules that either eliminate a logical connective or introduce it (e.g., conditional elimination, conditional introduction). Introductory logic books lean towards the traditional names, whereas formal logic books in mathematics and theoretical computer science lean towards Gentzen names. Many logic books, though, mention both naming conventions, which we will do here.
A. EIGHT BASIC RULES OF INFERENCE (non-hypothetical)
1. Negation Elimination (~E – version of double negation DN)
~~p
˫ p
Example:
1. If it is not the case that Bob is not here
2. Therefore, Bob is here
2. Conditional Elimination (→E – modus ponens MP)
p → q
p
˫ q
Example:
1. If Bob is here, then we are in big trouble
2. Bob is here
3. Therefore we are in big trouble
Meaning of “modus ponens”: the mode that affirms by affirming.
3. Conjunction Introduction (&I – conjunction CONJ)
p
q
˫ p & q
Example:
1. Bob is here
2. Joe is here
3. Therefore, Bob is here and Joe is here
4. Conjunction Elimination (&E – simplification SIMP)
p & q
˫ p
Example:
1. Bob is here and Joe is here
2. Therefore, Bob is here
5. Disjunction Introduction (vI – addition ADD)
p
˫ p v q
Example:
1. Bob is here
2. Therefore, Bob is here or my head turned into an octopus
6. Disjunction Elimination (vE – version of constructive dilemma CD)
p v q
p → r
q → r
˫ r
Example:
1. The U.S. will launch a nuke or Russia will launch a nuke
2. If the U.S. launches a nuke, then everyone on the planet will die
3. If Russia launches a nuke, then everyone on the planet will die
4. Therefore, everyone on the planet will die
7. Biconditional Introduction (↔I – version of material equivalence ME)
p → q
q → p
˫ p ↔ q
Example:
1. If I go to the movies with you, then you will pay for my ticket
2. If you pay for my ticket, then I will go to the movies with you
3. Therefore, I will go to the movies with you if and only if you pay for my ticket
8. Biconditional Elimination (↔E – version of material equivalence ME)
p ↔ q
˫ p → q
or
˫ q → p
Example:
1. Jill is here if and only if Jill’s ugly boyfriend is here
2. Therefore, if Jill is here, then her ugly boyfriend is here
3. Therefore, if Jill’s ugly boyfriend is here, then Jill is here
Example of a proof using the basic rules of inference
1. ~~P [assumption]
2. P ↔ Q [assumption]
3. P → Q [2, ↔E (ME)]
4. P [1, ~E (DN)]
5. Q [3, 4, →E (MP)]
6. R v Q [5, vI (ADD)]
7. ˫ P & (R v Q) [4, 6, &I (CONJ)]
B. DERIVED RULES
1. Modus Tollens (MT)
p → q
~q
˫ ~P
Example:
1. If Bob is here, then we are in for big trouble
2. It is not the case that we are in for big trouble
3. Therefore, it is not the case that Bob is here
Meaning of “modus tollens”: the mode that denies by denying.
2. Hypothetical Syllogism (HS)
p → q
q → r
˫ p → r
Example:
1. If you look back, then you will turn into a pillar of salt
2. If you turn into a pillar of salt, then deer will lick your face for eternity
3. Therefore, if you look back, then deer will lick your face for eternity
Meaning of “hypothetical syllogism”: an argument consisting of hypothetical (if-then) statements.
4. Disjunctive Syllogism (DS)
p v q
~p
˫ q
Example:
1. We will have hot dogs for dinner or we will have hamburgers for dinner
2. It is not the case that we will have hot dogs for dinner
3. Therefore, we will have hamburgers for dinner
Meaning of “disjunctive syllogism”: an argument that involves a disjunction.
5. Absorption (ABS)
p → q
˫ p → (p & q)
Example:
1. If Bob is here, then we are in for big trouble
2. Therefore, if Bob is here, then Bob is here and we are in for big trouble
Meaning of “absorption”: an argument where one part of a formula can be reattached (absorbed) inside another without changing truth value because it’s already entailed by it.
6. Constructive Dilemma (CD)
p v q
p → r
q → s
˫ r v s
Example:
1. Mom will come home first tonight or dad will come home first tonight
2. If mom comes home first tonight, then we will have hot dogs for dinner
3. If dad comes home first tonight, then we will have tofu for dinner
4. Therefore, we will have hot dogs for dinner or we will have tofu for dinner
Meaning of “Constructive Dilemma”: a two-pronged argument that constructively produces an affirmative disjunction in the conclusion.
6. Repeat (RE)
p
˫ p
Example:
1. I’m not going to say this again
2. Therefore, I’m not going to say this again
7. Contradiction (CON)
p
~p
˫ Any wff
Example:
1. Bob is here
2. It is not the case that Bob is here
3. Therefore, my head turned into an octopus
Explanation: if you assert two propositions that contradict each other, then the world of logic falls apart, and anything goes.
Proof (where Z is any arbitrary proposition)
1. P [assumption]
2. ~P [assumption]
3. P v Z [1, vI (ADD)]
4. ˫ Z [3, 2 DS]
8. Theorem Introduction
Theorem Introduction (TI):
Introduce any tautology,
Example: ~(P & ~P)
It is not the case that (Bob is here and Bob is not here)
Meaning of “theorem introduction”: Theorems are wffs that are tautologies (i.e., whose instances are logically necessary), and any theorem can be inserted into a line of a proof. They are provable without making any nonhypothetical assumptions. Biconditional equivalences are tautologies, and thus theorems. The symbol “˫” designates a theorem.
Examples:
˫ P → P
˫ P v ~P
˫ ~(P & ~P)
˫ P ↔ ~~P
˫ P → (P v Q)
˫ P → [(P → Q) → Q]
˫ (P → Q) ↔ (~Q → ~P)
˫ (P v Q) ↔ (Q v P)
C. EQUIVALENCES (also called rules of replacement)
These rules allow you to replace one wff with another that is logically equivalent to it. Unlike the previous rules, these apply to both complete premises and also sub-wffs within premises. The four-dot "::" symbol used below in these equivalence rules is another way of representing a biconditional relation, which so far we have been symbolizing with the double arrow "↔". The four-dot symbol is used here only because it makes the rules easier to understand upon first glance, in contrast with using the double arrow symbol which can be confusing. It helps to think of the :: sign (and also the ↔ sign) as an equal sign, where the wff one side of the :: is logically equivalent to the wff on the other side. The logical equivalence of the two wffs in question can be demonstrated on a truth table, where the truth assignment of the one wff is exactly the same as the truth assignment of the other wff. Each of these rules serves a particular strategy or purpose within logical proofs, as indicated beneath each of the following rules.
1. De Morgan’s Law (DM)
Version 1: ~(p & q) :: (~p v ~q)
Version 2: ~(p v q) :: (~p & ~q)
Purpose: Converts & into v (and vice versa).
Meaning of De Morgan’s law: the name is historically-based, but not meaningful in itself. Treat the name as a mere label, not a concept.
2. Commutation (COM)
Version 1: (p v q) :: (q v p)
Version 2: (p & q) :: (q & p)
Purpose: Allows reversing order of disjuncts or conjunct.
Meaning of “commutation”: comes from the notion of “commutativity” in algebra which means that the order doesn’t matter.
3. Association (ASSOC)
Version 1: [p v (q v r)] :: [(p v q) v r]
Version 2: [p & (q & r)] :: [(p & q) & r]
Purpose: Allows moving parentheses, regrouping the larger contents
Meaning of “association”: comes from the notion of “associative property” in algebra, where items propositions can be regrouped (associated) in different ways around the same connective without changing truth value.
4. Distribution (DIST)
Version 1: [p & (q v r)] :: [(p & q) v (p & r)]
Version 2: [p v (q & r)] :: [(p v q) & (p v r)]
Purpose: Allows pairing the first conjunct (or disjunct) with each part of the second conjunct (or disjunct).
Meaning of “distribution”: comes from the notion of “distributive property” in algebra, where one connective can be spread (distributed) across another so that it applies to each part inside parentheses without changing truth value.
5. Double Negation (DN)
p :: ~~p
Purpose: Introduces or eliminates ~~
6. Transposition (TRANS)
(p → q) :: (~q→~p)
Purpose: Modus tollens in one line.
Meaning of “transposition”: the positions of the antecedent and consequent in a conditional are switched (transposed) while each is negated, without changing truth value.
7. Material implication (MI)
(p → q) :: (~p v q)
Purpose: Converts → into v.
Meaning of “material implication: the name is historically-based, but not meaningful in itself. Treat the name as a mere label, not a concept.
8. Material Equivalence (ME)
Version 1: (p ↔ q) :: [(p & q ) v (~p & ~q)]
Version 2: (p ↔ q) :: [(p → q ) & (q → p)]
Purpose: Converts ↔ into other logical connectives.
Meaning of “material equivalence: the name is historically-based, but not meaningful in itself. Treat the name as a mere label, not a concept.
9. Exportation (EXP)
[(p & q) → r] :: [p → (q → r)]
Purpose: Converts & to → (and vice versa) in part of a wff.
Meaning of “exportation”: a compound conditional with a conjunction in its antecedent can be re-expressed (exported) as a nested conditional, and vice versa.
10. Tautology (TAUT)
Version 1: p :: (p & p)
Version 2: p :: (p v p)
Purpose: Creates an & or v from a single wff
D. HYPOTHETICAL RULES (rules using assumptions)
1. Conditional Introduction (→I – conditional proof CP)
The rule:
Assume p
Get q
˫ p → q (yellow designates the main conditional operator in conclusion)
Purpose: use as a shortcut in a proof when you need to conclude a conditional statement (the conclusion of all conditional proofs have a conditional as its main operator). The premises with the vertical lines, designate something like a quarantined work area where you are solving the problem based on your assumption.
Example 1:
1. P / ˫ P → P
2. | P [Hypothesis for CP (→I)]
3. | P [2 Repeat]
4. ˫ P → P [2–3 CP (→I)]
Explanation: We are given P and asked to conclude “P→P”. In premise 2, we now hypothesize the antecedent (“P”) to the conditional we want to prove (“P→P”). The hypothesis in premise 2, then, begins the quarantined area. In premise 3 (also in the quarantines area) we deduce “P” from premise 2 using the rule repeat. The conclusion in 4 (“P → P”) is a summary of what we did in the quarantined area. That is, we hypothesized P, and from that inferred P, which we notate P → P.
Tips: (1) in easy examples like this, as usual, bring down the conclusion in statement 1 to the conclusion in statement 4; (2) place the conclusion's antecedent into the first statement in the quarantined area (e.g., "P "); (3) place the conclusion's consequent in the last statement of the quarantined area (e.g., "P").
Example 2:
1. P / ˫ (P → Q) → Q
2. | P → Q [Hypothesis for CP (→I)]
3. | Q [2, 1 MP (→E)]
4. ˫ (P → Q) → Q [2-3 CP (→I)]
Explanation: you are given just "P", and asked to conclude from this "(P → Q) → Q". Conjunction Introduction (conditional proof), provides a short cut for doing this. Begin by assuming as a hypothesis that someone like Santa Claus magically gave you the antecedent of your conclusion (i.e., "P→Q"), which you then write down in your quarantine area on statement two. Using this assumption, along with what you are given in premise 1 (i.e., P), you can use modus ponens to conclude Q, which you write down in your quarantine area on statement three. The conclusion, then, is essentially a summary of what you just did in your quarantine area: by assuming (P → Q), you were able to infer Q. Written out formally in your conclusion as "(P → Q) → Q", the yellow conditional means that you inferred the consequent "Q" from the assumed antecedent (P → Q).
Example 3:
1. P
2. Q / ˫ P → (P & Q)
3. | P [Hypothesis for CP (→I)]
4. | P & Q [2, 3 &I (CONJ)]
5. ˫ P → (P & Q) [3–4 CP (→I)]
Explanation: We are given P and Q and asked to conclude “P → (P & Q).” To do this, we begin by hypothesizing the antecedent of the conditional we want to prove (“P”) in line 2, which starts the quarantined area. Using conjunction introduction (CONJ), we then combine P (line 3) and Q (line 2) get P & Q in line 4. The conclusion “P → (P & Q)” in line 5 summarizes what we did in the quarantined area: we assumed P and from that were able to infer P & Q. Thus, the conditional expresses the relationship that if P is true, then P & Q follows.
2. Negation Introduction (~I – indirect proof IP)
The rule:
Assume p
Get q & ~q
˫ ~p
Purpose: this is a quick way of proving a conclusion by (1) assuming the conclusion’s opposite, then (2) drawing an explicit contradiction from that assumption. An explicit contradiction (or an “absurdity”) is “p & ~p”. This rule is also called reductio ad absurdum (reduction to absurdity).
Example 1:
1. (P & Q) v P / ˫ P
2. | ~P [Hypothesis for IP (~I)]
3. | P & Q [1, 2 DS]
4. | P [3 SIMP (&E)]
5. | P & ~ P [4, 2 CONJ (&I)]
6. ˫ P [2-5 IP (~I)]
Explanation: We are asked conclude P. To use Negation Introduction, we begin by assuming the opposite of what we want to prove, namely “~P.” This assumption starts the quarantined area. Inside that area, we use Disjunctive Syllogism (DS) on line 1 and our assumption “~P” to infer “P & Q.” Next, by Simplification (&E), we take P out of that conjunction. At this point, inside our quarantined area, we have both P (line 4) and ~P (line 2), which together form an explicit contradiction (P & ~P). That contradiction allows us to discharge our assumption and conclude the negation of our hypothesis’s negation, namely P. In plain language, we temporarily supposed that P was false, but that led us to a contradiction (both P and ~P). Since assuming ~P results in absurdity, ~P must be false, and so P must be true.
Example 2 (without using modus tollens):
1. P → Q
2. ~Q / ˫ ~P
3. | P [Hypothesis for IP (~I)]
4. | Q [1, 3 →E (MP)]
5. | Q & ~Q [4, 2 &I (CONJ)]
6. ˫ ~P [3–5 IP (~I)]
Explanation: We are asked to conclude “~P.” To use Negation Introduction (indirect proof), we assume the opposite of what we want to prove (i.e., “P”), which starts the quarantined area (line 3). From that assumption together with line 1, Modus Ponens (→E) gives us “Q” (line 4). Now we have both “Q” (line 4) and “~Q” (line 2), which we can combine with conjunction introduction (CONJ) as an explicit contradiction “Q & ~Q” (line 5). Since assuming “P” led to a contradiction, we exit the quarantined area and conclude “~P” by negation introduction. (line 6). In short: supposing P forces Q, but Q conflicts with ~Q; so P must be false.
Example 3
1. ~(P & Q)
2. P / ˫ ~Q
3. | Q [Hypothesis for IP (~I)]
4. | P & Q [2, 3 &I (CONJ)]
5. | (P & Q) & ~(P & Q) [1, 4 &I (CONJ)]
6. ˫ ~Q [3–5 IP (~I)]
Explanation: We want “~Q” as indicated in the conclusion. So, we assume the opposite (“Q”) to start the quarantined area. With P (line 2) and Q (line 3) we build “P & Q” (line 4) through conjunction introduction (CONJ). That clashes with line 1 (“~(P & Q)”), giving an explicit contradiction. Since assuming Q led to absurdity, we conclude ~Q.
3. Guidelines for hypothetical rules
1. Each hypothesis introduced into a proof begins a new vertical line (initiating the quarantined area).
2. No occurrence of a formula to the right of a vertical line may be cited in any rule applied after that line has ended (at the close of the quarantined area).
3. If two or more hypotheses are in effect simultaneously, then the order in which they are discharged must be the reverse of the order in which they are introduced.
4. A proof is not complete until all hypotheses have been discharged.
4. Proof Strategies
1. When conclusion is an atomic formula: If no other strategy is immediately apparent, hypothesize the negation of the conclusion for ~I. If this is successful, then the conclusion can be obtained after the ~I by ~E.
2. When conclusion is a negated formula: Hypothesize the conclusion without its negation sign for ~I. If a contradiction follows, the conclusion can be obtained by ~I.
3. When conclusion is a conjunction: Prove each of the conjuncts separately and then conjoin them with &I.
4. When conclusion is a disjunction: Sometimes (though not often) a disjunctive conclusion can be proved directly simply by proving one of its disjuncts and applying vI. Otherwise, hypothesize the negation of the conclusion and try ~I.
5. When conclusion is a conditional: Hypothesize its antecedent and derive its consequent by →I.
6. When conclusion is a biconditional: Use →I twice to prove the two conditionals needed to obtain the conclusion by ↔I.
E. REFUTATION TREES (bonus material, not included on test)
General
Refutation trees are alternatives to truth tables for demonstrating the validity of arguments; they are shorter but conceptionally more challenging
Main intuition: if an argument is valid, and you negate its conclusion, then contradictions should arise everywhere. Similarly, if an argument is invalid when you negate its conclusion, then you will find at least one non-contradictory option
Easy example: p v q, ~ p ˫ q (valid DS)
“p v q, ~ p ˫ ~ q” (negated conclusion)
p in premise 1 is contradicted by ~p in premise 2, and q in premise 1 is contradicted by ~q in the conclusion
All options in the premises are contradicted when negating the conclusion, thus the original argument is valid
Easy example: p v q, p ˫ ~q (invalid DS)
“p v q, p ˫ ~~ q” (negated conclusion)
p in premise 1 is not contradicted by p in premise 2, and q in premise 1 is not contradicted by ~~q in the conclusion
All options in the premises are un-contradicted when negating the conclusion, thus the original argument is invalid
Closed and open paths
Closed path: one which ends in a contradiction and is designated with an X
Open path: one that ends with a consistency and is designated with an !
Basic point: if all paths are closed (i.e., contradictory), then the original version is valid; if any path remains open (i.e., consistency), then the original version is invalid
Basic rules
Begin working on non-branching paths
All branching paths must be converted into either disjunctions or conjunctions, and each path must terminate in a contradiction for the argument to be valid
Conditional: convert to disjunction using “material implication” rule (p → q) ↔ (~p v q)
Biconditional: convert to two conjunction using the “material equivalence” rule (p ↔ q) ↔ [(p & q) v (~p & ~q)]
Negated conjunction: convert to disjunction using “De Morgan” rule ~(p & q) ↔ (~p v ~q)
Negated disjunct: convert to conjunction using “De Morgan” rule ~(p v q) ↔ (~p & ~q)
Negated conditional: convert to conjunction using mystery rule ~(p → q) ↔ (p & ~q)
Negated biconditional: convert to two conjunctions using mystery rule ~(p ↔ q) ↔ [(p & ~q) v (~p & q)]
Explanation as appears in John Nolt's book Logic
Main description
Refutation trees provide a more efficient algorithm than truth tables for determining an argument’s validity
A refutation tree is an analysis in which a list of statements is broken down into sentence letters or their negations, which represent ways in which the members of the original list may be true. Since the ways in which a statement may be true depend on the logical operators it contains, formulas containing different logical operators are broken down differently.
All wffs containing logical operators fall into one of the following ten categories:
Negation — Negated negation
Conjunction — Negated conjunction
Disjunction — Negated disjunction
Conditional — Negated conditional
Biconditional — Negated biconditional
Steps
Construct a list consisting of its premises and the negation of its conclusion.
Break down the wffs on the list into sentence letters or their negations.
If we find any assignment of truth and falsity to sentence letters which makes all the wffs on the list true, then under that assignment the premises of the form are true while its conclusion is false. Thus we have refuted the argument form; it is invalid.
If the search turns up no assignment of truth and falsity to sentence letters which makes all the wffs on the list true, then our attempted refutation has failed; the form is valid.
Refutation Tree Rules
Negation (~): If an open path contains both a formula and its negation, place an “x” at the bottom of the path.
Negated Negation(~~): If an open path contains an unchecked wff of the form ~~p, check it and write p at the bottom of every open path that contains this newly checked wff.
Conjunction (&): If an open path contains an unchecked wff of the form p&q, check it and write p and q at the bottom of every open path that contains this newly checked wff.
Negated Conjunction (~&): If an open path contains an unchecked wff of the form ~(p&q), check it and split the bottom of each open path containing this newly checked wff into two branches, at the end of the first of which write ~p and at the end of the second of which write ~q.
Disjunction (v): If an open path contains an unchecked wff of the form pVq, check it and split the bottom of each open path containing this newly checked wff into two branches, at the end of the first of which write p and at the end of the second of which write q.
Negated Disjunction (~v): If an open path contains an unchecked wff of the form ~(p v q), check it and write both ~p and ~q at the bottom of every open path that contains this newly checked wff.
Conditional (→): If an open path contains an unchecked wff of the form p→q, check it and split the bottom of each open path containing this newly checked wff into two branches, at the end of the first of which write ~p and at the end of the second of which write q.
Negated Conditional ~(→): If an open path contains an unchecked wff of the form ~(p→q), check it and write both p and ~q at the bottom of every open path that contains this newly checked wff.
Biconditional (↔): If an open path contains an unchecked wff of the form p↔q, check it and split the bottom of each open path containing this newly checked wff into two branches, at the end of the first of which write both p and q, and at the end of the second of which write both ~p and ~q.
Negated Biconditional (~↔): If an open path contains an unchecked wff of the form ~(p↔q), check it and split the bottom of each open path containing this newly checked wff into two branches, at the end of the first of which write both p and ~q, and at the end of the second of which write both ~p and q.
Refutation Tree examples for conjunction
Instructions: Complete the refutation trees below for conjunction. At the end of each path, indicate that the path is closed with an X or open with an !,. Write “valid” or “invalid” in the final line. In brackets, explain your work for each step.
(1) Example
1. A & B / ˫ A
2. ~A [negated conclusion]
Path 1
3. A [from 1]
4. B [from 1]
x [2, 3 conflict]
Valid [path closed]
(2) Construct 1 path.
1. A & B
2. ~A / ˫ B
3. ~ B [negated conclusion]
Path 1
4. A [from 1]
5. B [from 1]
x [2, 4 conflict, 3, 5 conflict]
Valid [path closed]
(3) Construct 1 path.
1. A & B
2. A / ˫ ~B
3. B [negated conclusion]
Path 1
4. A [from 1]
5. B [from 1]
! [2, 4 consistency, 3, 5 consistency]
Invalid [path open]
Refutation Tree examples for disjunction
Instructions: Complete the refutation trees below for disjunction.
(1) Example
1. A v B
2. ~A / ˫ B
3. ~B [negated conclusion]
Path 1
4. A [from 1]
x [2, 4 conflict]
Path 2
5. B [from 1]
x [3, 5 conflict]
Valid [paths 1 and 2 closed]
(2) Construct two paths.
1. A v B
2. A / ˫ ~B
3. B [negated conclusion]
Path 1
4. A [from 1]
! [2, 4 consistency]
Path 2
5. B [from 1]
! [3, 5 consistency]
Invalid [paths 1 and 2 open]
Refutation Tree examples for conditionals
Instructions: Complete the refutation trees below for conditional.
(1) Example
1. A → B
2. A / ˫ B
3. ~B [negated conclusion]
4. ~A v B [1, MI]
Path 1
5. ~A [from 4]
x [2, 5 conflict]
Path 2
6. B [from 4]
x [3, 6 conflict]
Valid [paths 1 and 2 closed]
(2) Construct two paths.
1. A → B
2. ~B / ˫ ~A
3. ~A [negated conclusion]
4. ~A v B [1, MI]
Path 1
5. ~A [from 4]
! [3, 5 consistency]
Path 2
6. B [from 4]
! [2, 6 consistency]
Invalid [paths 1 and 2 open]
(3) Construct three paths.
1. A → B
2. B → C
3. A / ˫ C
3. ~C [negated conclusion]
4. ~A v B [1, MI]
5. ~B v C [2, MI]
Path 1
6. ~A [from 4]
x [3, 6 conflict]
Path 2
7. B [from 4]
x [5, 7 conflict]
Path 3
8. C [from 5]
X [3, 8 conflict]
Valid [paths 1, 2 and 3 closed]
(4) Construct three paths.
1. H → I
2. I → J
3. ~H / ˫ J
3. ~J [negated conclusion]
4. ~H v I [1, MI]
5. ~I v J [2, MI]
Path 1
6. ~H [from 4]
! [3, 6 consistency]
Path 2
7. I [from 4]
x [5, 7 conflict]
Path 3
8. J [from 5]
x [3, 8 conflict]
Invalid [path 1 open]