Proposal: define the not-free predicate

[Mario Carneiro]

Hi All,

This proposal originates from the definition checker v2.0 project, but it has more general application. I want to introduce definitions:

df-nf $a |- ( NF ( x , ph ) <-> A. x ( ph -> A. x ph ) )
df-nfc $a |- ( NF_ ( x , A ) <-> A. y NF ( x , y e. A ) )

which will replace the direct usage of |- ( ph -> A. x ph ) in all hb* theorems. This is obviously a large change, since these theorems are used across the whole database. The notation is modeled after the notation I have been using in my paper, but alternative suggestions are welcome. The parentheses and comma are unnecessary since it's a prefix axiom, but it looks a bit more natural that way IMO. The underscore in NF_ will be rendered as an underline, and is meant to resemble the similarity between [ A / x ] ph and [_ A / x ]_ B (but I think it is also unambiguous - if you prefer we could use the same symbol NF for both without issue).

Benefits:

* The expression (wi 1:wph (wal vx 1)) requires two steps and a backreference plus the proofs of x,ph, while (wnf vx wph) only requires one step. That's 2+ characters saved for every hb* step in every proof, which I'm certain more than pays for itself.

* Proving hb* theorems for classes is somewhat annoying due to the auxiliary dummy variable y. The definition of df-nfc hides this, so no such choices need to be made. In particular, the fact that hbeq and hbel have two dummies is one of the sources of non-disjoint substitutions mentioned in Norm's all-variables-disjoint test, which would be eliminated by this method. Also,
 (wi 1:(wcel (cv vy) cA) (wal vx 1)) requires 6 steps plus x,ph, so 5 steps are saved in this case, in addition to the 1 step saved by eliminating the extra dummy hypothesis in hb* theorems for classes.

* NF ( x , ph ) is a binding expression (not sure how best to show this in the notation, perhaps something like NF x : ph is better?), and I think that giving it a name will make the nested binders a bit more palatable, which is to say NF ( x , A. x ph ) is a bit easier to understand at a glance as meaning "x is not free in forall x, ph", while ( A. x ph -> A. x A. x ph ) consistently leaves seasoned logicians scratching their heads.

Mario

[David A. Wheeler]

On August 11, 2016 1:50:55 PM EDT, Mario Carneiro <di....@gmail.com> wrote:
>This proposal originates from the definition checker v2.0 project, but it
>has more general application. I want to introduce definitions:
>
>df-nf $a |- ( NF ( x , ph ) <-> A. x ( ph -> A. x ph ) )
>df-nfc $a |- ( NF_ ( x , A ) <-> A. y NF ( x , y e. A ) )
>
>which will replace the direct usage of |- ( ph -> A. x ph ) in all hb*
>theorems.

Cool! This seems very reasonable. I don't know if there are better syntaxes available, but creating definitions like these certainly makes sense.

I would keep thesm as 2 different definitions, as you've done.

>which is to say NF ( x , A. x ph ) is a bit easier to understand at a
>glance as meaning "x is not free in forall x, ph", while ( A. x ph ->
>A. x
>A. x ph ) consistently leaves seasoned logicians scratching their
>heads.

I think by itself that's a very good reason to do this, regardless of the other arguments such as smaller database size. To me, making statements understandable is extremely important. I'd rather have a larger database that can be understood, versus a small one that is a mystery. The reduction in size and complexity seem like icing on the cake.



--- David A.Wheeler

[Norman Megill]

On 8/11/16 1:50 PM, Mario Carneiro wrote:
> Hi All,
>
> This proposal originates from the definition checker v2.0 project, but
> it has more general application. I want to introduce definitions:
>
> df-nf $a |- ( NF ( x , ph ) <-> A. x ( ph -> A. x ph ) )
> df-nfc $a |- ( NF_ ( x , A ) <-> A. y NF ( x , y e. A ) )
>
> which will replace the direct usage of |- ( ph -> A. x ph ) in all hb*
> theorems. This is obviously a large change, since these theorems are
> used across the whole database. The notation is modeled after the
> notation I have been using in my paper, but alternative suggestions are
> welcome. The parentheses and comma are unnecessary since it's a prefix
> axiom, but it looks a bit more natural that way IMO. The underscore in
> NF_ will be rendered as an underline, and is meant to resemble the
> similarity between [ A / x ] ph and [_ A / x ]_ B (but I think it is
> also unambiguous - if you prefer we could use the same symbol NF for
> both without issue).

I have considered this on and off over the years and never felt happy
with it, so I never implemented it. A minor issue is that it doesn't
mean what the textbook usage of "free" means; for example, x is free in
x = x yet we have NF(x, x=x), so the notation is slightly misleading.
More importantly, this is a very nonstandard notation (meaning that
AFAIK it has never appeared in print anywhere) that would occur early in
the development, where we go out of our way to be faithful to the
literature and avoid any notation that isn't found in most logic and set
theory texts (minor exceptions being df-sb and df-mo, but even those
notations come from at least one logic book each). A person somewhat
familiar with standard logic and set notation would no longer able to
just jump into set.mm's elementary set theory without having to learn an
unfamiliar and nonstandard notation; in particular, a casual scan
through the elementary logic and set theory theorem lists would no
longer be completely familiar (notationally). It somehow feels like it
goes against the philosophy and/or purpose of set.mm.

If this was a specialized notation for a more advanced area of math, I
would probably have no problems with it. But it will permeate
everything and involve a major change to set.mm that would not be easy
to reverse. Non-standard notation can be off-putting to a beginner, who
is already struggling trying to correlate set.mm theorems to their
textbook notation.

(I have also never been thrilled with wikiproofs.org "not-free-in"
connective for the same reasons.)

This is something that we should put off at least until we have
significant feedback from several users.

> Benefits:
> * The expression (wi 1:wph (wal vx 1)) requires two steps and a
> backreference plus the proofs of x,ph, while (wnf vx wph) only requires
> one step. That's 2+ characters saved for every hb* step in every proof,
> which I'm certain more than pays for itself.
> * Proving hb* theorems for classes is somewhat annoying due to the
> auxiliary dummy variable y. The definition of df-nfc hides this, so no
> such choices need to be made. In particular, the fact that hbeq and hbel
> have two dummies is one of the sources of non-disjoint substitutions
> mentioned in Norm's all-variables-disjoint test, which would be
> eliminated by this method. Also,
> (wi 1:(wcel (cv vy) cA) (wal vx 1)) requires 6 steps plus x,ph, so 5
> steps are saved in this case, in addition to the 1 step saved by
> eliminating the extra dummy hypothesis in hb* theorems for classes.
> * NF ( x , ph ) is a binding expression (not sure how best to show this
> in the notation, perhaps something like NF x : ph is better?), and I
> think that giving it a name will make the nested binders a bit more
> palatable, which is to say NF ( x , A. x ph ) is a bit easier to
> understand at a glance as meaning "x is not free in forall x, ph", while
> ( A. x ph -> A. x A. x ph ) consistently leaves seasoned logicians
> scratching their heads.

Norm

[Mario Carneiro]

On Thu, Aug 11, 2016 at 10:56 PM, Norman Megill <n...@alum.mit.edu> wrote:

On 8/11/16 1:50 PM, Mario Carneiro wrote:

Hi All,

This proposal originates from the definition checker v2.0 project, but
it has more general application. I want to introduce definitions:

df-nf $a |- ( NF ( x , ph ) <-> A. x ( ph -> A. x ph ) )
df-nfc $a |- ( NF_ ( x , A ) <-> A. y NF ( x , y e. A ) )

which will replace the direct usage of |- ( ph -> A. x ph ) in all hb*
theorems. This is obviously a large change, since these theorems are
used across the whole database. The notation is modeled after the
notation I have been using in my paper, but alternative suggestions are
welcome. The parentheses and comma are unnecessary since it's a prefix
axiom, but it looks a bit more natural that way IMO. The underscore in
NF_ will be rendered as an underline, and is meant to resemble the
similarity between [ A / x ] ph and [_ A / x ]_ B (but I think it is
also unambiguous - if you prefer we could use the same symbol NF for
both without issue).

I have considered this on and off over the years and never felt happy with it, so I never implemented it.  A minor issue is that it doesn't mean what the textbook usage of "free" means; for example, x is free in x = x yet we have NF(x, x=x), so the notation is slightly misleading. More importantly, this is a very nonstandard notation (meaning that AFAIK it has never appeared in print anywhere) that would occur early in the development, where we go out of our way to be faithful to the literature and avoid any notation that isn't found in most logic and set theory texts (minor exceptions being df-sb and df-mo, but even those notations come from at least one logic book each).  A person somewhat familiar with standard logic and set notation would no longer able to just jump into set.mm's elementary set theory without having to learn an unfamiliar and nonstandard notation; in particular, a casual scan through the elementary logic and set theory theorem lists would no longer be completely familiar (notationally).  It somehow feels like it goes against the philosophy and/or purpose of set.mm.

Hehe, I found NF(x, ph) in print:
http://us2.metamath.org:88/ocat/model/model.pdf

More seriously, I think you overestimate the degree to which you are tracking "standard logic". Metamath is odd in some places; its oddity is maximal in the predicate calculus section, because that is where substitution is defined, and substitution is not done the same way in Metamath as in FOL. It is true that Metamath's notions are very subtly different from standard FOL, but I think that only makes it more important that they each be given names, and the names match the nearest equivalent from FOL. Forall is not a binder in Metamath, but we still call it forall. Substitution is not defined the same way as in FOL, but we still call it substitution. The not-free predicate is another core concept in Metamath, and to not give it a name means to not give users a place to look when they see these weird hypotheses in an unrelated theorem way later, such as cleqf. If there was an "NF" symbol they could at least use the symbol hints to find out about what this not-free stuff is all about. |- ( ph -> A. x ph ) showing up in a random theorem may not be unfamiliar and nonstandard *notation*, but it is absolutely an unfamiliar and nonstandard *concept*.

If this was a specialized notation for a more advanced area of math, I would probably have no problems with it.  But it will permeate everything and involve a major change to set.mm that would not be easy to reverse.  Non-standard notation can be off-putting to a beginner, who is already struggling trying to correlate set.mm theorems to their textbook notation.

Frankly, I've always found the foundations area to be the most complicated part, which is why my contributions are literally hundreds of times more away from introductory pred calc. I've always been afraid of that section, and I have absolutely no idea how you manage to prove theorems like ax10.

 

Mario

[Norman Megill]

> <http://set.mm>'s elementary set theory without having to learn an

> unfamiliar and nonstandard notation; in particular, a casual scan
> through the elementary logic and set theory theorem lists would no
> longer be completely familiar (notationally). It somehow feels like

> it goes against the philosophy and/or purpose of set.mm <http://set.mm>.

>
>
> Hehe, I found NF(x, ph) in print:
> http://us2.metamath.org:88/ocat/model/model.pdf
>
> More seriously, I think you overestimate the degree to which you are
> tracking "standard logic". Metamath is odd in some places; its oddity is
> maximal in the predicate calculus section, because that is where
> substitution is defined, and substitution is not done the same way in
> Metamath as in FOL. It is true that Metamath's notions are very subtly
> different from standard FOL, but I think that only makes it more
> important that they each be given names, and the names match the nearest
> equivalent from FOL. Forall is not a binder in Metamath, but we still
> call it forall.

