Skip to content
Free public beta until December 4, 2026: every course is open, no card needed. After that, the first chapter of each course stays free and full access is a one-time $39 ($19 for up to 100 founding members chosen for helpful feedback). Your progress is kept. How the beta works

discharge

Closing a subproof, so its assumption is no longer in force.

An assumption is discharged when the subproof it begins is closed by a rule such as →I, ¬I, ∨E, ↔I, or IP. After discharge, the result no longer depends on that assumption, and the subproof's lines are no longer available.

Examples

  • →I discharges the assumption P when it concludes P → Q.

See also

subproof assumption (in a proof)
Read the full section →