## Stream: Lean for teaching

### Topic: Bool vs Prop

#### Martin Dvořák (Dec 17 2023 at 08:49):

How would you explain the difference between Bool and Prop to (smart) highschoolers?

#### Kevin Buzzard (Dec 17 2023 at 11:08):

They're the same thing, but at different levels in the hierarchy: one is a type and one is a universe. I usually explain universes, types and terms on day 1

#### Alex J. Best (Dec 17 2023 at 14:06):

That said, why do you want to explain that to highschoolers? If you are just teaching them a bit about formalizing maths and not about computation it seems an unnecessary confusion to even introduce Bool at all

#### Martin Dvořák (Dec 17 2023 at 14:18):

Actually, I first taught them about computation, during which Bool appeared. Now I teach them about proving.

#### Martin Dvořák (Dec 17 2023 at 14:19):

Kevin Buzzard said:

They're the same thing, but at different levels in the hierarchy: one is a type and one is a universe. I usually explain universes, types and terms on day 1

D-D-D-Day 1? I hoped I could avoid talking about universes altogether!

#### Mario Carneiro (Dec 17 2023 at 14:24):

well, once you say "everything has a type" it's a pretty natural question to ask what the type of Type is, even at a high school level. For extra fun you can climb the universe hierarchy using lean's nested hovers

#### Kevin Buzzard (Dec 17 2023 at 14:37):

I say x : Real : Type and proof : statement : Prop and that's about it as far as type theory is concerned, so Prop is explained on day 1 yes. I never talk about bool because I'm talking to mathematicians

#### Yury G. Kudryashov (Dec 17 2023 at 14:53):

There are quite a few open questions that can be explained to high schoolers. E.g., "every triangle admits a periodic billiard trajectory". That's a Prop that you don't know how to convert to Bool.

#### Kyle Miller (Dec 17 2023 at 15:41):

A Bool is either true or false, and if you let Lean run for long enough it will tell you which it is. A Prop is either True or False, but you can't depend on Lean to tell you -- but you can try to write a proof.

You need some passing familiarity with incompleteness to appreciate that there really is a distinction. Otherwise, I guess you could say something like what Yury is suggesting, that Prop is like Bool but it doesn't come with any algorithms to evaluate the statements. (How would you evaluate a universal quantifier over Nat? That's like an infinite for loop.)

#### Flo (Florent Schaffhauser) (Dec 17 2023 at 17:28):

Martin Dvořák said:

Actually, I first taught them about computation, during which Bool appeared. Now I teach them about proving.

How about giving them some intuition of what a decidable proposition is, and then say that a decidable proposition can be converted into a boolean value?

def testAge (age : Nat) := age > 40
#check testAge 21  -- testAge 21 : Prop
#eval testAge 21  -- failed to synthesize  Decidable (testAge 21)

def testAgeBool (age : Nat) : Bool := age > 40
#check testAgeBool 21  -- testAgeBool 21 : Bool
#eval testAgeBool 21  -- false


Conversely, a term b : Bool can be converted into the proposition P := Eq b true  and we see that P has a proof if b = true  and that ¬P has a proof if b = false.

Surely, somebody will ask if every proposition is decidable :sweat_smile:

#### Eric Wieser (Dec 18 2023 at 10:50):

That looks like a lousy pedagogical example, because it leaves the reader baffled over whether age > 40 is decidable or not

#### Flo (Florent Schaffhauser) (Dec 18 2023 at 11:09):

Yes, that's the whole point.

#### Eric Wieser (Dec 18 2023 at 12:00):

So is the point in that example to teach the reader about reducibility?

#### Eric Wieser (Dec 18 2023 at 12:01):

Because certainly that seems to be what this extended example shows:

def testAge (age : Nat) : Prop := age > 40
#check testAge 21  -- testAge 21 : Prop
#eval testAge 21  -- failed to synthesize  Decidable (testAge 21)

abbrev testAgeAbbrev (age : Nat) : Prop := age > 40
#check testAgeAbbrev 21  -- testAgeAbbrev 21 : Prop
#eval testAgeAbbrev 21  -- false

def testAgeBool (age : Nat) : Bool := age > 40
#check testAgeBool 21  -- testAgeBool 21 : Bool
#eval testAgeBool 21  -- false


#### Flo (Florent Schaffhauser) (Dec 18 2023 at 12:54):

Oh, I see.

But no, I was hoping it would trigger questions surrounding decidability instead, in relation with #decPropToBool.

instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool where
coe := decide p


So, to sum up, two (hoped for) points:

1. Show that a decidable proposition can be converted into a boolean value.
2. Discuss non-decidable propositions (informally).

Last updated: Dec 20 2023 at 11:08 UTC