Mark Gritter (markgritter) wrote,
Mark Gritter
markgritter

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: complexity, geek, mathematics
Subscribe
  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments