Bool vs Prop

Stream: Lean for teaching

[Martin Dvořák]

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

[Kevin Buzzard]

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]

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]

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

[Martin Dvořák]

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]

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]

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]

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]

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)]

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]

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

[Flo (Florent Schaffhauser)]

Yes, that's the whole point.

[Eric Wieser]

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

[Eric Wieser]

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)]

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).

[Nilesh]

As a beginner, I find the foundational system very confusing.

Referring to https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/ and https://lakesare.brick.do/on-universes-in-lean-vByqZWpNnrEJ, I came up with this:

image.png

Green boxes are Types, non-green are Universes/Sorts.
In this sense, Bool and Prop are similar because both are contained in Type 0, but different because Prop is a universe whereas Bool just a Type.

Is my understanding correct?

[Henrik Böving]

The picture is not correct.

There is a difference between: docs#Boo.true, docs#Bool.false and docs#True, docs#False

Bool is a type with two values that happen to be called true or false, it is basically isomorphic to any set with two elements. It is interesting for programming or well, any case where you need something that behaves like a set with two elements.

True and False on the other hand are properties (not values) (hence why they live in Prop), Trueis a property that you can always prove because it requires no assumptions (True is not really an interesting or useful property most of the time) and False is a property that can never be proven, unless you have some contradiction at your hand.

[Nilesh]

Thanks @Henrik Böving I've updated the picture:

image.png

[Kevin Buzzard]

I think that Prop : Type is misleading (or at least it misled me when I was trying to make sense of all this nonsense). For me it's worth just focusing on the fact that everything is at one of three levels: a universe, a type and a term.

[Henrik Böving]

Nilesh said:

Thanks Henrik Böving I've updated the picture:

image.png

that looks more correct yes

[Florent Schaffhauser]

@Nilesh

I like your picture :sweat_smile:

I don’t know if I would say that they are similar, but Bool and Prop are indeed both terms of type Type 0 (or Sort 1, or just Type). So they are both types (by definition).

But the type Bool has just two terms, one called true and the other one called false, while Prop can be considered as having many more (all the formulas from first order logic).

And as Henrik pointed out, there are terms of type Prop (or Sort 0) called True and False, but they are spelled differently (capitalized). These can be thought of as truth values for decidable propositions.

Finally, your are right, Prop is a universe (in the sense that its terms are themselves types), while Bool is not.

[Florent Schaffhauser]

You might want to also capitalize True -> False in the new picture :blush:

[Kevin Buzzard]

I could imagine some other type theory where universes don't have types and then the two blue boxes would just sit next to each other instead of one arbitrarily being inside the other

[Nilesh]

@Flo (Florent Schaffhauser) Right. :thumbs_up:

#check True -> False indeed shows True -> False : Prop.
But #check true -> false shows true = true → false = true : Prop which I don't understand at all. :grinning:

[Kevin Buzzard]

-> takes two types, true is a term not a type, but there's a coercion from Bool to Prop sending b to b = true.

[Nilesh]

@Kevin Buzzard Ah, that makes sense.

Updated the picture.
image.png

[Florent Schaffhauser]

Kevin Buzzard said:

I could imagine some other type theory where universes don't have types and then the two blue boxes would just sit next to each other instead of one arbitrarily being inside the other

But then we wouldn’t be able to use types like Nat in the first order formulas of type Prop, would we?

EDIT: Although for that it is (probably) sufficient to have the two blue boxes seating inside one same box, so I get your point now.

[Henrik Böving]

If you want to get even closer to the way it is actually implemented you would find that R x R -> R is usually written R -> R -> R because we are in a functional programming language (they are equivalent)

[Nilesh]

So, if True and False are separate from true and false, I may be able to create a different variant of Bool using Sum True False?

[Henrik Böving]

No, that type would need to have a proof of False on the right values which is not possible. But for example Sum Unit Unit would indeed be the same as Bool

[Eric Wieser]

A comment on the latest image: docs#Empty is a Type, not a Prop