I disagree. Yes, the axiom schemes were carefully devised so that we
can pretend that forall behaves like a binary operation at the scheme
level. But the object language is _exactly_ standard textbook FOL
object language. From that object language we could back-derive the
textbook FOL schemes with their concepts of binding and everything else,
and with exactly the same properties and behavior of the forall. Once
we instantiate a Metamath scheme to the object language, the forall is a
binder in exactly the same sense as it is for standard FOL, because the
instantiation _is_ exactly standard FOL. This is what some people don't
seem to get, and I wish I knew how to communicate it better. Metamath's
FOL schemes generate exactly and only the same actual theorems as the
more complicated textbook schemes involving free and bound variable
concepts. Once again, there is no difference in the object language!
(I assume you know that, but I'm repeating it for everyone else.)

Actually, there is no difference in the metalanguage either! Metamath's
axiom schemes _are_ standard FOL theorem schemes using a subset of the
standard textbook FOL metalanguage (although not vice-versa). If our
axiom schemes are viewed as FOL schemes (which is what they really are),
forall is a binder in the same way as it is in standard FOL metalanguage
because it _is_ standard FOL metalanguage. If viewed as a computer
language, it _behaves_ like a binary operation because of the particular
subset of textbook FOL metalanguage that we chose for our axiom schemes.

> Substitution is not defined the same way as in FOL, but
> we still call it substitution.

Our (proper) substitution, in the form of dfsb7, is exactly the formula
used by Quine. And it is exactly equivalent to the recursive
definition. We call it substitution because it _is_ substitution.

> The not-free predicate is another core
> concept in Metamath, and to not give it a name means to not give users a
> place to look when they see these weird hypotheses in an unrelated
> theorem way later, such as cleqf. If there was an "NF" symbol they could
> at least use the symbol hints to find out about what this not-free stuff
> is all about. |- ( ph -> A. x ph ) showing up in a random theorem may
> not be unfamiliar and nonstandard *notation*, but it is absolutely an
> unfamiliar and nonstandard *concept*.

It is explained clearly in many places. Even without an explanation, I
can't believe that a competent logician couldn't figure out what the
idiom |- ( ph -> A. x ph ) is trying to say. For others it's a simple
pattern that is easy to learn and recognize. I don't see how it's
harder to learn that pattern as it is to learn the NF definition.

No one has ever complained to me about not understanding |- ( ph -> A. x
ph ) in all the years set.mm has existed. They have complained about
many other things but not this. I think that is because it is explained
clearly.

I think you are making a mountain out of molehill that will end up
polluting set.mm with nonstandard NF symbols that don't exist in any
book, unlike _every symbol_ in early set.mm. Right now, anyone familiar
with textbook FOL and intro set theory, but unfamiliar with Metamath,
can casually browse the theorem list and recognize the symbols in the
early theorem list, making it attractive to them. Unfamiliar,
nonstandard symbols may make or break that person's interest in looking
into Metamath more. On the FOM list you've seen complaints that other
proof languages look like computer garbage and would never be considered
seriously for a math journal proof, and I think that's largely because
symbols are unfamiliar and nonstandard.

If the idiom |- ( ph -> A. x ph ) such a problem, we can just put an
explanatory comment in every theorem that uses this idiom, as many of
them already have.

> If this was a specialized notation for a more advanced area of math,
> I would probably have no problems with it. But it will permeate

> everything and involve a major change to set.mm <http://set.mm> that

> would not be easy to reverse. Non-standard notation can be
> off-putting to a beginner, who is already struggling trying to

> correlate set.mm <http://set.mm> theorems to their textbook notation.

>
>
> Frankly, I've always found the foundations area to be the most
> complicated part, which is why my contributions are literally hundreds
> of times more away from introductory pred calc. I've always been afraid
> of that section, and I have absolutely no idea how you manage to prove
> theorems like ax10.

One of the reasons I was able to prove ax10 is that at that point in the
development, a very small set of defined notions is used by previous
theorems. There is a limit to the number of different symbols I can
intensely focus on at one time. If I had to mentally expand NFs all the
time, I don't know if I would have achieved it. Believe it or not, even
E. was stressful because I constantly had to mentally expand it to ~ A.
~, so few ax10 lemmas have E. in them.

People are different in their mental capabilities, and I can manipulate
in my head only n different symbols at a time where maybe as a wild
guess n ~= 7. Some people's n is smaller, A child I'm tutoring in math
can multiply 2 large numbers expressed explicitly, but "simplifying" it
with scientific notation is something he is struggling to get. Your n
is probably larger than most people's so you may not appreciate the
intimidation some people experience when seeing an unfamiliar math symbol.

Norm

[Mario Carneiro]

On Fri, Aug 12, 2016 at 8:46 PM, Norman Megill <n...@alum.mit.edu> wrote:

On 8/11/16 11:11 PM, Mario Carneiro wrote:

More seriously, I think you overestimate the degree to which you are
tracking "standard logic". Metamath is odd in some places; its oddity is
maximal in the predicate calculus section, because that is where
substitution is defined, and substitution is not done the same way in
Metamath as in FOL. It is true that Metamath's notions are very subtly
different from standard FOL, but I think that only makes it more
important that they each be given names, and the names match the nearest
equivalent from FOL. Forall is not a binder in Metamath, but we still
call it forall.

I disagree.  Yes, the axiom schemes were carefully devised so that we can pretend that forall behaves like a binary operation at the scheme level.  But the object language is _exactly_ standard textbook FOL object language.  From that object language we could back-derive the textbook FOL schemes with their concepts of binding and everything else, and with exactly the same properties and behavior of the forall.  Once we instantiate a Metamath scheme to the object language, the forall is a binder in exactly the same sense as it is for standard FOL, because the instantiation _is_ exactly standard FOL.  This is what some people don't seem to get, and I wish I knew how to communicate it better.  Metamath's FOL schemes generate exactly and only the same actual theorems as the more complicated textbook schemes involving free and bound variable concepts.  Once again, there is no difference in the object language! (I assume you know that, but I'm repeating it for everyone else.)

Sometimes I worry that you have not critically read the models paper, because some of the things it talks about are a bit different from your intuition, just as much as it is different from FOL. As I see it, metamath is not FOL, and it is not a metalanguage over FOL either. It however acts very similar to one, and you can be forgiven for thinking that this is what's under the hood. My claim is that there is no object language machinery under metamath. Instead, there is a metamachinery that acts in every way like there is an object language below, even though there isn't (necessarily). Once you free yourself of this notion, you begin to understand why, for example, unbundling is not necessarily a theorem, even though it is a true statement in all models that have an object language underneath.

The reason it acts so much like a scheme language over FOL is because of the axioms of set.mm. If it weren't for these, this wouldn't be the case, and in particular, when you are considering subsystems or justifications of the axioms, this may not be the case. The part which is not like a scheme language is the fact that the freshness relation may not be not-equal for sets. This has hampered my ability to translate these statements into FOL according to your original suggestion, although I think I'm getting close to something workable.

Actually, there is no difference in the metalanguage either!  Metamath's axiom schemes _are_ standard FOL theorem schemes using a subset of the standard textbook FOL metalanguage (although not vice-versa).  If our axiom schemes are viewed as FOL schemes (which is what they really are), forall is a binder in the same way as it is in standard FOL metalanguage because it _is_ standard FOL metalanguage.  If viewed as a computer language, it _behaves_ like a binary operation because of the particular subset of textbook FOL metalanguage that we chose for our axiom schemes.

This I can agree with. Metamath theorems concern statements that are true in every model, and FOL metalanguage is one such model, so you can soundly map Metamath statements into FOL schemes, once you provide the necessary auxiliary data stating that e.g. set is the collection of set variables, and wff is the collection of expressions of type bool with any number of free variables. But without this auxiliary data, you are hard-pressed to look at a metamath database and say, "oh, this here is a binder" just from the way it was defined. If you take off your FOL glasses, you see a syntax axiom "A. x ph" and infer that it has type (A, B) -> B. But is it a binder? Is the first argument bound in the second, or the second bound by the first, or neither? These are not easy questions.

Actually, I'm not sure FOL metalanguage is a model for Metamath. The natural model I gave in my paper is almost a FOL metalanguage, but it contains wff/class variables even at the object level, which is not possible in standard FOL.

Substitution is not defined the same way as in FOL, but
we still call it substitution.

Our (proper) substitution, in the form of dfsb7, is exactly the formula used by Quine.  And it is exactly equivalent to the recursive definition.

This is not true. There are certain things our substitution can do which the usual one can't, like having wff or class metavariables in it. And there are things their definition can do and ours can't, like substitute with proper class arguments. Just because it uses the same symbols doesn't mean it means the same thing, because the foundations are slightly different.
 

The not-free predicate is another core
concept in Metamath, and to not give it a name means to not give users a
place to look when they see these weird hypotheses in an unrelated
theorem way later, such as cleqf. If there was an "NF" symbol they could
at least use the symbol hints to find out about what this not-free stuff
is all about. |- ( ph -> A. x ph ) showing up in a random theorem may
not be unfamiliar and nonstandard *notation*, but it is absolutely an
unfamiliar and nonstandard *concept*.

It is explained clearly in many places.  Even without an explanation, I can't believe that a competent logician couldn't figure out what the idiom |- ( ph -> A. x ph ) is trying to say.  For others it's a simple pattern that is easy to learn and recognize.  I don't see how it's harder to learn that pattern as it is to learn the NF definition.

It wouldn't have to be "explained clearly in many places" if it were explained clearly in one central location, that is easy to find with a link on every page.

 

No one has ever complained to me about not understanding |- ( ph -> A. x ph ) in all the years set.mm has existed.  They have complained about many other things but not this.  I think that is because it is explained clearly.

It's not impossible to understand, it just takes a minute or two. But I think if "NF" shows up in the hypothesis and "not free" shows up in the theorem comment, this can be cut down to a few seconds. In this case the name makes it *easier* to understand, not harder, because it associates the hypothesis with the term "not free", which may not otherwise be obvious without training (I have never ever seen any source use this idiom to describe not-freeness except metamath).

If you think it will help, we could just go whole-hog with the notation and write

|- ( x Is-Not-Free-in ph )

instead of NF ( x , ph ), but that would be a bit outside of our usual naming standards.

I think you are making a mountain out of molehill that will end up polluting set.mm with nonstandard NF symbols that don't exist in any book, unlike _every symbol_ in early set.mm.  Right now, anyone familiar with textbook FOL and intro set theory, but unfamiliar with Metamath, can casually browse the theorem list and recognize the symbols in the early theorem list, making it attractive to them.  Unfamiliar, nonstandard symbols may make or break that person's interest in looking into Metamath more.  On the FOM list you've seen complaints that other proof languages look like computer garbage and would never be considered seriously for a math journal proof, and I think that's largely because symbols are unfamiliar and nonstandard.

It's not just about symbols. ax-11 takes a good half hour at least to understand if you encounter it for the first time, despite it not using any new symbols. (I mean understand why it's written like that, and what are all the parts of the expression there for.)

Also, I have heard exactly such complaints for metamath, concerning $d, not so much because it's a difficult symbol, but because it's a difficult concept. (Of course I don't see it as a particularly difficult concept, but that's the main source of friction from established logicians.) By comparison NF(x, ph) is much closer to what they are used to, and the fact that this is not syntactic not-freeness but instead not-freeness up to equivalence is really inessential and should be emphasized less.

 

One of the reasons I was able to prove ax10 is that at that point in the development, a very small set of defined notions is used by previous theorems.  There is a limit to the number of different symbols I can intensely focus on at one time.  If I had to mentally expand NFs all the time, I don't know if I would have achieved it.  Believe it or not, even E. was stressful because I constantly had to mentally expand it to ~ A. ~, so few ax10 lemmas have E. in them.

What I meant is, when you remove a metamath axiom, particularly in pred calc, you are thrown adrift in a world where none of the expressions necessarily mean what you think they mean, because of all the stuff I've mentioned. Once the full groundwork is laid, I have confidence in the meaning of everything, because I have a good model in mind, but if something core is missing in the early stages it is not obvious how to get it back. (Consider your current difficulty with ax-14c.)
 

People are different in their mental capabilities, and I can manipulate in my head only n different symbols at a time where maybe as a wild guess n ~= 7.  Some people's n is smaller,  A child I'm tutoring in math can multiply 2 large numbers expressed explicitly, but "simplifying" it with scientific notation is something he is struggling to get.  Your n is probably larger than most people's so you may not appreciate the intimidation some people experience when seeing an unfamiliar math symbol.

Haha, I don't have a large n either, I just pull other things from my environment as necessary. Your n ~= 7 reminds me of https://en.wikipedia.org/wiki/The_Magical_Number_Seven,_Plus_or_Minus_Two, although that may not be a coincidence.

Part of the reason I can understand a theorem like exlimi easily is because I parse the |- ( ph -> A. x ph ) as a unit, I don't think specifically about phi implying for all x, phi and why that's relevant. I'm sure you do too, and any reader will at some point need to learn this in order to read the proofs without getting bogged down. It seems to me we have all the criteria for a definition met: it's a unified and important concept, it is used extremely frequently, and it has a common name (even though it is not often referred to by a symbol).

Finally, what I didn't mention is that the real reason I introduced a name for this was to point a $j statement at it, so it would have to exist one way or another (similar to the situation with CondEq). It's just that in this case the definition actually seems like it would be really useful, and shoving it into a corner seems like a waste.

Mario

[David A. Wheeler]

Norm:

> > It is explained clearly in many places. Even without an explanation, I
> > can't believe that a competent logician couldn't figure out what the idiom
> > |- ( ph -> A. x ph ) is trying to say.

I'm not a professional logician, never mind a competent one, so
perhaps I can be forgiven that I needed a little time the first time :-).

Mario:

> It wouldn't have to be "explained clearly in many places" if it were
> explained clearly in one central location, that is easy to find with a link
> on every page.

This reminded me of something.
The "set.mm" file has embedded in it a lot of text that discusses
conventions, e.g., see the "3. Convention: ..." section.
However, I think many readers will *only* view the generated HTML,
and not the source "set.mm" file, in the same way that many people
will read a generated PDF and not the source LaTeX file.
That means that many of these conventions are NOT directly visible to readers.

I think the top-level page needs a new "conventions" subsection
that discusses various conventions used in MPE (naming, constructs, etc.).
Whether or not "NF" is created, there are many conventions that aren't
obvious, especially if you don't read the set.mm source file. Moving some of
that information from set.mm to the main HTML page would make it much more visible
to new readers.

--- David A. Wheeler

[Norman Megill]

> the axioms of set.mm <http://set.mm>. If it weren't for these, this

> wouldn't be the case, and in particular, when you are considering
> subsystems or justifications of the axioms, this may not be the case.
> The part which is not like a scheme language is the fact that the
> freshness relation may not be not-equal for sets. This has hampered my
> ability to translate these statements into FOL according to your
> original suggestion, although I think I'm getting close to something
> workable.

Sorry, when I said Metamath I meant the set.mm axiom schemes. Bad
habit. I agree with you w.r.t. the Metamath language.

More importantly, I meant the set.mm axiom schemes independent of
Metamath i.e. the set.mm axiom schemes as viewed by a mathematician.
The Metamath language is just a vehicle to implement and manipulate
them. The mm solitaire applet is a quite different vehicle that can
also manipulate them.

I'll use the terminology "set.mm axiom schemes" to mean these as FOL
schemes independent of the Metamath language. (Conversely, if need be
I'll use "set.mm axioms" to mean those implemented in the Metamath
language.)

As for the object language, again I meant actual FOL theorems that can
be instantiated from these schemes - as a mathematician would do. That
object language is the same as the object language of standard FOL schemes.

And when I say FOL, I informally mean FOL= (FOL+equality).

>
> Actually, there is no difference in the metalanguage either!
> Metamath's axiom schemes _are_ standard FOL theorem schemes using a
> subset of the standard textbook FOL metalanguage (although not
> vice-versa). If our axiom schemes are viewed as FOL schemes (which
> is what they really are), forall is a binder in the same way as it
> is in standard FOL metalanguage because it _is_ standard FOL
> metalanguage. If viewed as a computer language, it _behaves_ like a
> binary operation because of the particular subset of textbook FOL
> metalanguage that we chose for our axiom schemes.
>
>
> This I can agree with. Metamath theorems concern statements that are
> true in every model, and FOL metalanguage is one such model, so you can
> soundly map Metamath statements into FOL schemes, once you provide the
> necessary auxiliary data stating that e.g. set is the collection of set
> variables, and wff is the collection of expressions of type bool with
> any number of free variables. But without this auxiliary data, you are
> hard-pressed to look at a metamath database and say, "oh, this here is a
> binder" just from the way it was defined. If you take off your FOL
> glasses, you see a syntax axiom "A. x ph" and infer that it has type (A,
> B) -> B. But is it a binder? Is the first argument bound in the second,
> or the second bound by the first, or neither? These are not easy questions.

You are talking about the Metamath language and its models. But what I
mean is binding as it would be described by a user of standard FOL
schemes. Thus in ( x = y -> E. x x = y ), they would consider the first
x free, the 2nd x bound, and both y's free. Of course this binding is
not a notion built into the set.mm axiom schemes, nor do we need it for
manipulating these schemes.

For users of the standard FOL schemes, the notion propagates to the
object language: in ( v_0 = v_1 -> E. v_0 v_0 = v_1 ), the first v_0 is
free and the 2nd is bound; both v_1's are free. These notions are
useful for manipulating the object language directly, as many proof
languages do. But I would argue that they are not primitive notions of
the object language - otherwise, how could set.mm's axiom schemes
generate them without such notions?

BTW the proof that set.mm's axiom schemes generate the same object
language as standard FOL is Tarski's, whose system is a subset of
set.mm's schemes.

>
> Actually, I'm not sure FOL metalanguage is a model for Metamath. The
> natural model I gave in my paper is almost a FOL metalanguage, but it
> contains wff/class variables even at the object level, which is not
> possible in standard FOL.

Right, there are no wff or class variables at the object level in
standard FOL. In principle, class notation must be eliminated first
before we can generate object-level statements, although there are some
shortcuts that can be used like inferring v_0 = v_0 from A = A.

>
>
> Substitution is not defined the same way as in FOL, but
> we still call it substitution.
>
>
> Our (proper) substitution, in the form of dfsb7, is exactly the
> formula used by Quine. And it is exactly equivalent to the
> recursive definition.
>
>
> This is not true. There are certain things our substitution can do which
> the usual one can't, like having wff or class metavariables in it. And
> there are things their definition can do and ours can't, like substitute
> with proper class arguments. Just because it uses the same symbols
> doesn't mean it means the same thing, because the foundations are
> slightly different.

When I say proper substitution, I mean at the FOL level as defined in
standard logic textbooks. Their recursive algorithm is precisely
equivalent to df-sb. There is nothing textbook substitution can do that
df-sb can't and vice-versa.

Substitution of classes for set variables (df-sbc) is rarely defined in
set theory books. Quine's definition at proper classes is as far as I
can tell unique, definitely not standard, and I don't recall that he
even uses it for anything. Actually I don't recall seeing any df-sbc
equivalent other than Quine's. Most set theory texts informally just
use df-sb where the substituting term is always a set and thus can
replace the first set variable in df-sb.

I don't know what you mean by having wff variables in it.

>
>
> The not-free predicate is another core
> concept in Metamath, and to not give it a name means to not give
> users a
> place to look when they see these weird hypotheses in an unrelated
> theorem way later, such as cleqf. If there was an "NF" symbol
> they could
> at least use the symbol hints to find out about what this
> not-free stuff
> is all about. |- ( ph -> A. x ph ) showing up in a random
> theorem may
> not be unfamiliar and nonstandard *notation*, but it is
> absolutely an
> unfamiliar and nonstandard *concept*.
>
>
> It is explained clearly in many places. Even without an
> explanation, I can't believe that a competent logician couldn't
> figure out what the idiom |- ( ph -> A. x ph ) is trying to say.
> For others it's a simple pattern that is easy to learn and
> recognize. I don't see how it's harder to learn that pattern as it
> is to learn the NF definition.
>
>
> It wouldn't have to be "explained clearly in many places" if it were
> explained clearly in one central location, that is easy to find with a
> link on every page.
>
>
> No one has ever complained to me about not understanding |- ( ph ->

> A. x ph ) in all the years set.mm <http://set.mm> has existed. They

> have complained about many other things but not this. I think that
> is because it is explained clearly.
>
>
> It's not impossible to understand, it just takes a minute or two. But I
> think if "NF" shows up in the hypothesis and "not free" shows up in the
> theorem comment, this can be cut down to a few seconds. In this case the
> name makes it *easier* to understand, not harder, because it associates
> the hypothesis with the term "not free", which may not otherwise be
> obvious without training (I have never ever seen any source use this
> idiom to describe not-freeness except metamath).
>
> If you think it will help, we could just go whole-hog with the notation
> and write
>
> |- ( x Is-Not-Free-in ph )
>
> instead of NF ( x , ph ), but that would be a bit outside of our usual
> naming standards.

Is-Not-Free-in is used at wikiproofs.org, and I never liked it. Believe
me, I have thought about this for many years. It's a highly subjective
thing, maybe a personality quirk I have, but everything about it feels
like it goes against the grain of simplicity and faithfulness to math
that set.mm (at least the early parts) is all about. It is not
standard. Unlike other definitions, it doesn't buy significant space
savings. It is not even accurate about its claim, since x is free in x
= x. It feels like an ugly hack.

I wouldn't be so concerned if it was something in a specialized section
of set.mm. I would greatly dislike having it permeate all of set.mm
from the beginning. What I will do is put a link explaining |- ( ph ->
A. x ph ) in every theorem comment using it. The intended human purpose
of NF is to "explain" (inaccurately) what |- ( ph -> A. x ph ) is
supposed to mean, and there's no reason an accurate explanation can't be
linked to from the comment.

>
> I think you are making a mountain out of molehill that will end up

> polluting set.mm <http://set.mm> with nonstandard NF symbols that

> don't exist in any book, unlike _every symbol_ in early set.mm

> <http://set.mm>. Right now, anyone familiar with textbook FOL and

> intro set theory, but unfamiliar with Metamath, can casually browse
> the theorem list and recognize the symbols in the early theorem
> list, making it attractive to them. Unfamiliar, nonstandard symbols
> may make or break that person's interest in looking into Metamath
> more. On the FOM list you've seen complaints that other proof
> languages look like computer garbage and would never be considered
> seriously for a math journal proof, and I think that's largely
> because symbols are unfamiliar and nonstandard.
>
>
> It's not just about symbols. ax-11 takes a good half hour at least to
> understand if you encounter it for the first time, despite it not using
> any new symbols. (I mean understand why it's written like that, and what
> are all the parts of the expression there for.)

ax-11 is a technical axiom that is logically redundant but needed for
metalogical completeness. I assume by understanding it you mean not to
convince yourself that it holds in FOL= (that isn't too hard to see, I
hope) but to understand what its purpose is, and that is more difficult
but arguably not really necessary.

