Hacker News new | past | comments | ask | show | jobs | submit login

> That is a very subtly different question than the one I was trying to ask. Or.. well.. I think it is. What I was trying to ask was if there are formally provable theories that cannot be expressed in a way that would let a computer "compute" the proof.

It depends on the logical system + axioms that your formally provable theory is in respect to, and "how soon" you design the computer that verifies the proof. Recall that a proof is a finite sequence of applications of rules of inference on zero or more axioms to derive a new statement that may be regarded as an axiom for applications later in the sequence, so that the last step derives the theorem.

If there are a countable number of rules of inference and a countable number of axioms, and each rule of inference has finite valence (i.e. infer from finitely many formulae-patterns as hypotheses), then yes, there is a way of encoding the rules of inferences and possible axioms of the logical system that a Turing machine (TM) will find a proof of any provable theorem (i.e. verify it), simply by enumeration of axioms in rules of inferences in the positions in a sequence that constitute the proof, while checking whether the axioms legally fit the rules of inference. (It is always possible to check in finite time whether a (finite-length) formula satisfies the pattern it needs to satisfy by a rule of inference).

On the other hand, if there are an uncountable number of rules of inference or an uncountable number of axioms, there may be a computer that cannot verify all the formally provable theories. For example, trivially, if there are an uncountable number of axioms, then the axioms admit no encoding; that is, there is no set of finite strings in a finite alphabet that is able to uniquely label all the axioms. But an axiom is itself a formally provable theorem; its proof is just introducing itself, yet that proof cannot be represented for all the axioms. (dependent on definition of proof; this example may not be so if we accept a zero sequence as a proof; but in general this illustrates the fact that there are simple theorems in some formal systems + uncountable axioms that cannot be computed).

Yet, if we know beforehand the theorem and rules of inferences and axioms used in some proof of it, and the rules of inference all have finite valence, then that proof only invokes finitely many rules of inference on finitely many axioms, such that we can encode a fragment of the logical system + axioms + expressible formulae such that the TM can verify all formally provable theorems in that fragment, including the desired theorem.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact