# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeMay 2nd 2017

I gave proof by contradiction a little Idea-section. This came about with writing an Idea-section at classical logic, which we are discussing in another thread here.

• CommentRowNumber2.
• CommentAuthorMatt Earnshaw
• CommentTimeMay 2nd 2017

I added a paragraph on the distinction between proof of negation and proof by contradiction which are sometimes confused.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeMay 2nd 2017
• (edited May 2nd 2017)

Matt, thanks for the addition! And for the pointer to Andrej’s material, that’s nice.

  [Bauer 2010]({#bauer})


but it needs to be

  [Bauer 2010](#bauer)


(without the curly brackets).

• CommentRowNumber4.
• CommentAuthorTodd_Trimble
• CommentTimeMay 2nd 2017

I added some more glosses to the observation Matt just made.

1. I was never happy with Andrej’s blog post, because I think that the issue is rather that mathematicians conflate proof by contradiction and refutation by contradiction (i.e., two different modes of reasoning by contradiction), and that Andrej himself was guilty of conflating the latter with proof of negation. In intuitionistic logic, all refutations are by contradiction, so there is no distinction between proof of negation and refutation by contradiction. However, one can imagine settings where there are also more “direct” forms of refutation (just as intuitionistic logic has more direct forms of proof), and in which a proof of a negation requires this stronger form of reasoning. This is apparently an old idea in logic (see Nelson’s “constructible falsity”), but it’s also especially natural if you think of linear logic and linear negation. For example, a refutation of an additive conjunction $A \& B$ must be either a refutation of $A$ or a refutation of $B$, which is why in general it is impossible to refute $A \& \neg A$ (just as it is impossible in general to prove $A \vee \neg A$ in intuitionistic logic).

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeMay 3rd 2017

I don’t think Andrej is conflating anything; I think it’s just a matter of terminology. What Andrej calls “proof of negation” is a rule of reasoning. It’s reasonable to argue that “proof of negation” is a confusing name for that rule because there can be other ways to prove a negation, but he isn’t conflating that rule itself with any other such ways.

I wouldn’t express the distinction as one of intutiionistic vs other logics, but rather that “refutation by contradiction” is the “basic” method by which we prove a negation (i.e. its introduction rule), just as proof by cases is the “basic” method by which we prove a disjunction, whereas in general — in any logic — there can be other ways to prove a negation. It just so happens that intuitionistic logic has a canonicity result saying that any proof of a negation can be beta-reduced to a refutation by contradiction.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeMay 3rd 2017

Could you state this with some formal notation added in the entry?

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeMay 3rd 2017

I moved proof of negation to refutation by contradiction and updated the texts.

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeMay 3rd 2017
• (edited May 3rd 2017)

Thanks, Mike! Where you mention $P \to \bot$ I have added pointers to “function type” and “false”.

At formal proof we should list these and other “methods of proof” (or what’s the right terminology?)

2. Thanks for adapting the terminology. On this:

I wouldn’t express the distinction as one of intutiionistic vs other logics, but rather that “refutation by contradiction” is the “basic” method by which we prove a negation (i.e. its introduction rule)

I would still distinguish “refutation by contradiction” from plain “refutation”, which need not necessarily proceed by contradiction. The “logic agnostic” introduction rule for negation simply says that “To prove $\neg A$, it suffices to refute $A$”. In intuitionistic logic, the only way to refute $A$ is to assume it is true and derive a contradiction (and you are allowed to reuse the hypothesis “$A true$” arbitrarily many times, just as in classical logic when proving $A$ by contradiction you are allowed to reuse the hypothesis “$A$ false” arbitrarily many times). However, some logics (typically “paraconsistent logics” such as linear logic or dual intuitionistic logic) require stronger forms of refutation.

It just so happens that intuitionistic logic has a canonicity result saying that any proof of a negation can be beta-reduced to a refutation by contradiction.

These logics often have stronger canonicity results for refutations, e.g., any refutation of a conjunction $A \& B$ reduces to either a refutation of $A$ or a refutation of $B$.

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTimeMay 3rd 2017
• (edited May 3rd 2017)

Is this what you’re after (added to the entry)?

Rarely one finds logics that have a basic notion of “refutation of $A$” that is distinct from (though generally closely related to) a “proof of $\neg A$”. In that case, refutation by contradiction is more precisely a method of refuting $A$ by deriving a contradiction from an assumption of $A$, which then requires an extra step to get to a proof of $\neg A$.

3. Yes, that looks good, thank you! I’ve also added a reference to the Nelson article.

Under the Curry-Howard correspondence, logics with a “refutation” judgment correspond to programming languages with a first-class notion of continuation, so this distinction amounts to whether continuations are always constructed by abstracting in values (e.g., a continuation accepting type $A$ is of the form $k = \lambda x.c$, where $c$ is a well-typed command assuming $x:A$), or whether they have a finer inductive structure (e.g., a continuation accepting type $A\&B$ is either of the form $k = fst;k_1$ for some $k_1$ accepting $A$, or $k = snd;k_2$ for some $k_2$ accepting $B$).

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeMay 3rd 2017

Do they have a categorical semantics?

4. Do they indeed!

There have been different attempts at understanding continuations from a categorical perspective, starting with Andrzej Filinski’s master’s thesis (“Declarative Continuations and Categorical Duality”), through Hayo Thielecke’s PhD thesis on the categorical structure of continuation passing style and Peter Selinger’s work on control categories and lambda-mu, as well as of course Paul-André’s long-running work on dialogue categories and chiralities. But continuations are a very rich subject in programming languages, and I think that finding the right categorical tools for studying their many aspects is still an important open problem/project.

• CommentRowNumber15.
• CommentAuthorTodd_Trimble
• CommentTimeJul 26th 2018

Redirect for “proof of negation”.