Comment by tel | Hacker News Reader

Comment by tel | Hacker News Reader

The title is a bit misleading. The author doesn't really discuss whether computers can perform the act of proving. He's mostly focused on whether computer languages can represent proofs (yes) and whether computers can check them (yes).

Computer can also search for theorems and proofs to those plausible theorems. There are issues, of course. Both of these spaces are very, very large. It's not clear what makes for an "interesting" theorem to prove.

Proof through proof search is also semi-deterministic in that the search will continue until it finds an answer. If the search hasn't terminated yet, it's either because there is no proof or because it just hasn't worked hard enough... yet.

You could conceivably "race" searches between P and (not P) and hope that this would save you since now one of the two will return in finite time. Unfortunately, most of these proving languages are constructive and thus it's possible for both of those to be unprovable.

It's all very cool, but we're still not getting close to having computers realistically "prove" things of interest.

Edit: Worth also noting quickly that proof search is used pretty regularly in these systems, but it's a sort of localized, partial, and interactive proof search where "tactics" for the search are human specified or search is used as an interactive tool for skipping over "boring" parts of proof construction.

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

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

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

> You could conceivably "race" searches between P and (not P) and hope that this would save you since now one of the two will return in finite time.

Adding to black_knight's point, it's worth noting that even in complete theories this often isn't very heartening: interleaving searches for P and for (not P) will often take an enormous amount of time.

Even cleverer strategies can be hopeless. For example, the theory of real closed fields is complete (and hence by your interleaving argument, decidable), but appears to be EXPSPACE-complete (at least from a brief skim of the literature), hence known to be truly intractable. If standard complexity-theoretic conjectures hold up (e.g. P != NP, NP != coNP), then non-gargantuan proofs in proof systems for a wide variety of interesting problems will turn out to be both intractable to locate and incomplete.

None of this is to say that automated theorem proving can't or won't rise to the level of human mathematical activity (I think it will fwiw), but we need to be far cleverer about it.

Reply on news.ycombinator.com