Review: every connective | Propositional logic

This lesson has no new material and no step checklists. Each exercise mixes connectives from the course: or, not, false, if-and-only-if, and one or two classical steps.

Read the outermost connective of the goal and of each hypothesis. An ∨ in the context is split with cases; an ∨ goal needs a choice. A negation in the goal is introduced; a negation in the context is applied. A contradiction in the context proves anything.

Reach for by_cases or Classical.byContradiction only when the constructive moves run out. The hints name a direction only; plan with sorry when a proof has several branches.

Worked example

-- A different mix, read one connective at a time:
example (A B : Prop) (h : A ∨ B) (hna : ¬A) : B := by
  cases h with                     -- an ∨ in the context: split it
  | inl ha => exact absurd ha hna  -- this case is impossible
  | inr hb => exact hb

One branch is closed by a contradiction, the other directly. The first exercise has the same idea with one more step.

Takeaway

Each connective has an introduction move and an elimination move. Reading which one the goal or a hypothesis needs is most of the work.

Exercise 1 of 4

Prove R from a disjunction, a negation and an implication.

Exercise.lean

1theorem exercise (P Q R : Prop) (h : P ∨ Q) (hnp : ¬P) (hqr : Q → R) : R := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

P Q R:Prop

h:P ∨ Q

hnp:¬P

hqr:Q → R

⊢R

ReadyLn 1, Col 1Lean 4

Draft saved in this browser

Stuck?

Worked example

Knowledge check