It's the same situation as with some prop calc axiomatizations where the
axioms aren't necessarily intuitive. How would you explain the meaning
of ax-meredith to someone? The only meaning is in the fact that it
works. Maybe by studying the proofs you could identify the purpose of
some pieces, but overall it will probably remain a mystery at a high
level. (Actually I have some lecture notes by Ted Ulrich who did
identify common properties needed by sole axioms like Meredith's and
even found some new ones for various prop calc fragments.)

Actually for ax-11 (vs. say ax-12, which is more mysterious) the purpose
is to provide a substitution property. It is nearly identical to the
two references provided and even shows up informally on the 2nd page of
Tarski's paper, where he explains it. All object-language instances of
ax-11 can be proved in Tarski's system, so he doesn't need it, but we
need it for metalogical completeness.

>
> Also, I have heard exactly such complaints for metamath, concerning $d,
> not so much because it's a difficult symbol, but because it's a
> difficult concept. (Of course I don't see it as a particularly difficult
> concept, but that's the main source of friction from established
> logicians.)

I can't help but think they have other reasons for disliking Metamath
and use this as an excuse. The concept of a variable not occurring in a
formula is about as simple as it gets. Obviously they don't want to put
in even a minimal effort, for whatever reason.

Have you pointed them to Tarski's system and papers? Would they feel
that the $d in Tarski's system is hard to understand? Tarski's whole
point was to make a system _easier_ to understand than the standard FOL
axiomatization, since the concept of a variable not occurring in a
formula is much simpler than "not free" in a formula.

Would they be have trouble understanding the Tarski subset of set.mm's
axiom schemes? If they can manage those, then they can be told that the
4 extra axioms (ax-6,7,11,12) can be ignored for the purpose of
understanding the logic; they are merely technical devices needed to
achieve our so-called "metalogical completeness".

Yeah, I think it vaguely came from a psychology course I took. I feel
like even less than 5 before coffee in the morning, and rarely if ever
feel like a 9.

[Norman Megill]

I had nearly forgotten about that section, which was written well before
a web site was even conceived of. It still applies. I'll add a to-do
list item to put it on the site.

Speaking of which, mmset.html has grown to be rather huge compared to
conventional web pages, and I have considered breaking it up, but at the
same time there is an advantage to having everything in one place
instead of being scattered about in various pages that are likely to be
missed unless you know what you are looking for. I kind of like having
all of the general info related to set.mm on one page, with breakoff
pages only for special topics like the complex numbers. Does the size
bother anyone?

Norm

[Mario Carneiro]

Now this is an interesting thought. I've never attempted to consider set.mm without metamath, although I have obviously spent a lot of time on metamath without set.mm. The reason is simply because I don't find the equivalence of set.mm and it's FOL-ized version to be at all simple or obvious, even though it appears so at first glance. (This is the downside of using suggestive notation for almost, but not quite, the same concept.) I have no issues with the claim that FOL-ized set.mm is a valid axiomatization of FOL metatheory.

 

You are talking about the Metamath language and its models.  But what I mean is binding as it would be described by a user of standard FOL schemes.  Thus in ( x = y -> E. x x = y ), they would consider the first x free, the 2nd x bound, and both y's free.  Of course this binding is not a notion built into the set.mm axiom schemes, nor do we need it for manipulating these schemes.

For users of the standard FOL schemes, the notion propagates to the object language:  in ( v_0 = v_1 -> E. v_0 v_0 = v_1 ), the first v_0 is free and the 2nd is bound; both v_1's are free.  These notions are useful for manipulating the object language directly, as many proof languages do.  But I would argue that they are not primitive notions of the object language - otherwise, how could set.mm's axiom schemes generate them without such notions?

The concept of bound variables is built into standard FOL, because it is needed to define alpha-renaming. I explained it this way in discussions at CICM: In FOL, substitution is always possible but not always direct; in metamath substitution is always direct but not always possible. In this case a FOL substitution may not be direct because it needs to perform a renaming step (and there are ways to make this not involve any choices, such as de Bruijn indices), while in Metamath a substitution that would otherwise cause bound variable capture can be blocked by a $d violation.

 

Right, there are no wff or class variables at the object level in standard FOL.  In principle, class notation must be eliminated first before we can generate object-level statements, although there are some shortcuts that can be used like inferring v_0 = v_0 from A = A.

I'm not sure how those statements are even related to each other, besides both being true. I hope that doesn't come up in any FOL translations!
 

        Substitution is not defined the same way as in FOL, but
        we still call it substitution.


    Our (proper) substitution, in the form of dfsb7, is exactly the
    formula used by Quine.  And it is exactly equivalent to the
    recursive definition.


This is not true. There are certain things our substitution can do which
the usual one can't, like having wff or class metavariables in it. And
there are things their definition can do and ours can't, like substitute
with proper class arguments. Just because it uses the same symbols
doesn't mean it means the same thing, because the foundations are
slightly different.

When I say proper substitution, I mean at the FOL level as defined in standard logic textbooks.  Their recursive algorithm is precisely equivalent to df-sb.  There is nothing textbook substitution can do that df-sb can't and vice-versa.

Substitution of classes for set variables (df-sbc) is rarely defined in set theory books.  Quine's definition at proper classes is as far as I can tell unique, definitely not standard, and I don't recall that he even uses it for anything.  Actually I don't recall seeing any df-sbc equivalent other than Quine's.  Most set theory texts informally just use df-sb where the substituting term is always a set and thus can replace the first set variable in df-sb.

I don't know what you mean by having wff variables in it.

I mean that [ x / y ] ph is a valid wff, and not an abbreviation for a wff. In FOL [ x / y ] ph is an abbreviation for a replacement process, which is always applied immediately to result in an object level wff that does not contain any [x/y] in it. In our case, the recursive process can get stuck whenever it hits a metavariable, and this is okay, while in FOL that doesn't happen because there are no metavariables.

 

You can marginalize Quine's definition if you want, but it remains that Metamath cannot directly handle recursive definitions without "accidentally" introducing non-eliminable metavariables such as the "ph" wff metavariable.

An unfortunate fact that we have to live with is that regular mathematics is not entirely done with symbols. They use words as well, and we have to make symbols for them. A simple symbol like "NF" indicates this better than the expanded definition, in the same way that "E." is easier to read than "-. A. -." when reading an expression. On the other hand, the phrase "not free in" *is* standard, and needs to be written in the space around such assertions in conventional logic.

 

  Unlike other definitions, it doesn't buy significant space savings.

At least this claim is refutable: there are two occurrences of ph in the original expression and one in the definition, so if ph is large there can be significant space savings.

 

  It is not even accurate about its claim, since x is free in x = x.  It feels like an ugly hack.

This is what I meant by "we need to de-emphasize this". This *really* isn't an important distinction, and stressing it seems like a red herring when there are plenty of other actual differences for the reader to worry about. NF(x, ph) is true *exactly* when x is not free in ph in the conventional sense, up to equivalence of expressions. It would be rather more weird if

$e |- ( ph <-> ps )

$a |- ( NF ( x , ph ) <-> NF ( x , ps ) )

didn't hold, because then <-> would not be an equality.

 

I wouldn't be so concerned if it was something in a specialized section of set.mm.  I would greatly dislike having it permeate all of set.mm from the beginning.  What I will do is put a link explaining |- ( ph -> A. x ph ) in every theorem comment using it.  The intended human purpose of NF is to "explain" (inaccurately) what |- ( ph -> A. x ph ) is supposed to mean, and there's no reason an accurate explanation can't be linked to from the comment.

