Sound deductive systems with biggest set of provable sentences in second-order logic?

Question

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.

Answer 1

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.

Answer 2

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.