4 problems

0 votes0 replies1 view
Conjecture on the arithmetic equivalence of intuitionistic theories of strength Gamma-zero
Arithmetic-equivalence conjecture. All of these intuitionistic theories— $\mathbf{MLTT}^-$ , its extensional version, $\mathbf{ATR}_0^i$ , and…
Conjectureopenconstructive-set-theory intuitionistic-logic proof-theoryarXiv posted 2 days ago
0 votes0 replies0 views
Conjecture on the arithmetic strength of CZF with collection and choice principles
Arithmetic-strength conjecture. The theory
Conjectureopenconstructive-set-theory proof-theory reverse-mathematicsarXiv posted 2 days ago
0 votes0 replies0 views
Rathjen's full Separation conjecture for CZF
Rathjen's conjecture. Adding full Separation to CZF should elevate the theory's proof-theoretic strength from $\mathrm{ID}$ to full Second Order Arithmetic.
Conjectureopenconstructive-set-theory proof-theory second-order-arithmeticarXiv posted 2 days ago
0 votes0 replies1 view
The consistency-strength conjecture for CZF's failure of the existence property
The paper has shown that $\mathbf{CZF}$ does not have the existence property, using $\mathbf{ZFC}$ in several places and therefore proving the result only under the assumption that…
Conjectureopenconstructive-set-theory proof-theoryarXiv posted 2 days ago

Conjecture on the arithmetic equivalence of intuitionistic theories of strength Gamma-zero