In second-order logic (with standard semantics), we know that there are sound deductive systems, and we know that no sound deductive system can derive all true statements.

I was wondering whether there was a formalized sound deductive system which could be used as the basis of a "unique" computable algorithm to prove all sentences provable by humans, say in a mathematics textbook.

Is there for example a sound deductive system which can prove every sentences that are provable by at least one sound deductive system ?

Examples of such eventual real-world deductive systems (for instance used in HOL theorem solvers) are welcome.


A statement cannot be not just "provable" or "not provable", without further specification. It is provable in some specific deductive system or not.

So your question has a trivial answer: Yes, any sound proof system can prove exactly those sentences that are provable in that system. And that is the only form of "provable" there is to ask for.

(Note that a "deductive system" is exactly the same as a proof system: a set of rules for what constitutes a valid proof. It looks like you may be thinking that a deductive system has to be an algorithm, which is not the case -- though, of course, once you have defined a deductive system there's an algorithm to find proofs in it; if nothing else, there's the brute-force one that searches through all proofs in the system and looks for a particular conclusion).

Furthermore, every logically valid second-order statement is provable in at least one sound (and recursive) deductive system. Namely, we can just declare it to be an axiom and add it to a known sound system. So you can't get a sound (and recursive) system that will prove everything every other sound (and recursive) system can prove.

  • $\begingroup$ Oh thanks. But how are we able to "compare" different proof systems ? In FOL we sometimes say that two proof systems are deductively equivalent if any theorem deducible from one of them is deducible from the other. I thought that we could then say that some sound proof system could for example derive "more" theorems than others? Can we say that a proof system is able to derive "whatever a human is able to derive by hand" ? $\endgroup$ – Flop Jun 6 '15 at 20:51
  • $\begingroup$ @Flop: You still sound confused when you contrast a proof system with "whatever a human is able to derive by hand". When the human derives things by hand, the results of his efforts will be a proof in a particular proof system. The proof system is not a mechanical thing; it is just a rule that says what we're going to accept as a valid proof. The actual proofs that we apply this rule to can be constructed by hand or by machine; that makes no difference. $\endgroup$ – Henning Makholm Jun 6 '15 at 20:56
  • $\begingroup$ @Flop: Yes, some proof systems will be stronger than others, and they can be compared according to whether one can prove (which means "can be used to write down a proof of") a subset of the sentences another one can. $\endgroup$ – Henning Makholm Jun 6 '15 at 20:58
  • $\begingroup$ Ok, I think it's clearer. I'll try to reformulate my initial thoughts : Can we construct a sound proof system "stronger" than every other sound proof systems (a sound proof system which can prove all sentences which are provable by at least one sound proof system) ? $\endgroup$ – Flop Jun 6 '15 at 21:15
  • $\begingroup$ @Flop: No we can't -- since every sound system must be incomplete, if you come with a candidate system we can just take one of the logically valid statements it can't prove and add it as an additional logical axiom to get an even stronger, but still sound, one. (Finding a valid-but-unprovable statement to elevate to axiom status is not necessarily easy, but we know one is out there somewhere). $\endgroup$ – Henning Makholm Jun 6 '15 at 21:44

When you say "standard semantics" for higher order logic, this takes you well out of the realm of proof systems. It is true that the set of validities in first-order logic is recursively enumerable, so we have a hope of coming up with a recursive proof system which can prove all validities (and in fact plenty of such systems exist); however, for higher-order logics this is wildly false. These computability theoretic considerations rule out any hope of any kind of proof system for higher-order logic.

That is, your first two paragraphs are conflating some things:

  • It is true that the set of true sentences of higher-order logic is not recursively enumerable. But this is already true of first-order logic.

  • Fixing a given proof system, of course the things it proves are recursively enumerable.

  • But you're really interested in the sentences which "ought to be provable," that is the validities. In the context of the standard semantics, the set of validities is incredibly complicated ($\Pi^1_1$-complete, almost unimaginably more complicated than recursively enumerable); in the context of the Henkin semantics (http://en.wikipedia.org/wiki/Second-order_logic#Semantics), though, the validities are recursively enumerable.

Short version: for the standard semantics, no proof system can exist for purely computability-theoretic reasons. (There are also model-theoretic obstacles, such as the failure of compactness.)

But if you're interested in proof systems for higher-order logic, then you're probably interested in the Henkin, not standard, semantics. In this interpretation second-order logic is not really any different from first-order logic, and there do exist proof systems which will prove all validities. If your question is whether there are specific ones which are useable in practice, you have to be careful what you mean. Since the set of validities is incomputable, we can't hope for an algorithm which - on input some sentence $p$ - will answer "is $p$ a validity?" All we can hope for is a function enumerating the validities. But at this point it's not clear what "usable" means, so I don't have any answer.

  • $\begingroup$ I'm not sure of the motivation for the downvote, but this answer seems nice to me. $\endgroup$ – Carl Mummert Jun 6 '15 at 23:29
  • $\begingroup$ Thanks for you insight into those two different semantics. Actually, I was really thinking about the relationships between the sets of provable sentences of different sound (and of course not complete) proof systems in SOL with standard semantics. $\endgroup$ – Flop Jun 7 '15 at 11:33
  • $\begingroup$ @Carl: Someone may have taken issue with the claim that "a proof system is only worth studying if it is sound and complete". $\endgroup$ – Henning Makholm Jun 7 '15 at 11:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.