Here's another data point: Look at
https://ncatlab.org/nlab/show/axiom+of+separation , and try to figure out
what happens if the bound depends on the new variable.
In set theory, the axiom scheme of separation aka specification states
> that, given any set X and any property P of the elements of X, there is a
> set
> {X|P}={a∈X|P(a)}
> consisting precisely of those elements of X for which P holds:
> a∈{X|P}↔a∈X∧P(a).
>
> Note that {X|P} is a subset of X.
>
Here they have explicitly notated this operation as {X | P} to prevent the
question of where binding occurs, since this has no binders in it; but P is
a predicate on elements of X, and so in the theorem
a∈{X|P}↔a∈X∧P(a)
we must have that a is a variable disjoint from X, or else we would be able
to derive a contradiction.
In the theory BZ (bounded Zermelo set theory), we can only use restricted
quantifiers. From the same link:
> For bounded separation aka restricted separation aka Δ_0-separation, P
> must be written in the language of first-order set theory and all
> quantifications must be guarded by a set: of the form ∀x∈A or ∃x∈A for some
> set A.
>
This has been written a little bit cavalierly (∀x∈A is only a syntax
fragment) but the order of quantifiers in "for some set A" should make it
clear that A cannot depend on x. Indeed, if we allowed it to, then A. x e.
{ x } would be considered a bounded quantification (because { x } is a
set), but it is equivalent to just A. x so it breaks BZ (it's as if the
restriction isn't even there).
>From https://ncatlab.org/nlab/show/ZFC :
> Separation/Specification/Comprehension: Given any predicate ϕ[x] in the
> language of set theory with the chosen free variable shown, if U is a set,
> then there is a set {x∈U|ϕ[x]}, the subset of U given by ϕ, whose elements
> are precisely those elements xx of U such that ϕ[x] holds.
>
Here it is made explicit that ϕ[x] depends on x but U does not.
>From https://plato.stanford.edu/entries/quantification/#ManSorQua :
> However, the move to a many-sorted language is largely a matter of
> convenience. Many-sorted quantification may be analyzed in terms of
> restricted one-sorted quantification. For each many-sorted language with n
> styles of variable, we may introduce a one-sorted language, which comes
> with a one-place predicate, S_i, for each sort in the many-sorted language.
> We may set out to translate each formula of the many-sorted language into a
> formula of the one-sorted language: we translate each identity in terms of
> a single identity predicate; a quantification on a variable of sort i, ∀x^i
> A, is replaced with a formula of the form ∀x(S_i x → A).
>
This is not a perfect comparison, but it's talking more directly about
simulating bounded quantification in FOL. Again, from the order of
quantifiers, we see that S_i is introduced before x is, so S_i is implied
to not depend on x, and it is explicitly acquiring a reference to x inside
the scope of the bound via "S_i x".
I maintain that this is the universal convention for bounds in quantifiers
and binders of all kinds.
Mario
On Thu, Jun 20, 2019 at 7:49 AM Mario Carneiro <[email protected]> wrote:
> 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/CAFXXJSvAVZFZF307WhRuSpRXJFDuv%3DeVr5Z%3DgE-TCgT4jYwqnw%40mail.gmail.com.
