4 ms·

> 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

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

fnrslvr 7y ago
> 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.)
drdeca 7y ago
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 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) ?
- black_knight 7y ago
  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_negative_translation https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg...

fnrslvr 7y ago

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

drdeca 7y ago

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

black_knight 7y ago
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_negative_translation https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg...