Zulip Chat Archive

Stream: Lean for teaching

Topic: usage of the term 'proposition' in KR high school math

Bulhwi Cha (Oct 19 2024 at 03:23):

Here's the link to my short note about how the usage of the term 'proposition' in Korean high school mathematics is different from those in contemporary philosophy or interactive theorem provers like Lean: https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/docs/en/notes/chapter03/propositions.md.

Below is an excerpt from the note.

Propositions in School Mathematics in South Korea

문장 ‘2는 소수이다.’는 참이고, 식 ‘√2 + √3 = √5’는 거짓이다. 이와 같이 참, 거짓을 명확하게 판별할 수 있는 문장이나 식을 명제라고 한다. (전인태 n.d., 83)

The sentence ‘2 is prime’ is true and the expression ‘√2 + √3 = √5’ is false. We refer to a sentence or expression whose truth or falsehood can be clearly determined, like these examples, as a proposition.

Is Goldbach's Conjecture a Proposition?

Goldbach's conjecture states that every even natural number greater than 2 is the sum of two prime numbers. We don't know whether it's true or false as of 2024, so high school mathematics teachers in South Korea would have to answer no.

However, the conjecture can be defined as a proposition in the Lean theorem prover as follows:

import Mathlib.Data.Nat.Prime.Defs

def goldbach_conjecture : Prop :=
  ∀ n : ℕ, Even n ∧ n > 2 → ∃ p q : ℕ, (Prime p ∧ Prime q) ∧ n = p + q

My Closing Thoughts

I don't think the usage of the term 'proposition' in Korean high school mathematics coincides with those in contemporary philosophy or interactive theorem provers like Lean.

One can't clearly determine what the verb phrase 'clearly determine' really means, so Korean high school mathematics doesn't make it easier for students to understand the notion of a proposition.

Reference

Bulhwi Cha (Oct 19 2024 at 03:50):

This gives me a headache. I had to tell my mentees learning Lean that there are conflicts regarding the meaning of the term 'proposition' between Lean and school mathematics in South Korea.

Bulhwi Cha (Oct 19 2024 at 03:58):

Of course, most Koreans don't think too deeply about its meaning in Korean high school mathematics, so they overlook the clash of meanings.

Siddhartha Gadgil (Oct 19 2024 at 06:41):

This is a clash in English too. In mathematics "proposition" is a little theorem normally.

Bulhwi Cha (Oct 19 2024 at 07:56):

That's true. Nevertheless, we agree that 0 = 1 is false but still a proposition in Lean, as the following code shows:

#check 0 = 1 -- output: Prop
#eval  0 = 1 -- false

So, I think mathematicians are well aware of the two different meanings of the term 'proposition' in mathematics. (Edit: I fixed the example.)

Kevin Buzzard (Oct 19 2024 at 08:12):

Bulhwi Cha said:

That's true. Nevertheless, we agree that 0 = 1 is false but still a proposition in Lean, as the following code shows:

#check 0 = 1 -- output: Prop
#eval  0 = 1 -- false

So, I think mathematicians are well aware of the two different meanings of the term 'proposition' in mathematics.

I don't think this is true. Mathematicians see the word Proposition meaning "easy true statement" in all their courses. There might be one exception -- for example the unique and optional logic course which I attended as an undergraduate used Proposition in the same way as lean does. But this "weird" use of the word is the first thing I cover in my lean course.

Bulhwi Cha (Oct 19 2024 at 08:15):

Hmm, that's really interesting. My hypothesis is that South Korea is the only country that teaches the meaning of a proposition to high school students in mathematics classes. Can somebody disprove this?

François G. Dorais (Oct 19 2024 at 08:32):

The OED gives the primary definition: "a statement or assertion that expresses a judgment or opinion". So a proposition is believed to be true by the one making the assertion, but there is no implication that the proposition is true in an objective sense. This seems to somewhat agree with both uses of the word.

Bulhwi Cha (Oct 19 2024 at 08:32):

Bulhwi Cha said:

Hmm, that's really interesting. My hypothesis is that South Korea is the only country that teaches the meaning of a proposition to high school students in mathematics classes. Can somebody disprove this?

Note that Korean high school students don't learn propositional or predicate logic in detail.

They only learn the meaning of the terms, '명제' (命題, proposition) and '조건' (條件, condition), and the propositions of the following forms: '모든 x에 대해 p x이다' (For all x, p x) and '어떤 x에 대해 p x이다' (For some x, p x). They don't learn about propositional connectives, truth tables, quantifiers, or inference rules.

I've found only one English text about logic that uses the term 'condition.'

Kyle Miller (Oct 19 2024 at 08:39):

I don't know any Korean. In what sense is "명제" the word "proposition"? Does it have any other meanings? (Google tells me it could also mean "sentence" or "thesis".)

Bulhwi Cha (Oct 19 2024 at 08:46):

For reference, there's an entry '명제' in the Korean-English Learners' Dictionary: https://krdict.korean.go.kr/eng/dicSearch/SearchView?ParaWordNo=55438&lang=eng.

However, this dictionary is for Korean learners. I'll show you the meanings of the word in the Standard Korean Language Dictionary.

Bulhwi Cha (Oct 19 2024 at 08:56):

The entry '명제' in the Standard Korean Language Dictionary

I used ChatGPT to translate it into English. I've reviewed and paraphrased it.

Bulhwi Cha (Oct 19 2024 at 08:59):

The first usage of the word '명제' is really rare these days. I've never seen it so far.

Kyle Miller (Oct 19 2024 at 09:07):

Literally speaking, there's no clash between "명제" and "proposition" because these are two different words (and so I would believe you with your hypothesis that South Korea is the only country that teaches the meaning of "명제" to high school students :wink:)

It's helpful to see the definition. It's not clear to me that "can be evaluated as true or false" means that you are supposed to know which of the two it is. If that is the case, then this is like the word "proposition" as I have seen it in introductory logic.

But, maybe you're truly a constructivist and you don't believe that something can be true or false without a constructive proof. A constructive proof shows without a doubt that the proposition is a proposition.

Bulhwi Cha (Oct 19 2024 at 09:28):

Kyle Miller said:

It's helpful to see the definition. It's not clear to me that "can be evaluated as true or false" means that you are supposed to know which of the two it is.

I've paraphrased it as follows: "can be judged to be true or false." One could also translate the sentence containing the phrase as follows:

Its defining feature is that its content is one whose truth or falsehood can be judged.

Still, you made a good point and I agree with you. The wording itself doesn't seem to imply that we're supposed to know what the truth value of each proposition is.

Bulhwi Cha (Oct 19 2024 at 09:34):

In my experience, which was 12 years ago, Korean high school mathematics teachers and the textbook they used never discussed whether we should regard a sentence or expression whose truth value we don't know yet as a proposition. They only showed examples of "easy" true or false propositions. I'm pretty sure it's the same nowadays.

But, maybe you're truly a constructivist and you don't believe that something can be true or false without a constructive proof. A constructive proof shows without a doubt that the proposition is a proposition.

I suspect that the teachers, not me, seem to act like constructivists when they teach the term to students, but I need more evidence to support my claim. Unfortunately, I can't conduct a survey asking them about this matter. I'm not in a position to do that.

Bulhwi Cha (Oct 19 2024 at 09:41):

Please tell me if there's a grammatical error or semantically awkward wording in my messages above.

Bulhwi Cha (Oct 19 2024 at 09:46):

Related Philosophy Stack Exchange question I posted: https://philosophy.stackexchange.com/q/118144/58836.

Bulhwi Cha (Oct 19 2024 at 10:58):

François G. Dorais said:

The OED gives the primary definition: "a statement or assertion that expresses a judgment or opinion". So a proposition is believed to be true by the one making the assertion, but there is no implication that the proposition is true in an objective sense. This seems to somewhat agree with both uses of the word.

Oh, I also want to mention that the teachers and the textbooks they use always present an example like '99는 큰 수이다' (99 is a large number) as a non-proposition. See Question 1 in 전인태 n.d., 98.

