Metamath's set.mm and ISO 80000-2
60 views
Skip to first unread message
David A. Wheeler
Apr 27, 2015, 11:15:04 PM4/27/15
to metamath
I've been looking at improving set.mm's support for ISO 80000-2:2009 ("Mathematical signs and symbols to be used in the natural sciences and technology"), particularly for cases where it's not too painful to do. This international standard defines a set of signs and symbols that ISO thinks are widely used, and thus need defining. If the Metamath Proof Explorer is supposed to describe "familiar mathematical facts", I think it should be defining the facts widely used in documents such as this standard, using its notation where reasonable.
Here's what I see so far.
A LOT of stuff from ISO is already in set.mm. They recommend using italics for variables, and upright (non-italic) for constants (including the names of specific functions), and that seems to be generally true for the generated HTML. ISO recommends the form "∀x ∈ A φ", which is already supported by wral and df-ral (ISO also accepts "∀x φ" where the universe is defined, and that is the key underlying construct in metamath). The symbols for "and", "or", "not", "member", and so on, are all the same too.
Some of ISO 80000-2 is not in set.mm and I expect it would be too hard to implement. The most obvious is function application; the ISO spec uses f(x), while set.mm uses (f ` x). Similarly, ISO recommends g(x,y), with g(x;y) noted as an alternative. I actually wish metamath.mm did support f(x) and g(x,y), as that is what everyone else uses. However, I know the current set.mm notation was carefully chosen, and I presume that's not worth trying to change or that it would be impractical to do. Also, some symbols are fundamentally 2-dimensional, and that won't work in metamath; an example is the binomial coefficient where n is stacked over k inside parentheses (I've never been a fan of that notation anyway).
Some things are implementable but involve nontrivial changes. It's not clear those changes would be worth it, but it might be worth discussing. For example, ISO uses p => q for implication (two-line), not p -> q (they use -> for expressions involving limits), and same is true for "<=>". Metamath uses "->", not "=>", in its real notation (the "=>" is generated in the HTML in some special cases, but that could be changed to another symbol). Is that worth changing? I know that both "->" and "=>" are in use for implication out in the real world, and that some people use them for different meanings (e.g., connective vs. logical consequence). Is there a reason metamath uses "->" instead of "=>"?
Many changes are easily made as extensions to set.mm. A big potential change, which I think is vitally important but others do not, would be to add definitions for the standard mathematical symbols defined by ISO. These include greater-than, sinh, cot, lb [log base 2], N* [natural numbers not including 0], and so on. I'm well aware that my belief is not universally shared :-). Still, I think a work like set.mm that is supposed to arrive at "familiar mathematical facts" should include formal definitions of the mathematical symbols that are defined in the international standard for mathematical symbols. At least, I hope it helps make my case :-). My current evil plan is to stick some of these into my mathbox, and then see if I can talk you guys into promoting them into the main body :-).
--- David A. Wheeler
Here's what I see so far.
A LOT of stuff from ISO is already in set.mm. They recommend using italics for variables, and upright (non-italic) for constants (including the names of specific functions), and that seems to be generally true for the generated HTML. ISO recommends the form "∀x ∈ A φ", which is already supported by wral and df-ral (ISO also accepts "∀x φ" where the universe is defined, and that is the key underlying construct in metamath). The symbols for "and", "or", "not", "member", and so on, are all the same too.
Some of ISO 80000-2 is not in set.mm and I expect it would be too hard to implement. The most obvious is function application; the ISO spec uses f(x), while set.mm uses (f ` x). Similarly, ISO recommends g(x,y), with g(x;y) noted as an alternative. I actually wish metamath.mm did support f(x) and g(x,y), as that is what everyone else uses. However, I know the current set.mm notation was carefully chosen, and I presume that's not worth trying to change or that it would be impractical to do. Also, some symbols are fundamentally 2-dimensional, and that won't work in metamath; an example is the binomial coefficient where n is stacked over k inside parentheses (I've never been a fan of that notation anyway).
Some things are implementable but involve nontrivial changes. It's not clear those changes would be worth it, but it might be worth discussing. For example, ISO uses p => q for implication (two-line), not p -> q (they use -> for expressions involving limits), and same is true for "<=>". Metamath uses "->", not "=>", in its real notation (the "=>" is generated in the HTML in some special cases, but that could be changed to another symbol). Is that worth changing? I know that both "->" and "=>" are in use for implication out in the real world, and that some people use them for different meanings (e.g., connective vs. logical consequence). Is there a reason metamath uses "->" instead of "=>"?
Many changes are easily made as extensions to set.mm. A big potential change, which I think is vitally important but others do not, would be to add definitions for the standard mathematical symbols defined by ISO. These include greater-than, sinh, cot, lb [log base 2], N* [natural numbers not including 0], and so on. I'm well aware that my belief is not universally shared :-). Still, I think a work like set.mm that is supposed to arrive at "familiar mathematical facts" should include formal definitions of the mathematical symbols that are defined in the international standard for mathematical symbols. At least, I hope it helps make my case :-). My current evil plan is to stick some of these into my mathbox, and then see if I can talk you guys into promoting them into the main body :-).
--- David A. Wheeler
Mario Carneiro
Apr 28, 2015, 12:59:28 AM4/28/15
to metamath
On Mon, Apr 27, 2015 at 11:15 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
Some of ISO 80000-2 is not in set.mm and I expect it would be too hard to implement. The most obvious is function application; the ISO spec uses f(x), while set.mm uses (f ` x). Similarly, ISO recommends g(x,y), with g(x;y) noted as an alternative. I actually wish metamath.mm did support f(x) and g(x,y), as that is what everyone else uses. However, I know the current set.mm notation was carefully chosen, and I presume that's not worth trying to change or that it would be impractical to do.
Indeed,
this is a "necessary sacrifice", not a deliberate deviation from the
literature. It is impossible due to "technical difficulties". More
precisely, if df-fv was "A ( B )" then it would be a suffix notation (a
class expression that begins with a class expression), and it is
impossible to have both prefix and suffix constructors in the same
grammar without ambiguity - taking "-u A" as an example of a prefix
notation, "-u A ( B )" has the two derivations "cA cB cfv cneg" and "cA
cneg cB cfv". It is possible to use "` A ( B )" and hide the backtick,
but I wonder if this is not more strange and inconvenient.
Note
that it is possible to use the notation "XX ( B )" if XX is a constant,
by defining the entire thing as one piece of syntax. But this requires
"convenience theorems" like equality and hypothesis builders for each
new constant, so it is not generally used unless there are other reasons
to have special syntax, such as allowing the input or output to be a
proper class. Examples include df-if, df-rdg, df-sup.
Also, some symbols are fundamentally 2-dimensional, and that won't work in metamath; an example is the binomial coefficient where n is stacked over k inside parentheses (I've never been a fan of that notation anyway).
Some things are implementable but involve nontrivial changes. It's not clear those changes would be worth it, but it might be worth discussing. For example, ISO uses p => q for implication (two-line), not p -> q (they use -> for expressions involving limits), and same is true for "<=>". Metamath uses "->", not "=>", in its real notation (the "=>" is generated in the HTML in some special cases, but that could be changed to another symbol). Is that worth changing? I know that both "->" and "=>" are in use for implication out in the real world, and that some people use them for different meanings (e.g., connective vs. logical consequence). Is there a reason metamath uses "->" instead of "=>"?
I
have also noted this, as HOL seems to prefer "==>" for implication.
Since the change is trivial (even if it touches every theorem in the
database), I don't have a strong opinion for either -> or => .
However, it should be noted that the web page uses "&" and "=>"
for connectives between hypotheses and from hypothesis to conclusion,
which is to say that "|- ph & |- ps => |- ch" is the equivalent
to metamath's
thm.1 $e |- ph $.
thm.2 $e |- ps $.
thm $p |- ch $= ... $.
as it is displayed in one-line proof formats, namely in the statement list and on the explanatory web pages like ax-mp at http://us2.metamath.org:88/mpegif/mmset.html#scaxioms
. So in this sense one can understand "->" as an implication at a
"smaller level" than the statement implication "=>", and then if
"->" is changed to "=>" what should "=>" become?
Furthermore,
it appears to be standard in logic textbooks to use "->" in actual
formulas, especially when they are being nested. To me, => as
implication makes more sense if it is rare and surrounded by plain text,
and I wonder if this is the context being addressed by ISO 80000
Many changes are easily made as extensions to set.mm. ... These include ... lb [log base 2],
Are
you sure you got that right, because I would call that a misstep on
ISO's part. I have only ever seen "lg" to mean log base 2, not "lb".
(Perhaps they wanted to claim "lg" for log base 10, but that's just
confusing...)
This is actually a good point, though,
in that we have no definition of log with general base; since we have ^c
it seems reasonable to extend log to other bases as well. I'm a bit
torn on the notation, though; options are "( B log_ A )", "( ( log_ ` B )
` A )", and "( log_ B ` A )" to mean log base B of A. A possible
definition (according to the last notation) might be
log_ B = ( a e. ( CC \ { 0 } ) |-> ( ( log ` a ) / ( log ` B ) ) )
N* [natural numbers not including 0],
Now
here's a minefield. No one ever seems to be able to come to consensus
on whether 0 e. NN. Given such a choice, the "other" definition ( NN \ {
0 } ) = NN* or ( NN u. { 0 } ) = NN0 is easily notated, but NN itself
is certainly not "agreed upon" with either definition. That said, it is
simple to change this in the database (although from a pedagogical point
of view I would prefer the initial development start with NN0 and
define NN* in terms of it, if NN0 gets the more fundamental symbol).
Mario
David A. Wheeler
Apr 28, 2015, 10:24:05 AM4/28/15
to metamath, metamath
David A. Wheeler wrote:
> > Some of ISO 80000-2 is not in set.mm and I expect it would be too hard to
> > implement. The most obvious is function application; the ISO spec uses
> > f(x), while set.mm uses (f ` x)...
> > Some of ISO 80000-2 is not in set.mm and I expect it would be too hard to
> > implement. The most obvious is function application; the ISO spec uses
Mario Carneiro replied:
> Indeed, this is a "necessary sacrifice", not a deliberate deviation from
> the literature. It is impossible due to "technical difficulties". More
> precisely, if df-fv was "A ( B )" then it would be a suffix notation (a
> class expression that begins with a class expression), and it is impossible
> to have both prefix and suffix constructors in the same grammar without
> ambiguity...
> the literature. It is impossible due to "technical difficulties". More
> precisely, if df-fv was "A ( B )" then it would be a suffix notation (a
> class expression that begins with a class expression), and it is impossible
> to have both prefix and suffix constructors in the same grammar without
Technically it's possible to do both, since many parsers do *exactly* this,
but I know what you mean - it would require a fundamental change to support
them all directly.
> It is possible to use "` A ( B )" and hide the backtick, but I wonder if this is
> not more strange and inconvenient.
I guess the question is, what is more aesthetically pleasing:
( sin
> 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+u...@googlegroups.com.
> To post to this group, send email to meta...@googlegroups.com.
> Visit this group at http://groups.google.com/group/metamath.
> For more options, visit https://groups.google.com/d/optout.
David A. Wheeler
Apr 28, 2015, 11:00:15 AM4/28/15
to metamath
(Sorry, my previous email was sent when I was only halfway done writing it.)
David A. Wheeler wrote:
> > Some of ISO 80000-2 is not in set.mm and I expect it would be too hard to
> > implement. The most obvious is function application; the ISO spec uses
> > f(x), while set.mm uses (f ` x)...
Mario Carneiro replied:
> Indeed, this is a "necessary sacrifice", not a deliberate deviation from
> the literature. It is impossible due to "technical difficulties". More
> precisely, if df-fv was "A ( B )" then it would be a suffix notation (a
> class expression that begins with a class expression), and it is impossible
> to have both prefix and suffix constructors in the same grammar without
> ambiguity...
Technically it's possible to do both, since many parsers do *exactly* this,
but I know what you mean - it would require a fundamental change.
So let's presume that's *not* on the table.
> It is possible to use "` A ( B )" and hide the backtick, but I wonder if this is
> not more strange and inconvenient.
That's an interesting possibility. It basically treats ` as an "apply" operator.
I'm not even sure you need to hide the backtick; that might be a separate issue.
` sin ( x )
It's exactly the same number of symbols, and same number of characters.
Since ` sin ( x ) is more similar to traditional notation, perhaps
that should be seriously considered. It'd be a big change.
On the other hand, it's probably automatable and justifiable.
I typically look at the HTML as the "published" version of the work, and
I suspect this change would make the "published" version look much better
(it'd be closer in form to traditional notation).
How would multi-argument functions best be handled, if this big change were done?
> > Note that it is possible to use the notation "XX ( B )" if XX is a
> > constant, by defining the entire thing as one piece of syntax. But this
> > requires "convenience theorems" like equality and hypothesis builders...
From a *syntactic* view that'd be ideal, but I understand that the extra
work is undesirable.
> > > Some things are implementable but involve nontrivial changes. It's not
> > > clear those changes would be worth it, but it might be worth discussing.
> > > For example, ISO uses p => q for implication (two-line), not p -> q (they
> > > use -> for expressions involving limits), and same is true for "<=>".
> > > Metamath uses "->", not "=>", in its real notation (the "=>" is generated
> > > in the HTML in some special cases, but that could be changed to another
> > > symbol). Is that worth changing?...
> > I have also noted this, as HOL seems to prefer "==>" for implication. Since
> > the change is trivial (even if it touches every theorem in the database), I
> > don't have a strong opinion for either -> or => . However, it should be
> > noted that the web page uses "&" and "=>" for connectives between
> > hypotheses and from hypothesis to conclusion...
Right, that's what I meant when I said that the "=>" is generated in the HTML.
> ... if "->" is changed to "=>" what should "=>" become?
Lots of other symbols are available.
My immediate thought is the 3 dot "therefore" sign, documented here:
http://en.wikipedia.org/wiki/Therefore_sign
and available in HTML as ∴
> > Furthermore, it appears to be standard in logic textbooks to use "->" in
> > actual formulas, especially when they are being nested. To me, => as
> > implication makes more sense if it is rare and surrounded by plain text,
> > and I wonder if this is the context being addressed by ISO 80000
I suspect that many logic textbooks that use -> primarily focus only on logic,
and do NOT also include limits, derivatives, and integrals (which ALSO traditionally
use -> but for a completely different meaning). I note that the ISO spec uses ->
for these latter meanings.
> > Are you sure you got that right, because I would call that a misstep on
> > ISO's part. I have only ever seen "lg" to mean log base 2, not "lb".
> > (Perhaps they wanted to claim "lg" for log base 10, but that's just
> > confusing...)
ISO does indeed define log as the two-argument version, and then define:
lg: common/decimal log, base 10
lb: binary log, base 2
ln: natural log, base e
IIRC, this has been a typical problem. "Everyone" knows what the base of log is,
it's the one they use. Engineers presume that log is base 10,
Computer Scientists presume that log is base 2 (so they'll write "log x" meaning "log base 2"),
and some mathematicians presume that log is base e.
Engineers build the calculators, so "log" means "base 10" on calculators.
I've never seen "lg" to mean log base 2, but I *have* seen "log" to mean base 2.
> >
> > This is actually a good point, though, in that we have no definition of log
> > with general base; since we have ^c it seems reasonable to extend log to
> > other bases as well. I'm a bit torn on the notation, though; options are "(
> > B log_ A )", "( ( log_ ` B ) ` A )", and "( log_ B ` A )" to mean log base
> > B of A. A possible definition (according to the last notation) might be
> >
> > log_ B = ( a e. ( CC \ { 0 } ) |-> ( ( log ` a ) / ( log ` B ) ) )
I think the current current "log" should be renamed as "ln", because
that is unambiguous. Then define a 2-argument log.
If the function application notation were changed, this is an obvious example
of the question, "how can multi-argument functions best be handled?"
> > > N* [natural numbers not including 0],
> >
> > Now here's a minefield. No one ever seems to be able to come to consensus
> > on whether 0 e. NN.
> > Given such a choice, the "other" definition ( NN \ { 0
> > } ) = NN* or ( NN u. { 0 } ) = NN0 is easily notated, but NN itself is
> > certainly not "agreed upon" with either definition.
I'm well aware of this. It's very useful to have a set starting with 0, and a set
starting with 1, and it's sad that people can't universally agree on the names of these two sets.
On the other hand, if we can appeal to an international
standard, we at least have a good justification for the choice used.
I also like the "*" convention that means "do not include 0". 0 is special
(e.g., can't divide by it), so having a shorthand for it is useful in other areas.
> > That said, it is simple
> > to change this in the database (although from a pedagogical point of view I
> > would prefer the initial development start with NN0 and define NN* in terms
> > of it, if NN0 gets the more fundamental symbol).
Sure. As a long as the development makes sense.
--- David A. Wheeler
David A. Wheeler wrote:
> > Some of ISO 80000-2 is not in set.mm and I expect it would be too hard to
> > implement. The most obvious is function application; the ISO spec uses
> > f(x), while set.mm uses (f ` x)...
Mario Carneiro replied:
> Indeed, this is a "necessary sacrifice", not a deliberate deviation from
> the literature. It is impossible due to "technical difficulties". More
> precisely, if df-fv was "A ( B )" then it would be a suffix notation (a
> class expression that begins with a class expression), and it is impossible
> to have both prefix and suffix constructors in the same grammar without
> ambiguity...
Technically it's possible to do both, since many parsers do *exactly* this,
So let's presume that's *not* on the table.
> It is possible to use "` A ( B )" and hide the backtick, but I wonder if this is
> not more strange and inconvenient.
That's an interesting possibility. It basically treats ` as an "apply" operator.
I guess the question is, what is more aesthetically pleasing:
( sin ` x )
` sin ( x )
It's exactly the same number of symbols, and same number of characters.
Since ` sin ( x ) is more similar to traditional notation, perhaps
that should be seriously considered. It'd be a big change.
On the other hand, it's probably automatable and justifiable.
I typically look at the HTML as the "published" version of the work, and
I suspect this change would make the "published" version look much better
(it'd be closer in form to traditional notation).
How would multi-argument functions best be handled, if this big change were done?
> > Note that it is possible to use the notation "XX ( B )" if XX is a
> > constant, by defining the entire thing as one piece of syntax. But this
From a *syntactic* view that'd be ideal, but I understand that the extra
work is undesirable.
> > > Some things are implementable but involve nontrivial changes. It's not
> > > clear those changes would be worth it, but it might be worth discussing.
> > > For example, ISO uses p => q for implication (two-line), not p -> q (they
> > > use -> for expressions involving limits), and same is true for "<=>".
> > > Metamath uses "->", not "=>", in its real notation (the "=>" is generated
> > > in the HTML in some special cases, but that could be changed to another
> > I have also noted this, as HOL seems to prefer "==>" for implication. Since
> > the change is trivial (even if it touches every theorem in the database), I
> > don't have a strong opinion for either -> or => . However, it should be
> > noted that the web page uses "&" and "=>" for connectives between
Right, that's what I meant when I said that the "=>" is generated in the HTML.
> ... if "->" is changed to "=>" what should "=>" become?
Lots of other symbols are available.
My immediate thought is the 3 dot "therefore" sign, documented here:
http://en.wikipedia.org/wiki/Therefore_sign
and available in HTML as ∴
> > Furthermore, it appears to be standard in logic textbooks to use "->" in
> > actual formulas, especially when they are being nested. To me, => as
> > implication makes more sense if it is rare and surrounded by plain text,
> > and I wonder if this is the context being addressed by ISO 80000
and do NOT also include limits, derivatives, and integrals (which ALSO traditionally
use -> but for a completely different meaning). I note that the ISO spec uses ->
for these latter meanings.
> > Are you sure you got that right, because I would call that a misstep on
> > ISO's part. I have only ever seen "lg" to mean log base 2, not "lb".
> > (Perhaps they wanted to claim "lg" for log base 10, but that's just
> > confusing...)
lg: common/decimal log, base 10
lb: binary log, base 2
ln: natural log, base e
IIRC, this has been a typical problem. "Everyone" knows what the base of log is,
it's the one they use. Engineers presume that log is base 10,
Computer Scientists presume that log is base 2 (so they'll write "log x" meaning "log base 2"),
and some mathematicians presume that log is base e.
Engineers build the calculators, so "log" means "base 10" on calculators.
I've never seen "lg" to mean log base 2, but I *have* seen "log" to mean base 2.
> >
> > This is actually a good point, though, in that we have no definition of log
> > with general base; since we have ^c it seems reasonable to extend log to
> > other bases as well. I'm a bit torn on the notation, though; options are "(
> > B log_ A )", "( ( log_ ` B ) ` A )", and "( log_ B ` A )" to mean log base
> > B of A. A possible definition (according to the last notation) might be
> >
> > log_ B = ( a e. ( CC \ { 0 } ) |-> ( ( log ` a ) / ( log ` B ) ) )
that is unambiguous. Then define a 2-argument log.
If the function application notation were changed, this is an obvious example
of the question, "how can multi-argument functions best be handled?"
> > > N* [natural numbers not including 0],
> >
> > Now here's a minefield. No one ever seems to be able to come to consensus
> > on whether 0 e. NN.
> > Given such a choice, the "other" definition ( NN \ { 0
> > } ) = NN* or ( NN u. { 0 } ) = NN0 is easily notated, but NN itself is
> > certainly not "agreed upon" with either definition.
starting with 1, and it's sad that people can't universally agree on the names of these two sets.
On the other hand, if we can appeal to an international
standard, we at least have a good justification for the choice used.
I also like the "*" convention that means "do not include 0". 0 is special
(e.g., can't divide by it), so having a shorthand for it is useful in other areas.
> > That said, it is simple
> > to change this in the database (although from a pedagogical point of view I
> > would prefer the initial development start with NN0 and define NN* in terms
> > of it, if NN0 gets the more fundamental symbol).
--- David A. Wheeler
David A. Wheeler
Apr 28, 2015, 12:04:04 PM4/28/15
to metamath, metamath
Mario Carneiro replied:
for the function if there's no operation symbol in the operand and there's
only one operand. So perhaps this is an alternative syntax for the one-operand case:
` A B
e.g.:
` sin x
I know that many infix operations have parens that prevent ambiguity.
That said, I suspect that this won't work because of ambiguous cases
that makes this fail (e.g., if the function name isn't a constant).
But maybe not; I thought it'd be worth mentioning.
--- David A. Wheeler
> > It is possible to use "` A ( B )" and hide the backtick, but I wonder if this is
> > not more strange and inconvenient.
I just noticed that ISO 80000-2 section 3 permits omitting the parentheses after the symbol
> > not more strange and inconvenient.
for the function if there's no operation symbol in the operand and there's
only one operand. So perhaps this is an alternative syntax for the one-operand case:
` A B
e.g.:
` sin x
I know that many infix operations have parens that prevent ambiguity.
That said, I suspect that this won't work because of ambiguous cases
that makes this fail (e.g., if the function name isn't a constant).
But maybe not; I thought it'd be worth mentioning.
--- David A. Wheeler
Norman Megill
Apr 28, 2015, 12:35:13 PM4/28/15
to meta...@googlegroups.com, dwhe...@dwheeler.com
(Responding mainly to David)
The title of ISO 80000-2 is "Mathematical signs and symbols to be used in the natural sciences and technology" and not "...used in pure mathematics" or even more specifically "...used in logic".
Pure mathematics can have a different notation from applied, and set.mm is focused on the former. One example is "log", where a long time ago (in emails I could look up) we agreed that "log" essentially universally means natural log in pure mathematics. After discussion with people and looking at the literature, I finally chose "log" over my initial choice "ln".
In engineering, I've usually seen "ln" used for natural log and "log" for log_10; in computer science, I think I've only seen "lg" used for log_2 and don't recall ever seeing "lb". In the end, the ISO standard was authored by humans, and I don't know what their fields and biases are or whether they invented "standards" such as lb. For set.mm, we would introduce lg and log_ (to any base) when there becomes a clear advantage to having them (for shorter proofs, etc., after accounting for the extra overhead). I don't think we'll ever need log_10 in pure mathematics, but if we do, log_10 is probably the right symbol to make it clear and unambiguous to pure mathematicians, for whom log means log_e. In the end, though, changing "log" to "ln" is trivial if at some point in the future we want to do that, so it's not a pressing issue that we need to solve to move forward.
Also, in engineering, "j" is typically used instead of "i" for sqrt(-1), since "i" too often represents current. I do like the recent trend towards making constants like i use Roman font, and in the past few years I changed i, e, V, etc. to this, contrary to most older literature, and simultaneously freed up the italic versions for variable names.
One problem with emulating the literature exactly is that much conventional notation is ambiguous outside of a context that is implicit in the text. Obviously we can't have ambiguity in set.mm but try to do our best to approximate the literature within that constraint. Particularly notorious is A(B) which (aside from its ambiguity as a suffix notation in the presence of set.mm's prefix notation) can mean "the function value of A at B", "B substituted for some implicit variable in A", and "B is a parameter in A". The backtick notation we use for function value has a venerable history from Peano, Russell/Whitehead, and Quine through Takeuti/Zaring. It is somewhat disappointing it has fallen into disuse, but there is no other notation, historical or otherwise, that is as clear.
Outside of basic math symbols, a big problem is that much of the literature uses English language for which there are no standard symbols. ISO 80000-2 is silent on this issue, maybe because it is concerned more with applied math than pure math. I don't like that set.mm has to invent nonstandard "symbols" such as topGen, LMod, CMnd, mulGrp, etc. that appear nowhere in the literature. It seems that applied math often has better standard and unambiguous notation than pure math. Pure math seems to get more English-like, terse, and ambiguous out of context as it gets more advanced, with the expectation that the (advanced) reader is smart enough to figure out the implicit unstated things.
What would be nice is an ISO standard for a linear math notation for formalizing pure mathematics, that in principle can be interpreted unambiguously by a machine but is still relatively readable for humans. Such a notation has been a goal for set.mm. I think many proof languages have failed significantly in that regard, and as computer formalization of math becomes more common, the issue will be more important. I think most mathematicians, or at least logicians, can make sense of set.mm web pages without much effort, whereas other proof languages often require learning a cryptic computer language.
The title of ISO 80000-2 is "Mathematical signs and symbols to be used in the natural sciences and technology" and not "...used in pure mathematics" or even more specifically "...used in logic".
Pure mathematics can have a different notation from applied, and set.mm is focused on the former. One example is "log", where a long time ago (in emails I could look up) we agreed that "log" essentially universally means natural log in pure mathematics. After discussion with people and looking at the literature, I finally chose "log" over my initial choice "ln".
In engineering, I've usually seen "ln" used for natural log and "log" for log_10; in computer science, I think I've only seen "lg" used for log_2 and don't recall ever seeing "lb". In the end, the ISO standard was authored by humans, and I don't know what their fields and biases are or whether they invented "standards" such as lb. For set.mm, we would introduce lg and log_ (to any base) when there becomes a clear advantage to having them (for shorter proofs, etc., after accounting for the extra overhead). I don't think we'll ever need log_10 in pure mathematics, but if we do, log_10 is probably the right symbol to make it clear and unambiguous to pure mathematicians, for whom log means log_e. In the end, though, changing "log" to "ln" is trivial if at some point in the future we want to do that, so it's not a pressing issue that we need to solve to move forward.
Also, in engineering, "j" is typically used instead of "i" for sqrt(-1), since "i" too often represents current. I do like the recent trend towards making constants like i use Roman font, and in the past few years I changed i, e, V, etc. to this, contrary to most older literature, and simultaneously freed up the italic versions for variable names.
One problem with emulating the literature exactly is that much conventional notation is ambiguous outside of a context that is implicit in the text. Obviously we can't have ambiguity in set.mm but try to do our best to approximate the literature within that constraint. Particularly notorious is A(B) which (aside from its ambiguity as a suffix notation in the presence of set.mm's prefix notation) can mean "the function value of A at B", "B substituted for some implicit variable in A", and "B is a parameter in A". The backtick notation we use for function value has a venerable history from Peano, Russell/Whitehead, and Quine through Takeuti/Zaring. It is somewhat disappointing it has fallen into disuse, but there is no other notation, historical or otherwise, that is as clear.
Outside of basic math symbols, a big problem is that much of the literature uses English language for which there are no standard symbols. ISO 80000-2 is silent on this issue, maybe because it is concerned more with applied math than pure math. I don't like that set.mm has to invent nonstandard "symbols" such as topGen, LMod, CMnd, mulGrp, etc. that appear nowhere in the literature. It seems that applied math often has better standard and unambiguous notation than pure math. Pure math seems to get more English-like, terse, and ambiguous out of context as it gets more advanced, with the expectation that the (advanced) reader is smart enough to figure out the implicit unstated things.
What would be nice is an ISO standard for a linear math notation for formalizing pure mathematics, that in principle can be interpreted unambiguously by a machine but is still relatively readable for humans. Such a notation has been a goal for set.mm. I think many proof languages have failed significantly in that regard, and as computer formalization of math becomes more common, the issue will be more important. I think most mathematicians, or at least logicians, can make sense of set.mm web pages without much effort, whereas other proof languages often require learning a cryptic computer language.
> Mario Carneiro replied:
> > Indeed, this is a "necessary sacrifice", not a deliberate deviation from
> > the literature. It is impossible due to "technical difficulties". More
> > precisely, if df-fv was "A ( B )" then it would be a suffix notation (a
> > class expression that begins with a class expression), and it is impossible
> > to have both prefix and suffix constructors in the same grammar without
> > ambiguity...
>
> Technically it's possible to do both, since many parsers do *exactly* this,
> but I know what you mean - it would require a fundamental change to support
> them all directly.
> them all directly.
To do this requires the notion of operator precedence (binding strength), which is completely absent in Metamath, unlike most computer languages and to a certain extent math texts (such as 'and' having tighter binding that 'or'). In early days I was somewhat torn about whether I should greatly complicate the language by somehow incorporating it. Although not having it adds more parentheses, it isn't as bad as say lisp, and importantly for me it means I never have to memorize or reference a binding strength table.
Binding strength rules are not always a good thing. For example, does &a.b[c] in C mean &((a.b)[c]), &(a.(b[c])), (&(a.b))[c], (&a).(b[c]), or ((&a).b)[c]? I used to know but forgot (and may have to look it up when reading others' code), but it doesn't matter when writing code or reading my own code since I always use explicit parentheses. It just isn't that much harder to write &((a.b)[c]) and much easier for me to read confidently.
Alternately, we could leave the Metamath language alone and have an intelligent renderer for the HMTL, hiding parentheses based on some internal precedence table. Some Ghilbert display experiments do that, and personally I don't like it because when I'm uncertain it means an extra step looking up a precedence table, if I can even find it. One example frequently occurring in the literature is A. x ph /\ ps, which to some authors means A. x (ph /\ ps) and to others (A. x ph) /\ ps. Oddly, Ghilbert has chosen (or at least did) the former for its HTML display that hides parentheses, which I found confusing.
Binding strength rules are not always a good thing. For example, does &a.b[c] in C mean &((a.b)[c]), &(a.(b[c])), (&(a.b))[c], (&a).(b[c]), or ((&a).b)[c]? I used to know but forgot (and may have to look it up when reading others' code), but it doesn't matter when writing code or reading my own code since I always use explicit parentheses. It just isn't that much harder to write &((a.b)[c]) and much easier for me to read confidently.
Alternately, we could leave the Metamath language alone and have an intelligent renderer for the HMTL, hiding parentheses based on some internal precedence table. Some Ghilbert display experiments do that, and personally I don't like it because when I'm uncertain it means an extra step looking up a precedence table, if I can even find it. One example frequently occurring in the literature is A. x ph /\ ps, which to some authors means A. x (ph /\ ps) and to others (A. x ph) /\ ps. Oddly, Ghilbert has chosen (or at least did) the former for its HTML display that hides parentheses, which I found confusing.
> That's an interesting possibility. It basically treats ` as an "apply" operator.
> I'm not even sure you need to hide the backtick; that might be a separate issue.
IMO nothing should be hidden to make it more aesthetic, when it's at the expense of also making it harder for the reader to interpret exactly what's under it.
> I guess the question is, what is more aesthetically pleasing:
> ( sin ` x )
> ` sin ( x )
>
> It's exactly the same number of symbols, and same number of characters.
> Since ` sin ( x ) is more similar to traditional notation, perhaps
> that should be seriously considered. It'd be a big change.
> On the other hand, it's probably automatable and justifiable.
> I typically look at the HTML as the "published" version of the work, and
> I suspect this change would make the "published" version look much better
> (it'd be closer in form to traditional notation).
While the f(x) is common usage in applied mathematics, it is ambiguous out of context. The f`x is completely unambiguous and has a long, venerable tradition in logic and set theory literature. I would resist `f(x) because I have never seen it nor anything similar; it seems contrived. If anyone is unfamiliar with f`x, it's trivial to look it up, and sooner or later they will find it in the literature anyway if they study logic. No one has ever complained about not knowing what it means.
Norm
Norm
David A. Wheeler
Apr 28, 2015, 8:05:00 PM4/28/15
to Norman Megill, meta...@googlegroups.com
Yes, but every difference creates a risk of confusion and a barrier to understanding. I think set.mm can be a marvelous teaching tool, but every symbol with a significantly different meaning from what they have learned is confusing. Also, the boundary between "Pure" math and other areas is becoming porous (formal methods, crypto, physics, ...).
> One example is "log", where a long time ago (in emails I could look up) we agreed that "log" essentially universally means natural log in pure mathematics. After discussion with people and looking at the literature, I finally chose "log" over my initial choice "ln".
I think that should be revisited. This is confusing, and I am skeptical that this convention will continue. On all calculators today "log" means base 10, not e, so this definition is a barrier for modern students. In contrast, ln is unambiguous. I am sure every pure mathematician would also know what ln means. It is also trivial to do.
I have an EE degree so I directly experienced i vs. j. But this is old and well-worn... most engineers already know about that, and have no problem with i. I think using "i" is correct fot set.mm - j is a local convention of EE.
As I said, I did not expect the function notation to change. If that'd be easy, great, but I thought that would be too hard.
--- David A.Wheeler
> One example is "log", where a long time ago (in emails I could look up) we agreed that "log" essentially universally means natural log in pure mathematics. After discussion with people and looking at the literature, I finally chose "log" over my initial choice "ln".
I have an EE degree so I directly experienced i vs. j. But this is old and well-worn... most engineers already know about that, and have no problem with i. I think using "i" is correct fot set.mm - j is a local convention of EE.
As I said, I did not expect the function notation to change. If that'd be easy, great, but I thought that would be too hard.
--- David A.Wheeler
Mario Carneiro
Apr 28, 2015, 9:31:32 PM4/28/15
to metamath
A while ago I wrote up a proof of the unambiguity of set.mm's grammar:
https://www.dropbox.com/sh/stnwq0lyq3jmjpm/nzzDnpa9Ty/grammar-ambiguity.txt
and this proof is fairly flexible as regards new syntax, by categorizing syntax axioms into various "types" defined by their distinguishing features that keep them from being confused with any other syntax. In particular, any prefix axiom (type 2) is automatically unambiguous. This includes axioms of the form
https://www.dropbox.com/sh/stnwq0lyq3jmjpm/nzzDnpa9Ty/grammar-ambiguity.txt
and this proof is fairly flexible as regards new syntax, by categorizing syntax axioms into various "types" defined by their distinguishing features that keep them from being confused with any other syntax. In particular, any prefix axiom (type 2) is automatically unambiguous. This includes axioms of the form
NEWCONSTANT A ph , + x B
where the new constant is followed by any number of class, set, or wff variables and constants in any order. Thus your "` A B" is in type 2 and thus unambiguous, assuming that it replaces rather than augments df-fv so that the "`" can be considered unique to your syntax axiom. (This is the same argument that allowed me to add df-dec "; A B" without having to worry about ambiguity.) That said, I would not recommend this notation because it is very difficult to read when the nesting gets too deep.
(PS: Norm, could you put this file on metamath.org? I had planned to texify it at some point, but my priorities apparently lie elsewhere.)
Consider also that we are discussing here the notation for df-fv itself, not the "pseudo-function" notation used in df-sup and others. You say that it would be nice if all functions used such custom syntax, but let me convince you otherwise, even putting aside the problem of defining convenience theorems. A custom syntax such as
sin ( A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) )
does not define a function - it defines an abbreviation for another class expression. Note that nowhere here does the definition say that the domain is CC; in fact the most accurate interpretation of domain of this "function" is the collection of all classes (proper or otherwise). This is useful, if you need a function that can act on proper classes, but since "sin" does not exist on its own, you lose such statements as "sin : CC --> CC" or "sin e. ( CC -cn-> CC )", since "sin" is not actually a function. The closest you would be able to get is "( x e. CC |-> sin ( x ) ) e. ( CC -cn-> CC )", but then you have defeated the whole point of defining a custom notation.
The point is that df-fv is useful when you want the F in "(F ` A)" to have an independent existence. It is an actual set, a collection of ordered pairs, and you can manipulate it as such. Keep in mind that sometimes you want set variables that are functions, as in df-map where we have a collection of functions. We can't define a class constant for these functions, of course, because they are variable by definition. It is situations like these where it becomes useful to have a single definition df-fv handling function evaluation once and for all so that everything else can be defined in terms of it.
On Tue, Apr 28, 2015 at 11:00 AM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
> > This is actually a good point, though, in that we have no definition of log
> > with general base; since we have ^c it seems reasonable to extend log to
> > other bases as well. I'm a bit torn on the notation, though; options are "(
> > B log_ A )", "( ( log_ ` B ) ` A )", and "( log_ B ` A )" to mean log base
> > B of A. A possible definition (according to the last notation) might be
> >
> > log_ B = ( a e. ( CC \ { 0 } ) |-> ( ( log ` a ) / ( log ` B ) ) )
If the function application notation were changed, this is an obvious example
of the question, "how can multi-argument functions best be handled?"
The current convention for two-argument functions is df-ov, which uses infix notation. This works well on functions like + and passably on other functions that might normally be notated f(x,y), so I am loathe to change it. For three or more arguments, there is no convention; one option using the new ordered triple is "( F ` <. x , y , z >. )", but I find this notation a bit awkward. My current preference is to nest functions once you get past two arguments (in some sensible way), so that you end up with constructions like ( x ( y ( F ` z ) w ) u ) which is not pretty but at least is somewhat compact and avoids any new syntax. For a less ad-hoc approach or for a definition where readability is important, I would just define a syntax construction, which allows you to but as many arguments as you like, as in "myFunc ( x , y , z , w , u )".
There are two main reasons I wrote log_ B using a syntax construction for the B and not the A. For one thing, it is important to keep the readability; the df-ov standard would prescribe ( B log_ A ) but this is hopelessly confusing to someone looking for "log_b a". Keeping the B directly after the underscore in ( log_ B ` A ) helps emphasize that the B is in the subscript and hence should be interpreted as the base. Secondly, I am okay with using a syntax construction for B because I don't foresee much use for treating log_ B as a function of B or a two-argument function, since usually the base is held constant in a given application, although it definitely needs to be a function of A, so that one can make statements like
( B e. ( CC \ { 0 , 1 } ) -> log_ B : ( CC \ { 0 } ) --> CC )
( B e. ( CC \ { 0 , 1 } ) -> log_ B : ( CC \ { 0 } ) --> CC )
or "log_ _e = log".
On Tue, Apr 28, 2015 at 8:04 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
> One example is "log", where a long time ago (in emails I could look up) we agreed that "log" essentially universally means natural log in pure mathematics. After discussion with people and looking at the literature, I finally chose "log" over my initial choice "ln".
I think that should be revisited. This is confusing, and I am skeptical that this convention will continue. On all calculators today "log" means base 10, not e, so this definition is a barrier for modern students. In contrast, ln is unambiguous. I am sure every pure mathematician would also know what ln means. It is also trivial to do.
Regarding "log" vs other variants, my own opinion is that as long as log_e is the only definition in the database, it should remain as "log", not "ln", as there is no possibility of confusion. Logarithms to other bases are not currently needed, so for the time being any such definitions will be confined to a mathbox. I can also attest to the preference of "log" over "ln" in advanced math, which is the current focus of set.mm.
--- David A. Wheeler
Norman Megill
Apr 28, 2015, 10:13:14 PM4/28/15
to meta...@googlegroups.com
On Tuesday, April 28, 2015 at 9:31:32 PM UTC-4, Mario Carneiro wrote:
A while ago I wrote up a proof of the unambiguity of set.mm's grammar:
https://www.dropbox.com/sh/stnwq0lyq3jmjpm/nzzDnpa9Ty/grammar-ambiguity.txt
and this proof is fairly flexible as regards new syntax, by categorizing syntax axioms into various "types" defined by their distinguishing features that keep them from being confused with any other syntax. In particular, any prefix axiom (type 2) is automatically unambiguous. This includes axioms of the formNEWCONSTANT A ph , + x Bwhere the new constant is followed by any number of class, set, or wff variables and constants in any order. Thus your "` A B" is in type 2 and thus unambiguous, assuming that it replaces rather than augments df-fv so that the "`" can be considered unique to your syntax axiom. (This is the same argument that allowed me to add df-dec "; A B" without having to worry about ambiguity.) That said, I would not recommend this notation because it is very difficult to read when the nesting gets too deep.(PS: Norm, could you put this file on metamath.org? I had planned to texify it at some point, but my priorities apparently lie elsewhere.)
This has been added here: http://us2.metamath.org:88/downloads/grammar-ambiguity.txt
with a news item linking to it on the Most Recent page.
Norm
Norman Megill
Apr 28, 2015, 11:06:57 PM4/28/15
to meta...@googlegroups.com
On Tuesday, April 28, 2015 at 9:31:32 PM UTC-4, Mario Carneiro wrote:
There are two main reasons I wrote log_ B using a syntax construction for the B and not the A. For one thing, it is important to keep the readability; the df-ov standard would prescribe ( B log_ A ) but this is hopelessly confusing to someone looking for "log_b a". Keeping the B directly after the underscore in ( log_ B ` A ) helps emphasize that the B is in the subscript and hence should be interpreted as the base. Secondly, I am okay with using a syntax construction for B because I don't foresee much use for treating log_ B as a function of B or a two-argument function, since usually the base is held constant in a given application, although it definitely needs to be a function of A, so that one can make statements like
( B e. ( CC \ { 0 , 1 } ) -> log_ B : ( CC \ { 0 } ) --> CC )or "log_ _e = log".
I agree that df-ov's ( B log_ A ) would be a bad choice for readability. While I won't reject your version, my own choice would have been ( ( log_ ` B ) ` A ) which keeps the arguments in the right place while emphasizing that the B is more "tightly bound" to the log_ than A is. I think the entity ( log_ ` B ) has all the properties of your log_ B with no overhead associated with a new syntax construction. Admittedly log_ B is slightly more pleasing to the eye, but having log_ as a simple defined constant would make it something set.mm users are very comfortable working with without having to find or create special theorems for a new syntax. And it would give us the future flexibility of treating log_ as a function of B should there ever be a need for it (even if as you suggest that is unlikely).
Norm
Norman Megill
Apr 28, 2015, 11:24:53 PM4/28/15
to meta...@googlegroups.com
Actually I never thought of this before, and maybe there aren't any applications, but this is cute: "derivative of logarithm with respect to base" http://planetmath.org/derivativeoflogarithmwithrespecttobase :)
Although my suggested notation wouldn't necessarily make it easier since we would have to redefine it anyway as a function of the base with the argument held constant.
Norm
Although my suggested notation wouldn't necessarily make it easier since we would have to redefine it anyway as a function of the base with the argument held constant.
Norm
David A. Wheeler
Apr 29, 2015, 11:40:31 AM4/29/15
to nm, metamath
On Tue, 28 Apr 2015 09:35:13 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> One example is "log", where a long time ago (in
> emails I could look up) we agreed that "log" essentially universally means
> natural log in pure mathematics. After discussion with people and looking
> at the literature, I finally chose "log" over my initial choice "ln".
> ... log_10 is probably the right symbol to make it clear and unambiguous to
> One example is "log", where a long time ago (in
> emails I could look up) we agreed that "log" essentially universally means
> natural log in pure mathematics. After discussion with people and looking
> at the literature, I finally chose "log" over my initial choice "ln".
> pure mathematicians, for whom log means log_e.
As I mentioned earlier, I think that's a mistake; I think your initial intuition was correct.
I suggested "ln" earlier. If that's not desired, how about "log_e"?
Either symbol will be immediately understood by all pure mathematicians, but they will
*also* be understood correctly by others. There's a lot of variation in notation
anyway... best to choose a symbol that's more likely to be correctly understood by all.
Most people use "log" for base 10, including all calculators, and there's a significant
number of people for whom base 2 is what "log" means. I think your potential audience
is larger than you originally considered; I think your audience
includes anyone who's interested in the fundamentals of mathematics
(and who may be *learning* about math from set.mm)!
The "log" symbol has a different meaning to many potential readers,
and they will *NOT* look it up because they "know" it's base 10 (or 2).
A clearer, less ambiguous symbol should be used.
You're clearly *not* trying to exactly reproduce the typical
syntactic notation of conventional literature, which almost universally uses f(x).
I'm fine with that, but since you've already abandoned more common conventions
like f(x), replacing "log" with "ln" or "log_e" is a small change :-).
> One problem with emulating the literature exactly is that much conventional
> notation is ambiguous outside of a context that is implicit in the text.
In addition, a reader is likely to jump to a specific place in set.mm, and thus
*NOT* read all the context. That's not a problem with unfamiliar symbols, but
readers will typically not look up symbols if they think they know what the symbol means.
> Outside of basic math symbols, a big problem is that much of the literature
> I don't like that set.mm has to invent nonstandard
> "symbols" such as topGen, LMod, CMnd, mulGrp,
That is a big problem. However, I have hope that formalization systems like
> "symbols" such as topGen, LMod, CMnd, mulGrp,
metamath (along with HOL Light, Mizar, and others)
can help start to standardize the symbols. It might be interesting to try
to get dialogue going between HOL Light, Mizar, Coq, etc., on the names of symbols.
I would recommend *not* going to ISO, frankly, since they primarily
want to charge money for work they didn't do.
A small mailing list and wiki to work to agree on standard symbols,
where agreement can be found, might be useful.
--- David A. Wheeler
David A. Wheeler
Apr 29, 2015, 1:48:32 PM4/29/15
to metamath
> I'm a bit torn on the notation, though; options are
> "( B log_ A )", "( ( log_ ` B ) ` A )", and "( log_ B ` A )"
> to mean log base B of A.
> A possible definition (according to the last notation) might be
> log_ B = ( a e. ( CC \ { 0 } ) |-> ( ( log ` a ) / ( log ` B ) ) )
...
> A possible definition (according to the last notation) might be
> log_ B = ( a e. ( CC \ { 0 } ) |-> ( ( log ` a ) / ( log ` B ) ) )
> There are two main reasons I wrote log_ B using a syntax construction for
> the B and not the A. For one thing, it is important to keep the
> readability; the df-ov standard would prescribe ( B log_ A ) but this is
> hopelessly confusing to someone looking for "log_b a".
Norman Megill:
> the B and not the A. For one thing, it is important to keep the
> readability; the df-ov standard would prescribe ( B log_ A ) but this is
> hopelessly confusing to someone looking for "log_b a".
> I agree that df-ov's ( B log_ A ) would be a bad choice for readability.
Me too!
> While I won't reject your version, my own choice would have been
> ( ( log_ ` B ) ` A ) which keeps the arguments in the right place while emphasizing
> that the B is more "tightly bound" to the log_ than A is. I think the
> entity ( log_ ` B ) has all the properties of your log_ B with no overhead
> associated with a new syntax construction. Admittedly log_ B is slightly
> more pleasing to the eye, but having log_ as a simple defined constant
> would make it something set.mm users are very comfortable working with
I agree, I think ( ( log_ ` B ) ` A ) is pretty easy to read due to its
syntactic similarity to traditional notation.
I haven't looked up how to define this in metamath, but I presume it's possible (yes?).
I'm coming at this from a computing background, and ( log_ ` B ) looks
comfortably like a function constructor that returns the function "log with base B";
other people with a functional programming background will have 0 problems.
Log is such a common standard function that I think it'd be *okay* to
define a special syntax, but perhaps there's not a strong need in this case.
This might be an argument for using "log_e" for the natural logarithm;
it's clearly related syntactically to "log_" for "arbitrary base".
--- David A. Wheeler
Stefan O'Rear
May 5, 2015, 12:04:45 AM5/5/15
to meta...@googlegroups.com, n...@alum.mit.edu
On Tuesday, April 28, 2015 at 5:05:00 PM UTC-7, David A. Wheeler wrote:
> One example is "log", where a long time ago (in emails I could look up) we agreed that "log" essentially universally means natural log in pure mathematics. After discussion with people and looking at the literature, I finally chose "log" over my initial choice "ln".
I think that should be revisited. This is confusing, and I am skeptical that this convention will continue. On all calculators today "log" means base 10, not e, so this definition is a barrier for modern students. In contrast, ln is unambiguous. I am sure every pure mathematician would also know what ln means. It is also trivial to do.
ISO 80000-2 may say that "log" is base 10. ISO 9899:2011 (aka C, also IEEE 1003.1 POSIX) says that "log" is base _e while providing log2 and log10. Perhaps it would be better to ban "log" entirely and just have "ln" (which may be uncommon, but is at least recognized and unambiguous - I have never seen log_e), and "log_".
-sorear
Stefan O'Rear
May 5, 2015, 12:09:21 AM5/5/15
to meta...@googlegroups.com
On Tuesday, April 28, 2015 at 8:06:57 PM UTC-7, Norman Megill wrote:
I agree that df-ov's ( B log_ A ) would be a bad choice for readability. While I won't reject your version, my own choice would have been ( ( log_ ` B ) ` A ) which keeps the arguments in the right place while emphasizing that the B is more "tightly bound" to the log_ than A is. I think the entity ( log_ ` B ) has all the properties of your log_ B with no overhead associated with a new syntax construction. Admittedly log_ B is slightly more pleasing to the eye, but having log_ as a simple defined constant would make it something set.mm users are very comfortable working with without having to find or create special theorems for a new syntax. And it would give us the future flexibility of treating log_ as a function of B should there ever be a need for it (even if as you suggest that is unlikely).
I approve of this version. Note that I have a small number of glog* theorems that should probably be replaced, whatever the resolution.
-sorear
Stefan O'Rear
May 5, 2015, 12:25:37 AM5/5/15
to meta...@googlegroups.com, dwhe...@dwheeler.com
On Monday, April 27, 2015 at 8:15:04 PM UTC-7, David A. Wheeler wrote:
I've been looking at improving set.mm's support for ISO 80000-2:2009 ("Mathematical signs and symbols to be used in the natural sciences and technology"), particularly for cases where it's not too painful to do. This international standard defines a set
Two other points that I feel have been inadequately addressed:
1. Much of this ties into the fact that metamath does not distinguish its surface syntax from its internal representation in any significant way. Yes, we have one type of application node and treat most other stuff as functions (so does HOL). I've often thought that it would be nice to have multiple display modes: ASCII, linear symbolic (using some combination of Unicode and GIFs/private use characters), and nonlinear, and the ability to switch when things don't make sense.
I've heard a lot about this ghilbert thing, but it's frustratingly hard to find code or real information about it. I'm concerned I'm going to reinvent it.
2. A lot of logicians write fully parenthesized expressions, but there is no standard on how to do this (there are several places where you can remove parens from one context and add them to another without breaking unambiguity).
-sorear
Reply all
Reply to author
Forward
0 new messages