Hacker News Reader

Comment by black_knight | Hacker News Reader

> Unfortunately, most of these proving languages are constructive and thus it's possible for both of those to be unprovable.

The fact that it is possible for a given proposition P to be neither provable nor disprovable has nothing to do constructive mathematics. This happens in classical mathematics as well – in any incomplete theory. All theories which serve as foundation of mathematics are incomplete (ref. Gödel).

It is just that a constructive mathematician can be at peace with this situation, since they does not believe P ∨ ¬P to be a tautology – while a classical mathematician will forever be tormented by the existence of theorems they cannot prove in their chosen formalism.

View on HN

I was going to say "what if you look for a proof of (¬¬P)∨(¬P)" , but, to my surprise, apparently that is also not a tautology in intuitionistic logic? So, I knew that ¬¬(P ∨ ¬P) is a tautology in intuitionistic logic, but, to my surprise, (¬¬P)∨(¬P) is not.

Here is a twitter bot that evaluates whether statements are tautologies in intuitionistic logic, and it gives the answer that (¬¬P)∨(¬P) is not, and gives a "kripke counterexample" https://twitter.com/ipc_bot/status/1189953697486229504?s=20

Mentioning this because I was going to respond by saying "but isn't (¬¬P)∨(¬P) still a tautology? Then, how does intuitionistic logic / constructive logic, help with avoiding the problem?", but then I checked, and was surprised, so I thought other people might have the same misconception I had, so I'm saying this.

However, if (P is provable in classical logic)∨((¬P) is provable in classical logic), doesn't it follow that either ((¬¬P) is provable in intuitionistic logic) or ((¬P) is provable in intuitionistic logic) ?

I can give you some intution as to why (¬¬P)∨(¬P) isn’t provable. The essense of a proof of a disjunction A ∨ B is to either have a proof of A or a proof of B – as well as a label telling if we proved the left or the right hand side. So, to have a proof for every P that (¬¬P)∨(¬P) means that for every P you can either cough up a proof that ¬¬P or a proof of ¬P. This is impossible.

Your final paragraph mixes object level and meta-level in a way I am not quite able to decipher. But there are results in a similar vein, but restricted to particular theories:

The Gödel—Gentzen translation[0] translates formulas of Peano artithmetic into formuals in Heyting arithmetic in a way which preserves provability. But there are quite limited which theories this works for. For instance, such a translation does not exist in set theory between, say, ZFC and CZF. So there is in general no way for a constructivist to give meaning a classical proof.

[0]: https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg...

> while a classical mathematician will forever be tormented by the existence of theorems they cannot prove in their chosen formalism.

As a devotee to the law of excluded middle myself, I don't feel particularly tormented by this.

(I agree with your wider point that constructivism isn't the root cause of independent statements in mathematical foundation theories.)

Reply on news.ycombinator.com