Follow up to Hintikka on the analytic/synthetic distinction - some thoughts on proof depth, logical omniscience and tractability

Yesterday I wrote a blog post about Jaakko Hintikka's account of the analytic/synthetic distinction in mathematics and logic. This post is a direct follow up to that one, and refers to terms already defined there. I highly reccomend you read it first.

Bonus content - computational tractability

The authors of the "Depth-Bounded Natural Deduction" paper don't just define a notion for "analytic" proofs. They in fact construct a grading of depths of proofs and then define analytic judgements as those which can be proven at depth-0. At the end of the paper they pose an interesting question - namely whether depth-k provability for finite k can be decided in polynomial time.

This has an interesting relationship to Scott Aaronson's application of the Cobham Axioms to the problem of logical omniscience (section 5 of "Why Philosophers Should Care About Computational Complexity"), which was also motivated by a question raised by Hintikka. Namely:

Can we give some formal account of “knowledge” able to accommodate people learning new things without leaving their armchairs?^{1 2}

How exactly do these approaches relate? Aaronson's application of the Cobham axioms is about the functions which agents know how to use to answer questions. Aaronson defines 'knowing how' as being able to do so tractably from an agent's repertoire of existing question-answering functions. For example, consider a question like "how many whole numbers under 5 are even?". The Cobham axioms then let you work out whether an agent already "knows" how to do this without needing to add substantively new functions to their repertoire. Perhaps they already know how to check whether a number is even, how to add pairs of numbers, and how to count to five. The Cobham axioms let you show that this means they can tractably answer this question.

On the other hand Depth-Bounded Natural Deduction leaves open the question of how agents search for answers. It is a theory about the complexity of the proofs which agents use to show those answers, not the complexity of the functions they use to find them. In order to actually arrive at answers, an agent needs some further function for actually finding the proofs, for example, "search through all possible Depth-Bounded Natural Deduction proofs at depth-k".

You might ask whether an agent who "knows" how to find proofs for small k knows how to find proofs for any finite k. In other words, whether an agent who is able to make use of some small amount of virtual information is able to tractably make use of any finite amount of virtual information.

If the poly-time conjecture about finding finite-depth natural deduction proofs holds, then for every fixed finite depth k, there’s a polynomial-time way to search for depth-k proofs. However, this would not on its own show that, in Aaronson’s sense, an agent whose repertoire includes search procedures for depth-k knows how to search for depth-greater-than-k proofs. In order to establish this you'd also need to show that you can get from a method for finding proofs for small k to a method for finding proofs for any finitely large k just by application of the Cobham axioms.