MK+CCMK+CC as a foundation for category theory

Has any work been done on what MK+CC looks like as a foundation for category theory? Is it ‘the same’ as restricting to inaccessibles in some precise manner? According to wikipedia, any category with all unrestricted limits is thin. This is typically formulated in ZFC as the statement that any small category with all small … Read more

Apart from Tarski’s study, is there any other source that has been looking at the parallelism of concepts and theorems?

Alfred Tarski in his next study (Some Methodological Investigations on the definability of concepts, TARSKI, Logic, Semantics, Metamathematics. Papers from 1923 to 1938. Clarendon Press, Oxford, 1956, 296-308.) describes the parallelism between concepts and theorems: axiom – primitive concept, theorem – defined concept, proof and its rules – definition and its rules. I always thought … Read more

Theories and indiscernible propositions

Are there known examples of statements which are strong from a proof-theoretic standpoint but which are indistinguishable by one set of axioms (or proof system) yet distinct according to a stronger set of axioms? More specifically, I’m wondering if there are examples of the following kind: Let T1 and T2 be theorems in some formal … Read more

Class theory with support for self-application of class functions?

To every natural number n, we can assign its Church numeral n_. A formal definition would be: 0_(f)=iddom(f) n+1_(f)=n_(f)∘f where each line is to be understood as implicitly universally quantified over every endofunction f. This gives us nifty formulae like: a_∘b_=a⋅b_ a_(f)∘b_(f)=a+b_(f) Unfortunately, size issues block the existence of Church numerals inside models of ZFC. … Read more

Order Types and Replacement Schema

Using Replacement Schema we can prove any well-ordering is isomorphic to an ordinal number. Q: Is the following consistent? ZFC−Rep+¬Rep+Any well-ordering is isomorphic to an ordinal number Answer Let κ be a ℶ-fixed point — that is, let κ=ℶκ. Then Vκ models ZFC – Rep + “every well-order is isomorphic to an ordinal”. But ZFC … Read more

Survey of finite axiomatizability for relational theories?

An L-theory T is finitely axiomatizable if there is a finite set A of L-sentences with the same consequences as T, i.e. such that M⊨T iff M⊨A for every L-structure M. (Here L is a first-order language, and I am mostly interested in languages with relational symbols and no function symbols.) Is there a survey … Read more

What would be the effect of replacing Separation by Injective Replacement?

Let “Injective Replacement” be the following schema: If ϕ(x,y) is a formula in which only x,y occur free, and only free, then: ∀A [∀x∈A∃y(ϕ(x,y))∧∀x,y,z,u(ϕ(x,y)∧ϕ(z,u)→(x=z↔y=u))→∃B ∀y (y∈B↔∃x∈A(ϕ(x,y))] In English, we require that the replacement function be an injection. Now if we replace the Separation scheme in Zermelo’s set theory, Z, by the above axiom schema, call the resulting theory … Read more

two versions of the nested interval property

There appear to be two different nested interval properties for the reals with the punchline “… then the intersection of the intervals is non-empty”, and I’d like to know their respective histories (and the appropriate terminology to use for distinguishing between them). Here I am not concerned with the issue of “singleton-icity” of the intersection; … Read more