terminology : statement vs proposition

Stream: new members

[rzeta0]

I'm slowly starting to acclimatise to the Lean terminology.

A recent discussion about Odd raised the idea of it being a function that takes a number and outputs a proposition.

I was wondering whether there is a difference between proposition and statement, when speaking generally (maths, logic) and not specifically about Lean.

Is it the case that a proposition is a subset of statement?

That propositions are true/false but statements are more general sentences using the language and grammar of mathematics and logic?

[Kyle Miller]

I've heard the idea that a proposition is a sentence that has a definite truth value. Conjunctions, implications, quantifications are all ways to construct propositions out of other propositions — we use restricted language to ensure we are always using propositions. That excludes things like "this proposition is false".

I'm not sure what definitions of "statement" are out there, but if I heard "mathematical statement" I'd think "proposition".

[Mario Carneiro]

In logic, when "statement" is used in contrast with "formula", the distinction is that a "statement" has no free variables / it is "closed". In lean this is always the case, because theorems universally quantify over any parameters you pass either directly or via the variable command. A formula consists of many sub-formulae, but a statement is not composed out of smaller statements (at least in general), it has sub-formulae.

Also there is a general tendency to use the term "statement" for the things that are actually top level goals or theorem types, rather than for just arbitrary subexpressions of type Prop, which may be related to the technical usage in logic just mentioned.

[Mario Carneiro]

Also, looking back at your question I see I used the term "formula" instead of "proposition"; these are basically synonymous, although we tend to use "proposition" or "prop" because lean's syntax for propositions is p : Prop

[rzeta0]

@Mario Carneiro - thanks for your useful explanation.

I want to check I've understood with two examples:

---

Consider the h: Odd (14 : ℤ). Are the following true?

1. h is a proposition.
2. h is made up of sub-formulae, Odd and (14 : ℤ).
3. The formula Odd is not a proposition, because it is not complete enough to decide true/false.
4. The formula (14 : ℤ) is a proposition, because we can decide whether it is true or false.

Your second comment tells me that "formula" is synonymous with "proposition" . So everything in my list is a proposition and a formula. Is there anything in my example which is a "statement"?

---

Now consider g: (x=3) ∧ (y=4). Are the following true?

1. g is a proposition.
2. g is made up of sub-formulae, (x=3) and (y=4).
3. The logical conjunction symbol ∧ is a connective, so not really a formula itself.
4. Both formulae (x=3) and (y=4) are also statements, because we can decide whether they are true / false.

Again - your second comment tells me that "formula" is synonymous with "proposition" . So everything in my list is a proposition and a formula. Is there anything in my example which is a "statement"?

---

[Mario Carneiro]

Odd is not a formula/proposition, it is an expression. Formulae/propositions in lean are just the things with type Prop

[Mario Carneiro]

in first order logic formulae actually have a recursive structure (i.e. p /\ q is a formula whose subformulae are p and q) but in lean, which has higher order syntax, this is instead expressed using And p q where now there are additional sub-expressions like And and And p which are expressions that are not formulae

[Mario Carneiro]

In the first list, only 3 is true (with "formula" replaced by "expression"). (1) is false because h is not a proposition, it is an element of a proposition, we call these "proofs". Odd (14 : ℤ) is a proposition.

[Mario Carneiro]

For the second list: g is a proof, not a proposition. (x=3) ∧ (y=4) is a proposition/formula. It has subformulae x = 3 and y = 4, and it has several additional sub-expressions, including And, And (x = 3), x, Eq x, x = 3 etc. The conjunction symbol is not a formula indeed, but in lean it is a constant called And : Prop -> Prop -> Prop and it appears as a subexpression of (x=3) ∧ (y=4).

Formulae (x=3) and (y=4) are not statements: using the formal logic definition this is because they are open terms, they contain free occurrences of x and y respectively, and using the colloquial definition this is because they aren't appearing as self-contained expressions as the type of a hypothesis or goal at this point.

[rzeta0]

Thanks again @Mario Carneiro

I am less certain than before I asked the question - which is good because it means I had false confidence in my understanding.

I need to go away and think about this for a a few hours.

Is there a web page / short tutorial that explains this hierarchy of expression, formulae, propositions and statements (and anything else) ?

[Mario Carneiro]

nothing I can suggest off hand. Some of this complexity is because the terminology of formulae, propositions and statements comes from formal logic, which is then reinterpreted into type theory which adds additional notions and tries to identify the parts that still look kinda similar to their FOL counterparts

[Mario Carneiro]

(Actually that's not really true, the terminology really comes from informal mathematics, and formal logic tried to identify the parts of the formal system that look kinda like the informal notions.) This terminological evolution is how you get things like Cartesian Cubical Type Theory which I'm not sure Descartes would have approved of

[rzeta0]

I will go away for a few hours and see if that helps my brain.

I may also try, in the next few days, to draw a diagram and write some explanatory text, of a few of these concepts.

The idea won't be to create something that is fully encyclopaedic, but just sufficient to help beginners like myself at the beginning of their journeys with simple lean maths proofs.

[Julian Berman]

Take this with a grain of salt as a fellow "mostly beginner", but my opinion would be that these sorts of questions (this and one or two recent similar ones) are not very useful to your learning, and there are I think better uses of your time. I certainly don't think the majority of people using Lean for mathematics know or want to know these specifics in terminology at this level of detail unless they're logicians or studying foundations beyond Lean. If you say "is p \and q a statement? an expression? a formula?" I think 75%+ of Lean users will probably say "I don't know, probably yes to all 3." I do think it's useful that if you see a concept that surprises you or seems novel, and if you then think that concept deserves a name, that you use and learn the name others would use for that concept. And certainly there's a bunch of terminology you'll encounter in Lean and here on the Zulip, so you should keep an eye out for those and see if you understand them or otherwise try to learn what concept they're representing -- I just don't think lots of what's here is in that category. So in particular, oversimplifying, if I were in your shoes, I would have stopped at "Odd is a function from numbers to Prop" and moved on to something more useful to know. Again, just my 0.02 trying to be helpful, feel free to ignore if you really do care to chase these rabbit holes!

[Bulhwi Cha]

Julian Berman said:

I certainly don't think the majority of people using Lean for mathematics know or want to know these specifics in terminology at this level of detail unless they're logicians or studying foundations beyond Lean.

I've been introducing Lean to philosophy majors in South Korea. Some of them seem to care about the meanings of these terms because they've been studying formal logic, though they're unfamiliar with type theory. One of my Lean mentees was a philosophy major studying philosophy of science and artificial intelligence.

[Bulhwi Cha]

I'm just trying to introduce proof assistants to various people!

[Kevin Buzzard]

But I think Julian has a point. I have no idea about these technical logic terms. For me the key point is that you should know that there are four things in play: theorem statements (types in the Prop universe), theorem proofs (terms of those types), sets (types in the Type universe) and their elements (terms of those types). The statement/proof and set/element concepts are unified by the type/term idea in type theory. Everything else is just nomenclature. I'm sure it's important if you want to write tactics or whatever, but if you just want to do what rzeta0 is doing then this should be enough.

Edit: I guess the reason I wrote this blog post
(which I just remembered the existence of) was just to explain as much of the basics as I felt one needed to know in order to turn mathematics into Lean.

[rzeta0]

I agree with what's been written.

I, and I suspect many other beginners, don't need a complete familiarity with formal logic terminology in order to write simple proofs in simple lean.

I guess the level of knowledge should be enough to (1) feel comfortable when reading others' use of that terminology, eg the docs, and (2) to avoid misunderstandings when reading and writing your own content.

Kevin, I will print out your blog and probably read it over coffee tomorrow, it looks helpful.

All this started when I wrote the words:

(13 : ℤ) is intended to be a statement saying that 13 is an integer

and as soon as I wrote that I realised I didn't really know how Lean people used the word statement, and that led on to the other questions about expressions, propositions, etc

[Mario Carneiro]

This is actually an interesting example, because you would not be unreasonable to think that 13 : ℤ is a statement or proposition, since people like to say that : is just some type theory jargon and you can substitute it for ∈ from your traditional mathematics education, and 13 ∈ ℤ is a proposition in traditional mathematics

[Mario Carneiro]

But this is actually one place where type theory differs from traditional mathematics, because (13 : ℤ) is not a proposition, and it is important to realize that typing judgments don't act like propositions - they cannot be negated, they can only be asserted and checked by the type checker

[Mario Carneiro]

Rather than reading (13 : ℤ) as "13 is an integer" (which is a proposition), you should read it as "13, which is an integer, ..." which is a noun phrase with an embedded assertion in it

[rzeta0]

very interesting !

out of interest, if it shouldn't really be called a proposition, then what should it be called? (i realise this is a rabbit hole)

a "type assertion" ?

[Mario Carneiro]

13 is an integer :)

