Craig DeLancey · A Concise Introduction to Logic, Ch. 5 · CC BY-SA 4.0
Natural deduction proves conclusions from premises using inference rules. Each rule introduces or eliminates a connective. Subproofs (temporary assumptions) let you prove conditionals and handle disjunctions.
Modus ponens and modus tollens
Modus ponens (→E): from P and P → Q, conclude Q. Modus tollens: from ¬Q and P → Q, conclude ¬P.
Scheme
; Modus ponens: if P is true and P -> Q, then Q
(define (modus-ponens p p-implies-q)
(if p (p-implies-q p) "cannot apply: P is false"))
; Modus tollens: if not Q and P -> Q, then not P
(define (modus-tollens not-q p-implies-q)
; If Q is false and P -> Q, then P must be false
(if not-q "not P""cannot apply: Q is true"))
; Example: P = "it rains", Q = "ground is wet"
(define (rain-implies-wet p) "ground is wet")
(display "Modus ponens: it rains, rain->wet: ")
(display (modus-ponens #t rain-implies-wet)) (newline)
(display "Modus tollens: ground not wet, rain->wet: ")
(display (modus-tollens #t rain-implies-wet))
Python
# Proof rules as functionsdef modus_ponens(p, p_implies_q):
"""From P and P->Q, derive Q"""assert p, "Cannot apply MP: P is false"return p_implies_q(p)
def modus_tollens(not_q, p_implies_q_holds):
"""From not-Q and P->Q, derive not-P"""assert not_q, "Cannot apply MT: Q is true"returnTrue# not P# Example
rain_implies_wet = lambda p: True# Q = wet
result = modus_ponens(True, rain_implies_wet)
print(f"Modus ponens: rain + (rain->wet) = wet: {result}")
print(f"Modus tollens: not wet + (rain->wet) = not rain: {modus_tollens(True, True)}")
Conjunction and disjunction rules
Conjunction introduction (∧I): from P and Q separately, conclude P ∧ Q. Conjunction elimination (∧E): from P ∧ Q, conclude P (or Q). Disjunction introduction (∨I): from P, conclude P ∨ Q for any Q. Disjunction elimination (∨E): from P ∨ Q, if P leads to R and Q leads to R, conclude R.
Scheme
; Conjunction intro: from P and Q, derive P and Q
(define (conj-intro p q) (cons p q))
; Conjunction elim: from P and Q, derive P (or Q)
(define (conj-elim-left pq) (car pq))
(define (conj-elim-right pq) (cdr pq))
; Disjunction intro: from P, derive P or Q
(define (disj-intro-left p) (list (quote or) p (quote anything)))
; Disjunction elim: from P or Q, P->R, Q->R, derive R
(define (disj-elim p-or-q p-gives-r q-gives-r)
(if (car p-or-q)
(p-gives-r (car p-or-q))
(q-gives-r (cdr p-or-q))))
; Demo
(define pq (conj-intro "it rains""it is cold"))
(display "Conj intro: ") (display pq) (newline)
(display "Conj elim left: ") (display (conj-elim-left pq)) (newline)
(display "Conj elim right: ") (display (conj-elim-right pq))
Conditional proof and RAA
Conditional proof (→I): assume P, derive Q inside a subproof, then discharge the assumption and conclude P → Q. Reductio ad absurdum (RAA): assume P, derive a contradiction, conclude ¬P.
Scheme
; Conditional proof: assume P, derive Q, conclude P -> Q; In code: a conditional proof IS a lambda; Prove: P -> (P or Q); Assume P, apply disjunction intro, get P or Q
(define proof-1
(lambda (p) (or p #f))) ; P -> (P or Q)
(display "P -> (P or Q) with P=T: ")
(display (proof-1 #t)) (newline)
(display "P -> (P or Q) with P=F: ")
(display (proof-1 #f)) (newline)
; RAA: assume P, derive contradiction, conclude not P; Prove: not (P and not P); Assume (P and not P), that is itself a contradiction
(define (raa assumption)
; If assumption leads to contradiction, negate it
(not assumption))
(display "RAA on (T and not T): ")
(display (raa (and#t (not#t)))) (newline)
(display "Conclusion: not (P and not P) = ")
(display (not (and#t (not#t))))
Inference rules reference
Rule
From
Conclude
Modus ponens (→E)
P, P → Q
Q
Modus tollens
¬Q, P → Q
¬P
Conj intro (∧I)
P, Q
P ∧ Q
Conj elim (∧E)
P ∧ Q
P (or Q)
Disj intro (∨I)
P
P ∨ Q
Disj elim (∨E)
P ∨ Q, P→R, Q→R
R
Cond proof (→I)
[assume P ... Q]
P → Q
RAA
[assume P ... ⊥]
¬P
Neighbors
🍞 Staton 2025 — Hoare logic rules are proof rules for programs
✎ Proofs Ch.2 — direct proof is natural deduction without the formalism