On Wednesday, June 19, 2019 at 10:49:46 PM UTC-4, Mario Carneiro wrote:
>
> ...
>
You seem to be suggesting a massive revision and complication of set.mm
with a nonstandard notation, I assume in order to make it easier to
translate to type theory. Let's look at df-ral:
> One unsightly thing about the translation of df-ral is that it gets the
> type (set -> class) -> (set -> wff) -> wff; that is, *both* A and ph are
> allowed to refer to x, and occurrences are bound by it. This is a result of
> the straightforward definition:
>
> df-ral $a |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
>
Unsightly or not, this is the standard definition of A. x e. A ph in
essentially every set theory book, and there are no restrictions on A. The
string of symbols " A. x e. A ph" is merely an abbreviation of the longer
string " A. x ( x e. A -> ph )" to save some space on the page, nothing
more and nothing less. There is nothing deeper that I ever recall seeing,
at least in standard set-theory based mathematics.
I assume you would have no problems with the expression A. x ( x e. A -> ph
). If dealing with A. x e. A ph is problematic, can't you just expand it
to A. x ( x e. A -> ph ) before translation?
> Just from this definition, without knowing the purpose of A, one can see
> that A is in the scope of the quantifier so it should bind occurrences of
> x. In fact there isn't much difference between A and ph in that respect
>
That's right, it should behave the same as the A in A. x ( x e. A -> ph ),
where both A and ph are in the scope of the quantifier.
> . Compare that to this definition:
>
> df-ral2 $a |- ( A. x e. A ph <-> A. y ( y e. A -> [ y / x ] ph ) )
>
I don't recall seeing this definition anywhere. The difference in behavior
is going to be very confusing to someone used to the standard literature
definition.
>
> Now if there are free occurrences of x in A, they will not be bound at
> all. For example, A. x e. { x } ph is equivalent to A. x ph
>
if you use df-ral,
>
Yes, that is the literature definition.
> and equivalent to ph if you use df-ral2.
>
That is not the literature definition. The rules for figuring out the
scope of a variable are going to be more difficult, at the mercy of what
you may substitute for A at some point in the future. In the standard
definition the rule is very simple; x is bound in A. x x e. A ph because it
is also bound when its definition is expanded to A. x ( x e. A -> ph ).
> The automatic binding analysis for df-ral2 gives the expected type class
> -> (set -> wff) -> wff, that is, the restriction class is not participating
> in the binding behavior of x at all.
>
A goal of set.mm is to be faithful to the definitions in the literature,
not to "improve" them with something nonstandard with different behavior.
If df-ral2 truly has big advantages, I would almost prefer to introduce a
new symbol for it so as not to confuse the readers who are familiar with
standard set theory.
>From a practical point of view, df-ral is used about 200 times in set.mm,
meaning that each one of those uses is expecting the definition to be
precisely A. x ( x e. A -> ph ). The amount of work to retrofit it for
just this one definition would be huge.
Again, let me ask: How would your translation handle A. x ( x e. A -> ph
)? And why can't it do exactly the same when it sees A. x e. A ph?
Norm
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/ca52147f-161d-4cc5-ad10-a7fb368ec1de%40googlegroups.com.
