All Questions
1 question
3
votes
0
answers
257
views
Oracle separating FIP for bounded-depth Frege from FIP for Frege (and hardness conditions on DDH)
Is there an oracle such that in the relativized world, bd-Frege (bounded depth Frege propositional proof system) has FIP (feasible interpolation property) but Frege does not have FIP?
Such an oracle ...