Let's try another approach to the question. Consider some complicated
definition like df-sum, and suppose that you don't know or care about the
exact way the definition has been stated. If you see sum_ k e. A B, would
you guess that occurrences of k in A are bound? free? both? Using the
"naive approach" where you just write down the most natural thing assuming
that k is disjoint from A, and then applying it to the general case without
change, leads to incoherence. df-ixp shows this. Unless you consciously
take steps to address it, you end up with things being both bound and free
and you can't be sure which unless you check the definition carefully.
Another data point: FOL doesn't have built in bounded quantifiers, but HOL
does, and dependent type theory has bounded quantifiers where the bounds
can actually have dependencies on variables, so this question meaningfully
comes up. In *every* case, such binding constructs do not bind the variable
x in A. For example, the dependent pi has the following typing rule:
Gamma |- A : Type Gamma, x : A |- B : Type
-----------------------------------------------
Gamma |- Pi x : A, B : Type
In fact, it's not even possible to have it any other way, since having the
typing rule be Gamma, x : A |- A : Type makes no sense.
My proposal is to say that, following this practice, all bound-like
constructs do not have the bound participate in itself. I claim that in 99%
of cases, A will already be disjoint from x so it makes no difference, and
in the other 1% of cases you want occurrences of x in A to be bound in an
outer scope, not the scope just introduced.
On Thu, Jun 20, 2019 at 5:59 AM Benoit <[email protected]> wrote:
> I agree with Norm. I think the current definitions (df-opab, df-ral...)
> are simple and consistent, and the changes proposed by Mario, if needed for
> the translation, should be done by the translation engine.
>
These changes cannot be done by the translation engine, because they affect
the semantics of the definitions. It's simply not the same definition, so
it wouldn't be valid for the translation to change one for the other
without potentially breaking theorems. Again, I think that in every place
where the definitions are different, the version we actually want is the
version I proposed. To be clear, I'm not saying the precise symbol string
that I gave for df-ral2 is nicer than the current one, I'm saying that the
resulting definition has the correct behavior. If you want to write the
definition in another way that is provably equivalent to my definition, I'm
fine with that.
> As for df-ral, yes, the current definition of "A. x e. A ph" will bind
> occurrences of x in A, and I think this makes it syntactically simpler,
> with nothing hidden. Most often, we do not want x to appear in A, but it
> looks like with Mario's proposal
> df-ral2 $a |- ( A. x e. A ph <-> A. y ( y e. A -> [ y / x ] ph ) ) $.
> if one uses an A containing occurences of x, the "machine" says "oh, you
> inadvertently used an A containing x, let me free the occurrences of x in A
> for you". The machine means well, but this looks like a hidden mechanism,
> and indeed it may cause much confusion. Additionally, df-ral2 is much
> harder to understand than df-ral.
>
Again, apply this reasoning to df-sum and tell me if it still applies. If
not, it's an inconsistent convention.
By the way, since we want to avoid as much as possible using df-ral with A
> containing x, what do you think of:
> $( ... Use ~ dfral whenever possible. (New usage is discouraged.) $)
> df-ral $a |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) ) $.
> ${ $d x A $. dfral $p |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) ) $=
> ? $. $}
>
I'm fine with that. In fact it should be sufficient to use the definition
only in dfral and cbvral (which will no longer need the $d x A requirement).
A side question about Mario's proposal
> df-opab3 $a |- { <. x , y >. | ph } = { z | E. x E. w ( z = <. x , w >.
> /\ [ w / y ] ph ) } $.
> It looks to me that this is incorrect: an instance of it is
> |- { <. x , x >. | x = 2 } = { z | E. x E. w ( z = <. x , w >. /\ [ w /
> x ] x = 2 ) }
> which yields, if I'm not mistaken,
> |- { <. x , x >. | x = 2 } = { z | E. x z = <. x , 2 >. }
> which is clearly false.
>
This is intended behavior. I think we should probably more or less ban the
use of { <. x , x >. | ph }, but when it is used, I want it to have this
behavior; BOTH x's are new bound variables, and they are always bound in
the order written, so the second x shadows the first and hence you can
rename the "outer" one to get { <. x , x >. | x = 2 } = { <. y , x >. | x =
2 }. I think that using { <. x , x >. | ph } to mean a subset of the
diagonal is a horrible hack because it implies a flexibility on the left of
a set comprehension that we don't actually have, and it breaks the pattern.
If you have the general rule "all multiple binders are bound from left to
right" you can guess this behavior without having to read the definition
(assuming you realize that { <. x , y >. | ph } is a syntax constructor in
the first place, rather than the composition of <. x , y >. and a
nonexistent { A | ph }.)
In short, while we have the capability to bundle variables to interesting
effect, the results are weird at best and broken at worst, and I want a
consistent method for being able to look at an arbitrary syntax constructor
and guess its binding behavior. In MM0 you explicitly declare the binding
behavior of a term constructor; in MM you don't, and it's implicitly
defined via the definition of the term. I think if we had explicit binding
declarations this wouldn't be a question, because there is only one
reasonable binding declaration for wral, irrespective of the actual
definition:
term wral {x: set} (A: class) (ph: wff x): wff;
This doesn't mean that A cannot depend on x, it means that references to x
in A are bound in an outer scope. It is questions like this, prompted by
the translation procedure, that lead me to the conclusion that wral has the
wrong binding structure.
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/CAFXXJSuh0D1xjqJQfPQ3JjVh2bg6%2B_neQFR7Z4TGzG52c_5-fw%40mail.gmail.com.