[Florent Schaffhauser]

Oh, right! The empty proposition is called False, indeed :relieved:

docs#False

[Eric Wieser]

Or PEmpty.{0}

[Florent Schaffhauser]

Henrik Böving said:

No, that type would need to have a proof of False on the right values which is not possible. But for example Sum Unit Unit would indeed be the same as Bool

Nice. One question, though: how would you formalize the fact they are the same here? By setting up a bijection between the two? Or more categorically?

[Henrik Böving]

Lean does have a notion of type equality (like literally via =) but its not very nice to use. Generally speaking I would say formalize it how you need it in your bigger theory. Idk if mathlib has a stance on how to do this type of stuff canonically?

[Florent Schaffhauser]

Yes, I don’t know either, but I’m interested to find out :smile:

I guess one could try to prove the universal property of Sum Unit Unit for Bool, but it’s not clear if it would be useful (I agree that the statement to formalize depends on what you need it for).

And I thought that type equality would simply not work here, but maybe I’m wrong.

[Yury G. Kudryashov]

Mathlib uses docs#Equiv

[Patrick Massot]

Nilesh said:

As a beginner, I find the foundational system very confusing.

The good news is you can go very far with a very limited understanding of foundations. In particular the difference between Bool and Prop is 99% irrelevant if you are interested in formalized mathematics in Lean.

[Florent Schaffhauser]

Kevin Buzzard said:

I could imagine some other type theory where universes don't have types and then the two blue boxes would just sit next to each other instead of one arbitrarily being inside the other

I thought some more about your remark: one of the advantages of having the box Prop inside the box Type and not next to it is that terms such as Nat → Prop are also in Type, without having to go to Type 1 to be able to write that :thinking:

[Florent Schaffhauser]

Nilesh said:

Updated the picture.
image.png

Out of curiosity, what tool do you use to produce this picture? :sweat_smile:

[Kevin Buzzard]

I think the fact that Nat -> Prop doesn't have a higher type is a hack in the way the type theory works rather than the fact that Prop : Type. See imax, specifically designed to make this hack work. What I'm saying is that it's all hacks and there could have been other hacks instead. I'm arguing that Prop : Type is just one of these hacks and is not something that one has to take on board and understand in order to get a feeling for the type theory. But this is just my personal interpretation of what is going on. I teach students what (I think) they need to know about the type system (namely element : type, type : Type, proof : statement and statement : Prop) and no more, because I've decided that these are the important statements and everything else that goes on under the hood is confusing and irrelevant. But I'm not teaching a type theory course. I tell them Set X is the type of subsets of X and they don't ask themselves "how does this work internally in the type theory" for the same reason that they've never queried why the set of subsets of a set is a valid mathematical object in the informal set theory that they see used in other classes.

[Nilesh]

@Flo (Florent Schaffhauser) I used tldraw.com for this.

[Nilesh]

@Kevin Buzzard Yeah, a lot of truth in that. I've occasionally been nerd-sniped into looking for "the absolute minimal" foundations of types or computing or mathematics, but been learning recently that it's not a fruitful pursuit. Came across this bit from John McCarthy when reading about Turing Tarpit:

We thought if we were to find the smallest universal machine then we could learn a great deal about computability -- of course that wouldn't be so!

Another quote I liked:

Beware of the Turing tar-pit in which everything is possible but nothing of interest is easy.

[Nilesh]

Here is the corrected image after fixing the error @Eric Wieser pointed out.

image.png

[Kevin Buzzard]

There's also a way of defining group theory by using only one (very long) universally quantified equation which happens to be equivalent to the usual associativity, 1 and inverse axioms, and it doesn't tell you anything about group theory other than the fact that this axiom is hell to work with.

One of the first exercises that John Thompson set us in my basic group theory undergrad class was to show that of the five usual group theory axioms (associativity, left and right inverse, left and right identity) you can delete two of them (but you have to be careful about which two). At the time I found this intriguing but now I realise that really this is just a gimmick in some sense; I've never seen a practical use for "we have left inverses and left and right identity and associativity so now we don't have to check right inverses" for example, and if we really did drop one of these axioms and then there was some situation where one was easier to check than the other one then there would be a 50% chance that we dropped the wrong one anyway