Kyle Miller (Oct 19 2024 at 17:07):

Isn't "99 is a large number" not a proposition because "large number" has no meaning? If I define "a large number is a number greater than 3", then it becomes a proposition. Otherwise, if it's "whatever @Kyle Miller thinks is big enough", then it's not.

I believe this definition of proposition has to do with falsifiability -- if you put forward a claim, it is polite to make claims that others might be able to prove wrong. If I say "1 + 1 = 3" you can say "no, 1 + 1 = 2 and 2 is not equal to 3". If I say "99 is a large number", instead you can say it has no merit and I should not have put it forward.

(The word "proposition" comes from Latin for "something that is put forward." I think the current definition reflects that it is rude putting things forward for discussion if they are not falsifiable.)

Another note: interestingly, while a "large" number doesn't have any meaning, you can make "large enough such that" make sense. For example, "there is a large enough prime number" is true, where this means "there is a prime number, and for every prime number there is a larger prime number." In mathlib we can encode this using filters:

example : ∃ᶠ n in Filter.atTop, Nat.Prime n := by
  rw [Nat.frequently_atTop_iff_infinite]
  exact Nat.infinite_setOf_prime

"There is a large enough number such that it is 99" is false. While there is a number that is equal to 99, there are no larger numbers than that equal to 99.

Bulhwi Cha (Oct 19 2024 at 17:14):

Perhaps this excerpt from my note might also be helpful:

Is the Sentence 'Bulhwi Cha loves himself' a Proposition?

High school mathematics teachers in South Korea would answer no. On the contrary, it seems the authors of the entry "Propositions" in the Stanford Encyclopedia of Philosophy (SEP) would answer yes, judging from the following quotations:

E.g., if the proposition that a loves b is the ordered triple <loving, a, b>, it is distinct from the proposition that b loves a, which would be the ordered triple <loving, b, a>. (McGrath and Frank 2024)

Is the proposition that John loves Mary different from the proposition that Mary is loved by John? (ibid.)

Reference

Bulhwi Cha (Oct 19 2024 at 17:19):

Kyle Miller said:

Isn't "99 is a large number" not a proposition because "large number" has no meaning? If I define "a large number is a number greater than 3", then it becomes a proposition. Otherwise, if it's "whatever Kyle Miller thinks is big enough", then it's not.

In this case, its meaning is closer to the latter.

Kyle Miller (Oct 19 2024 at 17:21):

I don't think there's much sense in trying to absolutely determine whether a sentence is a proposition. It all depends on what we've agreed on in a discussion. Does "loves" have a meaning we have agreed to? If so, and if we agree it is something that either holds or not, and if we know who John and Mary are, then 'John loves Mary' is a proposition. Otherwise, it's not.

If we stick with math, then "loves" is certainly not admissible as part of a proposition unless it has a strict definition.

Bulhwi Cha (Oct 19 2024 at 17:25):

I'll read your messages again after I wake up! :full_moon:

Kyle Miller (Oct 19 2024 at 17:30):

Bulhwi Cha said:

In this case, its meaning is closer to the latter.

My point with this example is that we can only guess what "large" might mean, and that's why "99 is a large number" isn't a proposition.

Here is a dialogue that just came to mind:

Kyle: You know, 99 is a large number.

Bulwi: Oh really. What makes you say that?

Kyle: I don't know, I just have a feeling.

Bulwi: Ok, is 50 a large number to?

Kyle: No, certainly not.

Bulwi: Ok, how about 60?

Kyle: Yes, that one is large.

Bulwi: How about 59.

Kyle: Nope, not 59.

Bulwi: Ah! So a large number is one that is 60 or larger!

Kyle: Hmm, it would seem so, but I'm not so sure.

Bulwi: Let's test this. A million is a large number, right?

Kyle: Well, what time is it?

Bulwi: What do you mean what time is it? How can that matter?

Kyle: I don't know, it might :shrug:

Bulwi: Ok, it's 2:30AM in Korea right now.

Kyle: Oh, it turned 2:30AM? At that specific time in Korea, one million is not a large number, sorry.

Bulwi has left the chat

