Describability
This theory is basically is an extension of a Morse-Kelley "MK" like class theory, but with single point violation of extensionality as to allow just two non extensional sets, both of which are empty. Classes built form the first empty set 0 are denoted by term symbols raised to 0 while those from the second empty set ∅ are denoted by term symbols raised to ∅. Replacement works within each world but not across worlds. An axiom of describability simply states that if similar formulation leads to isomorphism of classes defined after them in both worlds, then this implies the set-hood of the defined classes. The question is whether this would be enough to prove existence of inaccessible sets!
Language: Mono-sorted first order predicate logic
Primitives: =;∈,∅,0 where the last two are constants.
Define: set(x)≡df∃y (x∈y)
Axioms: ID +
1. Weak Extensionality: nonempty(x)∧∀z(z∈x↔z∈y)→x=y
2. Empty sets: 0≠∅∧∀x(empty(x)↔x=0∨x=∅)
3. Foundation: ∃y(y∈x)→∃y∈x[∄c(c∈y∧c∈x)]
4. Class Comprehension: if ϕ is a formula in which x is not free, then all closures of:
∃x∀y(y∈x↔set(y)∧ϕ)
; are axioms.
Define: x={y|ϕ}≡df∀y(y∈x↔set(y)∧ϕ)
5. Pairing: ∀sets x,y (set({x,y}))
6. Subsets: set(x)∧y⊆x→set(y)
7. Power: set(x)→set(P(x))
8. Union: set(x)→set(⋃(x))
Define: x=yo≡dfx=o∨(nonempty(x)∧∀z∈TC(x)[empty(z)→z=o])
Where TC stands for transitive closure.
9. Modified Limitation of size: |xo|<|Vo|→set(xo)
Where Vo={xo|set(xo)}
Define:
x0≅y∅≡dfTC(x0) is ∈-isomorphic to TC(y∅)
Where TC stands for transitive closure.
10. Describability: if ϕ0 is a parameter free formula in which all variables are raised to 0, and if ϕ∅ is the formula obtained from ϕ0 by merely replacing every occurrence of the symbol 0 by the symbol ∅, then:
{x0|ϕ0}≅{x∅|ϕ∅}→{x0|ϕ0},{x∅|ϕ∅} are sets
, is an axiom.
Question: would this theory prove the consistency of "ZFC+ there exists an inaccessible set"?
See: