[johnnyjeans]

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]

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.

[johnnyjeans]

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.

[ndriscoll]

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.

[cmrx64]

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]

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?

[TimorousBestie]

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.

[Tainnor]

> 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]

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.