5 ms·

Why do you say that proof-by-contradiction is a "half-assed academic hack"? In particular, if someone isn't already an intuitionist or constructivist, what rea

Why do you say that proof-by-contradiction is a "half-assed academic hack"? In particular, if someone isn't already an intuitionist or constructivist, what reason can you give that would be valid in their frame of reference?

johnnyjeans 2y ago
Because they explain nothing and aren't useful for building new insights. It's not a direct verification of the existence or lack-of-existence of a thing with given properties. It relies on rules lawyering in a very specific logic to say something with basically no substance. Allowing it causes more problems for automated proofs than they solve, so long as your domain only deals with finites (which all real-world domains do exclusively.) They're also generally much easier to create than constructive proofs, which makes them a convenient go-to for lazy academics.
- ndriscoll 2y ago
  Proof by contradiction is fine for lack-of-existence (indeed, ¬P is defined in type theory as P -> false). I think also if I got my types right, you can do def eliminateTripleNot(f: ¬¬¬P): ¬P = {p: P => f({g: ¬P => g(p)})} For a constructive proof of ¬¬¬P => ¬P? So it's really just ¬¬P => P that causes trouble. It's not clear to me though whether LEM is actually okay in the "fast and loose reasoning is morally correct" sense (i.e. if it's okay as long as you don't cheat and do something like use a non-terminating loop or exception to make your ¬¬P) though? Are there cases where you didn't "obviously" cheat where it's "wrong" to use it? In some sense, I see ¬¬P => P as a "cast" from an opaque function type to specifically be a closure {f => f(p)} for some p: P.
  - cmrx64 2y ago
    that isn’t proof by contradiction, that’s plain old proof of negation. proof of negation is Neg : (P → False) → ¬P, proof by contradiction is PBC : (¬P → False) → P. a subtle yet crucial distinction
    - ndriscoll 2y ago
      Ah, right. It's been long enough that I've forgotten what the words mean, though I think with my ninja edit, PBC is actually still constructively valid as a method to prove a negation?
  - ndriscoll 2y ago
    Partially answering my own question: a starting point for synthetic differential geometry is to define a collection of infinitesimals which aren't not zero, but also zero isn't the only infinitesimal. So there are interesting/non-contrived objects that live in the space left by not assuming LEM.
  - johnnyjeans 2y ago
    Sorry, I'm rusty enough on my logic that I'll only embarrass myself if I try to match the depth of your post. > Are there cases where you didn't "obviously" cheat where it's "wrong" to use it? In particular, it prevents us from adapting the proof to non-binary valued logics full stop. > I see ¬¬P => P as a "cast" from an opaque function type to specifically be a closure {f => f(p)} for some p: P. Now this is an interesting thought.
- Tainnor 2y ago
  > They're also generally much easier to create than constructive proofs This is generally seen as a good thing by most "lazy academics". I guess your priorities are just different. Constructivism is also not at all opposed to infinite quantities (that would be finitism). "Real-world domains" deal with infinite spaces (e.g. of all functions R->R) quite regularly across all scientific domains.
  - johnnyjeans 2y ago
    My priorities are indeed different. Apologies for the inflammatory language. My remark WRT constructive proofs is more an observation I've made that most proofs which deal with non-finite values seem to be non-constructive. Not necessarily as a hard and fast rule, the two just don't seem to roll well together. Could be sampling bias, but poking and prodding with mathematician friends more or less confirmed it. Not well read enough to have more interesting things to say on it.
- TimorousBestie 2y ago
  This is needlessly aggressive. There’s nothing wrong with assuming the axiom of choice to prove a result, just as there’s nothing wrong with trying to develop a proof that doesn’t rely on it. Saying a nonconstructive proof “explains nothing” is myopic at best. Insights come from everywhere.
- deleted 2y ago
  [deleted]
zozbot234 2y ago
As others have explained, there is indeed nothing wrong with "proof by contradiction" of a negative statement. Intuitionistic logic does not view statements phrased in the "positive" and in the "negative" as fully equivalent, as classical logic does. (There are ways of formalizing this point of view quite rigorously, such as in so-called "ecumenical logics" where classical and constructive/intuitionistic reasoning can in fact coexist and interoperate, but statements derived from classical reasoning can only be translated in the negative as seen within constructive reasoning.)
- AnimalMuppet 2y ago
  So I asked specifically for you to assume that I don't already agree with intuitionist logic. Now, assuming that, what is wrong with proof by contradiction of a positive statement? Both you and johnnyjeans gave me answers that already assumed intuitionism. I don't assume that. Can you give me any reasons that start from where I am and show my why I should adopt intuitionism?
  - auggierose 2y ago
    You should not. Platonism is the only defensible mathematical philosophical position.
    - AnimalMuppet 2y ago
      That doesn't make platonism a "half-assed academic hack", though (which was the original claim I was questioning).
      - auggierose 2y ago
        I fully agree. Platonism isn't a hack, it is the only philosophy of math that makes sense to me. Something is either true, or it isn't. There is no third case. This is because mathematical objects are real, not just something our minds make up. To quote Arnold: Mathematics is the part of physics where experiments are cheap. That said, I don't have a problem with intuitionistic logic, but I think about it as a platonist, for example via Kripke models. I also don't have a problem thinking about it in terms of a certain restricted class of proofs, that people call constructive proofs.

