I am trying to implement Ackermann set theory.
The first approach is the code below. But there is an incorrect axiom "rs_ax". That's because for every x formula (F x) shouldn't contain predicate M. $\big((\mbox{M}\ x)\leftrightarrow (x\in\mbox{V})\big)$
1) Is it possible to define a subtype L of Prop, such that its elements are constructed without predicate M? (I am afraid that it is highly likely impossible.)
The second approach of implementing Ackermann set theory is to implement predicate logic syntactically. (re-invent the definition of formulas, substitution, etc)
2) Did you used such syntactic libraries? Could you provide some links or references?
Maybe there are other approaches?
Require Export Setoid.
Module Type ACK_sig.
Parameter
(class : Type)
(M : class -> Prop) (* is_set *)
(eq_class : class -> class -> Prop)
(in_class : class -> class -> Prop).
Notation "x \in y" := (in_class x y) (at level 60).
Notation "x == y" := (eq_class x y) (at level 70).
Parameter
(eq_class_ax : forall a b, a == b <-> (forall x, x \in a <-> x \in b)).
Parameter
(cc_ax : forall (F: class -> Prop),
(forall y, F y -> M y) -> (exists x, forall y, y \in x <-> F y)).
(rs_ax : forall (F: class -> Prop),
(forall y, F y -> M y) -> (exists x, (M x) /\ forall y, y \in x <-> F y)).