New answers tagged


The first problem is what does is even mean that a propositional proof system can prove its own properties: there is a serious discrepancy of the languages, because the propositional proof system can only express propositional formulas, whereas properties of the proof system are first-order statements in a language that can reason about finite strings, i.e., ...


There is no loop. The purpose of a formal system is to make reasoning principles explicit and to explain more precisely how reasoning works. The word "foundation" in "foundations of mathematics" does not mean "create a secure base for mathematics out of nothing" – that would be an indifensible position. There is absolutely ...


In general, proof systems can sometimes prove some of their properties within themselves. A nice example of this is the fact that NL=Co-NL can be proved "within NL". This video might also be useful:

Top 50 recent answers are included