[Mario Carneiro]

The syntax (e : T) is called a type ascription

[rzeta0]

is it useful to think of this as ≣ vs ∈

[Mario Carneiro]

it lets you take any subexpression and say "and also, that thing has this type"

[Bulhwi Cha]

Mario Carneiro said:

The syntax (e : T) is called a type ascription

Can it also be called a judgment? Never mind!

[Mario Carneiro]

although in practice it is also often used to disambiguate expressions, like in this case Odd 13 could also be talking about Odd (13 : Nat)

[Mario Carneiro]

Typing judgments don't usually appear directly in lean concrete syntax, but typechecking involves validating typing judgments, and they also have a similar appearance. You usually see them written something like
$\Gamma\vdash e:\tau$

[Mario Carneiro]

Mario Carneiro said:

although in practice it is also often used to disambiguate expressions, like in this case Odd 13 could also be talking about Odd (13 : Nat)

so you could also read (13 : ℤ) linguistically as "13 (the integer)", by contrast to the natural number or the matrix or whatever else. But again, notice that this is a noun phrase, not a complete sentence, it doesn't make sense to assert it as a true or false thing

[Kyle Miller]

@rzeta0 Are you the sort of person who would have read Let Over Lambda by Hoyte? He talks about designing things to have 'duality of syntax', which is where one syntactic form can have multiple related meaning depending on where it appears. In C for example, a[i] is both a value and lvalue, i.e. you can write x = a[i] to extract a value from an array, and a[i] = x to set a value. These are completely different if you think about it, but it feels very natural.

The (n : T) syntax also appears in multiple places, each with related meanings, but all linked by the idea of "is a":

• in expressions, (n : T) ensures that n is a T, and it evaluates to n
• in binder lists (like in a theorem statement, or after fun or forall), it declares a parameter
• in the InfoView or various error messages, it appears without parentheses to let you know the type of something

[Philippe Duchon]

One thing that should make it clear that 13: Nat is not a proposition, is that you cannot use a connective to build a bigger proposition with it as a sub-proposition. The definition of what constitutes a proposition in Lean's type theory is significantly more complex than, say, in propositional or first-order logic, but one thing they share is that if P and Q are both propositions, then things like P /\ Q and P -> Q are propositions too.

[Kyle Miller]

There's also the stronger reason that 13 : Nat isn't valid syntax. But that of course this design choice is motivated by what you are saying.

[rzeta0]

@Kyle Miller - thanks for the further explanation, and the suggested book, which I haven't read but looks really interesting - something to add to my to-do list !

[rzeta0]

What mario said about "noun phrase" is very helpful - thanks.

[Kevin Buzzard]

Right: (13 : ℤ) means "the integer thirteen" not "thirteen is an integer".

[Kyle Miller]

