stratified comprehension

Stream: new members

[Michael Beeson]

I am starting to develop Quine's New Foundations set theory (NF), but with intuitionistic logic, in Lean. To that end I
first had to learn how to use Lean at least a little. That done, I'm ready to proceed with the project. Now here is the difficulty:
NF has "stratified comprehension", which means we have a syntactic condition on the formula B to check before it is legal to form the set {x : x \in B}. I don't know how to do that in Lean and reading about metaprogramming scared me. (and I'm not too easily scared.) I have an equivalent finite axiomatization of intuitionistic NF (INF). There is an algorithm for translating a so-called "stratified" formula B so that you can construct {x : B(x)} from unions, intersections, and some other basic operations.
I was thinking I would just do that by hand whenever I need {x: B(x)}, and use the finite axiomatization in Lean. But it turns out to be quite a pain to do that by hand. So what I did so that I can get on with proofs is I put in the (known inconsistent!) full
comprehension axiom like this:

(comprehension: ∀f:M→Prop, ∀ z,(z∈ (setof f) ↔ f(z)))

(Here M is an instance of class Model in which the axioms are listed.) Then I can do stuff like this:

def FINITE:M := setof (λ x, ( ∀ w, (∀ u a, ((¬ (a ∈ u)) ∧ u ∈ w → (u ∪ (single a)) ∈ w)→ x ∈ w)))

lemma finite_members: ∀ x:M,
(
  (x ∈ (FINITE M)) ↔
   ∀ w, (∀ u a, ((¬ (a ∈ u)) ∧ u ∈ w →( u ∪ (single a)) ∈ w)→ x ∈ w))
   :=
  begin
    unfold FINITE,
    simp_rw ( comprehension  (λ (x : M), ∀ (w u a : M), (¬(a ∈ u) ∧ u ∈ w → u ∪ single a ∈ w) → x ∈ w)),
    ifinish,
  end

Then the plan would be to check the proof I want to check this way and then go back and replace
these applications of comprehension by constructions from the finite axiomatization.
For example, the set FINITE defined above using comprehension would eventually have to be constructed directly.

However, if anybody can show me a reasonable way to restrict the comprehension axiom to
stratified formulas or if anybody who is expert enough at metaprogramming will "just do it" that
would be wonderful. I could implement the algorithm easily in Python or C but then I would still have
to prove in Lean the lemmas saying that the resulting construction worked.

You can find out what "stratified" means at https://plato.stanford.edu/entries/quine-nf/