# Tag Info

Accepted

Accepted

### Understanding non-equivalence of proof lengths according to proof systems

I believe everything you said is correct. I note that your point #3 could hold regardless of points #1 and #2 - points #1 and #2 are just a concrete example of where this has provably happened.
Accepted

### How far is the distance between Mahlo Universe and Mahlo Cardinal?

It's awkward to ask yourself questions, but... Rathjen, M. (2003). Realizing Mahlo set theory in type theory. Archive for Mathematical Logic, 42(1), 89-101. The chapter 5, "Realizing set theory ...
Accepted

### Proving proof system properties within the proof system itself?

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 ...

### Proving proof system properties within the proof system itself?

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 ...
1 vote

### Proving proof system properties within the proof system itself?

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 ...
1 vote

### Understanding non-equivalence of proof lengths according to proof systems

A propositional proof system in which all tautologies have a "short" proof is called a super-propositional-proof system. Such a system exists iff NP = CoNP. If NP != CoNP then P != NP. So, it's not ...
1 vote

### Resolution vs Nondeterministic Search Problems

If I understood correctly the question, the so-called Buss-Pudlak game provides a simple transformation from a proof system to such a decision tree (see Buss-Pudlak '94 http://math.cas.cz/%7Epudlak/...

Only top scored, non community-wiki answers of a minimum length are eligible