Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
I added a paragraph on the distinction between proof of negation and proof by contradiction which are sometimes confused.
Matt, thanks for the addition! And for the pointer to Andrej’s material, that’s nice.
Notice that I fixed your anchor-link: you had
[Bauer 2010]({#bauer})
but it needs to be
[Bauer 2010](#bauer)
(without the curly brackets).
I added some more glosses to the observation Matt just made.
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 must be either a refutation of or a refutation of , which is why in general it is impossible to refute (just as it is impossible in general to prove in intuitionistic logic).
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.
Could you state this with some formal notation added in the entry?
I moved proof of negation to refutation by contradiction and updated the texts.
Thanks, Mike! Where you mention 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?)
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 , it suffices to refute ”. In intuitionistic logic, the only way to refute is to assume it is true and derive a contradiction (and you are allowed to reuse the hypothesis “” arbitrarily many times, just as in classical logic when proving by contradiction you are allowed to reuse the hypothesis “ 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 reduces to either a refutation of or a refutation of .
Is this what you’re after (added to the entry)?
Rarely one finds logics that have a basic notion of “refutation of ” that is distinct from (though generally closely related to) a “proof of ”. In that case, refutation by contradiction is more precisely a method of refuting by deriving a contradiction from an assumption of , which then requires an extra step to get to a proof of .
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 is of the form , where is a well-typed command assuming ), or whether they have a finer inductive structure (e.g., a continuation accepting type is either of the form for some accepting , or for some accepting ).
Do they have a categorical semantics?
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.
1 to 15 of 15