I'm reminded that a few years ago I was proposing syntax like the ℤ => 13 (this was back in Lean 3, so it probably was the ℤ, 13 instead) for (13 : ℤ). It's nicer when the value is something big to know what the type is supposed to be ahead of time. It's a bit different from show ℤ from 13, which is stricter in a number of ways, and also show results in a let_fun.

At least nowadays it's trivial to define it yourself:

notation "the " ty " => " val => (val : ty)

#check the ℤ => 13

[rzeta0]

Kevin, I have now read your blog: https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory

Thank you for sharing it. It is the first time I have even started to glimpse what "type theory" even means (I did maths up to a-level, nothing more).

Your blog was particularly helpful because it illustrated the ideas with examples.

For me, a key take away is that there are 2 universes in Lean - Type and Prop.

Your discussion of the distinction between a theory and its proof was also helpful.

I haven't mastered any of this, but some of the paths ahead are now clearer, at least for the next few yards.

[Mario Carneiro]

(I will suppress the urge to "umm actually")

[rzeta0]

Mario Carneiro said:

(I will suppress the urge to "umm actually")

go ahead - your previous "um actually" explaining the difference between a "noun phrase" and a statement was very helpful.

[Kyle Miller]

(Today's word is "apophasis", to say something by saying you won't say it :-) )

I think Mario might be wanting to say that there are infinitely many Type universes, not just one.

[Kyle Miller]

It's a technical thing that you don't need to worry about for now. This hierarchy of universes solves the problem "What is the type of Type?". The answer in Lean's type theory is Type 1, whose type is Type 2, and so on. Trying to make the type of Type be Type itself leads to paradox.

[Kyle Miller]

In some systems, notably Automath, there is simply two universes Prop and Type, and there just isn't a type of Type.

[rzeta0]

Is this picture i drew correct (enough for beginners)?

app_taxonomy.png

[Kyle Miller]

Yes, there are three degrees of objects: terms, types, and universes. The empty box on the right is "propositions".

