Formalize bounded formulas in iset.mm

[benjub]

Formalization of bounded formulas is ongoing in iset.mm / mathbox for BJ. It is needed to state certain axiom schemes of CZF (but also of bounded arithmetic, so it is not proper to intuitionism). This thread is mainly to gather future discussions in one place. Previous discussions took place in #1102 and #1152 , which I tried to summarize in the head comment of said mathbox (section beginning at http://us2.metamath.org/ileuni/wbd.html).

[benjub]

@digama0, you wrote in https://github.com/metamath/set.mm/pull/1152#issuecomment-538176766:

You don't need all those axioms. I would recommend:

|- Bdd x e. y
$d x y |- Bdd ph -> Bdd A. x e. y ph
|- ( ( Bdd ph /\ Bdd ps ) -> Bdd ( ph -> ps ) )
|- ( Bdd ph -> Bdd -. ph )
( ph <-> ps ) |- ( Bdd ph -> Bdd ps )

You should be able to derive everything else: boundedness of the other propositional connectives (true, false, and, or, iff), and boundedness of bounded exists.

Is this true in intuitionistic logic, where you don't have interdefinability of connectives (e.g. /\ and \/ in terms of -> and -. ) ? And why don't you need to posit "Bdd x = y" ? It is an atomic formula, after all.

And second: I forgot the DV condition you mention above, and I'm going to add it. Shoudn't we also require $d y ph $. ?

By the way: I rewrote all the axioms as inferences, and defined bounded classes in terms of bounded formulas, similarly to df-nfc in terms of nf (the merged #1176 is not yet on us2). But it appears I cannot prove |- A e. _V => |- Bddc A. Is it problematic ?

[digama0]

Oh, oops, indeed I was thinking classically there. You need additional axioms for and, or, and bounded exists in intuitionistic logic.

You don't need an axiom for x = y because it is equivalent to the formula A. z e. x z e. y /\ A. z e. y z e. x (alternatively, you can split that proof into a proof that x C_ y is bounded and x = y <-> x C_ y /\ y C_ x).

It's true that you cannot prove |- A e. _V => |- Bdd x e. A. In fact, I don't think you can sneak any class terms into a Bdd predicate directly. However, you can define Bddc A <-> Bdd x e. A and then you can just hold these as hypotheses to get a behavior like df-nfc. The problem is that |- A e. _V => |- Bdd x e. A has hidden the set bound on A. One property that we want bounded formulas to have is that the "size" of all things involved in the formula is controlled by the free variables of the formula.

If A e. V, then the size of the formula defining A is controlled by a variable that is enclosed in an unbounded existential quantifier (that is, E. x A. y ( y e. x <-> y e. A )), and this is not a bounded formula, it's Sigma_2. It's even higher than Sigma_1 because the reverse direction of that implication, E. x A. y ( y e. A -> y e. x ) is not even bounded in y, because y e. A is an arbitrary formula. This is exactly the problem with ~P x not being bounded, even though it is a set; it quantifies over all the subsets of x and these are not controlled by anything, hence we lose absoluteness and other nice properties of bounded formulas.

[david-a-wheeler]

This is really interesting.

Would it be possible to use this technique (or something like it) in set.mm and iset.mm to support expressing that a given variable is syntactically not free in some expression, e.g., SynNF x ph means "x is not syntactically free in ph"? In both databases we have df-nf ("not free"), but that is really "effectively not free" and is true for situations where it's NOT true for expressions where a variable is syntactically not free. It'd be nice to be able to express the traditional syntactical "x is not free in ph" without requiring significant additions to Metamath's language or big changes to the existing databases.

[digama0]

Yes, it is possible, but it requires lots of new axioms and so it probably wouldn't be welcome in set.mm. The axioms are conservative, because you can model SynNF x ph with F/ x ph.

[benjub]

Thanks @digama0. So it is not a problem (and it is actually expected) that |- A e. _V => |- Bdd x e. A. is not provable.

As for the definition of bounded classes, I first used |- Bddc A <-> Bdd x e. A but then I switched to |- Bddc A <-> A. x Bdd x e. A because it felt more in line with df-nfc (it should be on us2/ileuni by now). I think this does not change anything, given that all the axioms about bounded formulas are in inference form (as opposed to closed form), and |- A. x Bdd x e. A <=> |- Bdd x e. A . As you said, Bdd should be considered to bound any variable, that is, F/ x Bdd ph , but I think my definition is not problematic ?

By the way, it looks like the true formulas F/ x Bdd ph and Bdd Bdd ph are not provable, but it's not a problem, because Bdd is not a real predicate anyway and pertains more to the metalogic. Correct?

[benjub]

Concerning equality: your method (to prove |- Bdd x = y ) assumes extensionality. This is similar to defining equality using extensionality in a logic-without-equality. But in our formulation, using logic-with-equality, I think it is preferable to posit |- Bdd x = y , unless I'm missing something.

[david-a-wheeler]

@digama0 said:

The axioms are conservative, because you can model SynNF x ph with F/ x ph.

They aren't exactly the same. SynNF x x = x would be false, while F/ x x = x is true. I realize you're using a technical meaning for "model", but I mean "produces the same result". So A. x ( SynNF x ph -> F/ x ph ) but not the other way.

I certainly appreciate that @nmegill wants to minimize the number of axioms; makes sense to me too. But this wouldn't really an "axiom" in the usual sense, instead, it's a definition that happens to use $a to represent it. Providing a mechanism to describe "syntactically not free" doesn't change what the underlying system can do. In addition, "syntactically not free" is a pretty common case in mathematical notation.

I'd love to hear @nmegill 's thoughts about this.

[david-a-wheeler]

I created a separate issue to discuss adding syntactically-not-free SynNF to set.mm/iset.mm, since that's really a different issue. See: #1183