Hacker News Reader

Comment by talkingtab | Hacker News Reader

The connection to intuitionism (see https://en.wikipedia.org/wiki/Intuitionism) gives this kind of thinking much broader appeal and application. It seems to me we live in a time so dominated by analytical thinking that we completely ignore other useful and effective modes.

View on HN

Intuitionism in this context just means the proofs have to be constructive. (no proof-by-contradiction, or other half-assed academic hacks)

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?

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.

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.

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

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?

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.

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.

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

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.

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.

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.)

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?

You should not. Platonism is the only defensible mathematical philosophical position.

That doesn't make platonism a "half-assed academic hack", though (which was the original claim I was questioning).

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.

Reply on news.ycombinator.com