# Proof systems with shortcuts

Scott Aaronson posted a list of student-level research problems in complexity theory. This one seems reasonably easy to me, unless I'm misunderstanding what it asks for:

Are there proofs with (say) n^2 symbols, in a proof system of your choice, for which (a) there exist proofs of the same statements with n symbols, but (b) finding the shorter proofs is computationally intractable?

Let's say our proof system has axiom-schema:

A1. M * N + R = T for all valid combinations of integers with 0 <= R < N
A2. SHA( K ) = N for all valid integers such that SHA-256 applied to the binary representation of K results in the binary representation of N

As well as inference rules

I1. NO_DIVISORS_UP_TO( P, 2 ) if M * 2 + 1 = P for some M
I2. NO_DIVISORS_UP_TO( P, K ) if NO_DIVISORS_UP_TO( P, K - 1 ) and M * K + R = P for some M, R != 0
I3. ODD_PRIME( P ) if NO_DIVISORS_UP_TO( P, P - 1 )
I4. ODD_PRIME( P ) if NO_DIVISORS_UP_TO( P, S + 1 ) and S * S + R = P for some S, R != 0 and SHA( K ) = P for some K

In this system a proof of ODD_PRIME( P ) takes about 2P steps if we use inference rule I3, for example:

```5 * 2 + 1 = 11                 [A1]
NO_DIVISORS_UP_TO( 11, 2 )     [I1]
3 * 3 + 2 = 11                 [A1]
NO_DIVISORS_UP_TO( 11, 3 )     [I2]
2 * 4 + 3 = 11                 [A1]
NO_DIVISORS_UP_TO( 11, 4 )     [I2]
2 * 5 + 1 = 11
NO_DIVISORS_UP_TO( 11, 5 )
1 * 6 + 5 = 11
NO_DIVISORS_UP_TO( 11, 6 )
1 * 7 + 4 = 11
NO_DIVISORS_UP_TO( 11, 7 )
...
1 * 10 + 1 = 11                [A1]
NO_DIVISORS_UP_TO( 11, 10 )    [I2]
ODD_PRIME( 11 )                [I3]
```

But only about 2*sqrt(P) steps if we use inference rule I4. But in order to introduce the necessary axiom using A2 we have to perform a computationally intractable amount of work to identify K.

I think, however, that Dr. Aaronson was actually looking for propositional proof systems that can prove any tautology in classical logic--- a much more difficult exercise than my toy language here. However, the same sort of embedding might be feasible.
Tags:
• Post a new comment

#### Error

default userpic