Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I put an actual definition at theorem. It is still quite the stub, however!
I think you mean “that has a proof” as opposed to “together with a proof”. Yes?
Since this is by nature an exercise in being pedantic, let me try the following pedantry:
In fully formalized contexts such as, say, Coq, there is quite a difference between a theorem and a true proposition, as far as I am aware. A proposition is a certain type and it is true if it is inhabited / (-2)-truncated. But a theorem is an entirely different construct of the language alltogether.
Not sure if that is a useful remark. But anyway.
In Coq, “Theorem” is a synonym of “Definition”. The statement of the theorem is the same as the type of an object being defined, and the proof of the theorem is the thing being defined. From that point of view, I agree with Toby. However, since propositions are (-1)-truncated, any two proofs of the same proposition are equivalent, so “together with a proof” and “that has a proof” are equivalent statements in a category-theoretic sense. (-:
But what I mean is that the language construct “Theorem” is quite diffent from the type that it produces, isn’t it. Propositions / types are part of the type theory. The syntax “Theorem” is not part of the type theory, but part of the Coq interface to allow you to talk about type theory with Coq.
It seems to me. But it’s not so important…
In fully formalized contexts such as, say, Coq, there is quite a difference between a theorem and a true proposition, as far as I am aware. A proposition is a certain type and it is true if it is inhabited / (-2)-truncated. But a theorem is an entirely different construct of the language alltogether.
This is news to me.
In fully formalized first-order theories, I consider a theorem to be a statement in the underlying language that is provable from axioms according to rules of inference. That refers to a property of the statement.
When one says “true proposition”, it’s not a priori clear whether one means ’true’ relative to some given model, or whether one means something that is provable in the theory. In the former case, I do recognize the difference. In the latter, I call it a “theorem”. I am very surprised to hear disagreement on this! And feel that language has gotten twisted around from what is traditionally understood.
I’m not sure that we’re all communicating successfully. Let me try to explain my perspective and all the places that I can guess confusion might be coming from.
I consider a theorem to be a statement in the underlying language that is provable from axioms according to rules of inference.
That is also the case in Coq.
The “vernacular” language, which one uses to interact with the proof system, contains a command “Theorem”. When you issue the command “Theorem”, you specify both a statement and a purported proof of that statement, and the proof system verifies that your proof does in fact prove what it purports to prove.
I would say that the command “Theorem” in the Coq vernacular has the same ontological status as the word “Theorem” in a printed mathematical paper: it alerts the reader (whether that reader be a human being or a computer) of the activity of proving that is about to occur. I don’t know whether that is the source of any confusion.
The notable thing about type theory, however, is that a “statement” or “proposition” is identified with a special sort of “type”, and to give a proof of a proposition is a particular case of giving a term that inhabits a type. With respect to (say) a first-order axiomatization of set theory, there is a “inversion” of the role played by logic and sets/types. In a first-order axiomatization of set theory, we have an formal system which knows nothing but logic, and then within that system we talk about things like sets. In type theory, we have a formal system which knows about types, and then we find logic within that system by identifying propositions with particular types. I don’t know whether that is the source of any confusion either.
Finally, there is also the distinction between syntax/semantics and provable/true. Given any formal system, we can talk about models of that system (assuming some external “world” in which to build models). In some particular model, a statement may or may not be “true”, and a set/type may or may not be “inhabited”. If a statement is formally provable, then the soundness theorem says that it must be true in all models, and similarly if an element of a set/type can be constructed formally, then the soundness theorem says that such an element must exist in all models. (In set theory, these are separate statements; in type theory, the first is a special case of the second.) I don’t know whether that is the source of any confusion either.
Mike, you seem to be worried that I am “confused”. While I appreciate your explanations, which are presumably directed at me and meant helpfully to clear up my possible confusions, I do not think I am actually all that confused.
I am happy to see all these understandings communicated on the nLab page, provided that there is some acknowledgment that the traditional meaning of the word “theorem” is just the way I had it. Open up any traditional text on logic, where the meaning of the word “theorem” is given, and you will find something along the lines of “sentence which is provable from axioms (in a theory)”. If you disagree with that, then please cite a text that indicates otherwise.
Under that interpretation, “theorem” does not mean “sentence plus specified proof”. Maybe I’ll give some examples in a moment, but to get something out of the way, I can understand that the Theorem command in Coq calls for a specific “proof”, or a specific term that witnesses that a certain type is inhabited. But the word “theorem” on its own, in ordinary parlance, just means there is some such valid proof.
Turning to examples, consider that when a mathematician says that “the number of tree structures on vertices is ” is a theorem, she just means that theorem has a proof, and quite possibly several which might be different in some way. Open up Proofs from THE BOOK (no, I’m not shouting, that’s the title as spelled), and you’ll find this theorem. In fact, you’ll find this theorem proved in a variety of ways. Even though the proofs are purportedly different (perhaps in some not too well defined sense), it’s the same theorem being discussed throughout. This is a commonplace occurrence: in a paper, one might cite Theorem X followed by a list of references to proofs, quite possibly proofs which are different in character; similarly, someone might state in a paper a theorem followed by proof 1 and proof 2. It is understood by all that it’s the same theorem. The proof is a separate entity – that’s why you see the word “Proof” at the beginning of the argument.
Turning to a more formal example, we might say, e.g., the formula
is a theorem of MILL, without specifying a particular proof. This particular type actually admits two terms which are distinct in a well-defined way (two global elements in a free closed symmetric monoidal category), or in other language, two proofs that are not Lambek-equivalent, etc.
I suppose I’ve made my point, or perhaps belabored it. I’m talking about ordinary language use here.
Mike, you seem to be worried that I am “confused”.
No, I think this was addressed at me. After all you three are agreeing with each other!
Urs, if that’s the case, then I guess I really was confused after all! :-D
Okay, let me review the discussion according to how I read it (that “read” should be read as past, not present tense). My comment in #2 was meant to point out a possible misunderstanding that might result from “proposition with a proof”. This “with” can be read two ways: “that has” and “together with”. I was saying “that has” is the traditional understanding.
I see your #3 as siding more with “together with” (I actually interpreted your “true” in “true proposition” as meaning provable or “inhabited”, but since “true” also has more than one meaning, I thought I’d bring up the model-theoretic meaning as well, mostly as an aside, in #6).
I saw Mike’s #4 as also taking this side: if “theorem” is synonymous with “definition”, and if the definition consists of two parts, namely the type of the term being defined (“the statement”) as well as the term (“the proof”), then it would follow that the theorem consists of those two parts as well. Thus, Mike would appear to be advocating “together with”: that a Theorem, at least as interpreted in Coq, is more than just being a provably true statement. (When Mike said he agrees with Toby, I took that as also saying that my objection to what Toby had written was misplaced.)
Although I’ve never worked with Coq, something in your #5 resonated with me, that “the syntax “Theorem” is not part of the type theory, but part of the Coq interface to allow you to talk about type theory with Coq”.
I’m not sure Mike’s #7 was helpful for me personally, because I certainly found nothing wrong with it, and yet my reading of earlier arguments led me to suspect he was in some way still arguing against my position. In that respect, maybe I actually was getting more, not less confused by comment #7! :-)
Comment #8 was an over-the-top desperate effort to explain my position more fully. As I said in #6, I found it very surprising that there was apparent disagreement over the meaning of the word “theorem”. (In fact my position is less rigid than might at first appear: I am happy to entertain the thought that in some contexts, the notion of theorem being a statement together with a proof of that statement is a more useful notion than “provable statement”. Meanwhile, however, I believe the traditional meaning is “provable statement”, and this ought to be reflected in whatever goes into the nLab.)
Thanks. I certainly appreciate all that is being said here. But I still feel that the current statement in the entry
A theorem is a proposition [admitting a] proof.
misses something. I may well be wrong. But let me try to explain myself further, so that you all have a better chance to explain to me why I am wrong, if so.
So what troubles me is that the above statement is equivalent to saying:
A theorem is an inhabited type.
Or equivalently
A theorem is a (-1)-connected type.
Is this really what we want the definition of theorem to be?
I think you have all argued so far that a theorem involves an inhabited type. But I think it is more.
We don’t go and call any random inhabited type a theorem. This is clear from practical use because we are the more fond of calling an inhabited type a theorem, the less it is obvious that it is inhabited.
Look at Todd’s example in #8. We have an equivalence of types
Both are inhabited. For the one on the right this is evident, for the one on the left it is less evident. It seems to me that the content of saying that the expression on the left is a theorem is that it presents a type in a form that is not evidently inhabited.
That’s why I am thinking that “theorem” is something about us talking about a type theory, not something in the type theory. In the type theory, the above equivalence holds and there is no intrinsic difference between and .
Instead, the nontriviality rests all in the fact, I think, that the long expression on the left is really a somewhat involved itertation of procedures for constructing types from other types. The content of the theorem is that this procedure yields an output that is equivalent to . If however we forget the procedure and just regard the output, then there is nothing non-trivial left.
Do you see what I mean?
Urs, what’s ?
In case it wasn’t clear, the formula I wrote in #8 is a type in the theory of symmetric monoidal closed categories, aka an object of a free symmetric monoidal closed category generated by a set , where and were taken to be variable types (or objects in the image of ), and is the monoidal unit. I don’t recognize the expression as belonging to that theory.
what’s {a,b}?
The two proofs of the theorem.
Then I’m sorry, I don’t understand. Is supposed to be a type in MILL? But maybe I should bow out of the conversation for the time being, and hear how other people react to what you’re saying – maybe they will understand better.
So the point I am trying to make is stronger when we strictly regard propositions as (-1)-truncated types.
In that case, saying
A theorem is a proposition admitting a proof.
is equivalent to saying
A theorem is an inhabited (-1)-truncated type.
which is equivalent to saying
A theorem is a (-2)-truncated type.
There is precisely one of these, up to equivalence. Called true, of course.
So this can hardly be the definition of the notion theorem. The point of a theorem is that you start with something that is not explicitlly the (-2)-truncated type, and the content of the theorem is to assert that nevertheless it is equivalent to it.
Todd,
our last messages overlapped, so here is my actual reaction to your #14:
I don’t know MILL. I was just picking up your example, following your statement that
This particular type actually admits two terms which are distinct in a well-defined way
Whew!
Todd, I think I was confused in #7. I wasn’t saying that I thought you (or Urs, or anyone in particular) was confused, rather that we were failing to communicate. But because the text that you quoted in #6 didn’t look to me as though it really had anything to do with the original question (whether a theorem comes equipped with a proof), I wasn’t specifically addressing that point but rather some other confusing things that I thought might be causing disagreement.
Now I see that you are actually still talking about the point you raised in #2, whereas Urs seems to me to be making a different point.
It seems to me that Urs’ point isn’t uniquely about type theory, but is even a point about classical logic. For instance, Fermat’s last theorem is true. Therefore, Fermat’s last theorem is logically equivalent to the statement “”. But clearly FLT is a more interesting theorem than “”. Thus, two things may be logically equivalent yet not be the same “theorem”. Whether or not this is a problem with the definition “a theorem is a proposition with a proof” just pushes the question off to the definition of “proposition” — the point is that a theorem consists of a syntactic statement, like , with (I’m deliberately not addressing Todd’s point at the moment) another syntactic object called a “proof”. When we pass to semantics, every logical statement gets assigned a “truth value”, whether that be a -truncated type, an element of a Boolean algebra, or what-have-you, and the soundness theorem implies that theorems will get assigned a “true” truth value. Usually, there is only one “true” truth value, up to equivalence, so all theorems get assigned the same truth value; but that does not mean all theorems are the same truth value, as a theorem itself is a syntactic object.
So maybe what I want to say is that my response to
A proposition is a certain type and it is true if it is inhabited / (-2)-truncated. But a theorem is an entirely different construct of the language alltogether.
Is that, actually, if by “proposition” we mean h-proposition, then yes, it is a certain type, but in type theory a type is also a syntactic object. The types and are equivalent, in the sense that we can construct a term inhabiting the type of equivalences between them (hence, by univalence, a term inhabiting the type of equalities between them) but they are different syntactic objects (and the proof that they are equivalent is just another syntactic object). So “theorems” can be identified with h-propositions that are demonstrably inhabited, without worry of conflating FLT with .
As for the question of whether a theorem comes equipped with a proof, this may be another place where the constructive mathematician diverges from the classical one, although I never thought about it quite in this way before. Frequently the constructive mathematician says “equipped with” where the classical mathematician says “such that there exists”. Not really being a true card-carrying constructive mathematician myself, though, I hesitate to make general statements about what they might say. I look forward to hearing Toby’s input.
Personally, I do speak in the classical way; in particular I would talk about “a new proof of the same theorem” indicating that I regard the theorem as unchanged even though we may give it a different proof. But if we work in a type theory where all logical statements are (-1)-truncated, then we can prove that any two proofs of the same logical statement are equal, so that up to equivalence “it doesn’t matter”. (Admittedly, there is a bit of level-mixing going on, which is perhaps why I got myself confused in the first place — since theorems are syntactic objects, it makes sense to treat proofs as syntactic objects too; the proof that two proofs are “equal” is thus again a syntactic object, and only when we start to think a bit semantically does it really mean that the proofs are “the same”.)
Is that, actually, if by “proposition” we mean h-proposition, then yes, it is a certain type, but in type theory a type is also a syntactic object. The types and are equivalent, in the sense that we can construct a term inhabiting the type of equivalences between them (hence, by univalence, a term inhabiting the type of equalities between them) but they are different syntactic objects […]. So “theorems” can be identified with h-propositions that are demonstrably inhabited, without worry of conflating FLT with .
Thanks, that helps!
Maybe we can make this more explicit in the entry. Can we say
A theorem is a syntactic object that corresponds to a proposition which has a proof.
?
Or something like this.
I thought what I just said was that propositions are also syntactic objects. Saying “a theorem is a syntactic objects that corresponds to a proposition” implies to me that a proposition is not a syntactic object.
I originally wrote ‘a proposition that has a proof’, then I changed the wording to ‘a proposition with a proof’ on the grounds that this was shorter, without intending to actually change the meaning. Then I realised that ‘a proposition with a proof’ could be interpreted either as meaning the same as ‘a proposition that has a proof’ or as meaning the same as ‘a proposition together with a proof’. I decided that this was an acceptable ambiguity. Apparently not!
I expanded the page a bit, along lines that I had intended before this discussion.
Thanks, Toby. I think the ambiguity is acceptable, as long as we go into details along the lines of the above discussion. So, for example, saying “This could mean one of two things…” followed by the traditional understanding (“that has”), as well as whatever contrasting view is spelt out.
Thanks Toby! But now we have more to disagree about. (-:
I feel that even in the ordinary “informal” language of mathematics, the word “theorem” means a statement that has a proof, not merely something that “we know to be true even though it’s not immediately clear why”.
I also feel that “axiom” in ordinary usage nowadays is closer to its meaning in formal logic than to the perhaps older meaning of “something obviously true”, especially now that many mathematicians are familiar with axioms like Choice which are of questionable “obviousness”.
I have this vision that we adopt some type theoretic context and then give a fully precise quasi-formal definition of “proposition”, “theorem”, “proof”, etc. (in addition to more informal discussion, of course), the way Mike had been indicating above. Based on discussion with Mike I have a rough idea of how it should go, I guess, but I won’t make an attempt to implement it. I am just thinking it would be fun to highlight this way how far a type theoretic foundation of mathematics goes.
Since we’re talking about the everyday meanings of “theorem” etc, maybe it’s worth remembering that the everyday meaning of “proposition” is “same as a theorem, but less important”.
but less important
or more often: easier to prove! :-)
Just recently I had occasion to give a seminar on material where a theorem of an earlier article had become just a special case of a proposition in a later article: the machinery had improved meanwhile…
Agreed, Tom! That could perhaps be mentioned at proposition.
@ Tom #25: Yes, that’s there in theorem. (One might add it to proposition as well.)
@ Mike #23: I think that most mathematicians are aware of the logicians’ sense of ‘theorem’, but they still write ‘Proposition’ and ‘Lemma’ in their papers and monographs, saving ‘Theorem’ for the big stuff. But we can add some nuance to the article, which I have tried to do.
@ Urs #24: I don’t think that we’re lacking a formal definition (as long as we’re not trying to capture the importance or non-obviousness). To specify a formal system, you must specify what a proposition is and what a proof of such is, and a theorem is a proposition with a proof.
Toby, I wasn’t talking about the differences in meaning between “theorem”, “lemma”, and “proposition” — which I agree with — but rather that to me, even informally, all of them imply that the statement is proven, rather than being something “we know to be true even though it’s not immediately clear why”.
I don’t see the conflict. If we know it to be true, then that’s because it’s proven (unless we’re Doron Zeilberger), although probably not with a formal proof. For a proposition or a corollary, it is immediately clear why, at least once you see the statement written out. A theorem, in contrast, requires some argument; that’s what I meant by that bit.
At the same time, I think we can all agree that the lines between “lemma”, “proposition”, “theorem”, etc. are pretty blurry in practice.
Rather than try further to explain my point here, I’ve edited the page. Feel free to object.
I don’t think that we’re lacking a formal definition
I didn’t say that we are lacking a formal definition. But the entry doesn’t state it.
Many logic/type theory related entries on the Lab look awkward to me, in that they consist of lots of prose with few hard facts. They don’t look like other math pages. It’s curious: the more an entry is concerned with foundations, the more informal it is. Currently. My impression is that this need not be so. But of course I can only try to encourage you all to change it.
I believe Henry Whitehead once criticised Adams (when the latter was a student) for apologising that a theorem (which was significant in its implications) had a simple proof.
@Urs #33: That makes sense to me. We take a very open-minded approach to foundations here, so pinning things down too much would make them (for some purposes) wrong. Besides that, at the foundations we meet with undefined terms, so we can’t give precise definitions, only axioms and motivation.
Consequently, I don’t expect any precise definition at either proposition or proof. In any given logic, we can precisely state what a proposition is and what a proof is, but a single definition would apply only to a single logic, so instead we discuss what they’re supposed to be like and how they behave.
Things are different at theorem, however, where we have a precise definition: a theorem is a proposition with a proof.
@Mike: From my perspective, you’ve just replaced the intuitive phrase “known to be true” with the jargon term “proved”. If you like that better, OK.
I guess I’m a little uncomfortable with just “known to be true”. A lot of mathematicians will say or think or be convinced that they “know” something even if they can’t prove it. (An example of this sort of thinking can be found in the discussion here.) Thus, for many thinkers of Platonic bent, the existence of inaccessible cardinals is accepted as a straight-up fact, every bit as much as the existence of the set of natural numbers for even more mathematicians. Or, they say they “know” ZFC is consistent, etc. (akin to the position that axioms are ’self-evident truths’ or known to be true).
The point being not the rightness or wrongness of such positions, but the fact that people hold them. This makes “known to be true” a bit problematic IMO.
While it’s technically true that “proof” is a “jargon term”, it is well-understood jargon in the community of mathematicians, which contains most of the audience of the nLab. (I think any physicist or philosopher who’s going to read the nLab needs to know enough mathematics that the word “proof” is not going to put them off.) Its advantage over “known to be true” is that in my view, it is a significantly more correct description of the use of the word “theorem” by mathematicians even in informal language.
at the foundations we meet with undefined terms, so we can’t give precise definitions,
That’s what I used to think and say, until you guys told me otherwise.
That’s what I used to think and say, until you guys told me otherwise.
Urs, I think you might be referring to a discussion we had here on “collection” and membership” being undefined notions.
We seemed to have reached an agreement on the point that the fact that some terms in foundations being left undefined was a non-issue; what counts is being able to successfully teach a person or program a computer how to correctly manipulate terms at the syntactic level (which, at the bottom line, is extra-linguistic, in the sense that electrons moving through logic gates is a concrete physical event, not part of an abstract language).
I sense that I am well getting on your all nerves. Sorry for that. But with that being so already, I can maybe just as well put it this way:
I don’t believe that Lab entries on foundations need to be what I would call as “wishy-washy” as the average, say, Encyclopedia Britanica article on the corresponding topic would be. I think they could be much better, much more precise, and much more useful.
What I can fully understand is nobody having the energy to write such entries. That is probably so, and so we can just leave it at that. That’s fine.
But I have a hard time accepting the argument that this is just the only way one can (or even should, as #35 suggests) talk about foundations.
The current version of the Wikipedia entry Formal proof starts out a bit more ambitiously. But it seems to me that the level of expertise and insight in principle available here in Lab circles could go way beyond this (if somebody had the time, I know, but in principle).
For instance an improvement over that Wikiepia article would be the kind of discussion one can see in
The author there sets out to give the reader a fairly exact idea of what a Theorem really is in modern formalized mathematics (around page 5). I have added a pointer to that reference now to theorem.
I am sure that if, by some magic, we could free an hour free of any other duties, Mike could easily write something comparable if not better for the case of Coq instead of HOL (which Hale looks at). To repeat: I know there is no such hour, but I don’t accept that it couldn’t be usefully done if there were one.
A text with similar aim and achievement is
A pointer to this I have now also added to Theorem.
And I am sure there is something to be gained from genuinely contentful entries on foundational issues, with actual precise statements. I see for instance that pretty much exactly one year ago our very David Roberts inquired here on MO about what it actually means to have a formal theorem in say, Coq. And he got some pretty good replies, with pretty hard facts in them. All that and more could well be in the Lab entry.
If you see what I mean. Maybe you don’t. If not, please don’t get angry at me. We can just leave it at that. It’s not so important. I just throught I’d try once more to express myself.
I am not annoyed. I am just busy, which tends to make me terse. (-:
I think I agree with your overall sentiment, Urs. In particular, the fact that
In any given logic, we can precisely state what a proposition is and what a proof is, but a single definition would apply only to a single logic, so instead we discuss what they’re supposed to be like and how they behave.
doesn’t mean we can’t have precise definitions, only that there is no one precise definition. But we can perfectly well have a list of precise definitions, one for each logic. If, in a particular logic, a given word is an undefined term, then we can state that, along with the rules that determine how that undefined term is used — that is, we may not be able to give a “definition” in the sense that that word is usually used in precise mathematics, but we can at least give a precise description of how a word is used.
Urs, I think that your references would go better at proof than at theorem. Do you agree with me that the definition at theorem is perfectly precise, that it’s proposition and proof that lack formal definitions?
Wikipedia’s definition of Formal proof is a good start. (Of course, there’s also Mathematical proof, which is not the same thing.) It assumes a certain structure of the formal system (what one might call a one-dimensional deductive system). It leaves the rules of inference undefined (as well as the well-formed formulas, that is the propositions).
Urs, I think that your references would go better at proof than at theorem.
Okay, sure, I have copied them over to proof. But let’s leave them at theorem, too, okay?
Do you agree with me that the definition at theorem is perfectly precise, that it’s proposition and proof that lack formal definitions?
Okay, allright. Agreed.
On the meaning of ‘proof’ in mathematics (rather than logic), see the definitions here (starting with ‘Solow’).
Urs, you’re not getting on my nerves at all.
I’m working on something a little bit related, which I’ll report on soon.
1 to 46 of 46