Can one define some measure of progress towards a proof of a statement? I'm not sure if it's even possible for general first order logic statements so let's restrict ourselves to propositional ...
Why ZFC is placed in top of the proof system hierarchy? How it can p-simulate other systems?
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 ...