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 ...
I've just been asked for a good example of a situation in maths where using infinity can greatly shorten an argument. The person who wants the example wants it as part of a presentation to the general ...
Assume you have some notion of proof complexity: for instance, at the basic level, the length of a proof, or the number of symbols used, take your pick (there are more involved measures, but for sake ...
The Completeness Theorem in first-order logic states that any mathematical validity is derivable from axioms. Hence, any informal mathematical proof (which is rigorous) can be translated into a formal ...
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?