20
$\begingroup$

When constructing proofs using natural deduction what does it mean to say that an assumption or premise is discharged? In what circumstances would I want to, or need to, use such a mechanism?

The reason I'm asking this question is that many texts on logic use this term as understood by the reader and don't take the time to adequately explain the technical sense in which they are using it.

$\endgroup$
3
  • 5
    $\begingroup$ So very true! It's a weird term, and its everyday usage doesn't really correspond to its one in logic – so all the stranger that authors rarely take the time to explain it. $\endgroup$
    – Noldorin
    Apr 1, 2015 at 23:32
  • 3
    $\begingroup$ I know that 2009 was early days for MO, but still I wonder whether this question really belongs here. There isn't any research angle to it, is there, O logic people? $\endgroup$ Sep 25, 2018 at 7:12
  • 3
    $\begingroup$ @Gerry I think this is a perfectly fine question and that this forum is a good fit for it. $\endgroup$ Sep 28, 2020 at 1:09

4 Answers 4

8
$\begingroup$

As I understand it, to discharging a premise or assumption is the opposite of introducing it: you absorb it (for example) into the antecedent of an implication --- this means that it is no longer an assumption. A trivial example:

P 1. Assume P

__

P 2. From 1

__

P->P 3. Discharging 1

Thus I have concluded that P->P without any assumptions (iow |- P->P). If we didn't discharge the assumption, we would have P|-P

$\endgroup$
8
  • $\begingroup$ Thanks for this answer Apollo. One way of describing the purpose of discharging assumptions which I liked when I was reading up about this was that it's like introducing a temporary variable in programming - i.e. the scope is limited between the point where it's used in a rule and upwards to where it's discahrged; for example in inductive proofs the induction step requires you to assume P(n=k), showing P(n=k+1) and in doing so discharging P(n=k). (Btw, it's a bit nit-picky I know, but you can only discharge an assumption, not a premise (except when an assumption actually becomes an premise).) $\endgroup$ Nov 30, 2009 at 16:00
  • 9
    $\begingroup$ @axiomsofchoice It's more like the argument to a function. If you write a block of code that assumes you have something of type A and ends by returning something of type B then you can discharge the assumption by making the block into a function that takes an argument of type A and returns a result of type B. It's not just 'like' - the correspondence can be made precise with Curry-Howard. $\endgroup$
    – Dan Piponi
    Apr 12, 2010 at 17:03
  • 1
    $\begingroup$ @DanPiponi's comment is far superior to any of the "answers" on this page. $\endgroup$ Jan 5, 2016 at 17:22
  • $\begingroup$ @axiomsofchoice what's the difference between an assumption and a premise? $\endgroup$
    – ziggurism
    Mar 14, 2018 at 16:15
  • 2
    $\begingroup$ @PaulTaylor doesn't mention his book Practical Foundations of Mathematics, but it explains very well what is meant, and his "proof boxes" clarify the matter greatly. If one needs to prove p --> q in the course of an argument , then temporarily assume p and derive q from that assumption (p itself needn't be an assumption in the statement of the original theorem.) Once p --> q has been established, p isn't needed anymore as a temporary assumption, and so is "discharged". A proof box sequesters the mini-argument, opening with the temporary assumption and then closing by discharging it. $\endgroup$
    – Todd Trimble
    Sep 28, 2020 at 1:11
11
$\begingroup$

Apollo is correct. A slightly more technical way of putting it is that "discharging" is an application of a theorem of metalogic called the deduction theorem:

$$ T,P \vdash Q \quad\text{iff}\quad T\vdash P \rightarrow Q $$

The single turnstile symbol "$\vdash$" stands for the syntactic consequences relation. The deduction theorem basically says "Q is derivable from T and P iff if P then Q is derivable from T alone". T may, of course, be an empty class of statements, in which case $P\rightarrow Q$ is tautologous.

Many systems of natural deduction introduce conditional proof as a primitive rule, but there are simpler systems that are just as powerful in which the deduction theorem is proved and conditional proof is a derived rule supported by the deduction theorem. The deduction theorem is important because it shows you don't need conditional proof as a primitive rule, and this makes the proof of other theorems in metalogic a whole lot simpler. Basically, if you have as few rules as possible it gives you fewer cases to check. For practical purposes, however, it's a whole lot easier to teach and use a system that introduces lots and lots of primitive rules as opposed to one that uses as few rules as possible.

Mathematicians use conditional proof all the time, by the way. For example, in a proof of Q by cases you get conditionals P1->Q, P2->Q, etc. by for each case supposing the antecedents, deriving Q from the supposition, then "discharging" the supposition. Then you show the disjunction of the antecedents is exhaustive.

$\endgroup$
1
  • $\begingroup$ I think what confuses me the most right now is that discharging seems to place antecedents on the left of the proof line (|-) BUT that would imply P has been proved (or is an axiom), but we do NOT know that. Thus, it just seems very strange to me. How can we allow that without actually knowing if P is has been actually proved? $\endgroup$ Jan 29, 2020 at 17:48
7
$\begingroup$

Note that the standard natural deduction systems also have a premise introduced and then discharged in the negation-introduction rule.

For systems that explicitly track sub-proofs within the larger proof, a "discharge" step is just the end of a subproof, where you come to a conclusion that no longer depends on the additional assumption used in starting the subproof.

$\endgroup$
5
$\begingroup$

In the spirit of Kenny's observation, note also that we can formulate classical logic using a Peircian inference rule (equivalent to the usual theory in the presence of ex falso quodlibet) which clearly modifies the inferential properties of implication:

${{{A \rightarrow B} \atop \vdots} \atop A } \over A$

but in an odd way: is it an introduction rule? But there is no logical structure in the conclusion. Is it an elimination rule? But the implication above the rule appears among the assumptions to the subderivation, not the conclusion. It seems to be something like an implication elimination-eliminating rule, a kind of structurally double-negative introduction rule, where you can introduce logical structure by discharging it in the assumptions.

All the rules for adding classical-strength inference to the usual, well-behaved intuitionistic natural deduction involve inference rules that are eccentric in some way or another. Parigot's lambda-mu calculus shows how the fundamental structural glue of (through a classical Curry-Howard correspondence) natural deduction can be tweaked to make it as good a fit for classical logic as the sequent calculus.

In chapter 3 of my DPhil dissertation (Stewart 2000), I give what I think is a successful reconstruction of Prawitz's inversion principle for the lambda-mu-based natural deduction, and show how this provides the basis for something we might call "classical constructivism", where the principle of the excluded middle is admitted as having constructive content by being a principle that provides a constructive, dialectical mediation between proofs and refutations.

Ref. Stewart (2000) On the formulae-as-types correspondence for classical logic.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.