[Florent Schaffhauser]

Yes, I agree that looking for the minimal set of rules is not always the way to go! Both for transmission of ideas and for practical efficiency. Anyway, it's cool to be able to discuss this here (viz. should Nat → Prop be of type Sort 1 or higher?). As Kevin Buzzard made it clear, making Nat → Prop of type Sort 1 or Sort 2 is a choice (that we can picture with the boxes Sort 0 and Sort 1 being either imbricated or next to each other) and it's fun to think what would be the advantages of each choice :blush:

[Kevin Buzzard]

The way I would explain this to my class would be to say that Fermat's Last Theorem (for all naturals a b c n, some inequalities imply some other inequality) is clearly a true-false statement.

[Florent Schaffhauser]

What if somebody then asks you for an example of a statement that is not a true-false statement?

[Florent Schaffhauser]

Oops, I forgot the JOKE tag :wink:

[Dan Velleman]

I find the nesting of boxes in this diagram misleading, because the type hierarchy is not cumulative. 2 + 2 = 5 is inside Prop because it has type Prop, and Prop is inside Type because it has type Type. But because of the nesting, 2 + 2 = 5 is also inside Type, even though it does not have type Type.

I prefer to think of the collection of all expressions as a directed graph, with an edge from each expression to its type. Here's how I would draw it:
Types.png

[Eric Wieser]

Note that intro is not the name of the inhabitant of True, it's trivial (this is wrong in the other diagram too)

[Kevin Buzzard]

Yeah this is how I draw it in my (maths) class (except rotated 90 degrees, and I only draw the line from Prop to Type and add the other Type n at the very end in a "this is how it actually works but don't worry, this has nothing you do with maths" comment)

[Florent Schaffhauser]

The directed graph is very nice, indeed!

What I find difficult to explain to students is why the presence of terms such as Nat in terms of type Prop is licit, e.g. $\forall x : \mathbb{N}, x + 0 = 0$. Any suggestion?

If I understand Kevin’s rotation of 90 degrees correctly, I get a picture that is similar to the box diagram, but with directed arrows instead of boxes, and terms such as Nat and Prop are at the same level of the resulting tree.

[Dan Velleman]

Eric Wieser said:

Note that intro is not the name of the inhabitant of True, it's trivial (this is wrong in the other diagram too)

Or True.intro. But you're right, just intro isn't right.

[Kevin Buzzard]

My picture: take the diagram above, remove all vertical arrows and all Type n for n>=1, rotate 90 degrees if you like, and then claim that what you have left is all you need for undergraduate mathematics.

[Kevin Buzzard]

But if you want to understand type theory then that's a different question.

[Eric Wieser]

Huh, I didn't know about docs#True.intro. I guess .intro would be sufficiently correct

[Kevin Buzzard]

You thought there wasn't a constructor? ;-)

[Dan Velleman]

Flo (Florent Schaffhauser) said:

What I find difficult to explain to students is why the presence of terms such as Nat in terms of type Prop is licit, e.g. $\forall x : \mathbb{N}, x + 0 = 0$. Any suggestion?

Lots of expressions of one type contain within them subexpressions of other types. If x has type Nat, then Vector Nat x has type Type. Is that different from the occurrence of Nat and natural numbers in propositions?

[Florent Schaffhauser]

Indeed, it’s not different :smile:

[Kyle Miller]

That Vector example is a bit different though since Nat is a Type and the Vector is a Type. With the forall something special is happening, where the result is in a smaller universe, Prop. I believe that this is Prop being what's called an "impredicative universe".

[Kyle Miller]

In particular, quantification/functions usually gives you something at least as big as the domain and codomain, unless the codomain is a proposition, in which case you get a proposition. That's necessary for foralls to all be propositions.

