On Thu, Jun 20, 2019 at 1:40 AM Norman Megill <[email protected]> wrote:
> 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:
>
I use the language of type theory to make the point, but I am really
talking about the semantics of the metamath concept itself. The revision is
actually fairly small in terms of impact; for the most part it will be the
replacement of df-ral with dfral in various places and a change in $d's in
other places. I think that these definitions are written for "maximum
naivety" without regard to their behavior under metamath's "new behaviors"
involving name shadowing and bundling, with the hope that we just get the
right answer. I think that while this often works, we have to think
carefully about whether we actually get the result we want, and indeed what
result we intend in the first place.
> 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 cannot accept this justification. We aren't a set theory textbook;
metamath is not FOL. They are assuming variables have proper binding
semantics and metamath has its own methods for binding which differ from
FOL behaviors. I think that when pressed they will assume that x is a new
variable which is not bound in A, because otherwise weird and unforeseen
things will happen.
> 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?
>
That's exactly what I do, and yes I do have a problem with that expression.
Absent any information on A, I must assume that A can contain an x and it
will be bound. In the VAST majority of cases, when using A. x e. A ph, A is
actually not dependent on x. I would like that to be a requirement, but our
convention is to not have any restrictions on term constructors so the
definition should work even in that case.
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.
>
This is not the first time we have had this problem, and the solution is
simple. It is easy enough to say "see dfral for the usual definition" which
will say ( A. x e. A ph <-> A. x ( x e. A -> ph ) ), just as you expect,
with the perfectly reasonable constraint that $d x A.
> 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.
>
False. Like I said, it's a change of df-ral to dfral in all 200 cases, with
an added $d x A which is probably already there. My claim is that the
purpose of the A is to bound the quantification; it's not just another part
of the body of the expression. For a similar example, one would expect the
theorem ( A e. _V -> { x e. A | ph } e. _V ) to hold, but it currently
doesn't because A escapes its binding scope here, with the naive
definition. Show me one example where this kind of binding is desirable; I
can think of many examples where it is undesirable, and causes naive
definitions based on it to have the wrong behavior, like df-ixp.
Mario
--
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/CAFXXJSu1K8%2BpQ_SkAoapKJaGfbhNsN4maS0R6ToezC7rrxjThA%40mail.gmail.com.
