Mereological Logicism

Terminology: I'll denote this theory by "Mereological Logicism", because its primitive are Part-hood and, Predication, which are the primitives of Mereology and Logic. However those are here extending first order logic, so it is a first order logic theory about Mereological Logicism.

EXPOSITION: To first order logic with identity, add the binary relation P standing for "is a part of", and also add the primitive binary relation symbol "predicates".

Axioms: ID axioms plus Atomic General Extensional Mereology"AGEM" axioms, plus the following:

As a terminology every object of this theory is a "set".

Define "ϵ": x ϵ y⟺xPy∧atom(x) 

We have the following theorems:

i. ∀x∃y:y ϵ x 

ii. ∀xy[∀z(z ϵ x↔z=y)→x=y] 

iii. ∀xy (y ϵ x→∀m(m ϵ y↔m=y)) 

• 1. Downward Axiom: atom(Q)→∀x(Q predicates x→atom(x)) 

an Atom Predicates only predicate atoms.

• 1. Upward Axiom: ∀x∀Q[∀y(Q predicates y↔y ϵ x)→atom(Q)] 

A predicate predicating atoms, is itself an atom.

From the Unrestricted Composition Principle we have the following theorem of extending predicates:

∀Q[atom(Q)∧∃y(Q predicates y)→∃x∀y(y ϵ x↔Q predicates y)]

i.e.; for every atom predicate, there is an extension whose members are all and only what fulfills that predicate.

• 1. Axiom schema of predicate existence: if ψ is a formula in the language of predication, i.e. only the symbols ‘‘Predicates;="are allowed to be used as predicate symbols; i.e., the symbol "P" is not allowed. That has all and only symbols ‘‘y,x1,..,xn" occurring free in it, then:

  2. ∀x1,..,xn,x[(x1,..,xn are atoms∧∀y(y ϵ x↔ψ))→

     1. ∃Q∀y(Q predicates y↔y ϵ x)]

         is an axiom.

for any set of atoms that is definable after a formula in the pure predicate language from atom parameters, there exists a predicate whose extension is that set.

• 1. Empty: ∃X [atom(X)∧∄y(X predicates y)] 

There exists an atom predicate that doesn't predicate anything.

/Theory definition finished.

Now if we define the membership ‘‘∈"‘ as:

y∈x⟺x predicates y

then I'd think we can get to interpret Ackermann's set theory, which in turn would interpret ZFC.

The strong point is that this theory is almost a theory of logic! In some sense signaling revival of the program of Logicism!

So the crucial question: is Ackermann set theory equi-intepretable with this theory?

See the attached file, for more recent developments of this system.