[Dan Velleman]

Yes, you're right. This is something special about Prop.

[Kyle Miller]

I remember in Automath that some quantifications are "too big" and you don't get propositions, so this must not be a necessary part of type theory.

[Kevin Buzzard]

#tpil talks about it here https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html?highlight=imax#the-universal-quantifier (start at "The idea is as follows")

[Florent Schaffhauser]

Kyle Miller said:

That Vector example is a bit different though since Nat is a Type and the Vector is a Type. With the forall something special is happening, where the result is in a smaller universe, Prop. I believe that this is Prop being what's called an "impredicative universe".

Thanks for pointing that out @Kyle Miller ! Here is how I think about what is similar and what is not in the two examples that we have been discussing.

In docs#foundational_types, it says that, when β : α → Prop, the type of dependent functions (a : α) → β a is denoted by ∀ a : α, β a.

So the type ∀ n : Nat, n + 0 = n is the type of dependent functions (n : Nat) → (n + 0 = n) .

#check (n : Nat) → (n + 0 = n)  -- ∀ n : Nat, n + 0 = n

And indeed if we declare

def β : Nat → Sort 0 := fun n => n + 0 = n
def γ (n : Nat) : β n := Nat.add_zero n

then we get

#check @γ  -- γ : ∀ (n : Nat), β n
#check ∀ (n : Nat), β n  -- ∀ (n : Nat), β n : Prop

We can partly reproduce this type of behavior at every universe level k, not just k = 0. I say 'partly' because the last #check will give something different if k > 0.

import Lean.Level
universe k l

variable {L : Sort l}
def F : L → Sort k := sorry
def G (x : L) : F x  := sorry

#check @G L  -- G : (x : L) → F x
#check (x : L) → F.{k} x  -- (x : L) → F x : Sort (imax l k)

Or with an explicit, albeit slightly artificial, example of a term L' of type Sort l:

def L' := PUnit.{l}
def F' : L' → Sort k := fun (_ : L') => PUnit.{k}
def G' (x : L') : F' x  := PUnit.unit.{k}

#check @G'  -- G' : (x : L') → F' x
#check (x : L'.{l}) → F'.{k} x  -- (x : L') → F' x : Sort (imax l k)

where Nat.imax l k is equal to 0 if k = 0 and to max l k if k > 0 (docs#Nat.imax).

So, as you were saying, what is special about Sort 0, is that, given a function β : α → Sort k, where α is a term of type Sort l, the type of dependent functions (a : α) → β a is a term of type Sort (max l k) if k > 0 and of type Sort 0 if k = 0.

It looks to me that we should perhaps view this as the type-theoretic way to define a proposition starting with the universal quantifier: to prove it means to define a dependent function of the appropriate type (and this type is by definition a term of type Sort 0).

However, I don't know where in Lean the type of dependent functions (a : α) → β a is defined, as a term of type Sort (imax l k). I guess that is why it is one of the foundational types.

[Kyle Miller]

Flo (Florent Schaffhauser) said:

However, I don't know where in Lean the type of dependent functions (a : α) → β a is defined, as a term of type Sort (imax l k). I guess that is why it is one of the foundational types.

Yeah, dependent function types are foundational. They are one of the core types of expressions, and they appear as docs#Lean.Expr.forallE in the implementation of Lean. The rule about what its type is is explicitly encoded in the docs#Lean.Meta.inferType function. (We're well into the meta-level now!) Note: that's the elaborator's implementation. The kernel has its own independent implementation too.

[Kyle Miller]

Here's the implementation: https://github.com/leanprover/lean4/blob/b614ff1d12bc38f39077f9ce9f2d48b42c003ad0/src/Lean/Meta/InferType.lean#L139-L146

If you look carefully, you can see "imax" in mkLevelIMax'.

[Kyle Miller]

This function is a bit more complicated than you might expect since it handles arbitrarily nested dependent function types and calculates the Sort (imax u1 (imax u2 ... (imax un v) ...)) all at once, I assume as an optimization.