To be more precise about usage (I've already worked it out for the primitive operations):

* NF is introduced in section ""Pure" (equality-free) predicate calculus axioms ax-5, ax-6, ax-7, ax-gen" (wouldn't it be nice if there were a shorter name for this section?), right after df-ex. But it is not used except to prove the forward direction of the definition.

* Theorem nfth proves the equivalent of hbth in this section, as well as nfxfr alongside hbxfrbi. No existing theorems are removed or modified.

* Section ax-17 proves theorem nfd which is the equivalent.

* Starting in section ax-4, the reverse direction of the definition can be proven, so nf* versions of the hb* theorems are derived. After hbn and hbim, hbal, hba1 the derivations become algorithmic, so at this point we might want to consider dropping the old versions of hypothesis builders for advanced definitions such as hb3an.

* nfae and nfnae are versions of hbae, hbnae which have unusual derivations, as well as one for df-sb.

* Enter the class section, where nfsab1 is a version of hbab1.
* After this section, a new section "Class form not-free predicate" is introduced, which defines df-nfc as well as nfab1, which is a version of nfsab1 using NF_ instead of NF. In this section all remaining primitive hypothesis builders are added.

This is what I've done so far. No existing theorems have been modified or removed yet. What I would like to do:

* After section ax-4, make a new section collecting all theorems that so far have been proven with a HB hypothesis, and replace with NF. The original theorems are left as-is, but the naming convention for these theorems is changed to have a suffix "h". That is, exlimi becomes exlimih, and the new exlimi uses NF instead.

* Very popular theorems after this point in the pred calc section are defined with both versions, or theorems that use the hypothesis literally (as in, they make use of the particular shape (ph -> A. x ph) ). Less popular theorems, that only need it to satisfy some other NF assumption, are changed to only use NF.

* After the class builder section, NF and NF_ are used exclusively. The hb* theorems are renamed to nf*.

How well does this match your desire for the early work to use only simple notations? If you prefer, the NF stuff can be delayed longer, or even sent to the bottom of the pred calc section, but I would at least want NF versions of every single HB-using theorem in pred calc, because they will be the predominant mechanism in the rest of the database, so interspersing them seems more palatable.

 

Also, I have heard exactly such complaints for metamath, concerning $d,
not so much because it's a difficult symbol, but because it's a
difficult concept. (Of course I don't see it as a particularly difficult
concept, but that's the main source of friction from established
logicians.)

I can't help but think they have other reasons for disliking Metamath and use this as an excuse.  The concept of a variable not occurring in a formula is about as simple as it gets.  Obviously they don't want to put in even a minimal effort, for whatever reason.

I would guess that they are viewing it not as "from scratch" but from the POV of "how is this different from FOL", which brings a lot of extra baggage.
 

Have you pointed them to Tarski's system and papers?

This is generally hard to do "on the fly", i.e. when chatting on the way to dinner.
 

  Would they feel that the $d in Tarski's system is hard to understand?  Tarski's whole point was to make a system _easier_ to understand than the standard FOL axiomatization, since the concept of a variable not occurring in a formula is much simpler than "not free" in a formula.

Would they be have trouble understanding the Tarski subset of set.mm's axiom schemes?  If they can manage those, then they can be told that the 4 extra axioms (ax-6,7,11,12) can be ignored for the purpose of understanding the logic; they are merely technical devices needed to achieve our so-called "metalogical completeness".

I don't think this would help. The few times I've mentioned it the reaction is something like "one guy's random logic a long time ago", which makes me think that they are having a gut reaction to the system and references won't change that impression.

Mario

[David A. Wheeler]

On Sat, 13 Aug 2016 01:35:00 -0400, Norman Megill <n...@alum.mit.edu> wrote:
> Speaking of which, mmset.html has grown to be rather huge compared to
> conventional web pages, and I have considered breaking it up, but at the
> same time there is an advantage to having everything in one place
> instead of being scattered about in various pages that are likely to be
> missed unless you know what you are looking for. I kind of like having
> all of the general info related to set.mm on one page, with breakoff
> pages only for special topics like the complex numbers. Does the size
> bother anyone?

It's unusually large, but I can't say it bothers me.
As long as you have internal anchors (and you do), then it's easy to jump
to relevant materials.

The bigger problem is that MPE isn't mobile-friendly.
You can see this by running this check program:
https://www.google.com/webmasters/tools/mobile-friendly/

This affects both the special HTML pages (like the front pages) and the
generated pages. I think this important. Many people view pages from their
mobile devices, and I view the set of MPE HTML pages as a published
modern Principia Mathematica. It's important that the pages be accessible
to people on mobile devices.

The HTML should be tweaked so it's responsive, that is, so its display
automatically adjusts to the display available.

First step: Make sure every <head>...</head> section (manually written
and generated) includes this:
<meta name="viewport" content="width=device-width, initial-scale=1.0">

<rant>In my mind this should have been the default, but too many idiot designers
assumed that all screens were 640x480 and that IE6 was the only browser,
so now you have specially mark HTML to indicate that it correctly does *not*
depend on a particular size.</rant>

There will be more steps to really make it mobile-friendly, but
adding the viewpoint makes an improvement by itself AND will make
it clearer what to do next.

Lots of people use mobile; by some stats it's the majority of users:
http://www.smartinsights.com/mobile-marketing/mobile-marketing-analytics/mobile-marketing-statistics/


--- David A. Wheeler

[Norman Megill]

On 8/13/16 3:08 AM, Mario Carneiro wrote:
>
>
> On Sat, Aug 13, 2016 at 1:25 AM, Norman Megill <n...@alum.mit.edu
> <mailto:n...@alum.mit.edu>> wrote:

> An unfortunate fact that we have to live with is that regular
> mathematics is not entirely done with symbols. They use words as well,
> and we have to make symbols for them.

Two situations where words are used are (1) a side condition or proviso
imposed on a statement, and (2) English prose used to describe the
statements themselves like in say group theory theorems.

In the second case, of course we have to convert the English to formulas
with invented symbols because that is what the prose is intended to mean.

In the first case, the side condition isn't intended to be part of the
formula, and it doesn't make sense to convert the side condition to a
formula. If it did make sense, why wouldn't a formula be used in the
first place instead of an awkward side condition that can't be
manipulated easily? It is because the side conditions can't be
expressed in the language of the logic but involve a separate
metalogical notion.

In set.mm, $d's are side conditions. While we can approximate some
cases with devices like -. A. x x = y, in general there is no way to
express them in the language of the logic.

> A simple symbol like "NF"
> indicates this better than the expanded definition, in the same way that
> "E." is easier to read than "-. A. -." when reading an expression. On
> the other hand, the phrase "not free in" *is* standard, and needs to be
> written in the space around such assertions in conventional logic.

>
>
> Unlike other definitions, it doesn't buy significant space savings.
>
>
> At least this claim is refutable: there are two occurrences of ph in the
> original expression and one in the definition, so if ph is large there
> can be significant space savings.

The penalty for the two ph's is small after compression, since they get
replaced with the same expression. In most cases "( ph -> A. x ph )"
occurs only in the idiom |- ( ph -> A. x ph ) and is never nested, so
there is no exponential blowup caused by the two ph's.

We can debate what "significant" means, but I doubt the space savings
for set.mm would be even 1%. All hb* theorems, their comments, and
their proofs together occupy less than 130KB in set.mm.

>
>
> It is not even accurate about its claim, since x is free in x =
> x. It feels like an ugly hack.
>
>
> This is what I meant by "we need to de-emphasize this". This *really*
> isn't an important distinction, and stressing it seems like a red
> herring when there are plenty of other actual differences for the reader
> to worry about. NF(x, ph) is true *exactly* when x is not free in ph in
> the conventional sense, up to equivalence of expressions. It would be
> rather more weird if
>
> $e |- ( ph <-> ps )
> $a |- ( NF ( x , ph ) <-> NF ( x , ps ) )
>
> didn't hold, because then <-> would not be an equality.
>
>
> I wouldn't be so concerned if it was something in a specialized

> section of set.mm <http://set.mm>. I would greatly dislike having
> it permeate all of set.mm <http://set.mm> from the beginning. What

I don't want to do it at all. Instead, I will update the comment of
every occurrence of the |- ( ph -> A. x ph ) idiom to point to a clear
explanation. That will be much better than having a weird attempt to
partially mimic an English-language side condition. Whenever I have
pondered NF(x,ph) over the last decade or two, in the end it has always
felt like a kludge and the wrong thing to do.

To summarize my objections:

1. NF(x,ph) isn't a notation that occurs in the literature, unlike
_everything_ else in early set.mm. I put a lot of work into ensuring
that every definition is carefully sourced with a literature reference
and designed to have exactly the same behavior.

2. NF(x,ph) tries to shove an English language side condition into the
mathematical language proper. In standard FOL, "not free in" is a side
condition, not a logical predicate that can be manipulated. Side
conditions and predicates are two different things, like apples and oranges.

3. NF(x,ph) and the "not free in" side condition are not logically
equivalent (assuming it even makes sense to compare apples to oranges).
The x=x and similar cases (some not even decidable) may seem minor to
you, but to me, precise definitions matching the literature are important.

In principle, the proper way to add "not free in" would be a $nf x ph $.
metamath language extension where $d now goes, but of course that can't
be implemented in the present Metamath framework nor do we want to
complicate the language that way. So I just left the |- ( ph -> A. x
ph ) idiom alone instead of pretending it is a side condition when it
really isn't. It is a simple idiom and easy to recognize, and there
will be no mystery about it once I add the explanatory links I described.

If you really need NF, CondEq, etc. for your $j stuff, they should go in
a separate section. But why can't you have the software recognize the
patterns |- ( ph -> A. x ph ), |- ( x = y -> ph ), etc. directly? There
are likely many more useful patterns, and it would be a lot more
flexible than having to add a new, odd wff definition for each new
pattern, which is not something that is reader-friendly.

Norm

[Norman Megill]

On 8/13/16 10:29 AM, David A. Wheeler wrote:
> First step: Make sure every <head>...</head> section (manually written
> and generated) includes this:
> <meta name="viewport" content="width=device-width, initial-scale=1.0">

OK, I'll add this change to my to-do list for the next site build.

Norm

[David A. Wheeler]

> On 8/13/16 10:29 AM, David A. Wheeler wrote:
> > First step: Make sure every <head>...</head> section (manually written
> > and generated) includes this:
> > <meta name="viewport" content="width=device-width, initial-scale=1.0">

On Sat, 13 Aug 2016 12:20:24 -0400, Norman Megill <n...@alum.mit.edu> wrote:
> OK, I'll add this change to my to-do list for the next site build.

Thanks. It depends on the page, but that often (by itself) causes
larger (more-readable) fonts to be used on mobile devices.

As I said, there are typical other things that need doing for good
mobile display, but it's hard to tell until the viewport is set.

--- David A. Wheeler

[Mario Carneiro]

On Sat, Aug 13, 2016 at 11:59 AM, Norman Megill <n...@alum.mit.edu> wrote:

On 8/13/16 3:08 AM, Mario Carneiro wrote:

On Sat, Aug 13, 2016 at 1:25 AM, Norman Megill <n...@alum.mit.edu
<mailto:n...@alum.mit.edu>> wrote:

An unfortunate fact that we have to live with is that regular
mathematics is not entirely done with symbols. They use words as well,
and we have to make symbols for them.

Two situations where words are used are (1) a side condition or proviso imposed on a statement, and (2) English prose used to describe the statements themselves like in say group theory theorems.

In the second case, of course we have to convert the English to formulas with invented symbols because that is what the prose is intended to mean.

In the first case, the side condition isn't intended to be part of the formula, and it doesn't make sense to convert the side condition to a formula.  If it did make sense, why wouldn't a formula be used in the first place instead of an awkward side condition that can't be manipulated easily?  It is because the side conditions can't be expressed in the language of the logic but involve a separate metalogical notion.

The side condition is not part of the formula because in most cases it isn't possible, in the framework in question. I dare to say that in *every* case when a side condition can be converted to a term in the expression, this is always done. (Typing judgements come to mind.) Metamath is in the interesting situation that we have discovered that within our framework, "x is not free in the formula ph" is a condition that can be expressed with a formula, and we *have* been using formulas for this for a long time - that's not even new with my proposal.

In any case, side conditions are always an essential part of the statement and cannot be read separately. This is why $d's are always translated to an extra term in the FOL embedding, rather than a side condition, because in that context $d is an expression in the logic.
 

In set.mm, $d's are side conditions.  While we can approximate some cases with devices like -. A. x x = y, in general there is no way to express them in the language of the logic.

In set.mm *specifically* (and I'm only proposing NF for set.mm, so this goes without saying)), all $d's are expressible within the logic. $d x y becomes  -. A. x x = y,  $d x ph becomes A. x ( ph -> A. x ph ) , and $d x A becomes A. y A. x ( y e. A -> A. x y e. A ). However, because Metamath automatically calculates distributivity for $d and does not for these NF formulas, the former is preferred when it is possible. (Also, the fresh variable rule cannot be expressed in set.mm, so $d's must be relied on in that case to eliminate dummy variables.)

Note again that being formulas, they always have equality laws, so that you will claim "but sometimes NF is provable when $d is not valid". However, this does not matter in a very precise sense - equivalent expressions can be substituted in all contexts (this is what it means to be an equality), so anything you derive by one mechanism can be derived by the other.

A simple symbol like "NF"
indicates this better than the expanded definition, in the same way that
"E." is easier to read than "-. A. -." when reading an expression. On
the other hand, the phrase "not free in" *is* standard, and needs to be
written in the space around such assertions in conventional logic.

      Unlike other definitions, it doesn't buy significant space savings.


At least this claim is refutable: there are two occurrences of ph in the
original expression and one in the definition, so if ph is large there
can be significant space savings.

The penalty for the two ph's is small after compression, since they get replaced with the same expression.  In most cases "( ph -> A. x ph )" occurs only in the idiom |- ( ph -> A. x ph ) and is never nested, so there is no exponential blowup caused by the two ph's.

We can debate what "significant" means, but I doubt the space savings for set.mm would be even 1%.  All hb* theorems, their comments, and their proofs together occupy less than 130KB in set.mm.

You seem to forget that those theorems get uses beyond just other hb* theorems. We aren't deriving those just for fun! The primary consumers of such theorems are in doing alpha substitution which may involve bound scopes. To take a typical example, http://us.metamath.org/mpegif/flfcnp2.html#25. In these cases, we are quite obviously not interested in phi implying forall x phi specifically, and are focusing only on their "idiomatic" use as meaning NF. This is the part I'm really interested in changing. If you want pred calc to stay pure, fine, but I want, *eventually*, that we can use NF when we mean NF. As far as worthwhile definitions go, I'm pretty sure that you will find more instances of NF used in set.mm than, say, "or". And every book I can find on predicate calculus *does* define NF, and calls it "x is not free in ph" used as a side condition.

 

To summarize my objections:

1. NF(x,ph) isn't a notation that occurs in the literature, unlike _everything_ else in early set.mm.  I put a lot of work into ensuring that every definition is carefully sourced with a literature reference and designed to have exactly the same behavior.

NF does occur in the literature, and is called "not free in". It has the same behavior as these literature versions, up to equivalence.

 

2. NF(x,ph) tries to shove an English language side condition into the mathematical language proper.  In standard FOL, "not free in" is a side condition, not a logical predicate that can be manipulated.  Side conditions and predicates are two different things, like apples and oranges.

It's not "trying to shove it into the mathematical language", it has done so, and it has done so successfully. What's more, this is true whether or not you use the notation "NF", as it is already being used in set.mm today. In conventional logic you can't do this, in metamath you can (and we do). This is a win for us.

 

3. NF(x,ph) and the "not free in" side condition are not logically equivalent (assuming it even makes sense to compare apples to oranges). The x=x and similar cases (some not even decidable) may seem minor to you, but to me, precise definitions matching the literature are important.

They are logically equivalent, literally. NF(x, x=x) is logically equivalent to NF(x,y=y), which is logically equivalent to "x is not free in y=y". Perhaps you wanted something else, like metalogical equivalence or something that actually inspects the expression?

A correct and proper reading of NF(x, ph) is: "x is not free in some expression equivalent to ph". It is not decidable (both true and false are provable if valid), but it's a proof obligation so that's not a problem. The algorithm for deciding if x is not free in ph directly translates to an algorithm for proving NF(x, ph) in the positive case. In the negative case, no one cares because you made a mistake. I'd point out that no one uses hbth.

 

In principle, the proper way to add "not free in" would be a $nf x ph $. metamath language extension where $d now goes, but of course that can't be implemented in the present Metamath framework nor do we want to complicate the language that way.  So  I just left the |- ( ph -> A. x ph ) idiom alone instead of pretending it is a side condition when it really isn't.  It is a simple idiom and easy to recognize, and there will be no mystery about it once I add the explanatory links I described.

Eww. Why? Keywords are only for things that can't be done any other way.

 

If you really need NF, CondEq, etc. for your $j stuff, they should go in a separate section.  But why can't you have the software recognize the patterns |- ( ph -> A. x ph ), |- ( x = y -> ph ), etc. directly?  There are likely many more useful patterns, and it would be a lot more flexible than having to add a new, odd wff definition for each new pattern, which is not something that is reader-friendly.

I mentioned the reasoning earlier. I want to do as much as possible in the .mm file, to make the resulting verifier easier to trust, and make everything as explicit as possible.

The reason I haven't stopped with my counter-points is because your arguments do not sound like more than an emotional response. If anyone else is reading this, I'd really like to hear your view because this needs community response.

Mario

[Stefan O'Rear]

I've been reading this, I don't have much to add. My slight
preference would be for the definition check to recognize |- ( $0 ->
A. $1 $0 ) (your parser ought to support metametavariables anyway if
you want to use it in a proof assistant later), but I haven't actually
looked at how the definition check works. I'm not convinced the
abbreviation buys us much from a human-factors perspective, but it
wouldn't be the end of the world either.

-sorear

[Mario Carneiro]

On Sat, Aug 13, 2016 at 2:25 PM, Mario Carneiro <di....@gmail.com> wrote:

We can debate what "significant" means, but I doubt the space savings for set.mm would be even 1%.  All hb* theorems, their comments, and their proofs together occupy less than 130KB in set.mm.

You seem to forget that those theorems get uses beyond just other hb* theorems. We aren't deriving those just for fun! The primary consumers of such theorems are in doing alpha substitution which may involve bound scopes. To take a typical example, http://us.metamath.org/mpegif/flfcnp2.html#25. In these cases, we are quite obviously not interested in phi implying forall x phi specifically, and are focusing only on their "idiomatic" use as meaning NF. This is the part I'm really interested in changing. If you want pred calc to stay pure, fine, but I want, *eventually*, that we can use NF when we mean NF. As far as worthwhile definitions go, I'm pretty sure that you will find more instances of NF used in set.mm than, say, "or". And every book I can find on predicate calculus *does* define NF, and calls it "x is not free in ph" used as a side condition.

I was curious whether this claim actually holds up, so I compiled a list of all the usages of each syntax axiom in every step of every proof, as well as counting occurrences of (ph -> A. x ph), which would presumably be replaced by NF if it were adopted. The results are quite interesting independent of any NF considerations.

At the bottom of the list is two occurrences, once for the syntax axiom and once for the definition, for definitions that are never used. There are 1024 definitions in set.mm (apparently), and the top ten are maybe not what you would expect. (ph -> A. x ph) appears as 160th in the list, with 12617 occurrences, which is less than wo = #84 (so my above claim is not true) but more than some other predicate calc definitions such as E! = #273 and E* = #290.

Note that NF = #754 also appears in this list, because this is my local copy with a few basic NF theorems in it, but it is not used globally like (ph -> A. x ph).

cv: class x: 5500171
co: class ( A F B ): 3156682
cfv: class ( F ` A ): 3125370
wcel: wff A e. B: 2966757
wa: wff ( ph /\ ps ): 1482885
wceq: wff A = B: 1081141
wi: wff ( ph -> ps ): 952306
wbr: wff A R B: 825413
c1: class 1: 712027
cmul: class x.: 419186
cc0: class 0: 404943
w3a: wff ( ph /\ ps /\ ch ): 388326
c2: class 2: 361362
caddc: class +: 353934
cmin: class -: 325552
csn: class { A }: 310925
cdiv: class /: 293573
wss: wff A C_ B: 285197
cr: class RR: 275279
wn: wff -. ph: 270154
wne: wff A =/= B: 240383
wral: wff A. x e. A ph: 238020
cop: class <. A , B >.: 230525
cexp: class ^: 229904
cc: class CC: 226644
cle: class <_: 208852
cfz: class ...: 193897
cn: class NN: 192585
cin: class ( A i^i B ): 177244
clt: class <: 177111
wb: wff ( ph <-> ps ): 167760
c0: class (/): 166250
cmpt: class ( x e. A |-> B ): 159919
cbs: class Base: 153676
cxp: class ( A X. B ): 148884
wrex: wff E. x e. A ph: 145115
cres: class ( A |` B ): 142185
cdif: class ( A \ B ): 140693
cvv: class _V: 138417
cz: class ZZ: 137995
cdm: class dom A: 137059
cuni: class U. A: 135564
ccnv: class `' A: 135320
cima: class ( A " B ): 125551
crn: class ran A: 119509
cn0: class NN0: 112336
cabs: class abs: 109640
cneg: class -u A: 98722
ccom: class ( A o. B ): 97454
cif: class if ( ph , A , B ): 95833
cpw: class ~P A: 93692
chlt: class HL: 92979
wf: wff F : A --> B: 88817
crab: class { x e. A | ph }: 82998
cee: class EE: 81917
cun: class ( A u. B ): 79923
crp: class RR+: 74717
chash: class #: 71889
cfl: class |_: 70580
cicc: class [,]: 67059
cuz: class ZZ>=: 66339
com: class om: 64731
clog: class log: 64281
wal: wff A. x ph: 63245
cfn: class Fin: 63225
chil: class ~H: 61628
cxr: class RR*: 58318
c1st: class 1st: 57543
con0: class On: 56938
cid: class _I: 56507
c3: class 3: 55101
c2nd: class 2nd: 54961
ci: class _i: 54668
cpnf: class +oo: 53810
cioo: class (,): 52726
csuc: class suc A: 52371
cmap: class ^m: 52018
wex: wff E. x ph: 51935
cdivides: class ||: 51781
csu: class sum_ k e. A B: 46635
cplusg: class +g: 45976
c0g: class 0g: 39884
cpr: class { A , B }: 37954
wo: wff ( ph \/ ps ): 36742
wsbc: wff [ A / x ] ph: 35386
c1o: class 1o: 34331
csqr: class sqr: 32802
csb: class [_ A / x ]_ B: 31901
cprime: class Prime: 31222
cpi: class pi: 31176
cseq: class seq M ( .+ , F ): 29239
wfn: wff A Fn B: 28975
crest: class |`t: 28156
cof: class oF R: 27879
csca: class Scalar: 27056
chj: class vH: 26819
c4: class 4: 25990
ciun: class U_ x e. A B: 25700
cab: class { x | ph }: 25634
cdc: class ; A B: 24957
cbtwn: class Btwn: 24773
cmulr: class .r: 24282
ctop: class Top: 24264
cre: class Re: 24212
cbl: class ball: 23026
csp: class .ih: 23016
cple: class le: 22814
cint: class |^| A: 22751
ccn: class Cn: 22650
ccnfld: class CCfld: 22631
cgcd: class gcd: 22107
cvsca: class .s: 21540
cch: class CH: 21103
cno: class normh: 21006
cmpt2: class ( x e. A , y e. B |-> C ): 20871
wf1o: wff F : A -1-1-onto-> B: 20669
cico: class [,): 20286
cort: class _|_: 20263
cen: class ~~: 20172
cim: class Im: 19925
cgsu: class gsum: 19813
ccrd: class card: 19625
cmnf: class -oo: 19504
ctopon: class TopOn: 19010
csup: class sup ( A , B , R ): 18929
ce: class exp: 18742
c2o: class 2o: 18642
crmy: class rmY: 18359
ccgr: class Cgr: 18203
cva: class +h: 17682
comu: class .o: 17631
cnx: class ndx: 17496
cmo: class mod: 17476
cjn: class join: 17446
cpjh: class projh: 17397
cdom: class ~<_: 17393
coa: class +o: 17299
cr1: class R1: 17295
csubg: class SubGrp: 16894
csm: class .h: 16776
cfa: class !: 16587
cpc: class pCnt: 16521
cec: class [ A ] .~: 16502
cress: class |`s: 16415
cvol: class vol: 16403
cdv: class _D: 15701
cgrp: class Grp: 15699
cfzo: class ..^: 15342
coe: class ^o: 14915
clmod: class LMod: 14177
cii: class II: 13931
catm: class Atoms: 13790
crg: class Ring: 13787
cvma: class Lam: 13335
ccj: class *: 13287
cword: class Word S: 13279
wtru: wff T.: 13053
cdgr: class deg: 12904
c6: class 6: 12770
===============================> ph -> A. x ph: 12617
covol: class vol*: 12511
ctopn: class TopOpen: 12484
c0v: class 0h: 12367
cxmt: class *Met: 12165
crio: class ( iota_ x e. A ph ): 12047
wnel: wff A e/ B: 12002
cminusg: class invg: 11856
cur: class 1r: 11833
cmv: class -h: 11766
ctg: class topGen: 11602
crnk: class rank: 11467
ccl: class cls: 11444
c8: class 8: 11426
c5: class 5: 11421
cply: class Poly: 11281
wpss: wff A C. B: 11212
cq: class QQ: 10797
cmee: class meet: 10351
cale: class aleph: 10206
csin: class sin: 10144
cnpi: class N.: 10144
ccos: class cos: 10126
c7: class 7: 10068
csg: class -g: 10043
coc: class oc: 10022
wf1: wff F : A -1-1-> B: 9853
ctx: class tX: 9815
clat: class Lat: 9678
cixp: class X_ x e. A B: 9654
cep: class _E: 9530
ccxp: class ^c: 9433
wfun: wff Fun A: 9325
csdm: class ~<: 9268
cfil: class Fil: 9187
cchp: class psi: 9095
cdom_: class dom_: 9079
cltrn: class LTrn: 8915
crdg: class rec ( F , I ): 8798
cpred: class Pred ( R , A , X ): 8730
ccda: class +c: 8663
clss: class LSubSp: 8600
cmgp: class mulGrp: 8547
ctp: class { A , B , C }: 8344
cph: class +H: 8314
copab: class { <. x , y >. | ph }: 8202
c9: class 9: 8155
cds: class dist: 7998
crmx: class rmX: 7997
cnp: class P.: 7991
clspn: class LSpan: 7989
cnei: class nei: 7795
cotp: class <. A , B , C >.: 7573
cofr: class oR R: 7572
cfi: class fi: 7569
cconcat: class concat: 7459
ccld: class Clsd: 7343
cpp: class +P.: 7329
cnv: class NrmCVec: 7315
cdprd: class DProd: 7275
ccoe: class coeff: 7182
cli: class ~~>: 7166
cmi: class .N: 7094
citg2: class S.2: 7003
clh: class LHyp: 6885
cbc: class _C: 6879
ccmp: class Comp: 6817
wtr: wff Tr A: 6734
cnq: class Q.: 6729
cgr: class GrpOp: 6583
citg1: class S.1: 6542
cxad: class +e: 6509
wlim: wff Lim A: 6505
c0h: class 0H: 6424
wfo: wff F : A -onto-> B: 6375
c-bnj14: class _pred ( X , A , R ): 6358
cnt: class int: 6321
cdvh: class DVecH: 6222
word: wff Ord A: 6217
cmnd: class Mnd: 5872
w3o: wff ( ph \/ ps \/ ch ): 5620
cco1: class coe1: 5592
ccod_: class cod_: 5426
cba: class BaseSet: 5387
c0p: class 0p: 5296
wrel: wff Rel A: 5261
cmg: class .g: 5191
csubrg: class SubRing: 5154
crngo: class RingOps: 5089
csubstr: class substr: 5046
cmp: class .P.: 5024
cxne: class -e A: 5003
wor: wff R Or A: 4857
clmhm: class LMHom: 4788
wiso: wff H Isom R , S ( A , B ): 4769
wnan: wff ( ph -/\ ps ): 4751
cioc: class (,]: 4727
clgs: class /L: 4681
cp0: class 0.: 4519
cat: class HAtoms: 4484
wwe: wff R We A: 4446
cmu: class mmu: 4445
cghm: class GrpHom: 4430
cns: class .sOLD: 4362
ctendo: class TEndo: 4352
csh: class SH: 4322
cpv: class +v: 4291
crelexp: class ^r: 4267
c1p: class 1P: 4185
citg: class S. A B _d x: 4171
cmzp: class mzPoly: 4167
clm: class ~~>t: 4133
wfal: wff F.: 4115
weu: wff E! x ph: 4074
ccnp: class CnP: 4071
c10: class 10: 4066
cxmu: class *e: 4061
cnop: class normop: 4036
cmr: class .R: 3990
cgi: class Id: 3964
ccf: class cf: 3942
w-bnj17: wff ( ph /\ ps /\ ch /\ th ): 3928
cs1: class <" A ">: 3878
cmq: class .Q: 3811
wreu: wff E! x e. A ph: 3777
cpt: class Xt_: 3773
cmopn: class MetOpen: 3773
cme: class Met: 3766
cpws: class ^s: 3743
cnmcv: class normCV: 3740
wmo: wff E* x ph: 3711
crecs: class recs ( F ): 3703
cui: class Unit: 3649
ctan: class tan: 3634
cdg1: class deg1: 3634
csur: class No: 3621
cspn: class span: 3612
c0r: class 0R: 3582
clsm: class LSSum: 3566
cfbas: class fBas: 3547
cqs: class ( A /. .~ ): 3478
cabel: class Abel: 3476
ciin: class |^|_ x e. A B: 3414
coi: class OrdIso ( R , A ): 3412
cid_: class id_: 3347
cplq: class +Q: 3284
ccncf: class -cn->: 3263
chot: class .op: 3255
cado: class adjh: 3190
cpl1: class Poly1: 3177
cngp: class NrmGrp: 3122
clvec: class LVec: 3087
cnr: class R.: 3080
ceu: class _e: 3075
cltq: class <Q: 3071
cs2: class <" A B ">: 3062
coch: class ocH: 3061
cplt: class lt: 3053
cprds: class Xs_: 3047
clcd: class LCDual: 3046
cpco: class *p: 3037
cgn: class inv: 3027
ccrg: class CRing: 3022
chod: class -op: 3017
cmrc: class mrCls: 3008
chos: class +op: 2922
cmpl: class mPoly: 2907
catan: class arctan: 2863
cmbf: class MblFn: 2824
cdih: class DIsoH: 2794
ch0o: class 0hop: 2777
cmps: class mPwSer: 2771
cqg: class ~QG: 2769
cqtop: class qTop: 2759
csquarenn: class []NN: 2752
cphtpc: class ~=ph: 2740
ctrl: class trL: 2733
cgru: class Univ: 2714
cpm: class ^pm: 2697
cbday: class bday: 2675
ccat: class Cat: 2667
cplr: class +R: 2664
cnm: class norm: 2662
cio: class ( iota x ph ): 2662
cip: class .i: 2641
crglmod: class ringLMod: 2622
ctb: class TopBases: 2597
cflim: class fLim: 2586
ccht: class theta: 2584
w-bnj15: wff R _FrSe A: 2575
csubmnd: class SubMnd: 2548
cfg: class filGen: 2540
cinvr: class invr: 2526
ccon: class Con: 2525
chmeo: class Homeo: 2520
cmre: class Moore: 2516
czn: class Z/nZ: 2485
cha: class Haus: 2469
ckq: class KQ: 2441
ckgen: class kGen: 2441
cer: class ~R: 2421
ctgp: class TopGrp: 2383
c-bnj18: class _trCl ( X , A , R ): 2374
cdr: class DivRing: 2354
cflf: class fLimf: 2342
cordt: class ordTop: 2311
cmhm: class MndHom: 2303
co1: class O(1): 2290
char: class har: 2274
cphi: class phi: 2262
ckln: class Kleene: 2255
cppi: class ppi: 2213
crq: class *Q: 2194
crli: class ~~>r: 2192
cho: class HrmOp: 2152
ccvr: class <o: 2128
ccnf: class CNF: 2114
ccmrcase: class MorphismSetCat: 2109
coppr: class oppR: 2068
cbtw: class btw: 2038
cerq: class /Q: 2036
cibl: class L^1: 2028
clfn: class LFnl: 2028
cidl: class Idl: 2020
crpss: class [C.]: 2012
clk: class LKer: 2004
cn0v: class 0vec: 1986
cnlly: class N-Locally A: 1972
cts: class TopSet: 1964
cslt: class <s: 1936
copab2: class { <. <. x , y >. , z >. | ph }: 1927
club: class lub: 1885
czrh: class ZRHom: 1879
cxko: class ^ko: 1867
cops: class OP: 1856
cgz: class Z[i]: 1844
coml: class OML: 1830
cltr: class <R: 1830
co_: class o_: 1816
cdvn: class Dn: 1794
cphl: class PreHil: 1792
cal: class AtLat: 1788
cseg: class seg: 1780
wpo: wff R Po A: 1739
cfcls: class fClus: 1736
ctsk: class Tarski: 1720
ccla: class CLat: 1715
cod: class od: 1711
cp1: class 1.: 1711
cpell14qr: class Pell14QR: 1689
cvdwa: class AP: 1675
c1q: class 1Q: 1661
cablo: class AbelOp: 1646
chli: class ~~>v: 1624
clo: class LinOp: 1615
ctpos: class tpos F: 1603
creverse: class reverse: 1596
cram: class Ramsey: 1585
ccolin: class Colinear: 1581
cstv: class *r: 1549
ccmn: class CMnd: 1545
csplice: class splice: 1545
cfm: class FilMap: 1540
cufil: class UFil: 1533
col: class OL: 1525
cnlm: class NrmMod: 1521
cpo: class Poset: 1520
cnsg: class NrmSGrp: 1509
chio: class Iop: 1490
ccntz: class Cntz: 1485
wer: wff .~ Er A: 1479
csts: class sSet: 1473
crh: class RingHom: 1473
cplcv: class +cv: 1471
cdomcase: class domSetCat: 1439
cpli: class +N: 1432
cascl: class algSc: 1421
cmd: class MH: 1409
cidp: class Xp: 1401
cbr: class bra: 1399
cga: class GrpAct: 1386
wfr: wff R Fr A: 1381
ccph: class CPreHil: 1376
cem: class gamma: 1375
wse: wff R Se A: 1367
ctmd: class TopMnd: 1367
cpellfund: class PellFund: 1359
cps: class PosetRel: 1350
c1stc: class 1stc: 1332
cm1r: class -1R: 1329
cpgp: class pGrp: 1323
cpoints: class PPoints: 1313
crsp: class RSpan: 1284
cdia: class DIsoA: 1279
ceq: class ~Q: 1278
clc: class CvLat: 1273
cgch: class GCH: 1257
cdioph: class Dioph: 1239
cocv: class ocv: 1233
cnsb: class -v: 1216
ces: class evalSub: 1202
cltrr: class <RR: 1200
ccm: class C_H: 1199
cnghm: class NGHom: 1192
cvec: class Vec: 1183
cltp: class <P: 1182
cvdg: class VDeg: 1173
cpmap: class pmap: 1168
cipo: class toInc: 1166
cpcon: class PCon: 1159
cdenom: class denom: 1155
cedring: class EDRing: 1150
clly: class Locally A: 1142
cdib: class DIsoB: 1131
cclm: class CMod: 1124
candc: class andc: 1123
cglb: class glb: 1106
ccvm: class CovMap: 1103
cms: class CMet: 1084
cslw: class pSyl: 1083
chdma: class HDMap: 1073
cwdom: class ~<_*: 1069
cbnd: class Bnd: 1064
ccol: class coln: 1061
ctc: class TC: 1051
cline2: class Line: 1049
ccfil: class CauFil: 1045
ctps: class TopSp: 1038
clln: class LLines: 1030
cdit: class S_ [ A -> B ] C _d x: 1028
cldgis: class ldgIdlSeq: 1024
cplines: class PLines: 1020
ctmt: class toMetSp: 1013
clsa: class LSAtoms: 1005
wsmo: wff Smo A: 997
clidl: class LIdeal: 994
cacs: class ACS: 987
cidom: class IDomn: 980
ccgr3: class Cgr3: 975
cdmd: class MH*: 973
cmt: class MetSp: 970
clti: class <N: 969
crtrcl: class t*rec: 959
cconc: class conc: 958
cspw: class supw: 945
cld: class LDual: 939
clf: class LinFn: 939
cbp: class BernPoly: 937
cxrs: class RR*s: 935
cscon: class SCon: 933
cnzr: class NzRing: 926
cdgraa: class degAA: 923
cmpd: class mapd: 922
cgs: class /g: 921
cpolN: class _|_P: 916
cphtpy: class PHtpy: 906
clpl: class LPlanes: 904
cims: class IndMet: 903
cv1: class var1: 903
cdsr: class ||r: 901
ccphlo: class CPreHilOLD: 898
wvd1: wff (. ph ->. ps ).: 879
ccodcase: class codSetCat: 878
cvdwm: class MonoAP: 874
c0cv: class 0cv: 857
coutsideof: class OutsideOf: 848
cnrg: class NrmRing: 845
caa: class AA: 844
crrn: class Rn: 837
cbo: class BndLinOp: 827
clsp: class limsup: 826
cquot: class quot: 825
ccv: class <oH: 824
ctskm: class tarskiMap: 813
cnmoo: class normOpOLD: 803
cca: class Cau: 797
cdrs: class Dirset: 793
cq1p: class quot1p: 793
cshi: class shift: 788
cxme: class *MetSp: 787
cvc: class CVecOLD: 785
ctar: class tar: 763
cimpc: class impc: 760
cbic: class bic: 759
cded: class Ded: 754
cors: class ors: 751
cnotc: class notc: 750
cfrlm: class freeLMod: 743
ctxp: class ( A (x) B ): 741
ctsr: class TosetRel: 740
crnghom: class RngHom: 736
casa: class AssAlg: 733
wacn: class AC_ A: 729
cevl: class eval: 727
clsh: class LSHyp: 722
ctail: class tail: 713
chvm: class HVMap: 712
cprd: class prod_ k e. A G B: 706
cfne: class Fne: 699
clindf: class LIndF: 698
cseqom: class seqom ( F , I ): 697
codz: class odZ: 692
cfrmd: class freeMnd: 691
chlo: class CHilOLD: 686
cpmtr: class pmTrsp: 683
cmagm: class Magma: 681
culm: class ~~>u: 680
casin: class arcsin: 679
cdip: class .iOLD: 677
cpro: class pr: 674
css: class SubSp: 666
cidcase: class IdSetCat: 663
cnrm: class Nrm: 662
c1r: class 1R: 661
cmpq: class .pQ: 659
cdic: class DIsoC: 656
cplpq: class +pQ: 650
cPc: class Pc: 635
cnumer: class numer: 628
cdomn: class Domn: 626
cps1: class PwSer1: 624
cvrgp: class varFGrp: 622
cmvr: class mVar: 616
cst: class States: 602
ccnfn: class ConFn: 592
ctrpred: class TrPred ( R , A , X ): 592
cpell1qr: class Pell1QR: 586
creg: class Reg: 583
crocase: class roSetCat: 573
csingle: class Singleton: 570
ctsu: class tsums: 568
clnm: class LNoeM: 565
ccms: class CMetSp: 564
cghom: class GrpOpHom: 559
cnmf: class normfn: 558
coppg: class oppG: 554
cco: class ConOp: 552
cbigcup: class Bigcup: 551
cpresetrel: class PresetRel: 543
ccring: class CRingOps: 543
clo1: class <_O(1): 543
cstf: class *rf: 542
ct1: class Fre: 538
cgim: class GrpIso: 533
cpsubsp: class PSubSp: 532
calg: class Alg: 526
ccpn: class C^n: 508
cuo: class UniOp: 500
csingles: class Singletons: 497
cufl: class UFL: 494
cexid: class ExId: 488
cnmo: class normOp: 488
cumg: class UMGrph: 487
ck: class ketbra: 486
cprop: class Prop: 482
cfin2: class Fin2: 481
clfig: class LFinGen: 480
cimage: class Image A: 474
cmzpcl: class mzPolyCld: 471
chst: class CHStates: 470
cina: class Inacc: 470
cpj1: class proj1: 470
cqus: class /s: 466
comi: class Om1: 466
chdma1: class HDMap1: 463
ccyg: class CycGrp: 460
cgraphcase: class graphSetCat: 458
cdchr: class DChr: 451
cleo: class <_op: 450
cfin3: class Fin3: 447
ce1: class eval1: 445
cpi1: class pi1: 444
cfals: class _|_c: 441
cnl: class null: 436
cigen: class IdlGen: 428
cdir: class DirRel: 426
ccbn: class CBan: 425
cvdwp: class PolyAP: 424
cabv: class AbsVal: 423
cpadd: class +P: 421
csem: class SemiGrp: 413
clinds: class LIndS: 407
cplusf: class +f: 406
cefg: class ~FG: 404
capply: class Apply: 404
c2ndc: class 2ndc: 401
wvd2: wff (. ph , ps ->. ch ).: 395
csegle: class Seg<_: 394
cismty: class Ismty: 386
cmmul: class maMul: 378
ceup: class EulPaths: 370
cocaN: class ocA: 369
clnr: class LNoeR: 368
chmph: class ~=: 365
ctotbnd: class TotBnd: 364
cpell1234qr: class Pell1234QR: 364
cdvr: class /r: 363
cchr: class chr: 361
clp: class limPt: 360
csubc: class SubCat: 359
csgm: class sigma: 358
clpsc: class psc: 357
cphc: class phc: 354
claut: class LAut: 352
cfunpart: class Funpart F: 351
cobs: class OBasis: 350
cref: class Ref: 341
cwina: class InaccW: 340
cfin4: class Fin4: 340
chg: class HGMap: 334
cpprod: class pprod ( R , S ): 324
cub: class ub: 320
cxps: class Xs.: 319
cslot: class Slot A: 318
ct0: class Kol2: 314
clno: class LnOp: 313
cfullfn: class FullFun F: 312
caltop: class << A , B >>: 310
cands: class /\c: 307
cibg: class Ibg: 303
ccm1: class Com1: 294
cdomain: class Domain: 292
crngiso: class RngIso: 285
chsup: class \/H: 281
cdsmm: class (+)m: 280
cmpaa: class minPolyAA: 277
cimas: class "s: 277
wac: wff CHOICE: 274
csubgo: class SubGrpOp: 273
cdrng: class DivRingOps: 273
csymg: class SymGrp: 270
wcirc: wff () ph: 270
cline: class line: 262
cmcv: class -cv: 260
cgex: class gEx: 259
csr: class *Ring: 259
wunt: wff ( ph until ps ): 257
cnacs: class NoeACS: 255
cfix: class Fix A: 249
cinf: class infw: 249
c0o: class 0op: 247
cimg: class Img: 246
csymdif: class ( A (++) B ): 244
clmim: class LMIso: 244
cblo: class BLnOp: 244
cfunc: class Func: 242
cei: class eigvec: 241
chtpy: class Htpy: 239
cldil: class LDil: 237
cfcf: class fClusf: 235
wbox: wff [.] ph: 233
cel: class eigval: 231
cfin1a: class Fin1a: 228
cig: class Ig: 223
cgic: class ~=g: 223
csra: class subringAlg: 221
cund: class Undef: 220
cntrl: class Natural: 219
ctrg: class TopRing: 217
clocfin: class LocFin: 215
codu: class ODual: 215
cstr: class Struct: 213
cdveca: class DVecA: 211
csset: class SSet: 209
ctopx: class topX: 208
cdjh: class joinH: 207
clcv: class <oL: 205
cltb: class <bag: 204
cmn1: class Monic1p: 204
climits: class Limits: 203
ccss: class CSubSp: 195
clines2: class LinesEE: 195
cge: class ge: 193
cuvc: class unitVec: 189
cnmhm: class NMHom: 187
cmndo: class MndOp: 186
cuc1p: class Unic1p: 181
ccau: class Cauchy: 180
clpidl: class LPIdeal: 180
cnvc: class NrmVec: 177
csuccf: class Succ: 175
crlreg: class RLReg: 173
clbs: class LBasis: 172
chl: class CHil: 169
crisc: class ~=r: 163
cpscN: class PSubCl: 162
ccm2: class Com2: 161
wvd3: wff (. ph , ps , ch ->. th ).: 158
cpj: class proj: 158
cptfin: class PtFin: 158
ccur1: class cur1: 157
cflimfrs: class fLimfrs: 156
cmon: class Mono: 153
csrce: class Source: 153
wnf: wff NF ( x , ph ): 151
cpridl: class PrIdl: 151
crange: class Range: 149
cr1p: class rem1p: 147
csmcv: class .cv: 145
ctrans: class Trans: 136
carea: class area: 136
clatalg: class LatAlg: 135
cscaf: class .sf: 134
cvrmd: class varFMnd: 134
ctlm: class TopMod: 131
clvol: class LVols: 130
copws: class ordPwSer: 130
cofs: class OuterFiveSeg: 129
cdivcv: class /cv: 128
chom: class hom: 127
cacos: class arccos: 123
cmend: class MEndo: 123
wprt: wff Prt A: 121
cbn: class Ban: 121
ctransport: class TransportTo: 118
cpreset: class Preset: 114
cmat: class Mat: 112
cfld: class Fld: 110
chft: class .fn: 108
cmdg: class mDeg: 107
cdmn: class Dmn: 107
cfrgp: class freeGrp: 104
ccart: class Cart: 104
ctdrg: class TopDRing: 103
cfield: class Field: 101
ctng: class toNrmGrp: 100
cdpj: class dProj: 99
crestrict: class Restrict: 98
clmic: class ~=m: 97
cgx: class ^g: 97
w-bnj19: wff _TrFo ( B , A , R ): 97
chlh: class HLHil: 94
cs3: class <" A B C ">: 94
cltpq: class <pQ: 94
crgspn: class RingSpan: 94
cs4: class <" A B C D ">: 94
ctch: class toCHil: 92
wxo: wff ( ph \/_ ps ): 90
ccnrm: class CNrm: 89
ccup: class Cup: 88
cpnrm: class PNrm: 87
cplusr: class +r: 85
cray: class Ray: 85
cwpointsN: class WAtoms: 84
cfuns: class Funs: 82
wdia: wff <> ph: 82
cs6: class <" A B C D E F ">: 82
caj: class adj: 80
cwrd: class Words: 80
cintvl: class Intvl: 79
cs5: class <" A B C D E ">: 79
clincl: class IndCls: 78
ctpsOLD: class TopSpOLD: 77
cpsgn: class pmSgn: 75
clines: class Lines: 73
cipf: class .if: 70
coriso: class OrIso: 69
clpir: class LPIR: 68
ccmtN: class cm: 68
citgo: class IntgOver: 67
cfin7: class Fin7: 65
casp: class AlgSpan: 65
cmxl: class mxl: 64
cmaxidl: class MaxIdl: 63
cproj: class prj: 60
cprrng: class PrRing: 60
cs7: class <" A B C D E F G ">: 58
cir: class Irred: 58
cimps: class =>c: 56
c2idl: class 2Ideal: 56
cbis: class <=>c: 54
cig1p: class idlGen1p: 54
ctos: class Toset: 54
cse: class leR: 53
clors: class \/c: 53
cass: class Ass: 52
cedring-rN: class EDRingR: 51
csdrg: class SubDRing: 50
csas: class ss: 50
cnegcv: class -ucv: 49
ccot: class cot: 47
csgn: class sgn: 46
cpclN: class PCl: 46
ccap: class Cap: 45
wvhc2: wff (. ph , ps ).: 45
ctgrp: class TGrp: 45
cmnc: class Monic: 44
cmnl: class mnl: 44
c3o: class 3o: 44
crtcl: class t*: 43
csec: class sec: 43
cnots: class -.c: 42
cla: class LatRel: 42
cifs: class InnerFiveSeg: 41
caltxp: class ( A XX. B ): 41
czlm: class ZMod: 40
wcdeq: wff CondEq ( x = y -> ph ): 40
wnfc: wff NF_ ( x , A ): 37
cdlat: class DLat: 37
cpautN: class PAut: 36
ccsc: class csc: 36
ccntr: class Cntr: 36
ccst: class cset: 34
cepi: class Epic: 33
cdilN: class Dil: 33
w-bnj13: wff R _Se A: 28
cdp2: class _ A B: 28
ctvc: class TopVec: 28
wvhc3: wff (. ph , ps , ch ).: 27
cray2: class ray: 27
cminusr: class -r: 27
cthl: class toHL: 27
ctimesr: class .v: 27
ccon2: class con: 26
cs8: class <" A B C D E F G H ">: 23
cgoe: class e.g: 23
ccinv: class cinv: 23
w3nand: wff ( ph -/\ ps -/\ ch ): 23
cmpr: class .pR: 23
cplpr: class +pR: 23
ccosh: class cosh: 22
csinh: class sinh: 20
cmdat: class maDet: 20
c-bnj16: class _fns A: 20
cfin5: class Fin5: 20
chfs: class +fn: 19
cfs: class FiveSeg: 19
cder: class der: 19
cdjaN: class vA: 19
cplig: class Plig: 19
cdwords: class dWords: 18
chs: class Hil: 18
clmct: class LimCat: 17
cgol: class A.g N U: 17
clpoN: class LPol: 16
cfin6: class Fin6: 16
cmgra: class Dgra: 15
cge-real: class >_: 14
c4o: class 4o: 14
cgcdOLD: class gcdOLD ( A , B ): 14
cgt: class >: 14
cgoi: class ->g: 13
cdp: class .: 13
cidln: class IdlNEW: 12
cSeg: class Segments: 12
cgiso: class GrpOpIso: 11
cgox: class E.g N U: 11
cpointsN: class Points: 11
ciobj: class InitObj: 11
ctrnN: class Trn: 10
ctr: class tr: 9
ccaset: class SetCat: 9
corhom: class OrHom: 9
cvr: class RVec: 9
cspc: class Lambda: 9
chmo: class HmOp: 9
ccei: class ceiling: 9
ccytp: class CytP: 8
csvec: class SubVec: 8
cpid: class PID: 8
cgoa: class /\g: 8
cgon: class -.g U: 8
cprv: class |=: 8
cgob: class <->g: 6
cgna: class |g: 6
ctanh: class tanh: 5
clsupp: class sup_ x e. A B: 5
ciso: class Iso: 5
csf: class splitFld: 4
cgrm: class Grammar: 4
comn: class OmN: 4
cconvex: class convex: 4
cpsl: class polySplitLim: 4
cibcg: class Ibcg: 4
cgoq: class =g: 4
crqp: class /Qp: 4
csegc: class segc: 4
cfmla: class Fmla: 4
csat: class Sat: 4
cangle: class angle: 4
cqp: class Qp: 4
cgze: class AxExt: 3
cptdfc: class PtDf ( A , B ): 3
cslices: class slices: 3
clgam: class log_G: 3
chlb: class HomLimB: 3
cgzr: class AxRep: 3
csubsmg: class SubSemiGrp: 3
crr3c: class RR3: 3
csf1: class splitFld1: 3
clb: class lb: 3
cqpa: class _Qp: 3
cgzg: class AxReg: 3
cgzu: class AxUn: 3
csmhom: class SemiGrpHom: 3
cpfl: class polyFld: 3
cangc: class angc: 3
csate: class SatE: 3
chlim: class HomLim: 3
ccut: class Cut: 3
citr: class IntgRing: 3
cunif: class Unif: 3
cgzi: class AxInf: 3
cprdct: class prdct: 3
ceqp: class ~Qp: 3
ccpms: class cplMetSp: 3
czr: class ZRing: 3
csbsgrg: class subSemiGrpGen: 3
cgzp: class AxPow: 3
crs: class RingIso: 2
cgfo: class GF_oo: 2
ccp: class Cp: 2
cgam: class _G: 2
ces1: class evalSub1: 2
craffsp: class RAffSp: 2
csnk: class Sink: 2
cunifsp: class UnifSp: 2
crpm: class RPrime: 2
ctopfld: class TopFld: 2
cifunc: class Isofunc: 2
csumo: class SumObj: 2
ctoplnd: class TopLnd: 2
cfsm: class FreeSemiGrp: 2
cfrf: class Frf: 2
cprd2: class prod2_ k e. A G B: 2
czeta: class zeta: 2
czerodiv: class zeroDiv: 2
ctobj: class TermObj: 2
cxmat: class xm: 2
cgf: class GF: 2
clinm: class Hom: 2
cpsd: class mPSDer: 2
ccircle: class Circle: 2
ctcl: class t+: 2
cderv: class derv: 2
ccur2: class cur2: 2
clbl: class BndLat: 2
cai: class AlgInd: 2
clsg: class ^md: 2
cprodo: class ProdObj: 2
csmat: class .m: 2
cgzf: class ZF: 2
csym: class sym: 2
cpin: class piN: 2
copfn: class opfn: 2
cact: class Action: 2
cmhp: class mHomP: 2
cline3: class line3: 2
csfld: class *-Fld: 2
ctp1: class toPoly1: 2
cneug: class Neug: 2
czp: class Zp: 2
ctofld: class Tofld: 2
cmmat: class +m: 2
cslv: class selectVars: 2
cgoo: class \/g: 2
cantidir: class AntiDir: 2
clinfp: class inf_ x e. A B: 2
cretr: class Retr: 2
cplylt: class Poly<: 2
cprd3: class prod3_ k e. A G B: 2
cza: class _ZZ: 2
cisopt: class IsolatedPt: 2
ctopsep: class TopSep: 2
cmadu: class maAdju: 2
ctriangle: class triangle: 2

[Mario Carneiro]

Also, it hasn't come up in our discussion much, but NF_ also brings something to the table. In the example proof http://us.metamath.org/mpegif/flfcnp2.html#25, there is a dummy variable z which is used only because it is needed in the not free idiom, and must usually be disjoint from everything. This is exactly the sort of thing which definitions are used for hiding. Leaving it as this idiom means the user has to make unnecessary choices about irrelevant things, and this adds to the disjoint variable list for the theorem. When you are doing a big proof like pntleml, every dummy variable decision is one more thing to think about, and getting those hidden away is a big part of why I want this.

If you recall my description for mmj2 automatic derivations, I said that it will autoderive theorems that don't introduce new metavariables and shrink the terms. These extra dummies are new metavariables, so that's why mmj2 currently won't autoderive hb* theorems even though it could in principle. If the same statements were written with NF and NF_, these constraints would be satisfied, and it would be able to apply the theorems automatically with the current automation.

Mario

[Stefan O'Rear]

On Sat, Aug 13, 2016 at 3:07 PM, Mario Carneiro <di....@gmail.com> wrote:
> Also, it hasn't come up in our discussion much, but NF_ also brings
> something to the table. In the example proof
> http://us.metamath.org/mpegif/flfcnp2.html#25, there is a dummy variable z
> which is used only because it is needed in the not free idiom, and must
> usually be disjoint from everything. This is exactly the sort of thing which
> definitions are used for hiding. Leaving it as this idiom means the user has
> to make unnecessary choices about irrelevant things, and this adds to the
> disjoint variable list for the theorem. When you are doing a big proof like
> pntleml, every dummy variable decision is one more thing to think about, and
> getting those hidden away is a big part of why I want this.

Hidden variables in definitions are sound because of the chvar system.
If we make chvar depend on definitions with hidden variables, that
circularity would seriously erode my confidence in the soundness of
the system.

-sorear

[Mario Carneiro]

That's the whole point of all these $j annotations. You aren't taking it on faith (anymore), you are specifically linking in a collection of theorems whose properties are known to imply that NF is sound.

Additionally, NF would not be introduced so early as to cause circularity. It would only come in after the relevant theorems have been proven, *without* using it. That is, chvar would be renamed to chvarh but it would otherwise be exactly the same as it is now, and NF_ would not be used in the derivation. The new chvar would then be introduced later, to use NF_ as a replacement for the (ph -> A. x ph) hyp.

Mario

[Norman Megill]

On 8/13/16 10:29 AM, David A. Wheeler wrote:

> The bigger problem is that MPE isn't mobile-friendly.
> You can see this by running this check program:
> https://www.google.com/webmasters/tools/mobile-friendly/

Every html page on us2 should pass this now. If you find one that
doesn't, let me know.

On 8/14/16 9:33 PM, David A. Wheeler wrote:
> Norm:
>

> In file:
> http://us.metamath.org/other.html#verifiers
>
> after the list of verifiers, would you please add:
>
> <a
href="https://github.com/david-a-wheeler/metamath-test">metamath-test</a>
> contains test cases (positive and negative)
> for metamath verifiers and automatically runs them against
> a collection of verifiers.

Done.

On 8/9/16 7:02 PM, David A. Wheeler wrote:
> Also - you might want to update that error message. Macintoshes now
also use
> the line feed character for line breaks (carriage return hasn't been
used for that
> purpose for a long time).

Updated in metamath.exe 0.133.

Norm

[Norman Megill]

On 8/13/16 2:25 PM, Mario Carneiro wrote:
>
>
> On Sat, Aug 13, 2016 at 11:59 AM, Norman Megill <n...@alum.mit.edu
> <mailto:n...@alum.mit.edu>> wrote:
>
> Two situations where words are used are (1) a side condition or
> proviso imposed on a statement, and (2) English prose used to
> describe the statements themselves like in say group theory theorems.
>
> In the second case, of course we have to convert the English to
> formulas with invented symbols because that is what the prose is
> intended to mean.
>
> In the first case, the side condition isn't intended to be part of
> the formula, and it doesn't make sense to convert the side condition
> to a formula. If it did make sense, why wouldn't a formula be used
> in the first place instead of an awkward side condition that can't
> be manipulated easily? It is because the side conditions can't be
> expressed in the language of the logic but involve a separate
> metalogical notion.
>
>
> The side condition is not part of the formula because in most cases it
> isn't possible, in the framework in question. I dare to say that in
> *every* case when a side condition can be converted to a term in the
> expression, this is always done

Then why doesn't the literature use ph -> A. x ph? That is expressible
in the metalanguage of standard FOL.

(Typing judgements come to mind.)
> Metamath is in the interesting situation that we have discovered that
> within our framework, "x is not free in the formula ph" is a condition
> that can be expressed with a formula, and we *have* been using formulas
> for this for a long time - that's not even new with my proposal.

In one of Tarski's 1965 systems (not the set.mm one) he has an axiom:
|- ( ph -> A. x ph ) with the side condition, "if x is not free in ph".
The converse doesn't always hold. In his system that we used for
set.mm, he states our ax-17 as |- ( ph -> A. x ph ) with the side
condition, "if x is not among the variables occurring in ph". Nothing
about not-free-in.

Monk's paper in the 1965 trilogy, p. 113 bottom, states what are
essentially our hbim, hbn, and hbal as axioms to construct cases of ph
-> A.x ph, although he does not give these names other than equation
numbers (nor is ph -> A. x ph ever named).

Nowhere in the trilogy of papers do they identify ph -> A. x ph and
not-free-in. Indeed, if we adopt Tarksi's strict formalism where
everything, even the "not free in" side condition, is defined set
theoretically, the two concepts are provably different.

...

> They are logically equivalent, literally. NF(x, x=x) is logically
> equivalent to NF(x,y=y), which is logically equivalent to "x is not free
> in y=y". Perhaps you wanted something else, like metalogical equivalence
> or something that actually inspects the expression?

However, "x is not free in x=x" is false but NF(x, x=x) is true.

>
> If you really need NF, CondEq, etc. for your $j stuff, they should
> go in a separate section. But why can't you have the software
> recognize the patterns |- ( ph -> A. x ph ), |- ( x = y -> ph ),
> etc. directly? There are likely many more useful patterns, and it
> would be a lot more flexible than having to add a new, odd wff
> definition for each new pattern, which is not something that is
> reader-friendly.
>
>
> I mentioned the reasoning earlier. I want to do as much as possible in
> the .mm file, to make the resulting verifier easier to trust, and make
> everything as explicit as possible.

If you need NF for your verifier, I have no objection to putting it into
a special section of set.mm for that purpose.

> The reason I haven't stopped with my counter-points is because your
> arguments do not sound like more than an emotional response.

In an earlier post you said,

But I think if "NF" shows up in the hypothesis and "not free" shows
up in the theorem comment, this can be cut down to a few seconds.
In this case the name makes it *easier* to understand, not harder,
because it associates the hypothesis with the term "not free", which
may not otherwise be obvious without training (I have never ever
seen any source use this idiom to describe not-freeness except
metamath).

That's because it doesn't mean "not free-in". Tarski et.al. 1965 papers
use both ph -> A. x ph and not-free-in, and for them they are not the
same thing. Unfortunately, they don't give ph -> A. x ph a name.

I think a careful reader could be puzzled when they look up the
definition of ( x not-free-in ph ) and realize that it doesn't really
mean "not free in". That reader may then wonder what other definitions
we are playing fast and loose with and even feel a slight discomfort in
casually trusting other familiar notation.

As I proposed, we can have a hyperlink with a careful explanation in the
comment for each use of ph -> A. x ph. I don't think we should give it
a name, at least not in early set theory, because it isn't named in the
literature. In early set.mm, everything has a literature definition, so
essentially all symbols are immediately recognizable by someone with
some acquaintance with set theory, and I have gone out of my way to
ensure that.

> If anyone
> else is reading this, I'd really like to hear your view because this
> needs community response.

Yes, I would like to hear from others.

Norm

[David A. Wheeler]

On Thu, 18 Aug 2016 17:04:07 -0400, Norman Megill <n...@alum.mit.edu> wrote:
> That's because it doesn't mean "not free-in". Tarski et.al. 1965 papers
> use both ph -> A. x ph and not-free-in, and for them they are not the
> same thing. Unfortunately, they don't give ph -> A. x ph a name.

...

> As I proposed, we can have a hyperlink with a careful explanation in the
> comment for each use of ph -> A. x ph. I don't think we should give it
> a name, at least not in early set theory, because it isn't named in the
> literature.

If you don't want to give it a name early, fine, but it's used often enough
later that a name would be helpful soon afterwards. I think
well-named definitions really help someone understand an expression.

If "not-free-in" is misleading, then that's an argument for a different name.
But what would it be? Anyone have any ideas?

--- David A. Wheeler

[Jens-Wolfhard Schicke-Uffmann]

Hi,

On Thu, Aug 18, 2016 at 05:04:07PM -0400, Norman Megill wrote:
> I think a careful reader could be puzzled when they look up the
> definition of ( x not-free-in ph ) and realize that it doesn't
> really mean "not free in". That reader may then wonder what other
> definitions we are playing fast and loose with and even feel a
> slight discomfort in casually trusting other familiar notation.

I fully agree with this argument. If it looks like a duck, it should
really be as most similar to a duck straight from the literature as
possible. And indeed x is not not-free in x = x.

> As I proposed, we can have a hyperlink with a careful explanation in
> the comment for each use of ph -> A. x ph. I don't think we should
> give it a name, at least not in early set theory, because it isn't
> named in the literature. In early set.mm, everything has a
> literature definition, so essentially all symbols are immediately
> recognizable by someone with some acquaintance with set theory, and
> I have gone out of my way to ensure that.

As a computer science student, I took various courses on formal logic,
but non-freeness was never given a separate symbol and always occurred
as a side-condition.

The start of set.mm has the nice property of only using (ASCII
renderings of) symbols everyone with a minimum background in formal
math seen. Raising non-freeness to a separate symbol would break
this property.

> >If anyone
> >else is reading this, I'd really like to hear your view because this
> >needs community response.
> Yes, I would like to hear from others.

For technical purposes (i.e. writing Igor), I have a slight preference
for keeping ph -> A. x ph; but only because otherwise I'd have to update
code in various places.

But since ph -> A. x ph is not the same as not-free-in, _if_ you decide to
define a separate symbol for it, please don't name it NF. Spontaneous
alternative proposals:
* "SNF" (Semantically non-free)
* "NFE" Non-free in some equivalent
* <] x ph or some other random symbols... The point is to make it
non-alpha, because anything in a formula with only letters is a variable
in the early sections. (c.f. T. / F. )


Regards,
Drahflow

[Mario Carneiro]

On Wed, Aug 24, 2016 at 6:13 PM, Jens-Wolfhard Schicke-Uffmann <drah...@gmx.de> wrote:

Hi,

On Thu, Aug 18, 2016 at 05:04:07PM -0400, Norman Megill wrote:
> I think a careful reader could be puzzled when they look up the
> definition of ( x not-free-in ph ) and realize that it doesn't
> really mean "not free in".  That reader may then wonder what other
> definitions we are playing fast and loose with and even feel a
> slight discomfort in casually trusting other familiar notation.
I fully agree with this argument. If it looks like a duck, it should
really be as most similar to a duck straight from the literature as
possible. And indeed x is not not-free in x = x.

In a literal sense, this is true: NF is "as close to not free as possible", in the sense that we cannot formalize any other predicate that is more like not-free than NF.

> As I proposed, we can have a hyperlink with a careful explanation in
> the comment for each use of ph -> A. x ph.  I don't think we should
> give it a name, at least not in early set theory, because it isn't
> named in the literature.  In early set.mm, everything has a
> literature definition, so essentially all symbols are immediately
> recognizable by someone with some acquaintance with set theory, and
> I have gone out of my way to ensure that.
As a computer science student, I took various courses on formal logic,
but non-freeness was never given a separate symbol and always occurred
as a side-condition.

This continues to baffle me, since it is definitely possible to state that a predicate does not vary with respect to a given parameter as a formula. The only thing I can think is that there are simpler ways to do this if one uses the "explicit parameter list" style (which almost all predicate logics use), by simply omitting the parameter.
 

The start of set.mm has the nice property of only using (ASCII
renderings of) symbols everyone with a minimum background in formal
math seen. Raising non-freeness to a separate symbol would break
this property.

Would moving it out of the early sections resolve this complaint?

> >If anyone
> >else is reading this, I'd really like to hear your view because this
> >needs community response.
> Yes, I would like to hear from others.
For technical purposes (i.e. writing Igor), I have a slight preference
for keeping ph -> A. x ph; but only because otherwise I'd have to update
code in various places.

This is interesting. As I mentioned, making it easier for verifiers is exactly one of the reasons I would like to implement NF or an equivalent. If you were to start from scratch, or if you otherwise did not have to worry about inertia from the current set.mm, would it be easier or harder to use NF and NF_ instead of ph -> A. x ph?
 

But since ph -> A. x ph is not the same as not-free-in, _if_ you decide to
define a separate symbol for it, please don't name it NF. Spontaneous
alternative proposals:
* "SNF" (Semantically non-free)
* "NFE" Non-free in some equivalent
* <] x ph          or some other random symbols... The point is to make it
  non-alpha, because anything in a formula with only letters is a variable
  in the early sections. (c.f. T. / F. )

I actually think that one must be *more* careful to match the literature if one is using a symbol, while an expression of the form ACRONYM ( x , y , z ) can mean whatever we want. Norm has been calling this "(effectively) not free"; does ENF ( x , ph ) do the job?

Mario

[Cris Perdue]

If there is to be such a named predicate, could someone kindly explain to me why it would not be more appropriate to give it a name based on the idea that the formula ph does Not Depend on the variable x, or that the variable x is Not Relevant to formula ph?

E.g.

NR ( x , ph ) or

ND ( ph , x ) or perhaps even

invariant ( ph , x )

Much of the discontent in the discussion appears to be rooted in the fact that whether a variable is free is a syntactic question, but this  predicate is semantic, i.e. does not rely on the variable being syntactically free.

Also, I wonder if such a definition might also be usefully extended to support concepts such as "the absolute value of x does not depend on the sign of x" (with a signum function standing in for "sign"). In other words allowing "x" to be a term that is not necessarily a variable. Such a thing seems like it could be useful also, though a definition might become a bit complex.

-Cris

--
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 metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[David A. Wheeler]

On Thu, 25 Aug 2016 12:25:32 -0700, Cris Perdue <cris....@gmail.com> wrote:
> If there is to be such a named predicate, could someone kindly explain to
> me why it would not be more appropriate to give it a name based on the idea
> that the formula ph does Not Depend on the variable x, or that the variable
> x is Not Relevant to formula ph?
>
> E.g.
> NR ( x , ph ) or
> ND ( ph , x ) or perhaps even
> invariant ( ph , x )

I like this. Maybe there are two steps: Identify the underlying phrase,
then identify its syntax.

1. Possible underlying words: Not relevant, Irrelevant, not depend,
independent, not free, unfree, invariant, ignored.
I don't like "invariant" - that has incompatible meanings in many circles.
I like "Irrelevant", but it's very close to other terms
(Irreflexive, Irrational, irreduceable).

So "Not relevant" is pretty good, let's start there.

2. Next, syntax. The symbol "NR" isn't bad in:

NR ( x , ph )

However, are the parens really helping? This construct is a lot like for-all,
it tells you something about a set variable for a given wff.
I suspect you might be better with this syntax, which is similar to A. and E. :
NR x ph

> Much of the discontent in the discussion appears to be rooted in the fact
> that whether a variable is free is a syntactic question, but this
> predicate is semantic, i.e. does not rely on the variable being
> syntactically free.

Agreed. Using a different term like "not relevant" resolves it
(if there's a new symbol at all).

> Also, I wonder if such a definition might also be usefully extended to
> support concepts such as "the absolute value of x does not depend on the
> sign of x" (with a signum function standing in for "sign"). In other words
> allowing "x" to be a term that is not necessarily a variable. Such a thing
> seems like it could be useful also, though a definition might become a bit
> complex.

I think that'd be overly complex. I think it'd better to have a different
definition for something like that.

BTW, if you want a definition of signum, there's a certain mathbox that can
provide you one free-of-charge :-). I'd love to see signum (sgn) moved into
the "main" part of MPE. It's a standard widely-defined function
(e.g., it's a core part of NIST's standard for math notation).
Anyone have a strong objection to that?

--- David A. Wheeler

[Mario Carneiro]

On Thu, Aug 25, 2016 at 4:27 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Thu, 25 Aug 2016 12:25:32 -0700, Cris Perdue <cris....@gmail.com> wrote:
> If there is to be such a named predicate, could someone kindly explain to
> me why it would not be more appropriate to give it a name based on the idea
> that the formula ph does Not Depend on the variable x, or that the variable
> x is Not Relevant to formula ph?
>
> E.g.
> NR ( x , ph ) or
> ND ( ph , x ) or perhaps even
> invariant ( ph , x )

I like this.

I also agree that this nicely avoids the problems of the "not free" naming.

 

  Maybe there are two steps: Identify the underlying phrase,
then identify its syntax.

1. Possible underlying words: Not relevant, Irrelevant, not depend,
independent, not free, unfree, invariant, ignored.
I don't like "invariant" - that has incompatible meanings in many circles.
I like "Irrelevant", but it's very close to other terms
(Irreflexive, Irrational, irreduceable).

I vote "independent", at least in informal discussion, because "f(x) is independent of x" is probably the most common way to describe this in the literature.

 

So "Not relevant" is pretty good, let's start there.

2. Next, syntax.  The symbol "NR" isn't bad in:
  NR ( x , ph )

For an acronym matching "independent" I might suggest ND = not dependent (although this overlaps a previous usage of ND in some labels meaning non-disjoint), or IND. Alternatively, we could keep the acronym NF but describe it as "independent" in the text of most theorems, with the explanation of the subtleties of "not free" (and why we use the term "independent" instead) described in df-nf.

 

However, are the parens really helping? This construct is a lot like for-all,
it tells you something about a set variable for a given wff.
I suspect you might be better with this syntax, which is similar to A. and E. :
  NR x ph

This I think will render weirdly, since there won't be any space between the "x" and the "ph" (especially when the ph is replaced with a larger expression), unlike A. which is unfortunately being special-cased in the metamath program. You can get some more room with "NR x , ph" but this will conflict with some other uses of the comma, which will make it a bit strange to read, such as "if ( NR_ x , A , B , C )". (It's not ambiguous, but is not parsed the way people would guess at first.) The parens solve this problem by making it clearly a function of two arguments. The downside is that it looks like a function of two arguments, rather than a binding expression (it binds occurrences of x in ph). "NR x : ph" is another alternative that keeps the binder feel without using a comma.

 

> Also, I wonder if such a definition might also be usefully extended to
> support concepts such as "the absolute value of x does not depend on the
> sign of x" (with a signum function standing in for "sign"). In other words
> allowing "x" to be a term that is not necessarily a variable. Such a thing
> seems like it could be useful also, though a definition might become a bit
> complex.

I think that'd be overly complex.  I think it'd better to have a different
definition for something like that.

This would certainly be a different definition, but it's worth consideration anyway. What does it mean though? To say that f(x,y) does not depend on y means that f(x,y) = f(x,z) for all x,y,z. The problem is that this depends not only on the explicit parameter y, but also the implicit other parameter x. If one is given a set with no a priori parameterization, it must be parameterized first, and the choice of parameterization affects the result. For example, there are (at least) two parameterizations (injective functions) for the set R^2: F(x, y) = (x, y) and G(x, y) = (x+y, y). If f:R^2->R is given by f((u,v)) = u+v, then under the first parameterization we have f(F^-1(x, y)) = x+y and in the second we have f(G^-1(x, y)) = x. Then treated as a two argument function w.r.t the parameterization F, it is not independent of y, but it is independent of y in the second parameterization.

The statement that |x| does not depend on sgn(x) actually has nothing to do with sgn(x). It is referring to a parameterization of R with two variables, F(x) = (|x|, sgn(x)), so that if f(z) = |z| we are saying f(F^-1(x,y)) = x (for (x,y) in ran F) which does not depend on y. If we use a different parameterization, such as G(x) = (x, sgn(x)), and write f(G^-1(x,y)) = xy, then it does depend on the second argument.

 

Here's a very general way to state independence along arbitrary contours: If F: A -> B and G : A -onto-> C, then F depends only on G if G(x) = G(y) implies F(x) = F(y). For the standard case of a function of x,y,z not depending on x, let A = R^3 and C = R^2, G(x,y,z) = (y,z). Then (u,v) = (y,z) implies F(w,u,v) = F(x,y,z), or equivalently F(x,y,z) = F(w,y,z). In this case there is a uniquely defined F' : C -> B such that F' o G = F. I'm certain there is a category theory name for this but I'm not sure what it is.

Mario

[David A. Wheeler]

On Sat, 27 Aug 2016 01:00:58 -0400, Mario Carneiro <di....@gmail.com> wrote:
> I vote "independent", at least in informal discussion, because "f(x) is
> independent of x" is probably the most common way to describe this in the
> literature.

That sounds sensible. In the science an "independent" variable has a different meaning,
but there's probably no term that hasn't been used somewhere :-).

> For an acronym matching "independent" I might suggest ND = not dependent
> (although this overlaps a previous usage of ND in some labels meaning
> non-disjoint), or IND. Alternatively, we could keep the acronym NF but
> describe it as "independent" in the text of most theorems, with the
> explanation of the subtleties of "not free" (and why we use the term
> "independent" instead) described in df-nf.

I think "ND" ("not dependent") is a much better choice than "not free".
"Not free" already has a similar but not-the-same meaning, and so I think
using "not free" would confuse instead of enlighten.

David A. Wheeler:

> > However, are the parens really helping? This construct is a lot like
> > for-all,
> > it tells you something about a set variable for a given wff.
> > I suspect you might be better with this syntax, which is similar to A. and
> > E. :
> > NR x ph
> >
>
> This I think will render weirdly, since there won't be any space between
> the "x" and the "ph" (especially when the ph is replaced with a larger
> expression), unlike A. which is unfortunately being special-cased in the
> metamath program.

In for a penny, in for a pound. If "A." is already getting special-cased, just
special-case them both. In the *longer* term you could get rid of the
special-casing by slightly extending the rendering language
("render this as XXXX and after its first term add YYYY")... so there's
a clear path to un-special case it.

> You can get some more room with "NR x , ph" but this will
> conflict with some other uses of the comma, which will make it a bit
> strange to read, such as "if ( NR_ x , A , B , C )". (It's not ambiguous,
> but is not parsed the way people would guess at first.) The parens solve
> this problem by making it clearly a function of two arguments. The downside
> is that it looks like a function of two arguments, rather than a binding
> expression (it binds occurrences of x in ph). "NR x : ph" is another
> alternative that keeps the binder feel without using a comma.

I agree that the comma is a bad choice. I'd mildly prefer no separator,
but I agree that ":" is very decent. So if you'd prefer to not add more
rendering special cases, "ND x : ph" seems very reasonable to mean
"ph is not dependent on the value of x".

--- David A. Wheeler

[Norman Megill]

On 8/24/16 6:58 PM, Mario Carneiro wrote:
>
>
> On Wed, Aug 24, 2016 at 6:13 PM, Jens-Wolfhard Schicke-Uffmann
> <drah...@gmx.de <mailto:drah...@gmx.de>> wrote:
>
> Hi,
>
> On Thu, Aug 18, 2016 at 05:04:07PM -0400, Norman Megill wrote:
> > I think a careful reader could be puzzled when they look up the
> > definition of ( x not-free-in ph ) and realize that it doesn't
> > really mean "not free in". That reader may then wonder what other
> > definitions we are playing fast and loose with and even feel a
> > slight discomfort in casually trusting other familiar notation.
> I fully agree with this argument. If it looks like a duck, it should
> really be as most similar to a duck straight from the literature as
> possible. And indeed x is not not-free in x = x.
>
>
> In a literal sense, this is true: NF is "as close to not free as
> possible", in the sense that we cannot formalize any other predicate
> that is more like not-free than NF.
>
> > As I proposed, we can have a hyperlink with a careful explanation in
> > the comment for each use of ph -> A. x ph. I don't think we should
> > give it a name, at least not in early set theory, because it isn't

> > named in the literature. In early set.mm <http://set.mm>, everything has a

> > literature definition, so essentially all symbols are immediately
> > recognizable by someone with some acquaintance with set theory, and
> > I have gone out of my way to ensure that.
> As a computer science student, I took various courses on formal logic,
> but non-freeness was never given a separate symbol and always occurred
> as a side-condition.
>
>
> This continues to baffle me, since it is definitely possible to state
> that a predicate does not vary with respect to a given parameter as a
> formula. The only thing I can think is that there are simpler ways to do
> this if one uses the "explicit parameter list" style (which almost all
> predicate logics use), by simply omitting the parameter.

The focus of the traditional approach to predicate calculus is to
describe the object language and provide a method for working directly
with the object language. "Not free" is a condition that can be
computed, outside of the logic, to determine if an object-language wff
is or is not an axiom. Once the wff qualifies, a single step would be
added to the actual object-language proof, since the effort to determine
"not free" is not counted.

If we were to replace "not free" with "ph -> A. x ph" in traditional
axiom schemes, we would then have a hypothesis that needs to be proved,
not just a side condition to be calculated.

Actually, the equality axioms are essential ingredients that make
Tarski's and set.mm's systems work, and it isn't clear to me whether we
could dispense with "not free in" and/or "free for" in predicate
calculus _without_ equality, even with additional axioms.

>
>
> The start of set.mm <http://set.mm> has the nice property of only

> using (ASCII
> renderings of) symbols everyone with a minimum background in formal
> math seen. Raising non-freeness to a separate symbol would break
> this property.
>
>
> Would moving it out of the early sections resolve this complaint?

NF is a pretty drastic change to the philosophy and presentation of
set.mm, especially the early parts that are intended to be friendly for
general math/logic audiences without made-up notation they've never seen
before. I still have misgivings about whether it would accomplish
anything useful (outside of your definitional checker) other than a
minor reduction in some proof sizes, with a somewhat heavy price to pay
in terms of being unconventional.

I would like to first see NF uses in a mathbox to begin with, say with
many of the hb*s reproved with the new notation, so we (I) can get a
feel for it. Over time we can decide how far up we feel comfortable
moving them, but I think we should keep them out of the early sections
at least initially and perhaps permanently. Not sure what the cutoff
for "early section" is.

>
> > >If anyone
> > >else is reading this, I'd really like to hear your view because this
> > >needs community response.
> > Yes, I would like to hear from others.
> For technical purposes (i.e. writing Igor), I have a slight preference
> for keeping ph -> A. x ph; but only because otherwise I'd have to update
> code in various places.
>
>
> This is interesting. As I mentioned, making it easier for verifiers is
> exactly one of the reasons I would like to implement NF or an
> equivalent. If you were to start from scratch, or if you otherwise did

> not have to worry about inertia from the current set.mm <http://set.mm>,

> would it be easier or harder to use NF and NF_ instead of ph -> A. x ph?

An issue that hasn't been discussed is the exact definition of NF.

We have to decide whether to use "A. x ( ph -> A. x ph )" or just "( ph
-> A. x ph )" for the NF definition. Let me call these "closed NF" and
"open NF". Virtually all of our uses have open NF as a hypothesis, but
the NF that has been proposed is closed.

Perhaps at some philosophical level, the closed NF version could be
considered desirable since x is (effectively) not free in it. But I
don't think a need for this property arises very often. I doubt we'd
ever need to apply NF to itself, for example. The primary purpose of NF
is as a hypothesis emulating not-free-in, and it is almost always used
stand-alone, just like the real not-free-in.

The more I think about it, a closed NF definition is starting to seem
like the wrong way to do it. Here are 3 reasons for using open NF:

1. An open NF would be easier to retrofit directly, perhaps with some
proofs being slightly smaller that with a closed NF since we don't have
to invoke ax-gen/a4i to add/delete the outer quantifier. It would also
be easier to revert, a consideration (for me at least) if in the future
we change our minds.

2. An open NF has the advantage of communicating to the reader, once its
definition is expanded, its primary purpose of proving instances of |-
ph -> A. x ph (its exact definition). This form always occurs in
Tarski's paper as well as nearly all of our uses. The extra quantifier
is an unnecessary distraction that may cause the reader to wonder why it
is there.

3. Perhaps most important in the long term, the closed NF version is
less general. It is always possible to change open NF to closed by
prefixing it with A. x, but it is impossible to go the other way. This
can be a problem when NF is used as an antecedent. If the theorem can
be proved with an open NF and no A. x prefix, this is a much stronger
result than the same theorem having a closed NF as the antecedent.

Norm

[Mario Carneiro]

On Sat, Aug 27, 2016 at 10:15 PM, Norman Megill <n...@alum.mit.edu> wrote:

On 8/24/16 6:58 PM, Mario Carneiro wrote:

On Wed, Aug 24, 2016 at 6:13 PM, Jens-Wolfhard Schicke-Uffmann
<drah...@gmx.de <mailto:drah...@gmx.de>> wrote:
    As a computer science student, I took various courses on formal logic,
    but non-freeness was never given a separate symbol and always occurred
    as a side-condition.


This continues to baffle me, since it is definitely possible to state
that a predicate does not vary with respect to a given parameter as a
formula. The only thing I can think is that there are simpler ways to do
this if one uses the "explicit parameter list" style (which almost all
predicate logics use), by simply omitting the parameter.

The focus of the traditional approach to predicate calculus is to describe the object language and provide a method for working directly with the object language.  "Not free" is a condition that can be computed, outside of the logic, to determine if an object-language wff is or is not an axiom.  Once the wff qualifies, a single step would be added to the actual object-language proof, since the effort to determine "not free" is not counted.

If we were to replace "not free" with "ph -> A. x ph" in traditional axiom schemes, we would then have a hypothesis that needs to be proved, not just a side condition to be calculated.

So? If this means that no "not free" discussion needs to come up, that seems like a plus. Then again, you probably would want the equivalent of ax-17 in any logic, and then "not free" must arise (unless you can prove it as a metatheorem).
 

Actually, the equality axioms are essential ingredients that make Tarski's and set.mm's systems work, and it isn't clear to me whether we could dispense with "not free in" and/or "free for" in predicate calculus _without_ equality, even with additional axioms.

I don't know what you mean by this. NF does not need equality for its definition. What does it mean to "dispense" with NF? Since it's a definition, you have it automatically given forall and implies. If you mean the FOL "not free", we don't even have that in set.mm (as you have gone to pains to point out, NF the definition is not the same thing).

 

    The start of set.mm <http://set.mm> has the nice property of only
    using (ASCII
    renderings of) symbols everyone with a minimum background in formal
    math seen. Raising non-freeness to a separate symbol would break
    this property.


Would moving it out of the early sections resolve this complaint?

NF is a pretty drastic change to the philosophy and presentation of set.mm, especially the early parts that are intended to be friendly for general math/logic audiences without made-up notation they've never seen before.  I still have misgivings about whether it would accomplish anything useful (outside of your definitional checker) other than a minor reduction in some proof sizes, with a somewhat heavy price to pay in terms of being unconventional.

I would like to first see NF uses in a mathbox to begin with, say with many of the hb*s reproved with the new notation, so we (I) can get a feel for it.  Over time we can decide how far up we feel comfortable moving them, but I think we should keep them out of the early sections at least initially and perhaps permanently.  Not sure what the cutoff for "early section" is.

Well, I can show you my branch that introduces NF and works some basic stuff out; since there are some 100 or so hb* theorems to replace I'd prefer not to go whole-hog with a project of uncertain future, but if I can get some clearance for NF or ND or the other isomorphic versions, I could work it out and see how much size reduction there is. (Of course the size reduction is much more if the hb* theorems are deleted.) The "early section" thing is very much cosmetic; it is very simple to take df-nf and all its dependents and move it downward to any later point (including into a mathbox).
 

    > >If anyone
    > >else is reading this, I'd really like to hear your view because this
    > >needs community response.
    > Yes, I would like to hear from others.
    For technical purposes (i.e. writing Igor), I have a slight preference
    for keeping ph -> A. x ph; but only because otherwise I'd have to update
    code in various places.


This is interesting. As I mentioned, making it easier for verifiers is
exactly one of the reasons I would like to implement NF or an
equivalent. If you were to start from scratch, or if you otherwise did
not have to worry about inertia from the current set.mm <http://set.mm>,
would it be easier or harder to use NF and NF_ instead of ph -> A. x ph?

An issue that hasn't been discussed is the exact definition of NF.

We have to decide whether to use "A. x ( ph -> A. x ph )" or just "( ph -> A. x ph )" for the NF definition.  Let me call these "closed NF" and "open NF".  Virtually all of our uses have open NF as a hypothesis, but the NF that has been proposed is closed.

Let me start with my explanation for this choice. As part of the LF translation, I need to figure out, for each definition containing a set variable, if the variable's appearences in other (wff/class) variables are bound, free, or both. It appears bound if the wff variable is in a forall for the set variable, these determine the dependencies for the wff variable; then if there are any free occurrences of the variable it appears free in the definition. For the case of open NF (ph -> A. x ph), since ph is in the quantifier A. x, it depends on x, so this is annotated as (ph(x) -> A. x ph(x)). Since ph(x) depends on x, occurrences of x in ph are bound in openNF(x, ph), but because the first x is free, occurrences of x in ph are also free in openNF(x, ph).

This means that as a binding definition, openNF has type set -> (set -> wff) -> wff, that is, it takes both ph(x), a function of x outputting a wff, as well as x itself (in order to evaluate that ph(x) on the left). This would be used in LF using the notation (openNF x (lambda x: ph)), so x shows up twice. (A similar issue occurs with df-ixp, in which A has x both bound and free because it appears twice in the definition, once inside a forall and once outside, causing the x to "leak" out).

By contrast, with (closed) NF, we have both occurrences of ph(x) bound by the outer A. x, so occurrences of x in ph are only bound, not free, so NF gets the type (set -> wff) -> wff, which is the same as wal : (set -> wff) -> wff, as well as wex and other simple binders. This gets invoked as (NF (lambda x: ph)).

The question about this extra parameter is: is it needed? What exactly is the meaning of the first parameter of openNF? Now, you probably aren't interested in the LF interpretation of these definitions, but this is actually visible in standard set.mm. The fact that wal and wex are simple binders that don't have any free occurrences of x means that you get a bound variable changing theorem:

$e |- ( x = y -> ( ph <-> ps ) )

$p |- ( A. x ph <-> A. y ps )
$p |- ( E. x ph <-> E. y ps )
$p |- ( NF ( x , ph ) <-> NF ( y , ps ) )

 

With openNF, you only get the weaker form for "mixed binding" operators:

$e |- ( x = y -> ( ph <-> ps ) )

$p |- ( x = y -> ( openNF ( x , ph ) <-> openNF ( y , ps ) ) )

Perhaps at some philosophical level, the closed NF version could be considered desirable since x is (effectively) not free in it.  But I don't think a need for this property arises very often.  I doubt we'd ever need to apply NF to itself, for example.  The primary purpose of NF is as a hypothesis emulating not-free-in, and it is almost always used stand-alone, just like the real not-free-in.

The more I think about it, a closed NF definition is starting to seem like the wrong way to do it.  Here are 3 reasons for using open NF:

1. An open NF would be easier to retrofit directly, perhaps with some proofs being slightly smaller that with a closed NF since we don't have to invoke ax-gen/a4i to add/delete the outer quantifier.  It would also be easier to revert, a consideration (for me at least) if in the future we change our minds.

This is not a problem, because |- openNF ( x , ph ) iff |- NF ( x , ph ), so they *are* freely interchangeable. The very first theorems I prove for NF are translations from |- NF(x, ph) to and from |- (ph -> A. x ph). openNF is never used in any position except at the top level; when it does appear in other positions it is always closed over.

Furthermore, even these theorems are only used in the proofs of primitive NF theorems nfim, nfa1, nfa, nfn. For basically everything else it is just NF distribution theorems, so you don't even need to refer to the definition.

 

2. An open NF has the advantage of communicating to the reader, once its definition is expanded, its primary purpose of proving instances of |- ph -> A. x ph (its exact definition).   This form always occurs in Tarski's paper as well as nearly all of our uses.  The extra quantifier is an unnecessary distraction that may cause the reader to wonder why it is there.

It is really the *statement* ph -> A. x ph that appears, or the *theorem* |- ph -> A. x ph? The statement is not of much use, while the closed NF better represents, as a statement, the theorem expressed by NF (that is, the predicate "ph is independent of x"), which allows it to be used as a regular statement, which can be negated or placed in a hypothesis like any other statement. (In particular, it makes the statements of closed form hypothesis builders like hbnt much simpler and easier to interpret.)

 

3. Perhaps most important in the long term, the closed NF version is less general.  It is always possible to change open NF to closed by prefixing it with A. x, but it is impossible to go the other way.  This can be a problem when NF is used as an antecedent.  If the theorem can be proved with an open NF and no A. x prefix, this is a much stronger result than the same theorem having a closed NF as the antecedent.

Please point me to such a theorem; they seem to be exceedingly rare. The *overwhelming* majority of occurrences of open (ph -> A. x ph) in set.mm are in root position. More to the point, if such a theorem exists, it is not talking about independence in the sense meant by NF, so I think it is quite appropriate to not allow this to use the definition, and instead write out (ph -> A. x ph) directly. The statement that ph(y) -> A. x ph(x) for a *specific* y has little to do with ph(x) being independent of x, but knowing that this is true for all y implies that ph(x) <-> ph(y) which is what we are trying to capture.

Mario

[Norman Megill]

I'm tired of discussing this and admit defeat. :) Mario, you can add
the predicate (the closed version as you prefer) wherever you want in
set.mm. The definition should have a very clear descriptive comment,
since a lot of people will be clicking on the "syntax hint" for it. DAW
may want to review it from his perspective.

As for notation, "Independent" (Ind, ND, etc.) is a reasonable choice
that distances the notation from "not free in". However, the idiom "|-
( ph -> A. x ph )" is really asserting something almost but not quite
"not free in", and "Ind" may be going to far in the other direction,
suggesting it's an unrelated concept.

On the other hand, we've more or less agreed that NF is too close to
"not free in" and possibly misleading, suggesting the two concepts are
identical.

So I'm casting a vote for "effectively not free in" (ENF or similar)
that I think suggests exactly what the notation means: something almost
("effectively") but not quite "not free in".

I don't have a strong preference for the exact syntax ["( x ENF ph )",
"ENF x ph", "ENF ( x , ph )", etc.] and will let others iron it out.

Norm

[Mario Carneiro]

Any objection to using "ENF" for the symbol and "nf" for the label segment? I'd like to have a two-letter label to keep it as short as "hb" theorems, but "nd" is already taken for non-disjoint ZFC axioms (e.g. axacnd).

Mario

Norm

[Norman Megill]

On 8/28/16 2:52 PM, Mario Carneiro wrote:
> Any objection to using "ENF" for the symbol and "nf" for the label
> segment? I'd like to have a two-letter label to keep it as short as "hb"
> theorems, but "nd" is already taken for non-disjoint ZFC axioms (e.g.
> axacnd).

No objection.

Norm

[Norman Megill]

It might be useful to rename old version of a theorem reproved with ENF
with an "ENF" suffix, meaning "this is the old version of a theorem
reproved with ENF". Eventually *ENF could be treated like *OLD and
deleted, but in the interim it could provide for before/after
comparisons and other statistics. It could also guide the conversion;
for example, "show usage hbimENF" will list only *ENF theorems when all
conversion is done.

In the case of hb*ENF, the new version would be named nf*, but for all
others the new name would normally be the old name without the ENF
suffix. The ones without *ENF in the "show label hb*" listing would
indicate which hb*'s haven't been converted.

Norm

[Jens-Wolfhard Schicke-Uffmann]

Hi,

sorry for late reply, but just in case...

On Wed, Aug 24, 2016 at 06:58:01PM -0400, Mario Carneiro wrote:
> On Thu, Aug 18, 2016 at 05:04:07PM -0400, Norman Megill wrote:
> > >If anyone
> > >else is reading this, I'd really like to hear your view because this
> > >needs community response.
> > Yes, I would like to hear from others.
> For technical purposes (i.e. writing Igor), I have a slight preference
> for keeping ph -> A. x ph; but only because otherwise I'd have to update
> code in various places.
> This is interesting. As I mentioned, making it easier for verifiers is exactly
> one of the reasons I would like to implement NF or an equivalent. If you were
> to start from scratch, or if you otherwise did not have to worry about inertia
> from the current set.mm, would it be easier or harder to use NF and NF_ instead
> of ph -> A. x ph?

It would be pretty much the same in the igor codebase, really.

Where ph -> A. x ph is treated as a special case, I could just as
well have matched against ENF x : ph Since it would be parsed in
a single step, runtime on large proof scripts would probably improve
marginally by such a change.


Regards,
Drahflow