The Mechanics of Proof : 3.2.2. Example :

Stream: new members

[David Leroie]

3.2.2. Example : https://hrmacbeth.github.io/math2001/03_Parity_and_Divisibility.html#id14

What does the term "variant terminology" mean in this sentence ? : "We also use all the same variant terminology and the same notation a ∣ b for integer divisibility. "

According to chat gpt and my own interpretation, we assume that he was talking about this :

b is divisible by a
b is a multiple of a
a is a divisor of b
a is a factor of b
a divides b

But how can I be 100% sure without interpretation, knowing that I can't find a definition for "variant terminology" and when I look for the terms separately I'm no further ahead, for a variant we're talking about something slightly different while the different sentences above mean the same thing

[Kenny Lau]

@David Leroie in the given context, I think what she meant is that we use the same word "divisible" and the same symbol $a \vert b$ to notate both the relation between naturals and the relation between integers.

[David Leroie]

Kenny Lau said:

David Leroie in the given context, I think what she meant is that we use the same word "divisible" and the same symbol $a \vert b$ to notate both the relation between naturals and the relation between integers.

How can I be sure and not interpret?

[metakuntyyy]

It can be possible that the divisibility relation is defined on pairs of naturals or integers respectively. What that usually means is that you can transfer the proofs from the naturals to the integers. Given a | b on the naturals and the goal (a:Int) | (b:Int) you can have a coercion that respects both those notions.

The variant terminology just means that the divisibility relation is "polynorphic". If a | b then there exists a c such that b=ac. It does not matter if a, b, c are integers, natural numbers or some weird ring like $K[X]$

[Kenny Lau]

David Leroie said:

Kenny Lau said:

David Leroie in the given context, I think what she meant is that we use the same word "divisible" and the same symbol $a \vert b$ to notate both the relation between naturals and the relation between integers.

How can I be sure and not interpret?

even though it's a book on a formal prover, it's still english

[David Leroie]

metakuntyyy said:

It can be possible that the divisibility relation is defined on pairs of naturals or integers respectively. What that usually means is that you can transfer the proofs from the naturals to the integers. Given a | b on the naturals and the goal (a:Int) | (b:Int) you can have a coercion that respects both those notions.

The variant terminology just means that the divisibility relation is "polynorphic". If a | b then there exists a c such that b=ac. It does not matter if a, b, c are integers, natural numbers or some weird ring like $K[X]$

He already says that in another sentence, I don't think he says it again here.

[David Leroie]

Kenny Lau said:

David Leroie said:

Kenny Lau said:

David Leroie in the given context, I think what she meant is that we use the same word "divisible" and the same symbol $a \vert b$ to notate both the relation between naturals and the relation between integers.

How can I be sure and not interpret?

even though it's a book on a formal prover, it's still english

You said "I think," so you're interpreting. I myself have to try to interpret, but I don't like interpretations. How can I be sure of the meaning of these terms without any interpretation? Yes, it's English, but it's precisely a sentence in English that doesn't seem clear; it's confusing. Otherwise, I understood the mathematical proof perfectly.

[Kenny Lau]

well, you can always look at the lean code

[David Leroie]

Kenny Lau said:

well, you can always look at the lean code

How consulting the lean code will help me understand what he meant by undefined terms, here it is not a problem of lean code but a problem of a sentence in a tutorial which does not seem understandable

[Kenny Lau]

well so you're asking about how to interpret english, and i gave you one interpretation, and then you declined it, i don't know what i can do

[Kenny Lau]

you can ask heather directly

[David Leroie]

Kenny Lau said:

well so you're asking about how to interpret english, and i gave you one interpretation, and then you declined it, i don't know what i can do

Why would your interpretation be better than the commenter above, better than mine or chat gpt's???

That's why I want to understand the sentence without having to interpret it. If I say that book X is bad, then we can't interpret the sentence, but if I say that book X is atypical, then we can suddenly interpret it because atypical can mean good or bad. Do you understand the problem?

Who is Heather?

[Tom de Jong]

Who is Heather?

Judging from the url (github.com/hrmacbeth), that would be the author Heather Macbeth

[David Leroie]

To understand what she meant without any dubious interpretation, do we have to ask her directly?

It's this term I really don't understand: "variant terminology"

What is the definition of "variant terminology"?

[Tom de Jong]

FWIW, I agree with Kenny's interpretation, but yeah, if you want to know unambigiously what someone meant, the only way is to ask I suppose. (I also don't think it's particularly important what was meant, but you may disagree.)

[David Leroie]

Tom de Jong said:

FWIW, I agree with Kenny's interpretation, but yeah, if you want to know unambigiously what someone meant, the only way is to ask I suppose. (I also don't think it's particularly important what was meant, but you may disagree.)

For Kenny's interpretation, does the term "variant terminology" mean divisible?

In that case, she would have directly used the term "divisible" rather than variant terminology. She used the term "divisible" several times in the previous example.

It's not very important, actually. I always want to understand everything, but the only important thing is to understand the mathematical example and how to implement it in Lean. I understand that.

I can't be bothered to contact her. I don't think it's possible, and I'm not sure she'll respond. I'll just move on. I have to accept that the text is poorly written and focus on the example. That's why I'm reading this book, after all.

[Tom de Jong]

What I understood was: "variant" is referring to the fact that it's applied to both integers and natural numbers and terminology is referring to the word "division".

[Dan Velleman]

I would like to suggest that if you want to understand what Heather means here, you look at the context.

Section 3.2.1 defines divisibility for natural numbers. After the definition, she says "there are several different names for it," and she lists several ways of expressing the fact that $b$ is divisible by $a$. Below that, she introduces the notation $a \mid b$.

Section 3.2.2 gives the "corresponding definition for integers," and then comes the sentence that is under discussion. I think she is just saying that the stuff she said before about natural number divisibility also applies to integer divisibility. The phrase "variant terminology" refers to the "different names" that were introduced in Section 3.2.1. In other words, the phrases "is divisible by," "is a multiple of," and so on that were listed in Section 3.2.1 for natural number divisibility can also be used for integer divisibility. "Variant terminology" is not an undefined technical term, it's just another way of saying "different names."