*
debates derailing topic*
*
...*
*
obviously yes*
EDIT: Also, as to representing additive operations with multiplicative notation, that wasn't the point. The point was to show that notation is merely a convention -- we choose '+' and '1' to have specific meanings and then compose them ad hoc when necessary, but there's no reason you couldn't specialize a symbol to mean that. It's like the '++' operation in C, or the add1 function in many Lisp dialects.
One of the things that bothers me about modern education, and that I've been trying to address in Honoka's lessons, is that concepts are very rigid. Things are taught in a specific way and in discrete chunks that make it hard to integrate knowledge. What Kagome is teaching is a really easy way to move from arithmetic directly into algebra; once you have the concept that numerals are just a conventional representation of a number then the rest is easy.
[NB: This is an attempt to say "I think this way of thinking about math and the teaching of it is helpful," not a criticism or an attempt at a debate, which I don't think the text makes clear.]
I basically agree with you, but I think I see it in a slightly different light. You're right that the power of math is at the semantic level, not the symbol level, but for me it feels vital in some intangible sense to get across that this all arises out of the foundational rules that constitute the meta-level. That is, the thing that allows you to deduce "♮" is the successor function applied postfix is not the equation '1 + 1 = 1♮', but the
declaration, "let ♮ denote ...", or, in kid-speak, "when I write ♮ after a value, ...". You can only start solving at the semantic level when you already have sufficiently specific semantics in place that you can meaningfully operate on the symbols you have.
This is important because I think it captures an essence of math that is rarely explained well: that the rules and relationships are either primitive, and declared directly in the meta level, or a necessary consequence of other meta-level claims. When you go from "a + b = c + b" to "a = c", you can think of this at the syntactic level ("when you have these symbols you can move them around this way"), or you can think of it at the semantic level ("when this statement is true, then this other statement is true"), and this is an improvement, but neither captures the essence that the semantic level is
equally arbitrary, and you can define semantics as ever you want.
By expecting someone to draw the conclusion "1 + 1 = 1♮", therefore "♮ = succ", you are risking imparting the idea that the semantic level is determined in essence by its syntactic properties, rather than the fact that someone at some point said "let ♮ denote ..." at this higher meta-level.
To give this a concrete instance of something being confusing, I was explaining syntax for lambda functions on Reddit a month ago. I started like this
No, a b c = d is literally just shorthand for a = λb. λc. d.
The = is working at a higher level than the lambda functions; it says that the lambda function a is equivalent to the lambda function λb. λc. d. You can't have an = inside a lambda function.
This has a similar issue where what is really a rule derived from the semantics is interpreted at the syntax level, which makes it incorrect. So I clarified,
Actually, let me clarify, since this isn't really 100% correct.
a b = d is an equation that says passing the argument b to a
results in a lambda term that is equivalent to d.
In order for this to be the case, a must be a function, because you can only apply arguments to functions. It must accept one argument, and the function's resulting lambda term must be itself equal to d.
Therefore, a b = d is an equivalent statement to a = λb. d. We normally write this claim as (a b = d) ⇔ (a = λb. d). That is,
- the equation between lambda terms a b = d is true if the equation between lambda terms a = λb. d is true, and
- the equation between lambda terms a = λb. d is true if the equation between lambda terms a b = d is true.
Note that something like
f (λx. x) = (λx. x)
is a valid equation, but it can
not be turned into
f = λ(λx. x). (λx. x)
That doesn't make any sense! It's not even syntactically valid! Rather, you could have
f = λg. (λx. x)
or
f = λg. g
or
f = λg. g g
All of which are valid ways of satisfying the first equation. It's only true that "a b c = d is literally just shorthand for a = λb. λc. d" if b and c are just basic names.
Hopefully that clarifies things.