johnnyjeans 2y ago

Because they explain nothing and aren't useful for building new insights. It's not a direct verification of the existence or lack-of-existence of a thing with given properties. It relies on rules lawyering in a very specific logic to say something with basically no substance. Allowing it causes more problems for automated proofs than they solve, so long as your domain only deals with finites (which all real-world domains do exclusively.) They're also generally much easier to create than constructive proofs, which makes them a convenient go-to for lazy academics.

ndriscoll 2y ago
Proof by contradiction is fine for lack-of-existence (indeed, ¬P is defined in type theory as P -> false). I think also if I got my types right, you can do def eliminateTripleNot(f: ¬¬¬P): ¬P = {p: P => f({g: ¬P => g(p)})} For a constructive proof of ¬¬¬P => ¬P? So it's really just ¬¬P => P that causes trouble. It's not clear to me though whether LEM is actually okay in the "fast and loose reasoning is morally correct" sense (i.e. if it's okay as long as you don't cheat and do something like use a non-terminating loop or exception to make your ¬¬P) though? Are there cases where you didn't "obviously" cheat where it's "wrong" to use it? In some sense, I see ¬¬P => P as a "cast" from an opaque function type to specifically be a closure {f => f(p)} for some p: P.
- cmrx64 2y ago
  that isn’t proof by contradiction, that’s plain old proof of negation. proof of negation is Neg : (P → False) → ¬P, proof by contradiction is PBC : (¬P → False) → P. a subtle yet crucial distinction
  - ndriscoll 2y ago
    Ah, right. It's been long enough that I've forgotten what the words mean, though I think with my ninja edit, PBC is actually still constructively valid as a method to prove a negation?
- ndriscoll 2y ago
  Partially answering my own question: a starting point for synthetic differential geometry is to define a collection of infinitesimals which aren't not zero, but also zero isn't the only infinitesimal. So there are interesting/non-contrived objects that live in the space left by not assuming LEM.
- johnnyjeans 2y ago
  Sorry, I'm rusty enough on my logic that I'll only embarrass myself if I try to match the depth of your post. > Are there cases where you didn't "obviously" cheat where it's "wrong" to use it? In particular, it prevents us from adapting the proof to non-binary valued logics full stop. > I see ¬¬P => P as a "cast" from an opaque function type to specifically be a closure {f => f(p)} for some p: P. Now this is an interesting thought.
Tainnor 2y ago
> They're also generally much easier to create than constructive proofs This is generally seen as a good thing by most "lazy academics". I guess your priorities are just different. Constructivism is also not at all opposed to infinite quantities (that would be finitism). "Real-world domains" deal with infinite spaces (e.g. of all functions R->R) quite regularly across all scientific domains.
- johnnyjeans 2y ago
  My priorities are indeed different. Apologies for the inflammatory language. My remark WRT constructive proofs is more an observation I've made that most proofs which deal with non-finite values seem to be non-constructive. Not necessarily as a hard and fast rule, the two just don't seem to roll well together. Could be sampling bias, but poking and prodding with mathematician friends more or less confirmed it. Not well read enough to have more interesting things to say on it.
TimorousBestie 2y ago
This is needlessly aggressive. There’s nothing wrong with assuming the axiom of choice to prove a result, just as there’s nothing wrong with trying to develop a proof that doesn’t rely on it. Saying a nonconstructive proof “explains nothing” is myopic at best. Insights come from everywhere.
deleted 2y ago
[deleted]

zozbot234 2y ago

As others have explained, there is indeed nothing wrong with "proof by contradiction" of a negative statement. Intuitionistic logic does not view statements phrased in the "positive" and in the "negative" as fully equivalent, as classical logic does. (There are ways of formalizing this point of view quite rigorously, such as in so-called "ecumenical logics" where classical and constructive/intuitionistic reasoning can in fact coexist and interoperate, but statements derived from classical reasoning can only be translated in the negative as seen within constructive reasoning.)

AnimalMuppet 2y ago
So I asked specifically for you to assume that I don't already agree with intuitionist logic. Now, assuming that, what is wrong with proof by contradiction of a positive statement? Both you and johnnyjeans gave me answers that already assumed intuitionism. I don't assume that. Can you give me any reasons that start from where I am and show my why I should adopt intuitionism?
- auggierose 2y ago
  You should not. Platonism is the only defensible mathematical philosophical position.
  - AnimalMuppet 2y ago
    That doesn't make platonism a "half-assed academic hack", though (which was the original claim I was questioning).
    - auggierose 2y ago
      I fully agree. Platonism isn't a hack, it is the only philosophy of math that makes sense to me. Something is either true, or it isn't. There is no third case. This is because mathematical objects are real, not just something our minds make up. To quote Arnold: Mathematics is the part of physics where experiments are cheap. That said, I don't have a problem with intuitionistic logic, but I think about it as a platonist, for example via Kripke models. I also don't have a problem thinking about it in terms of a certain restricted class of proofs, that people call constructive proofs.