(The only complexity beyond this is that Lean lets you treat a universe like it was a type. For example, Prop is also a type in the Type universe. I think this is something you can overlook until you realize it's something you need.)

[Kyle Miller]

(A keyword is "universe polymorphism": you can make definitions that work for types no matter which universe they come from. That way you don't have to write one definition for Prop and another for Type.)

[rzeta0]

thanks @Kyle Miller - it is reassuring that the framework is broadly correct.

my next diagram will try to explain how propositions are built - that stuff about "formulae / expressions / logical connectors aka constants like And / labels or aliases like h:"

[Kyle Miller]

Speaking of 'duality of syntax' from earlier, in some type theories there is a difference between the concepts t : Ty ("term t has type Ty") and Ty : U ("type Ty is in universe U"). Lean combines them into a single concept, which is convenient, but it can also be confusing because there really are three broad classes of objects.

[Kevin Buzzard]

I find the fact that "proposition" and "Prop" are different things quite confusing; this is why I use "theorem statement" when I'm teaching. My experience with mathematicians is that they are sometimes vague about the difference between "theorem statement" and "theorem proof" when speaking informally. You can "apply the Poincare' conjecture" but only because it's been proved, so you're really applying the proof of the Poincare' conjecture. You can't apply the Goldbach conjecture, unless you want to add a hypothesis to your argument.

@rzeta0 there are other universes much bigger than Type, which are usually referred to as Type* in Lean, or Type 1, Type 2, Type 3,.... But again when I'm teaching undergraduates I never mention these higher universes as they are completely unnecessary for undergraduate level mathematics; they are only there for technical reasons coming from CS/logic, and are basically only useful to mathematicians when they start doing category theory or other kinds of mathematics which start reasoning about the "collection of all sets" as a mathematical object. We don't get that far in my class so Type and Prop are the only universes that my students ever see.

[Kevin Buzzard]

The main reason that I avoid them is that your picture has a very pleasing symmetry to it and adding the higher universes breaks the symmetry for no good pedagogical reason (at least if your main concern is undergraduate level mathematics).

[rzeta0]

So I created another diagram, but am far less certain of its correctness. I welcome replies with corrections / clarifications.

Key points / questions:

• I am now avoiding the words formula and statement
• I am now only using the words proposition, proof, expression - because I think these sufficiently cover most beginner needs - am I right?
• proposition is something that is true or false
• proof is a bunch of propositions which justify another proposition
• expression is any code that is recognised as correct lean/mathlib - why are = and `∧ not expressions?
• re-reading the thread I was surprised that h was called a proof. I see it as a "label" which points to a proposition.

app_taxonomy_expressions.png

[Julian Berman]

I don't personally think it's important for a beginner to know or use the term "expression" (i.e. to a beginner I don't see value in the whole bottom row getting a name).

[Julian Berman]

I think you're also missing the most important (IMHO) concepts, namely that x = 1 \or y = 3 is a proposition yes, and a type! and a term of that type, i.e. h : x = 1 \or y = 3 is a proof of this proposition.

[Julian Berman]

Perhaps you're missing the nuance between x = 1 \or y = 3 and h : x = 1 \or y = 3.

[rzeta0]

@Julian Berman - I am definitely missing the nuance between x = 1 \or y = 3 and h : x = 1 \or y = 3.

Would you be able to explain? (if you have the patience)

I don't understand your middle paragraph about the most important concepts, perhaps I will after the explanation?

[Mario Carneiro]

Remember that e : T is not itself syntax for an expression in lean, the syntax is (e : T), but either way this is generally interpreted to be talking about e (but with a side remark that it has type T). So h : x = 1 \or y = 3 would be read as just h (which by the way has type x = 1 \or y = 3), which is quite different from x = 1 \or y = 3 (which by the way has type Prop)

[Mario Carneiro]

The object h whose type is x = 1 \or y = 3 is called a proof, and the object x = 1 \or y = 3 whose type is Prop is called a proposition

[Mario Carneiro]

there is an underlying operation here, "the type of", which goes from h to x = 1 \or y = 3 and from x = 1 \or y = 3 to Prop. For example, "Mario" is of type "Human" and "Human" is of type "Species" and "Species" is of type "Classification of living things". Sometimes people talk about the "is-a" relationship for this notion: Mario is-a Human but not vice versa

[Mario Carneiro]

it is important not to confuse the class with an element of the class

[Mario Carneiro]

For proofs and propositions this is possibly slightly weird and unintuitive, but the idea is that a proposition is taken to be a classification of all of its proofs. The "elements" of a proposition are all the "ways it can be true", so in particular True has one way to be true, named trivial in lean, and False has no ways to be true, so it is an empty class of proofs.

[rzeta0]

@Mario Carneiro - your first paragraph I think is extremely helpful.

Comparing 3 : ℕ and e : T and then h: x>5to see they are the "same" is really helpful.

It hadn't sunk in properly that h is an element of x>5.

But to say h is a proof that x^2 ≥ 0 does feel odd until I can see what h actually is.

Is this what := does?

That is, h: x^2 ≥ 0 := P is read as h is a proof of the proposition x^2 ≥ 0, and P is a more verbose elaboration of h, specifically, verbose enough that a proof checker can check it.

[rzeta0]

@Julian Berman

I think you're also missing the most important (IMHO) concepts, namely that x = 1 \or y = 3 is a proposition yes, and a type! and a term of that type, i.e. h : x = 1 \or y = 3 is a proof of this proposition.

Looking back at my first diagram I can see that

• x = 1 \or y = 3 is a proposition
• and a type because it is in the middle layer
• and that h is in element of that type, which is in the bottom layer (proofs)

Can I ask why you think this is very important - I think I am missing some important implication of all this.

[Julian Berman]

The reason I think it's super important is somewhat precisely your last realization -- namely that 3 : ℕ is the same notion to Lean as h: x>5, and that this may not match people's intuitions (mathematicians or otherwise) who are not previously familiar with a proof assistant, so it's important to make this clear and to give names to the concepts, and "term" and "type" are the terminology someone will hear for this. In Kevin's post (which I haven't read in awhile but I recall being very helpful) this is a bit of the punchline – in the headline "Propositions are types, proofs are terms."

[rzeta0]

Thanks Julian - you are right, this is not natural to how we've been thinking about maths, so it will take time for it to sink it.

At least now I don' think it is wrong - just a new way to look at it.

Thanks again!

[rzeta0]

Is my understanding of := correct, in my previous message?

That it reads as "this is proof is elaborated as" ?

[Mario Carneiro]

Like my comments about e : T, e : T := val is also not valid syntax on its own, although as @Kyle Miller has mentioned with the points about duality of syntax, := is used to mean related things in many contexts in lean. Most likely the place you have seen this syntax is with either def or theorem before it. theorem foo : 1 = 1 := proof means that we are defining a new name foo for the proof proof, which is a term whose type is 1 = 1, that is, a proof that 1 = 1 is a true statement. After this declaration, foo will also be a term whose type is 1 = 1.

[Mario Carneiro]

we read def c : T := val as "Define c to be a name for the expression val, whose type is T." Thereafter we may use c and know that it also has type T, and we also know that c and val are equal to one another.

[Eric Wieser]

Mario Carneiro said:

here is an underlying operation here, "the type of",

This operation is actually available to you in lean as type_of%, though you should be careful of using it with #check since this applies type_of% a second time:

#check 1          --   1 : Nat
#check type_of% 1 -- Nat : Type

[Julian Berman]

I think a bunch of @rzeta0's questions come from notation seen in the infoview, or at least that's why I'm quite happy with being slightly more willy nilly about calling e : T a thing, and why I'm assuming that your question (@rzeta0 ) is about seeing := in the infoview rather than as something you're typing in a Lean file. I could be assuming wrong of course.

But if that's where you're asking about, that's Lean telling you which term you have. More precisely -- when you see foo : bar in the infoview, that's Lean saying "foo is a bar" like Mario explained. bar here is a type -- it could be a type you've known about all your life like the natural numbers, or a "bend your mind a bit" type, like the type of "proofs of x > 3" -- but if all you see is foo : bar... which bar is it? If you see n : Nat that says "n is a natural number", and there's no specific information about which number it is within n itself. Now you may have some other hypothesis h : n = 37 -- but that is a separate proof that n equals 37. If you see the infoview say n : Nat := 37 that's the infoview saying "n is a natural -- and it's the number 37" all at once. (You can get this kind of thing typically from the let or set tactics, as opposed to have).

[rzeta0]

@Julian Berman I'm definitely typing it.. here 3 times:

import Mathlib.Tactic

example {a : ℕ} (h1: a = 4) : a > 1 := by
  calc
    a = 4 := by rw [h1]
    _ > 1 := by norm_num

I will read the above comments when I wake up later :)

[Julian Berman]

OK, then never mind my last comment.

[Mario Carneiro]

The first := is a variant on the def / theorem thing I described before. example : T := val is equivalent to def _discarded_name : T := val, which is to say it makes a definition but immediately discards it. The purpose is just to check that val actually has type T.

[Mario Carneiro]

The second := is part of the calc notation, and provides a proof for the steps of the transitivity chain. Here again the steps have the form T := val where val is asserted to have type T. (Once upon a time calc used a colon based syntax i.e. T : val instead but people rightfully pointed out that this is backwards, since val has type T and not vice versa.)

[rzeta0]

we read def c : T := val as "Define c to be a name for the expression val, whose type is T." Thereafter we may use c and know that it also has type T, and we also know that c and val are equal to one another.

The first := is a variant on the def / theorem thing I described before. example : T := val is equivalent to def _discarded_name : T := val, which is to say it makes a definition but immediately discards it. The purpose is just to check that val actually has type T.

Thanks - this answers that question.