Frustrating, right? The spirit of a proposition is that you are giving something to someone that they can understand well enough that they can reason about it.

Bulhwi Cha (Oct 20 2024 at 02:00):

In logic, we are only interested in sentences that can figure as a premise or conclusion of an argument, i.e., sentences that can be true or false. So we will restrict ourselves to sentences of this sort, and define a sentence as a sentence that can be true or false.

You should not confuse the idea of a sentence that can be true or false with the difference between fact and opinion. Often, sentences in logic will express things that would count as facts— such as ‘Rudolf Carnap was born in Ronsdorf’ or ‘Simone de Beauvoir liked taking walks’. They can also express things that you might think of as matters of opinion—such as, ‘Rhubarb is tasty’. In other words, a sentence is not disqualified from being part of an argument because we don’t know if it is true or false, or because its truth or falsity is a matter of opinion. If it is the kind of sentence that could be true or false it can play the role of premise or conclusion.

Also, there are things that would count as ‘sentences’ in a linguistics or grammar course that we will not count as sentences in logic. (Magnus 2024)

Reference

Bulhwi Cha (Oct 20 2024 at 02:05):

Although the authors of this textbook didn't use the term 'proposition,' we can give a similar explanation to it.

Bulhwi Cha (Oct 20 2024 at 05:34):

Kevin Buzzard said:

I don't think this is true. Mathematicians see the word Proposition meaning "easy true statement" in all their courses. There might be one exception -- for example the unique and optional logic course which I attended as an undergraduate used Proposition in the same way as lean does. But this "weird" use of the word is the first thing I cover in my lean course.

A user of Philosophy Stack Exchange gave the following comment in which the title of Dolciani's text mentioned is "Modern Introductory Analysis."

Conifold said:

Mirriam-Webster also has 2a and is not controlling for mathematical uses anyway. √2 + √3 = √5 and the like are propositions in English mathematics, and not just of school kind, see e.g. Dolciani's text: proposition is a statement that is either true or false, but not both true and false. Mathematical terminology is one of the most internationalized.

I added the link to the dictionary to this quote.

Bulhwi Cha (Oct 21 2024 at 00:08):

Bulhwi Cha said:

In my experience, which was 12 years ago, Korean high school mathematics teachers and the textbook they used never discussed whether we should regard a sentence or expression whose truth value we don't know yet as a proposition. They only showed examples of "easy" true or false propositions. I'm pretty sure it's the same nowadays.

But, maybe you're truly a constructivist and you don't believe that something can be true or false without a constructive proof. A constructive proof shows without a doubt that the proposition is a proposition.

I suspect that the teachers, not me, seem to act like constructivists when they teach the term to students, but I need more evidence to support my claim. Unfortunately, I can't conduct a survey asking them about this matter. I'm not in a position to do that.

Recently, a high school student from Korea asked two math teachers which of the following is a proposition: (a) a subjective value judgment and (b) a mathematical statement whose truth value we don't know yet. Both responded that (a) isn't a proposition.

However, they were divided on whether (b) is a proposition. One of them said that (b) is also a proposition since we can determine its truth or falsehood. The other argued that linguistically speaking ("국어적으로 해석한다면"), we can determine the truth or falsehood of (b), but mathematically speaking, it can't be a proposition.

Tyler Josephson ⚛️ (Nov 12 2024 at 14:10):

Interesting discussion. I haven’t found any of my students to be interested in the details of this definition. They seem to readily accept whatever definition Lean uses to define what a proposition is. Would the lesson, as this pertains to Lean, be that only statements of type ‘Prop’ are propositions? Maybe the connection to natural language might be: just as statements which don’t type check cannot be propositions, statements about nonsense cannot be propositions?

Bulhwi Cha (Nov 12 2024 at 14:44):

Tyler Josephson ⚛️ said:

Would the lesson, as this pertains to Lean, be that only statements of type ‘Prop’ are propositions?

I think this is the simplest explanation of propositions. Although it can't be a philosophical definition of a proposition, most students would be satisfied with it.

Last updated: May 02 2025 at 03:31 UTC