Talk:Theorem

Grothendieck's universes

The sentence "A notable exception is Wiles's proof of Fermat's Last Theorem, which involves the Grothendieck universes whose existence requires adding a new axiom to the set theory" is completely misleading and should be removed.

First of all, even without entering a technical discussion, it cannot be in the second paragraph of the page, giving the idea that this is an important point. FLT is proved in any reasonable mathematical sense, it is accepted by the mathematical community without any doubt.

Moreover, the sentence is almost entirely false, see for example all the discussions in https://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof. It's not true that "many specialists think that it is possible [to remove the use of Grothendieck's universes]". The reality is that all the specialists that care about this have checked and are sure Grothendieck's universes can be avoided here, and those who don't care simply don't care about logical foundations.

Removed by me as WP:OR

I removed the sentence "A notable exception is Wiles's proof of Fermat's Last Theorem, which involves the Grothendieck universes whose existence requires the addition of a new axiom to the set theory." as WP:OR. The author is free to revise to include reliable external references. Erxnmedia (talk) 12:52, 16 May 2023 (UTC)

I have edited the revert to reflect the current state of play: McLarty's old article was cited, but not a more recent article of his reproving the universe-dependent ingredients in a way that doesn't use universes. I agree that this shouldn't be in the second paragraph, because the situation is more subtle than a generic WP reader is prepared for. But keeping it in a discussion later about what a theorem really relies on might be ok. 110.174.47.229 (talk) 22:50, 16 May 2023 (UTC)

Fermat's Last Theorem is not special in this regard. Enormous amounts of modern number theory and algebraic geometry make use of Grothendieck universes on a superficial level. And everyone in the field agrees that any particular statement can also be established without universes by taking a bit more care. (Case in point: the Stacks Project is a 8000-page reference text on algebraic geometry, and it carefully avoids universes. But many other texts don't bother taking this care.) The entire discussion of ZFC vs ZFC+u should not be so high up on this page. It would make much more sense to have it in a later section. — Preceding unsigned comment added by 132.230.196.70 (talk) 05:49, 17 May 2023 (UTC)

How Tos

I would like to learn more on how to create my own basic theorems and proofs. Are there any good sites covering this subject?

How does

Could someone please provide a reference or statement of how a theorem, like Clausius' entropy theorem, evolves into a 'principle', and how a 'principle' evolves into a physical law, like entropy the second law of thermodynamics. Sholto Maud 09:20, 13 December 2005 (UTC)

You're confusing "theorem" with theory. -- llywrch 20:51, 13 December 2005 (UTC)

• Ok thanks. But could you then please clarify what the term "theorem" refers to on the maximum power theorem entry? I'd really appreciate it. Sholto Maud 22:23, 13 December 2005 (UTC)

Looking at the material on this page, the theory page & the Maximum power theorem, I would conclude the following:

• A theorem is a statement which we can prove is true by at least one argument based on other theorems & axioms. (ISTR Gauss once creating several proofs for one theorem, in a quest to find the simplest & most elegant proof for that statement -- so a theorem can have more than one proof.)
• A theory is a statement which we can't prove is true -- but we can prove is false -- based on experimentation, & to some degree on arguments based on other theories. For example, no one really knows if the Theory of Thermodynamics is true, but experiments designed to verify it have failed to shown it to be false so many times that many people have for convenience assumed it is true. (And a theory that has become so enshrined as true or correct often is renamed as a Law, e.g., the Law of Thermodynamics.)

Let's stop for a moment & review the differences here. In one case, we can prove a statement true; in another, we can only prove it false. These are not the same thing, unless we also assume that a statement can only be true or false: & experience shows us that statements are often partly true or partly false. Thus, no matter how many times we prove a theory is not false, we can never be 100% sure that it is true.

• The maximum power theorem. Here it gets a little confusing: theorems are usually associated with mathematics, & theories with science. However, in a science-related field (electrical engineering), we find a statement labelled as a theorem. Reading the article, I noticed that there is a section labelled "Proof of theorem for resistive circuits": because this statement's truth rests on an argument based on other theorems & axioms, we can conclude this statement is a theorem.

Now it may happen that someone encounters a case for which this theorem is not true. What would happen is that one would need to review the truth of all of the theorems & axioms this particular theorem depends on, & reformulate the statement that made this statement false. (This would be the same procedure a mathematician would need to follow -- although such an event would shatter the entire structure of this discipline, as it did with the discovery of non-Euclidean geometry. But I understand that as of this writing there are few such surprises remaining to be found.)

Does this help? -- llywrch 18:14, 14 December 2005 (UTC)

Thank you for your considered contribution lywrch. It does help a little. I like the distinction between theorem as provable as true, and theory as not so and only falsifiable. This interpretation seems to me to make a theorem a more powerful statement qua epistemic truth, than a theory. But as with life, this also beggs more questions.

• Firstly, the transition between theory and law does not seem adequate for the rigor demanded by most systems of science. For instance, there is no specification of how many times we need to fail to show a theory false in order for it to be renamed a law, and thus considered true, as a "pseudo theorem". "Failiing to show" seems to be a measurable phenomenon, but there is no specification of what measure will change the status of a theory.
• Secondly, what happens in transdiscipline known as "mathematical physics"? I mean if theorem → mathematics, and theory → science & physics, then is mathematical physics, "theorem theory"? Such that we have a statement or proposition that is both falsifiable and provable? When you say ""Proof of theorem for resistive circuits": because this statement's truth rests on an argument based on other theorems & axioms, we can conclude this statement is a theorem." is it not also the case that the statement's truth rests on the actual measurable properties of the electromagnetic system, and so it is both a theory and theorem?
• Thirdly, if a theorem-theory can evolve into the status of a theorem-principle, and then theorem-law, by a process of repeated observations, then this suggests that we may be able to generate new laws, of thermodynamics for instance, over time. But when at what critical point does the theory become law?

Sholto Maud 21:48, 14 December 2005 (UTC)

Sholto, you're now asking questions that a philosopher of science would be better prepared to answer. I'm just a guy who adds articles to Wikipedia, & while I'm willing to share my opinions, I doubt that they may be as insightful as someone who has studied these issues would be; your thoughts are likely just as valid as my own. But I'll offer a few points for you to ponder further:

• The scientific disciplines extend in a continuum from the "hard" sciences (which are most like mathematics like physics or astronomy) to the "soft" sciences (like sociology or anthropology). Those at the one end best lend themselves to a rigorous approach like mathematics, & offer some basis for arguing the truth of theorems; those at the other at best offer theories, which sometimes do not lend themselves to being proven false. So none of the sciences are really as rigorous as we might think.
• The difference between "theory" & "law" is a fitting philosophical problem -- & I also suspect that a certain amount of subjectivity enters into promoting a theory to a law. In other words, I don't have a concise, clear answer for determining the difference -- but an academic who specializes in the philosophy of science might.
• I don't think that the statements described by "theory" & "theorem" are disjunctive groups: a statement that is true is also not false. If both approaches point to a statement being correct, then how would they conflict?
• Lastly, theorems depend on axioms, which by definition are assumed to be true; as I suggested above, experience may show that an axiom is indeed false. (This was the case with Euclid's famous axiom about parallel lines: doubt about this axiom led to the discovery of non-Euclidean geometries, thus demonstrating the underlying natures of logical proof & geometry.) Despite the certainty that logical reasoning gives us, we don't know if our conclusions are true until we encounter something that clearly proves that they are not.

I sincerely believe you are struggling with a worthy problem. However, I don't think I can provide you the help you need to be successful with this search. -- llywrch 04:42, 15 December 2005 (UTC)

Comments

While this article is useful as an introduction or definition of this term, it would improve this article if it answered questions like:

• What is the relationship of theorems in mathematics? Are they similar to experiments in the empirical sciences?
• How are the theorems of Euclid's Elements different from today's more rigorous theorems?
• What form did theorems have before Euclid?
• Do the concepts "theory" & "theorem" have more in common than a similar name?

This article could cover a lot more points. -- llywrch 20:51, 13 December 2005 (UTC)

• Seconded. Sholto Maud 19:16, 11 February 2006 (UTC)

References

This page needs references. Some parts seem correct, but others are illogical (incorrect typological order, among other grammatical issues). I've made a few corrections. Fuzzform 00:16, 31 March 2006 (UTC)

Badly placed text

This text should be in an article called "Mathematical Terminology". There's no structural reason to put all these definitions together in the same article called "Theorem".

And there are some fundamental errors in the definitions, we need to find external sources. But I think that first this name problem should be corrected.

And just one more thing: there is NO difference between mathematical algorithms and the ones in Computer Science! Arthur Gabriel de Santana a.k.a. Rox 11:38, 28 December 2006 (UTC)

What have mathematical algorithms got to do with theorems? Sholto Maud 21:54, 1 March 2007 (UTC)

I think the point is that the Division algorithm is really a theorem, despite it's name. But it's certainly rather unclear at the moment. Algebraist 02:03, 4 March 2007 (UTC)

Well, an algorithm is a procedure, and a theorem is a (provable) assertion -- orthogonal concepts, except that we often prove theorems about algorithms. For instance, the theorem often referred to as "division algorithm" is actually a theorem about the division algorithm, asserting that it always terminates in finite time, that its outputs (the quotient and remainder) have certain properties, and that its outputs are the only integers having these properties. Calling this theorem "division algorithm" rather than "theorem on the division algorithm" is just normal human sloppiness sanctioned by long usage.Hippasus the Younger 04:12, 17 April 2007 (UTC)

Well, I edited it some. What would be really helpful would be a guide to mathematical writing that we could cite for some of this stuff. CMummert · talk 04:29, 4 March 2007 (UTC)

Definition of 'hypothesis"

This article (Theorem) says "In this case A is called the Hypothesis" but hypothesis in wiki has a definition that does not seem to accord with this usage of the term "hypothesis". So there needs to be some good disambiguation.Nznancy 22:17, 9 January 2007 (UTC) nznancy, 10 Jan 2007

Corollary

In the Terminology section, Corollary links back to Theorem. What IS this, some sort of a Moebius article? Lou Sander 01:18, 22 January 2007 (UTC)

I noticed the same thing just now, why doesn't corollary have its own article, if proposition and lemma do? -Dmz5*Edits**Talk* 03:39, 22 January 2007 (UTC) (i keep getting signed out)

It once had its own very short article, but somebody merged it. You can see the old stuff by clicking the link in the "redirected from" line of the Theorem article when you get to it through Corollary. Once you are there, look at History.

I just checked out Proposition and Lemma. The Lemma article definitely pertains to math. The Proposition article pertains mostly to philosophy and logic, though Proposition (disambiguation) mentions its mathematical meaning. Somebody needs to write articles on Corollary and on Proposition (mathematics). I don't have enough subject matter knowledge to do it myself. Lou Sander 05:17, 22 January 2007 (UTC)

It seems to me that the article Lemma (mathematics) is just a definition; I would rather see all these definitions gathered into one article where they can be properly compared and contrasted rather than in separate articles. And WP:NOT#DICT says that articles should not be created just to give definitions. CMummert · talk 13:19, 22 January 2007 (UTC)

That seems like a good idea to me. Proposition merits the same treatment, as do maybe some others. Lou Sander 18:23, 22 January 2007 (UTC)

I would also like to see all definitions gathered into an article, with discussion of how they are related and why they are useful with examples. Sholto Maud 21:56, 1 March 2007 (UTC)

I just noticed the same thing when trying to search for Corollary. I think it should have its own article, I'll bring it up with the people at the Mathematics wikiproject.--Jersey Devil 00:24, 29 March 2007 (UTC)

This article is perpetually under-referenced; I don't see how we are going to find enough references to make TWO articles that are more than just dictdefs. CMummert · talk 00:39, 29 March 2007 (UTC)

classification of finite simple groups

Imagine my surprise, after reading in the lede about how a proof should not be confused with the theorem it proves, that the section on trivia explains that the classification of finite simple groups is the "longest theorem"! The theorem actually is not so long; even if you went into some details about the groups it would still be not so long. I suppose if you started explaining about all the sporadic groups like the Monster, it would start getting longer but that's true of any complex theorem. --C S (Talk) 00:38, 22 April 2007 (UTC)

Lead too long and other problems

This article is still a mess, despite being WP:MATHCOTW. There seems to be a lack of boldness in improving the article, which really needs a lot of reorganisation. I would like to help, but cannot do it tonight, so please bug me on my talk page if I forget. Geometry guy 21:51, 28 April 2007 (UTC)

I've now written a new lead and moved some of the previous lead material into sections. These sections still need reorganisation and expansion, but it would be more fun to do it in collaboration. Anyone? ;) Geometry guy 14:39, 5 May 2007 (UTC)

Well, okay, the weekend is not the best time to find collaborators. Anyway, I've added a few pictures and controversial points, which I hope begin to answer Salix alba's question: "Is there anything more which could be said which is not covered by proof?" Geometry guy 19:59, 5 May 2007 (UTC)

Excellent edits! One thing -- there are in fact many more particles in the observable universe than 1.59*10^40 (see googol, for instance), so I removed that claim from the article. Kier07 16:52, 6 May 2007 (UTC)

Thanks for the ref, but the Mertens bound involves the exponential of 1.59*10^40, which is vastly larger, cf. googolplex! Geometry guy 19:17, 6 May 2007 (UTC)

Woops -- sorry about that! Kier07 00:00, 7 May 2007 (UTC)

By the way, what does it mean in the lead: it can be shown (indeed proven) that there are mathematical statements which are true but not formally provable? I know about statements such as the continuum hypothesis which are not disprovable (and hence could be called "true"), but which are also not provable. Is this what we're referring to, or is it something else? We should say somewhere in the article what we mean by this. It was my understanding that the only "truth" a theorem has is that it follows from axioms and other theorems. Kier07 17:54, 6 May 2007 (UTC)

This is a vague reference to Godel's first incompleteness theorem, which should be discussed in the body of the article, but is not at present. It states that in any axiomatic system strong enough to contain arithmetic, there are true statements which are not provable within the system. I'm glad you pointed this out! Geometry guy 19:17, 6 May 2007 (UTC)

It is certainly the case that one can talk about mathematical statements being true, even if they are not provable. Usually, if a mathematician, and indeed probably you or anybody else, were to say that the statement "every even number greater than two is the sum of two primes" were true, s/he would mean that every even number greater than two is the sum of two primes. To pick the classical example, "snow is white" is true if and only if snow is white. Note all this makes perfect sense. It is not a mathematical statement's fault, however, if it is in fact not a theorem, i.e. provable within your formal system. --C S (Talk) 19:51, 6 May 2007 (UTC)

The lead is looking great. I'm still confused by the statement that "The concept of a theorem is therefore fundamentally deductive, in contrast to the notion of a scientific theory, which is empirical." I'd like to raise the maximum power theorem again (see above). This "theorem" is related to "empirical phenomenon" of electronic circuits - even though the theorem is provable, it's truth is dependent on empirical observation and verification. Hence theorem does not seem to be fundamentally deductive... Sholto Maud 01:31, 7 May 2007 (UTC)

Thanks. I have had a look at maximum power theorem and clarified it in a couple of places. From a mathematical point of view, there seem to be two theorems here, but one is a generalization of the other. To state the theorem as a mathematical theorem, one simply needs to add the hypothesis "For an electrical circuit satisfying Ohm's law and Joule's law". However, in physics and engineering, it is common to omit such hypotheses, since everyone knows (empirically) that electrical circuits satisfy Ohm's law and Joule's law under reasonable physical assumptions.

The mathematical formulation of the theorem is purely deductive, independent of any empirical observation and verification (as the proof shows). It proves, for example, that the empirically observed "maximum power principle" (that you maximize power when the load resistance equals the internal resistence) is a logical consequence of the empirical observations of Ohm and Joule.

I just want to break this down a little - "..the empirically observed X is a logical consequence of the empirical observations made by Y." Is this saying that an emprical observation is a logical consequence of an empirical observation? Sholto Maud 13:21, 7 May 2007 (UTC)

Yes, although your wording is open to misinterpretation, so let me give a precise example. Suppose you vary the voltage in a resistive electrical circuit and measure the current and power output. From your measurements you make the following empirical observations.

1. The current is proportional to the voltage.
2. The power output is proportional to the product of the current and the voltage.
3. The power output is proportional to the square of the voltage.

Then, for example, the third of these empirical observations is a logical consequence of the first two. Geometry guy 13:56, 7 May 2007 (UTC)

But I would apply the same method with Pythag theorem - from length measurements make empirical observations - so then what is the difference between mathematical and physical theorems? Sholto Maud 21:55, 7 May 2007 (UTC)

In principle there should be no difference! This is exactly the point I made below. Geometry guy 22:05, 7 May 2007 (UTC)

Hence if you find a circuit for which the maximum power theorem does not hold, you can conclude either that Ohm's law, or Joule's law (or both) is not valid for the given circuit.

All that has happened here is a blurring of the distinction between a principle and the theorem which may be used to derive it from other principles. This is no different in spirit from the blurring of the distinction between the division algorithm and the theorem which proves that it works. Geometry guy 12:21, 7 May 2007 (UTC)

Copyediting and physical theorems

I did some minor copyediting this evening. The only controversial point is whether theorems "should" be expressed as symbolic statements, and are not for convenience, or whether there is no need to worry about formalization. Different people take different positions, so I toned down the lede to take less of a stand about this. Also there was some confusion about Godel's theorem. CMummert · talk 02:56, 7 May 2007 (UTC)

Re: copyediting. "Mathematical theorems, on the other hand, are purely abstract formal statements: the proof of a theorem cannot involve experiments or other empirical evidence in the way that such evidence is used to support scientific theories."

At issue is the separation of theorem (purely abstract) from theory (empirical/concrete reality). It seems to be the case that the maximum power theorem is a statement that cannot be shown to be true by mathematical proof only, but that the truth of the statement requires empirical evidence.

a) are there theorems of mathematical-physics that are not purely abstract?

b) does empirical evidence (e.g. of electronic circuits) influence the truth value of a proof?

If it is the case that maximum power in electronic circuits is the domain of empirical inquiry & hence theory, does maximum power theory generate the maximum power theorem and associated hypotheses?Sholto Maud 04:12, 7 May 2007 (UTC)

When I went through, I added the adjective "mathematical" several times, and changed the lede to start with "in mathematics," to make it clear that this article is currently about mathematical theorems only, not theorems in physics and engineering. The proof given in the maximum power theorem article does appear to be rigorous, however. I am not quite sure what you re asking. CMummert · talk 11:48, 7 May 2007 (UTC)

I think it is appropriate that this article should be primarily, but not exclusively, about the mathematical notion of a theorem. However, more could certainly be said about the use of the term theorem in physics and engineering. I already introduced a sentence at the end of the section on "Relation with theories" and would encourage other editors, such as Sholto Maud, to expand it. From my point of view, many physical theorems are closely related to mathematical ones, except that certain physical assumptions are not explicitly mentioned. I have explained this for maximum power theorem above, but it can also be seen at equipartition theorem: despite having worked extensively on the latter article, I still do not know what the hypotheses of this theorem are! The lack of explicit hypotheses makes physical theorems more flexible than mathematical ones: for instance one says that "the equipartition theorem applies to the canonical ensemble and to the microcanonical ensemble, but it does not apply when quantum effects are significant". From a mathematical point of view, this language sounds odd, because mathematical theorems always apply. More could be said about this in the present article. Geometry guy 12:38, 7 May 2007 (UTC)

Perhaps the article should acknowledge the ambiguity at the outset. E.g., "In mathematics, a theorem is a statement that can be shown to be true by a mathematical proof on the basis of explicitly stated or previously agreed assumptions. ... In physics, a theorem is ... In mathematical physics a theorem is understood to be..." If there are three different interpretations there should be an argument for why any one should have priority over the others. Sholto Maud 13:11, 7 May 2007 (UTC)

I think that goes too far. I have already explained how the use of the word "theorem" in the physical sciences is closely related to (and indeed derives from) the mathematical notion. It is not a different idea; it is simply that different standards of preciseness and rigour are applied in different areas (this is true even within mathematics). When you claim that a physical theorem can state an empirical truth, I think you are confusing the conclusions of the theorem with the theorem itself, and I have demonstrated that the maximum power theorem is deductive. In any case, the lead of an article should reflect its content, so this discussion needs to be more fully developed in the body of the article. Geometry guy 14:12, 7 May 2007 (UTC)

Yes I think the max pow theorem is deductive as you say, but I haven't seen the suggested derivation of the physical science theorem from mathematical theorem. I'm also a little unclear on the role of hypotheses: When one predicts that a conclusion is emprically observable as a logical consequence of prior empirical observations (are these the premises?) is this predicted conclusion called the hypothesis (which would seem to be the same meaning as employed in science)? Sholto Maud 21:55, 7 May 2007 (UTC)

Outside of mathematics hypothesis has too many meanings. A better word is premise. The prior emperical observations in the mathematically-phrased maximum power theorem are only premises in the sense that they are assumed to hold, not in the sense that they have been observed experimentally. The mathematically-phrased maximum power theorem would be true even if Ohm's law were never true. Geometry guy 22:15, 7 May 2007 (UTC)

Ok. I think I'm following. So, most theorems have two components, called the premises and the conclusions. In principle, there is no difference between physical and mathematical theorems. However in practice there is a difference, and this difference depends on how the theorem is "phrased". A theorem may be phrased in many different ways, it can be mathematically-phrased, physically-phrased, biologically-phrased, financially-phrased etc. As Geometry guy stated above, a mathematically-phrased maximum power theorem would be true even if Ohm's law were never true. This means that there is no truth test required for the assumptions made in the premises (which makes it close to a mathematical-logic-phrasing). However a physically-phrased maximum power theorem can only be true when Ohm's law is also true - a truth test is required for the premises. And these are the different standards of preciseness and rigour that are applied. Have I understood? Sholto Maud 02:15, 8 May 2007 (UTC)

Partly, but I still think you are over-egging the pudding. Probably I took the discussion in the wrong direction with "mathematically-phrased". The only real difference between different fields is which assumptions are explicitly stated. In practice, in any domain of mathematics or physics or whatever, the premise of a theorem will include implicit assumptions which are not written down in the statement. These take various forms.

• Logical foundations. See Carroll's paradox for the difficulties which arise when you try to make assumptions about the nature of logical argument explicit! This is not a trivial point: proof by contradiction uses the law of the excluded middle; this is seldom mentioned in the premise, despite the fact that it can be useful to work without this law. In contrast, the axiom of choice is quite often mentioned when it is used, but again this depends on the context. More generally...
• Axioms e.g., any natural number n has a successor n+1. When talking about foundations, such axioms are mentioned explicitly, but usually they are just implicitly assumed. Alternatively they can be viewed as...
• Definitions. In the premise "Let G be a group" there is an implicit assumption that a group is a set with certain operations and properties. Whether such definitions are given depends on the context. Even the intended meaning varies from context to context, e.g. a ring sometimes has a multiplicative identity, sometimes not.

Thus even within mathematics the use of implicit assumptions varies depending on the context. So if you start talking about "mathematically-phrased" theorems, you might as well also say "set-theoretically phrased", "number-theoretically phrased", "geometrically-phrased", and so on.

Physics and engineering are no different. For instance the implicit assumption that Ohm's law holds is not a "truth test": it is part of the definition of a "resistive electrical circuit" in this context! The only difference between the two formulations is which assumptions are implicit, and which are explicit. This is not fundamental to the nature of a theorem, just a context-dependent convenience. Geometry guy 15:12, 8 May 2007 (UTC)

I appreciate your efforts, but perhaps we're talking about a different pudding. I think I'm questioning whether the conclusions of the maximum power theorem are true or not, since this will affect the truth of the assumptions - agreed that the implicit assumption that Ohm's law holds is not a "truth test". But the truth of the assumption can be tested against a real circuit (in fact many mathematicians refuted Ohm's reasoning and it was, apparently, empirical repeatable reality that gave support to Jacobi's law). We know that the theorem is proven, but the truth seems stronger than the proof in this instance. Truth makes a phenomenological claim about the measureable properties of any specific electronic circuit. I can only confirm the truth value of the theorem if I make an empirical electronic circuit and measure kW with different load resistance. If this is right then the truth of some theorems seems to be linked to empirical content and the strict separation between theorem and scientific theory is brought into question: if the electronic circuit does not give the predicted results, then the theorem, while proven, is not true and falsifiable. Sholto Maud 21:44, 8 May 2007 (UTC)

Questioning whether the conclusions of a theorem are true or not is different than saying a theorem is not true. The theorem "if 0 = 1, then every prime number is composite" is clearly true. You can question the conclusion all you want, and indeed the conclusion is false. But the theorem isn't. The maximum power theorem is true, regardless of whether a person finds the conclusion objectionable or not. Just because a theorem isn't phrased in an "if then" format doesn't mean there aren't implicit assumptions that fit into the "if" portion. --C S (Talk) 22:04, 8 May 2007 (UTC)

Okay, I think I understand what you're saying, although I misunderstood before (my earlier response is left above since Geometry guy commented on it). But I think what you are talking about isn't too relevant to the main thrust of the article, but may be very nice in a small section on applicability of mathematics to science. As a mathematical theorem, the maximum power theorem is true; however, you are right that in order for it to be useful it should agree with and predict real world results. I think the confusion here is that when we talk about truth we are really talking about mathematical truth. In science, there really is no equivalent. Even when you say the theorem would be true if you tested it and found it agreed with the results, I don't believe it's actually correct to say it's true. It just hasn't been falsified. A scientific theory isn't "true", it's either "useful" or not, falsified within a certain domain or not. Newton's theory isn't true or false. It's useful in certain contexts, less useful or completely falsified in others. --C S (Talk) 22:17, 8 May 2007 (UTC)

Chan-Ho Suh pre-empted my response in fine form, but here it is anyway (you/your = Sholto Maud, not Chan-Ho Suh)...

That is a completely independent (though quite reasonable) question. Whether the conclusions of a theorem are true has no logical implication for the validity of the premise. For example, "If 0 = 1 then 1 = 1" is a theorem, but the fact that the conclusion is true does not imply that the premise is! Nevertheless, in practice, conclusions are used to provide evidence for hypotheses. For instance the Riemann hypothesis has many plausible consequences, and these support (but do not prove) the idea that it may be true. Similarly, the empirical observation of the maximum power principle provides evidence for Ohm's law. Such reasoning, however, has nothing to do with the notion of a theorem. You don't confirm the truth value of a theorem by making a measurement, you do it by giving a proof! You have understood nothing if you do not understand this! In particular, your last sentence is pure nonsense (sorry to be so blunt!). Geometry guy 22:10, 8 May 2007 (UTC)

Thankyou Chan-Ho Suh, and Geometry guy. I agree that the last sentence reads poorly - I have no excuse - and agree that a conclusion being true does not imply that the premise is. Despite both efforts I feel there is a small bit missing that needs to be locked down.

1. Useful: Chan-Ho Suh introduced the concept of 'usefulness' - this needs definition. It assumes a distinction between useful and non-useful theorems, but this has not been previously discussed. Is the proposition that a useful theorem should both agree with and predict real world results, and a non-useful theorem should not agree with or predict real world results?

2. Mathematical truth: again introduced by Chan-Ho Suh. I think this is used by Geometry guy in the statement, "You don't confirm the truth value of a theorem by making a measurement..." - a mathematically true theorem is one that is proven, if it is not proven it is not mathematically true. Note that Geometry guy says we may empirically observe the maximum power principle, but Geometry guy does not use the term maximum power theorem (Wikipedia has 2 different entries for these terms). Is the proposition that one cannot empirically observe a theorem?

3. So it seems that a useful theorem which agrees with and predicts real world results should be empirically observable. But this is outlawed in 2, hence no theorem is useful (or perhaps this should read no theorem is empirically useful as opposed to mathematically useful) Sholto Maud 01:44, 9 May 2007 (UTC)

This is pure nonsense again. There is no need at all to define "useful" or categorize theorems by "usefulness", and the rest of the logic is fallacious. The answer to your two questions are "no" and "no", and your conclusion is false.

• The maximum power theorem is empirically observable in the sense that one can observe empirically that circuits which satisfy Ohm's law and Joule's law satisfy the conclusions of the maximum power theorem (which is what I meant by the maximum power principle: please reread my comment in the previous section instead of confusing the issue by linking to its philosophical meaning). Such empirical observations do not prove the theorem, however.
• The maximum power theorem is useful because it tells you that you don't actually need to check empirically whether a circuit satisfies the conclusions, as long as you know it obeys Ohm's law and Joule's law. The contrapositive could be useful as well, as I have already remarked.

Geometry guy 11:01, 9 May 2007 (UTC)

Actually I'm not the one that introduced usefulness into this discussion, Sholto Maud...you are! You were confusing what everyone else would call usefulness with "truth", so I merely pointed it out.

"As a mathematical theorem, the maximum power theorem is true; however, you are right that in order for it to be useful it should agree with and predict real world results." Could you explain how you are using useful in this sentence Sholto Maud 22:17, 9 May 2007 (UTC)

But as I explained, whether a theorem is useful, applicable, or whatnot, in the real world, is not very relevant to whether a theorem is true. I think the prime source of confusion here is that you don't realize that scientific theories are not true or false.

No, no. I'm comfortable with this notion. Sholto Maud 22:17, 9 May 2007 (UTC)

They are useful or not in certain domains. Scientific theories are also stated in a manner called "falsifiable", but that doesn't have to do with "truth value". --C S (Talk) 17:24, 9 May 2007 (UTC)

It's probably overkill, but I just can't resist! Here's one of my favorite quotations from Albert Einstein, as quoted by Ludwig von Mises in Human Action.

How can mathematics, a product of human reason that does not depend on any experience, so exquisitely fit the objects of reality? Is human reason able to discover, unaided by experience, through pure reasoning, the features of real things? ... As far as the theorems of mathematics refer to reality they are not certain, and as far as they are certain, they do not refer to reality.

So if Einstein couldn't figure out why some "theorems" fit the world of our experience so neatly, how can we possibly hope to do so?  ;^> DavidCBryant 17:02, 15 May 2007 (UTC)

Pure nonsense (continuation)

Please excuse my reasoning and thankyou both for your persistence. I act from good intention, but I'm confused again.

• From the article: "Mathematical theorems ... are purely abstract formal statements"
• From the article: "...the proof of a theorem cannot involve experiments or other empirical evidence in the way that such evidence is used to support scientific theories."
• Geometry guy: "You don't confirm the truth value of a theorem by making a measurement, you do it by giving a proof!"

I think I'm ok with this much: proving a theorem makes it true. But I have an impedance mismatch with the above and the below...

• Geometry guy: "The maximum power theorem is empirically observable in the sense that one can observe empirically that circuits which satisfy Ohm's law".

Please quote/reread the full sentence and note the use of the words "in the sense that". It is not empirically observable in the sense that its truth follows from empirical observation. My statement was quite clear: you are just confusing the issue by using the slipperiness of language to tie yourself up in knots. Geometry guy 12:25, 9 May 2007 (UTC)

Full sentence reads: "The maximum power theorem is empirically observable in the sense that one can observe empirically that circuits which satisfy Ohm's law and Joule's law satisfy the conclusions of the maximum power theorem (which is what I meant by the maximum power principle: please reread my comment in the previous section instead of confusing the issue by linking to its philosophical meaning)." - sorry I'm a little confused by the distinction between maximum power principle_Wikipedia and maximum power principle_{Geometry guy} and maximum power theorem_Wikipedia, so I left out the parenthesis. As for "...and Joule's law satisfy the conclusions of the maximum power theorem..." I didn't see the second meaning of "observe empirically" I think you may be referring to. hmmmm.... Sholto Maud 12:56, 9 May 2007 (UTC)

Perhaps I shouldn't have shifted the meaning, but this situation is no different from observing that two oranges and three oranges together give five oranges. This observation illustrates the theorem that 2+3=5 but does not establish its truth. Geometry guy 13:23, 9 May 2007 (UTC)

If a theorem is empirically observable then can't it be faslified? For example:

• Chan-Ho Suh: "Even when you say the theorem would be true if you tested it and found it agreed with the results, I don't believe it's actually correct to say it's true. It just hasn't been falsified."

If a theorem can be falsified then this would seem to imply that an empirical observation has the capacity to adjust the truth value of the theorem, regardless of the proof. But this result doesn't seem to agree with the article. Sholto Maud 12:07, 9 May 2007 (UTC)

This disagreement arises simply because you have misquoted me and interpreted "empirically observable" in two subtly different ways. The beauty of having a proof is that if someone happens to observe one day a circuit which satisfies Ohm's law and Joule's law but not the conclusions of the maximum power theorem, then this does not falsify the theorem — instead it shows that something went wrong during the experiment! Geometry guy 12:25, 9 May 2007 (UTC)

So would you say then that theorems can't actually be falsified? Sholto Maud 12:45, 9 May 2007 (UTC)

Yes. However, people are fallible, and so a mathematical statement and argument which claims to be a theorem and its proof might not be. The claim to theoremhood can be denied either by finding an error in the proof (so the statement is unproven) or by finding a counterexample (which shows that the statement is false). The latter process is similar to the scientific notion of falsifiability, but using the term here only generates confusion. In particular, a statement for which there is a counterexample is not a theorem. Geometry guy 13:23, 9 May 2007 (UTC)

Chan-Ho Suh were you implying that theorems can be falsified with the sentence ""Even when you say the theorem would be true if you tested it and found it agreed with the results, I don't believe it's actually correct to say it's true. It just hasn't been falsified."  ? Sholto Maud 22:20, 9 May 2007 (UTC)

• I was thinking about this last night, and perhaps my confusion is a result of the term "maximum power theorem", and that it should rather be "maximal theorem_power", so that we know that the theorem does not have to be specifically about kiloWatts. Rather the maximal theorem is generic and could be applied anywhere, and electrical engineers have just applied it to electric circuits. Would that explain it? Sholto Maud 23:36, 9 May 2007 (UTC)

Circuit theorem

I noticed that the maximum power theorem has recently been reclassified as "circuit theorem" - but there is no Wikipedia entry for circuit theorem, and theorem doesn't state the criteria for mathematical theorem, circuit theorem etc. Sholto Maud 04:47, 12 May 2007 (UTC)

"I think the definition of a mathematical theorem ("a theorem is a statement that can be shown to be true by a mathematical proof on the basis of explicitly stated or previously agreed assumptions") works equally well for circuit and physics theorems. There could very well be a difference, but I can't think of one, sorry. Roger 02:46, 11 May 2007 (UTC)"

This has been done to death already, but since I like to beat a dead horse I'll try to clarify two or three things for Sholto Maud.

When physicists speak of theorems they're not using the word the same way mathematicians do. Natural languages are inherently ambiguous. The word "theorem" has two different meanings (for mathematicians, and for physicists).

When mathematicians speak of "assumptions" and "axioms" they are speaking of purely logical propositions that do not have any necessary connection to the "real world". The ideas of mathematics, including its theorems, exist only in our minds.

Physical laws would (in the view of most physicists) exist whether there were human beings to observe them, or not. So the "assumptions" the physicists make are not the same as mathematical axioms, because the physicist is making an assumption about a world that exists outside of his mind.

The logical thought processes that connect a physical theorem with the physicist's assumptions are indeed the same as the deductive logic of mathematics. The difference is in the nature of the assumptions. If the physicist discovers that his assumptions were incorrect, he'll have to start all over again, because there is only one "real world" to which his theories can apply. The mathematician doesn't care about that – rather than proclaim an axiom "wrong", he'll just invent a new branch of mathematics by choosing a new set of assumptions. For example, the discovery of non-Euclidean geometries did not invalidate Euclidean geometry; it merely broadened the field of geometry.

If none of this seems very helpful, try chewing on the article about David Hume and then the one about the problem of incomplete induction. DavidCBryant 16:13, 14 May 2007 (UTC)

Maybe the article should start with, "The word "theorem" has two different distinct meanings, a mathematic meaning, and a physical meaning. When physicists speak of theorems they're not using the word the same way mathematicians do. The difference appears to be that mathematical theorems are not applied to the real world, whereas physical assumptions are applied. In mathematics, assumptions exist only in our minds. In contrast when a the physicist discovers that their assumptions are incorrect, they have to start their system (see Mind-Body_Dualism)." is this right? Sholto Maud 21:40, 14 May 2007 (UTC)

I'm not sure such a distinction belongs in the article. This article is about mathematics, and it says so in the very first sentence.

I'm not convinced. In strict terms the article is about the word 'theorem', and the very first sentance implies ambiguity, or at least the need for greater clarification. The qualification "In mathematics..." says that one might also have started the article, "In physics...". Sholto Maud 05:22, 16 May 2007 (UTC)

Depending on one's philosophical point of view, the difference between "arbitrary axioms" and "axioms that agree with the real world" is not necessarily as great as I've tried to paint it. See, for instance, Birkhoff's theorem. That theorem can be understood as a purely mathematical statement about the solutions to Maxwell's equations. It's only when one starts to think of electromagnetic fields as actually existing in the real world that the more subtle point about the nature of one's assumptions becomes significant and Birkhoff's theorem becomes a physical (and not merely mathematical) theorem. DavidCBryant 10:30, 15 May 2007 (UTC)

Circuit theorem just means "theorem in the theory of circuits". The same is true, modulo variations of grammar, for pretty much any X in the phrase X theorem. These derived concepts do not need to be defined and the criteria are obvious (e.g., "the theorem is about electrical circuits").

The concept of a theorem is fundamentally mathematical, and other uses of the term are variations on the same basic theme. Geometry guy 12:18, 25 May 2007 (UTC)

Substantive concerns

I think the article is fairly good, stylistically speaking. Here are a few more substantive concerns I have.

• In the section Formal and informal notions, the form of proof involving logical equivalency (if and only if theorems) isn't mentioned. Such theorems are very common, and probably ought to be discussed.
• The same section might also benefit by mentioning the difference between existence theorems and constructive theorems. I guess the discussion of Merten's conjecture in the next section hints at this (existence of a counterexample, without actually producing it), but the distinction ought perhaps to be more explicitly drawn. I guess we don't want to drag in a lot of stuff about Brouwer, but it might be good to mention him.
• I know that this article is about theorems, and not proofs, but the two concepts are pretty closely connected. One or two more examples of theorems might be worked into the discussion somehow, to illustrate subtle differences between different methods of proof, or how the same theorem might be stated (and proved) in two slightly different ways. My favorite example along these lines is Euclid's proof that there are an infinity of prime numbers, versus Euler's demonstration that the sum of the reciprocals of the primes diverges. Another good example is the demonstration that √2 is irrational, either by contradiction, or by actually constructing the sequences of Pell numbers that approach the limit from above and from below.
• In the section Terminology many of the distinctions drawn are fairly fuzzy, and the wiki-links aren't as helpful as they might be. I tried to rectify some of that by avoiding links through dab pages, but more work is needed. One thing that occurs to me is that certain phrases (e.g. "Law of Large Numbers") have assumed a precise meaning in mathematics, so they serve as a sort of shorthand for mathematicians. Can that idea be used to help explain the distinctions between identities, rules, principles, and laws?
• I'm not sure exactly where it ought to fit, but the structure of axioms and theorems in Euclid's Elements is commonly held up as a model of well-organized logic. Without getting into all the pros and cons, I wonder if a nod in that direction might improve the article. Maybe a short section on why mathematicians construct theorems, building up from "self-evident" truths or axioms through very simple theorems and ultimately arriving at statements that are fairly hard to prove would benefit some readers. DavidCBryant 18:01, 15 May 2007 (UTC)

Misses the point of being a theorem

"In mathematics, a theorem is a statement that can be proved on the basis of explicitly stated or previously agreed assumptions."

The ideas of "provability" and "truth" come into the picture only as interpretations of theorems. A theorem is a "derivation" from the alphabet and rules of the language.

The example I have seen is the language FS (stands for 'Formal System' from Benson Mates) whose alphabet consists of stars and daggers *, †, and whose formation rule for wffs is:

'Any string of symbols of FS which is at least 3 symbols long, and which is not infinitely long, is a formula of FS. Nothing else is a formula of FS.'

The single axiom of FS is: '†*†'

The transformation rule for FS is:

'Any occurrence of '†' in a formula of FS may be replaced by an occurance of the string '†*' and the result is a formula (wff) of FS.'

Theorems in FS are defined as those formulae in FS of which a derivation can be constructed, the last line of which is that formula.

• 1) †*† (Given as axiom)
• 2) †**† (transformation rule)
• 3) †**†* (transformation rule)

Therefore '†**†*' is a theorem of FS. Yet no one would claim it as "true" or "proved." It is merely derived.

Two metatheorems of FS are:

• Every theorem of FS begins with '†'
• Every theorem of FS has exactly two daggers.

This article would seem to neglect this more fundamental definition of a theorem. Gregbard 21:54, 5 July 2007 (UTC)

The definition of a "theorem" as any derivable expression in a given formal system is not completely uncommon, but it isn't the meaning that mathematicians in general attach to the word. They mean a particular type of mathematical statement expressed in natural language. The more general definition does belong in this article, but in a new section on more general meanings of the term. Would you be interested in writing that section? — Carl (CBM · talk) 23:01, 5 July 2007 (UTC)

I kept the content that User:Gregbard added, but I moved it around a little. The lede section, per WP:LEDE, is meant to be a summary of the overall article, a mini-article that can stand alone, so too much detail isn't right. I think it's important to keep the link to mathematics near the top, as well as the link to logic. I made a whole section on theorems in logic, which could be longer than it is right now. By having a section, we can give a much more complete picture than is possible in the lede. — Carl (CBM · talk) 05:14, 6 July 2007 (UTC)

Hmm. How silly is a NPOV box going to look on the top of an article about 'theorem?' "A mere general sense of the term is used in logic, where a theorem is..." The wikipedia is math-centric rather than logic-centric. This phenomenon that has just occurred I find fascinating.

I'm pretty sure an encyclopedia article should be organized from general to specific. The opening paragraph is dumbed down so as to totally ignore the one essential property of theoremhood. The interpretation as "truth" or "proof" is a "mere" interpretation that mathematicians use.

The key is derivability not truth or proof. The logical aspect of it should come first, then the math aspect. The same organization applies to math articles with computer science applications. The CS part comes after the math part. Gregbard 08:43, 6 July 2007 (UTC)

Wikipedia is reader-centric. We proceed from the general to the specific only in the sense of proceeding from the broad interest and general use to minority interest and specialist use. A theorem is a statement with a proof based on previously agreed assumptions. This already includes the idea that the statement might be a wff in a formal system, and that a proof is a derivation based on the axioms and transformation rules of that system. It also includes the notion of a theorem used in physics, in which some of the assumptions are implicit, or "physical".

I agree there is a distinction between "truth" and "theorem" and this article already makes it. There is no such distinction between a derivation and a proof except in a very specialist arena. This article is supposed to encompass the notion of a theorem in physics, logic, mathematics, engineering, computer science... You may regard the other uses as mere interpretations of the logical use, but that is a niche view. It should be expressed for encyclopedic completeness, but it should not drive the article. Geometry guy 12:26, 6 July 2007 (UTC)

If it is indeed true that the distinction is limited to a "very specialist arena" like you say, is that supposed to be a good thing? Do you think we're better off with it staying that way? It isn't my "niche view" that makes these other uses interpretations of the logical principle. The existence of an interpretation means something to a logician. The use of theorem by mathematicians to mean truth is an interpretation. It is to confuse the reality for the interpretation of the reality. You can go around saying it's true all day long. That model works well for mathematicians. But please don't portray theorems to the general public as 'the reality' rather than as a model of reality. I think they can take it. Although I think some mathematicians who are attracted to the field by it's apparent certainty may get their hearts broken if they faced the truth. Gregbard 13:11, 6 July 2007 (UTC)

The distinction between truth and theorem is widely appreciated, even by mathematicians! And even physicists understand the distinction between reality and a model of reality. So I do not see where you are coming from here. For instance, most mathematicians I know are delighted, not disheartened, by results like Godel's incompleteness theorems.

As for portrayal: this is an encyclopedia. There is no original research here. If proof and derivation are widely regarded as synonyms, then that is what we write. It makes no difference whatsoever whether we are better off staying that way or not. If you want to change the world, this is not the place to do it! Geometry guy 13:35, 6 July 2007 (UTC)

Indeed, the usage that calls a string generated by a term rewriting system a "theorem" is muchless common than the general mathematical usage. I have tried, in the lede, to clearly distinguish the notion of derivability from the notion of truth; the second paragraph, written by Gregbard, stresses this. — Carl (CBM · talk) 15:33, 6 July 2007 (UTC)

Gregbard, please think about WP:NPOV. I just consulted the Oxford English Dictionary, in which a theorem is defined to be "A universal or general proposition or statement, not self-evident (thus distinguished from AXIOM), but demonstrable by argument (in the strict sense, by necessary reasoning)". Just to be sure that this reflects a majoritarian view, I also consulted Webster's Third New International Dictionary, which gives as the first definition "A statement in mathematics that has been proved". So it appears that the ideas of "proof" and by implication "truth" are closely associated with the word theorem, in popular usage.

The distinction between an "interpretation" of a logical principle and the principle itself is vacuous. You can say that a "well-formed formula" is "derived" and "valid" – I can say with equal force that it has been "proved" and is therefore "true". The distinction between the two forms of expression is purely semantic. But the second way of talking about it is more widely accepted by people who speak English, and the majoritarian point of view is the one this article ought to stress.

One other thing. The dictionary does not define the word "theoremhood", so I am excising it from the article, on the ground that it is a neologism. DavidCBryant 15:51, 6 July 2007 (UTC)

I am completely outside this discussion, but I just wanted to mention that it seems odd to me that "theorem" would be defined as "a statement that has been proved". I was taught back in school that a proven statement is a postulate, while a theorem is a statement that is accepted as true, but which has not been fully proven or for which no full proof exists or can exist, due to the nature of the statement. Your thoughts? — KieferSkunk (talk) — 21:32, 28 July 2007 (UTC)

It's the opposite. The postulate is accepted (like an axiom), a theorem has a derivation associated with it, although not necessarily a "proof" (This I think, is the point these guys are getting lost on.) If it has a "proof" there is a derivation to which the proof corresponds. Be well, Gregbard 23:07, 28 July 2007 (UTC)

Okay, thanks for clarifying. :) — KieferSkunk (talk) — 16:04, 31 July 2007 (UTC)

lede

I did intend to say "more general", thanks for fixing that.

Geometry Guy mentioned in an edit summary that the lede is too long. I don't think it's so bad - the first four paragraphs are a reasonable summary of the material in the article, which is desirable for WP:LEDE. The last paragraph, perhaps, could move down to the section on terminology. — Carl (CBM · talk) 15:21, 6 July 2007 (UTC)

I'm not satisfied with the lede. It needs a statement of what a theorem is. The qualification "in mathematics" is against the rules, unless there are equivalent statements, "in logic", "in metaphysics", "in physics" etc... But then it needs to be explained why there are different interpretations in different fields - perhaps with some history as to how the different uses came about. If theorems are about proofs or derivations as argued above, then the rest of the article needs an commonly accepted good example of a proof and a derivation. Sholto Maud 06:07, 31 July 2007 (UTC)

All theorems have a derivation associated with them, that is why it is my view that that should be first. I'm indifferent to a having the "in logic" or "in math," etcetera, although that should be somewhere. The theorem as derivation is more a more fundamental definition because it does not presume truth or justification etc. We should always begin articles with a more general or fundamental overview. This is so that people learning from them are not prejudiced forever. Gregbard 07:03, 31 July 2007 (UTC)

In its ordinary sense in mathematical logic, the word "proof" doesn't assume truth either - it refers to a derivation. The idea that a derivation is not a "proof" without some semantical interpretation is not found in mathematical logic. The fact that the deduction rules used in most mathematical proofs are sound is of course important, but not part of the definition of a proof.

I have already pointed out to Gregbard that Samuel Buss's article in the Handbook of Proof Theory claims exactly the opposite of what Gregbard claims - Buss claims that the idea of a proof as a logical derivation is less general than the concept of a natural language proof. Buss says,

"There are two distinct viewpoints about what a mathematical proof is. The first view is that proofs are social constructions by which mathematicians convince one another of the truth of theorems. ... Of course, it is impossible to precisely define what constitutes a valid proof in this social sense, and the standards for valid proofs may vary with the audience and over time. ... The second view of proofs is more narrow in scope: in this view, a proof consists of a string of symbols which satisfy some precisely stated set of rules and which prove a theorem, which must also be expressed as a string of symbols. ... Proofs of the latter kind are called "formal" proofs to distinguish them from "social" proofs. (p. 2)"

This viewpoint is not uncommon. — Carl (CBM · talk) 04:52, 4 August 2007 (UTC)

I think if you read this quote carefully, you will realize that brother Buss is talking about comparing "social" theorems with "formal" theorems. He is not comparing "logical" theorems to "mathematical" ones. The formal proof is more narrow than the social proof because social proofs range from "aw c'mon" to "This here fact A implies that there fact B, and fact A is undisputed, therefore B is true." In that regard, what consists of a social proof is more broad than a formal proof whose requirements for proofhood are more narrow.

The mathematical use of proof assumes that justification goes along with the derivation. We are supposed to be compelled to believe something by such a proof. That is a presumption. A goal of philosophy and logic is to strip away the presumptions.

The description of the formal proof as "more narrow" refers to the fact that there are requirements of a formal proof that there are not for a social one. That's true. But that is not what is being discussed. The sense of "more broad" and "more narrow" that matters as it concerns the organization of an encyclopedia is the one definition includes all of the cases of the other.

"Buss claims that the idea of a proof as a logical derivation is less general than the concept of a natural language proof."

The word "proof" which is a form of the word "prove" can hardly be thought not to imply justification. That is baggage. The goal is to put forward a definition that does not have baggage. Then talk about the different kinds baggage in the article. In this regard theorem as derivation is a more general definition than theorem as proof (or proved).

It seems we are refering to different pairs of things when we are saying A is more general then B. The use of the word theorem in logic is more general then the usage in mathematics. Perhaps brother Buss would agree in this. Every theorem of mathematics corresponds to a logical derivation, not the other way around.

It is also of note that Buss says "...that the IDEA of a proof as logical derivation is less general ... " The derivation itself is in fact more general. Be well, Gregbard 13:38, 6 August 2007 (UTC)

Ok so if we step back from the task making a definition for a moment, what we can say is that there is no commonly agreed definition of the "theorem" concept. This is the most general statement one can deduce from all the above comments. I propose we start the lede saying that there is no commonly agreed definition of the "theorem" concept, and then say what the various different definitions are and how they differ. Sholto Maud 02:30, 6 August 2007 (UTC)

(←) It's not true that there is no commonly accepted definition; what's true is that there are two commonly accepted definitions. While you are free to try to rephrase the lede more clearly, it already explains what the two definitions are and how they relate to each other. — Carl (CBM · talk) 12:02, 6 August 2007 (UTC)

Token revert

Greg, I reverted because I think what you added was OR. Of course, I could be wrong - so, please give some sources that verify what you are saying about tokens, abstract objects, and so forth - because it sounds just like what you were trying to add to some other articles. Thanks. Tparameter (talk) 01:52, 13 May 2008 (UTC)

Until I get some good material on this, I have placed the tag for lacking interdisciplinary content. Be well, Pontiff Greg Bard (talk) 18:24, 14 May 2008 (UTC)

I still don't agree with this addition:

It is universally acknowledged that numbers and the other objects of pure mathematics are abstract. In essence, a theorem is a type of abstract object. We only experience them as tokens of that abstraction. For instance, one token of a theorem is the formula of a formal language which is derived in a formal system; another token of which is the equivalent statement in natural language, which can be proved in a mathematical proof; and another of which may be chalk marks on a board representing that theorem.

First, whether a number is an abstract object doesn't reflect on whether a theorem is. But more importantly, I don't think there is any support demonstrated in the literature for the idea that a theorem consists of both a formula in a formula language and a natural language statement. Not only is no support demonstrated, I don't think there is support in the literature for it. I'll see if I can't find some actual references on a theorems in those "introduction to higher mathematics" books. — Carl (CBM · talk) 22:24, 16 May 2008 (UTC)

Under what interpretation is a theorem not an "object of pure mathematics." I am really just shocked at this point. Pontiff Greg Bard (talk) 22:38, 16 May 2008 (UTC)

You seem to be completely ignoring the actual use of the word. We refer to each of these things as, for instance, a modus ponens theorem: the chalk on the board, the idea of it. However, if I asked you if the theorem written in yellow chalk is a "yellow theorem" you would think I'm nuts. It an abstract object, and that is obviously how we treat it. Pontiff Greg Bard (talk) 22:47, 16 May 2008 (UTC)

Please see the quotes below, which each support my contention that a theorem is simply a statement. What I disagree with isn't particularly the "abstract" part, which I think only misses the point. The thing I find doubtful is the claim about tokens that represent the same theorem. I'm going to rephrase your sentences some while leaving the abstract object part. — Carl (CBM · talk) 23:11, 16 May 2008 (UTC)

References

Some quotes

Each of the following supports the general viewpoint that a theorem is a statement that has been (can be) proved.

• Smith, Eggen, Andre, A transition to advanced mathematics, p. 26

  "A proof is a justification of a statement called a theorem."

• Encyclopedia Britannica, "theorem (logic and mathematics)":

  "in mathematics and logic, a proposition or statement that is demonstrated. ... The statement “If two lines intersect, each pair of vertical angles is equal,” for example, is a theorem."

• Tarski, Introduction to logic, the very first paragraph:

  "Every scientific theory is a system of sentences which are accepted as true and which may be called laws or asserted statements of, for short, simply statements. In mathematics these statements follow one another in a definite order which will be discussed in detail in Chapter VI, and they are, as a rule, accompanied by considerations intended to establish their validity. Considerations of this kind are called proofs, and the statements established by them are called theorems."

• Enderton, A mathematical introduction to logic, p. 117

  "Notice that we use the word "theorem" on two different levels. We say that α is a theorem of Γ if $\Gamma \vdash \alpha$. We also make numerous statements in English, each called a theorem, such as the one below. ..."

— Carl (CBM · talk) 23:11, 16 May 2008 (UTC)

Carl, it will shock and amaze you to learn that a statement is also an abstract object. (I am not really very interested in inserting that fact in that article, although ...) Furthermore, logicians always deal with the idealized version of a statement. I will try to find where I read that recently. If the tokens of the type of statement that it is do not properly reflect the idea, then it is not a token of that type of thing. It's the token that's wrong, not the idea. Logicians act accordingly. The following is false:

"In each of these settings, a theorem is an abstract expression of a proposition that can be logically deduced; the difference between the settings is, essentially, whether the statement is in natural language or in a formal language."

Actually, in each of those settings, we are talking about only the tokens, not the type. Therefore those are not "abstract expressions" (a term from somewhere?? or OR), those are the concrete ones. You identify a difference in culture, however certainly it makes no difference as far as the theorem is concerned whether it is in natural, or formal language. Pontiff Greg Bard (talk) 23:29, 16 May 2008 (UTC)

It's not clear to me that the theorems are not themselves tokens, that is, expressions in a natural or formal language. What they are tokens of is a question that I cannot answer.

I disagree that it makes no difference whether a theorem is expressed in a natural or formal language. A formal statement of a mathematical theorem can be said to formalize the theorem, or to represent the theorem, but is not itself the same as the natural language theorem. At least, that is a reasonably common viewpoint, in my estimation; I am not claiming it is a unanimous opinion. I am certain is it more common for texts to say that a natural language theorem can be turned into a formalized one than for them to say that a natural language theorem is the same as the corresponding formal theorem.

I think it's your turn to provide some sources, since I have found four above that seem to simply identify a theorem with a statement. Is there any source that describes a theorem as a type with various tokens? Note that, even if there is such a source, I'm not convinced that we should discuss that here, since it may be a very nonstandard text, or just mention it in passing. But if there isn't any mainstream text that mentions type/token issues in the context of theorem, that would be a sign that we don't need to do so in this article. — Carl (CBM · talk) 00:27, 17 May 2008 (UTC)

Obviously, there must not be an easy verification of the type/token claims, which means that most likely it's trivial information or wrong information. Either way, shouldn't be in the article. Tparameter (talk) 04:29, 17 May 2008 (UTC)

Where did you get these ideas about what is trivial, wrong, or obvious. 0 for 3 mister. The fact is, if you must know, that I have limited time and resources. I think I have explained it all sufficiently. Philosophers of language study theorems because they are statements that tell us about truths of the world. Logicians care about the type-token distinction because failure to care may result in ambiguity. This is all straightforward. I think you had compared apples to theorems at one point. I'm sorry, but there really is much for you guys to learn here. Pontiff Greg Bard (talk) 10:30, 17 May 2008 (UTC)

(←) One of the reasons I enjoy contributing to WP is because I learn a lot of things from other people. There is much more that I don't know than I do know. On the other hand, there are a few areas I am very familiar with, particularly within mathematical logic.

If you asked me for an off-the-cuff, unresearched opinion, I would agree that there is a universal called theoremhood of which individual theorems are tokens. I would also agree that there is a universal called "Fermat's-last-theoremhood" that includes all theorems that are different expressions of the underlying idea of Fermat's last theorem. But Fermat's-last-theoremhood is not itself a theorem, it's a type of theorems (it corresponds to something like red-chairhood vis-a-vis chairhood).

The claim I believe you are making is different - that Fermat's-last-theoremhood is the theorem, and that the things I call theorems are merely tokens of it. In the way I ordinarily use the language, the theorem itself is a token, not a type. (In a particular sense; of course each theorem has a corresponding type of similar theorems, just as Fermat's last theorem has Fermat's-last-theoremhood).

So my doubt that the type/token distinction is relevant in the context of theorems comes both from my own mental analysis of what's going on, and from my doubt that there are texts in mathematical logic or mathematics that discuss theorems in those terms. I can certainly be wrong, but the best way to demonstrate that is with some sources to back up your position. — Carl (CBM · talk) 12:21, 17 May 2008 (UTC)

Hi guys, can I join in? Not to be outdone quotation-wise:-

• [in the language L] "A sentence Φ is a theorem in logic (or theorem, for short) if an only if is derivable from the empty set of sentences." (Mates, 1972, p. 127)
• [in the axiomatic system for L1] "A sentence Φ is a theorem if an only if Φ is the last line of a proof. We shall write
  |- Φ
  as an abbreviation for
  all closures of Φ are theorems" (Mates, ibid, p. 166)

It is clear that the term theorem in the above two quotations is referring to a sentence in a language and as such a theorem is, being a sentence, a string of symbols. To allow the possibility that there are other meanings of the (English) word theorem lets give it the name theorem1, so we will say a theorem1 is a string of symbols which &c. We would then say e.g. that Fa is a string of symbols which is a sentence (in some languages) but is not a theorem1 (in a consistent theory) but Fa v ~Fa is a string of symbols, and is a sentence and is a theorem &c. And so is (x)(Fx v ~Fx) In other words in one sense of theorem, i.e. theorem1, a theorem is just string of symbols (marks on paper, verbal utterances &c., and Fa v ~Fa and (x)(Fx v ~Fx) are examples of same.

Does the term, or could the term theorem have any other meaning? I turn to my copy of Euclid, The Thirteen books of the elements Dover 1956, in which Proclus (ed. Friedein) is quoted p. 124 as distinguishing between problems and theorems the latter exhibiting the essential attributes of the generation, division &c. of figures and again, page 126 "...when any one enunciates that' [emphasis added] ‘‘In isosceles triangles the angles at the base are equal we must say that he enunciates a theorem." The words in isosceles triangles the angles at the base are equal is a string of symbols. On my reading it is not the string of symbols that is being describes as a theorem but what is asserted’’’ when the words are used to make an enunciation. On that reading the theorem that isosceles triangles the angles at the base are equal for which Euclid provides a proof (Book 1, proposition 5) can be enunciated by the string of symbols isosceles triangles the angles at the base are equal but IS not the string of symbols isosceles triangles the angles at the base are equal. To suggest that the theorem proved by Euclid was the string of symbols in isosceles triangles the angles at the base are equal would be to suggest that Euclid wrote or uttered that string of symbols meaning then in the sense understood in English speaking countries several centuries later. Lets us call that sense of the word theorem theorem2. Far be if for me to say that Proclus was right to think that there is something apart from the strings of symbols he read, wrote, heard and said, something which he calls a theroem2, and which he believes Euclid proved. Nevertheless he does, rightly or wrongly, appear to use the term theorem in a different sense, a sense which does NOT denote a string of symbols.

I put it to you that:

Hans is saying that

a theorem1 is a string of symbols, "tokens, that is, expressions in a natural or formal language"

and

Gregbard is saying that

a theorem2 is "an abstract object" and, if I understand him, a theorem2 is an "idealized version of" a corresponding theorem1.

Perhaps Gregbard would say that the sense of a theorem1 is a theorem2, that many theorems1 (e.g. isosceles triangles the angles at the base are equal and the same translated into German, or written in the original Greek) have the same theorem2 as their sense. Being theorems, i.e. proven to be true, the reference (bedeuten) are the same, the True.

I may be quite wrong in surmising what Hans and Greg mean by the word theorem. If they mean the same thing then they definitely disagree about its status and proprieties. If they mean different things by the word then it is not obvious that there is any disagreement of that kind at all. I suggest both parties define just what they DO mean by the word "theorem" before they continue their debate about. --Philogo 03:34, 18 May 2008 (UTC)

I think you have mistaken me (Carl) with Hans. There is the same issue here as in many areas of mathematics: two statements can be intensionally different theorems (as in the example of translation from Greek to English you provided), but still be equivalent in some way. Similarly, two knots can be intensionally different (tied according to different instructions, say) but be equivalent ("the same") knots. In the case of knots, there is a precise definition in knot theory of when two knots are equivalent. In the case of theorems, there is no good definition I know of that expresses when two theorems express the same abstract assertion.

My goal in presenting the references above was to demonstrate the common viewpoint that a theorem is a statement, sentence, or proposition. The difference between a theorem qua statement and theorem qua proposition is not particularly germane in most areas of mathematics, so there is little written about it in mathematics texts as far as I can tell.

My specific concerns with text I have removed from the article are:

• I don't agree that a statement in a formal language, and a different statement in a natural language, should be described as tokens of the same "theorem". This is a way people could look at things, but I don't know of any evidence that this way of looking at it is common in the literature. Rather, they would say that each of the two statements is a theorem (compare Enderton's quote above), but that they express the same idea.
• Upon reflection, I believe I identify a theorem with a token, not with a type. I don't believe there is a well-established word for the type of things of which theorems are tokens (for example, there are many seemingly independent statements equivalent to the Riemann hypothesis. Do these express the "same" theorem as the Riemann hypothesis does? In many cases the equivalence is very subtle, and the statements were not intended to be equivalent.)

I don't see that these issues warrant discussion in the article, because they seem to be mostly ignored in the literature. But I am open to being proved wrong. — Carl (CBM · talk) 12:17, 18 May 2008 (UTC)

What you are describing is a formulation. There are many formulations of the RH, however we still say that they are "of the RH." We don't call each formulation a new hypothesis. People in their vernacular, call a theorem the chalk on the board, and it works pragmatically just fine. It's serviceable. However, strickly speaking there is a distinction. I am not so interested in saying the abstract part is the theorem and the chalk is merely a token of it. They are both referred to correctly as the theorem just fine. There is a sense in which the theorem of chalk on the board is a theorem, and then there is the sense in which it is a type of abstract object. However, as I stated earlier, that logicians always deal with the idealized version. This is what we are talking about that someone asserted this theorem. Nobody thinks that logicians assert the chalk on the board. However, there is also a sense in which a theorem written in yellow chalk is a "yellow theorem." If one made such a claim, they would need to address the type token distinction in order to be clear. I believe it is a WP goal to cover all senses of a term. Under that justification alone, this distinction belongs in.

Also, it does not matter if, for instance, Fred believes that theorems "float in the air," and Joe believes that a theorem reflects a "structure in God's brain," etc. These metaphysical issues have nothing to do with what I am talking about. Logicians with such beliefs can perfectly well work together on the same theorems just fine. So if Carl believes in "theoremhood" that is fine. However, the type-token distinction is intended to follow reason (its not metaphysics). In that regard it is not merely a matter of looking at it differently as a "way of understanding." The point is to identify a legitimate distinction, so therefore it is not a POV issue in the article. Pontiff Greg Bard (talk) 13:28, 18 May 2008 (UTC)

As I said above, I think the burden is on you here to provide some sort of published source to show that not only are your ideas plausible (of course they are plausible), but that they are of sufficient interest to the mathematics or logic community to include here. As I also pointed out, it seems to me that theorems are tokens, not types, so in particular I would appreciate any source to the contrary, so that I can see the argument that is being presented there. My guess is that such a source would be using the word theorem in a different sense than mathematicians do. — Carl (CBM · talk) 13:46, 18 May 2008 (UTC)

Burden, indeed. Thanks for that. What do you have to say about the SEP saying that it is universally accepted that all mathematical objects are abstract object? Can you with a straight face, say that a theorem is not a mathematical object? It seems that your view is one that is on the fringe there.

Please Carl, you are harping about the sources at this point. Have I reinserted any text? No. You guys have sufficiently sent me marching off. Just be careful about what you wish for. With that said, this only needs sources because you and a few others say it does. That's how it works. However, I do not have to pretend about the reasons. There are volumes of mathematics articles with complex formulations which no one challenges, even if they do not know for sure if it is the correct formulation. There is a great deal of faith going on all over the math department. Some statements stand in need of justification, and other do not. This adds up to a strong bias. Sufficient interest is not a criterion for WP. If it was, the least reflective, and least intellectual among us would be the final say on deleting content. That is obviously not acceptable. Furthermore, mathematicians are not the only academicians seriously studying and making advances in the study of theorems. Basically, what I am saying is that you need to learn some respect for the interdisciplinary nature of the topic. I didn't randomly decide that this article needed this content. The type token distinction is important to understanding theorem particularly. This whole discussion stands in testimony to that fact.

It is the case that a statement in a formal language, and the same statement in natural language, should be described as tokens of the same "theorem." Is that not what you meant to say above?

Remind me never to play 20 questions with you. In your mind you can "assert" something with chalk, while I would not think to say that. Upon relfection after losing such a game I will see that your response was consistent with the way we use theorems, but would not help me figure out what the object was. Way to go Carl.

Pontiff Greg Bard (talk) 22:16, 18 May 2008 (UTC)

RE: "The type token distinction is important to understanding theorem particularly." Then why can't you find one source that says as much? Please answer this question Greg. If it's so fundamentally important to understanding what a theorem is, then why is there no easily found source? Believe me, I've been looking. My sister-in-law, a librarian, has made some effort as well - but, neither of us has found any discussion on the nature of theorems discussing the ever-important type-token distinction. BTW, This surely is an interdisciplinary topic - but, if the content can't be verified, then it may not be true. That has nothing to do with math/science/philosophy. Instead, that's a wiki guideline. I, for one, support the no original research guidelines here. On a tangent, I find the type/token thing to be very interesting, so I'm hoping you find a source, because I'd like to look further into it. You mentioned that you studied this in "Advanced Logic". Was that a symbolic logic course, or a reasoning course, or what? Also, what textbook? Tparameter (talk) 00:15, 19 May 2008 (UTC)

Stop beating me up over sources. Am I not marching fast enough for you? Quine, Tarski, and Carnap all care about the type-token distinction, and so should you. Pontiff Greg Bard (talk) 01:32, 19 May 2008 (UTC)

I'm not beating you up about it. I'm assuming good faith and trying to find sources. But, I question your claim that type-token is key to understanding theorem, intellectually or otherwise. You keep commenting about how surprised you are that some people haven't heard these key points, and you imply that those of us that want your claims verified are somehow missing the "intellectual" points - yet there are no sources to be easily found. You studied this - which text book did you use? Tparameter (talk) 02:13, 19 May 2008 (UTC)

Do you agree or not agree Carl that you are saying (a) that there is a definition of the term Theorem by which it is string of symbols "tokens, that is, expressions in a natural or formal language" and (b) that that is the definition, i.e. definition (a), that is pertinent to the article?

Do you agree or not agree Gregbard that you are saying (c) that there is another definition of the term Theorem by which it is "an abstract object" which is an "idealized version of" theorem in the sense (a) above and (d) that that is the definition, i.e. definition (c), that is pertinent to the article? --Philogo 19:40, 18 May 2008 (UTC)

We know that a theorem is an abstract object (or type) in a more primary way than it is a token because there exist theorems which are longer than can be written with all of the matter in the universe. No token exists of such a theorem, however this type of theorem does exist.

Different formulations of the same theorem attempt to mirror the idealized version of the theorem which we simply call "theorem" but mean the type that is that theorem. Each formulation is a different token of the same theorem. Pontiff Greg Bard (talk) 09:28, 19 May 2008 (UTC)

I'll take that as "Yes" then, shall I?--Philogo 12:32, 19 May 2008 (UTC)

No, it's one definition that makes a distinction between two aspects of the same thing. That is why it needs to be covered in the article. Pontiff Greg Bard (talk) 18:27, 20 May 2008 (UTC)

Come then give me the other definition.--Philogo 21:42, 20 May 2008 (UTC)

Holy Moly. I just said that it's one definition. It's one concept that is understood through two aspects (at least). A complete definition will account for these aspects. Furthermore, if it doesn't cover both aspects (i.e. identifying that the distinction exists), then it is not a complete definition.

Be well, Pontiff Greg Bard (talk) 22:36, 20 May 2008 (UTC)

Come then give me the complete definition. Don't be mean, share it with us!--Philogo 12:01, 21 May 2008 (UTC)

See also Talk:Logical consequence#Just Quotes--Philogo 21:45, 20 May 2008 (UTC)...seen -GB

Draft shortened lead

In mathematics, a theorem is a statement proven on the basis of previously accepted or established statements. In mathematical logic, theorems are modeled as formulas that can be derived from axioms according to the inference rules of a fixed formal system without any additional assumptions.

The expression that results from a derivation is a syntactic consequence of all the expressions that precede it, regardless of semantics. In mathematics, the derivation of a theorem is often interpreted as a proof of the truth of the resulting expression, but different deductive systems can yield other interpretations, depending on the meanings of the derivation rules. Although they can be written in a completely symbolic form using, for example, propositional calculus, theorems and their proofs are often expressed in a natural language such as English.

The statements of theorems have two components, called the hypotheses and the conclusions. The proof of a mathematical theorem is a logical argument demonstrating that the conclusions are a necessary consequence of the hypotheses, in the sense that if the hypotheses are true then the conclusions must also be true, without any further assumptions. The concept of a theorem is therefore fundamentally deductive, in contrast to the notion of a scientific theory, which is empirical.

A theorem which may be simply stated but with a proof that involves surprising and subtle connections may be referred to as "deep", for example Fermat's Last Theorem.

I deleted the sentence "Theorems have two components, called the hypotheses and the conclusions" from the lede, for four reasons. First, the point is better addressed in "Informal accounts". Second, it was interrupting a paragraph primarily about the nature of proof, and so was out of place. Third, it is grammatically strained since "Theorems", "hypotheses", and "conclusions" are all plural, but the latter two must be counted as singular if they compose "two components". Finally, many natural language theorems do not cleave so tidily into two easily identified halves. (Howald (talk) 02:25, 28 November 2011 (UTC))

Shortening lead, definition of hypothesis and example for converse

The last paragraph of the lead, about theorems being "trivial", "deep" etc., is practically the same as the fourth paragraph of the section "Formal and informal notions", and therefore too repetitive in my opinion. Also, the lead is too long: WP:LEAD says "The lead should contain no more than four paragraphs". In the section above I give the text for a suggested shortened lead. Material deleted from the fourth paragraph of the current lead should perhaps be worked into the body of the article somehow, and material from the last paragraph of the current lead can be merged into the similar paragraph already in another section, as I just mentioned.

The word "hypothesis" is currently used inconsistently in this article. The lead currently says "The proofs of theorems have two components, called the hypotheses and the conclusions." I suggest changing this to "the statements of theorems" instead of "the proofs of theorems". This will make it consistent, in my opinion, with the first paragraph of the section "Formal and informal notions"; however, the third paragraph of that section seems to be using a different definition again and should perhaps use a different word instead, such as "axioms" or "premises" or "propositions", or state explicitly that it's using a different definition of "hypothesis", as is done later in the article.

In the following sentence, I think it would be better to give a slightly more specific example than "A is related to B", because generally in such a theorem we don't just prove that two things are related but that they are related in some specified way. Currently it says, "For example, If a theorem states that A is related to B, its converse would state that B is related to A." I suggest "For example, if a theorem states that A implies B, its converse would state that B implies A." or possibly "For example, given a set of points, if a theorem states that A is the closest point in the set to B, its converse would state that B is the closest point in the set to A." ☺ Coppertwig (talk) 01:45, 26 August 2008 (UTC)

Proposition

The article says:

A proposition is a statement not associated with any particular theorem.

That seems weird. Any statement is a proposition; the two words, "statement" and "proposition" are synonymous. Michael Hardy (talk) 23:47, 5 December 2008 (UTC)

Revert 2009-11-9

I reverted an edit by Gregbard just now. This talk page has already featured extensive discussion of the "abstract object" claims, so I will just point to that above. Also, the new text focused on formalized theorems, while this article is not primarily about them. Finally, the new text was confused about the existence of other formal deduction systems that do not satisfy "a proof is a sequence of formulas". — Carl (CBM · talk) 14:09, 9 November 2009 (UTC)

The abstract object issue is sufficiently covered by the mention that it is a concept. That will suffice. I don't think you are incorrect about what "this article is [or is not] not primarily about." I think that is a POV judgment, and the latest formulation consists in 'subject matter; and not any particular POV AT ALL. If you have some reformulation of the truths communicated in the article please let them take the form of a reformulation and not a deletion. Pontiff Greg Bard (talk) 21:45, 9 November 2009 (UTC)

I also have reverted to an older version. The lead section is not the place for a fully abstract formulation of a concept, useful as that may be at some point of the article. Charles Matthews (talk) 22:58, 9 November 2009 (UTC)

It looks like there is no critical analysis going on here, just sweeping generalizations. Pontiff Greg Bard (talk) 22:57, 9 November 2009 (UTC)

Well now Charles will make me take it back. That is actually at least a somewhat constructive statement. Charles, we don't agree about how fundamental the "abstract" nature of a theorem is. In my mind the first sentence of an article should tell us what something is. A theorem is the idea in the mind primarily, and the rest is supposed to conform to that. That is the way all logicians and mathematicians work. If the stuff you are writing doesn't correspond to the idea, then what you are writing is wrong, and you have to reformulate (I'm talking about a formulating a theorem, not the article). This would seems to be fundamental to communicating to readers "what is a theorem". I would like to have this material covered in one article, but since there has proven to be a need and a way to deal with this situation, I have split out theorem (logic). I hope we can work things out together instead. Pontiff Greg Bard (talk) 23:21, 9 November 2009 (UTC)

What a theorem "is" can be judged experimentally by picking up a book full of theorems - not hard to do. The obvious thing, unless you have picked up a very strange book, is that what is headed a theorem is a semi-formal statement, in a mixture of natural language and some symbols, purporting to be an adequate representation (adequate to experts - assume here we are dealing with mathematics or mathematical economics, since if we get started on physics we'll all despair). The adequacy means that an expert given enough time and motivation could produce a completely formal statement. So, it's a statement in mathematical jargon purporting to be uniquely translatable into the sort of theorem a theorem-proving machine might be set to print out. And as we know it must be brought forward as a consequence of other statements admitted as axiomatic or at least true. This sense of theorem did not change dramatically around 1900 at the hands of the logicians (though the stock of theorems did get adjusted as supposed proofs were reconsidered and analysed). Charles Matthews (talk) 15:51, 10 November 2009 (UTC)

Small but important objection: The translation is very far from unique. Oh, all the translations should be equivalent, though equivalent over what theory is not unproblematic. But there is no canonical way to turn a human-readable proposition into a sentence of first-order logic. --Trovatore (talk) 23:36, 14 November 2009 (UTC)

I have always thought a theorem is a statement, not an idea in the mind. — Carl (CBM · talk) 01:13, 10 November 2009 (UTC)

I quite often find that if what I'm writing down doesn't correspond with what I'm thinking then what I'm thinking is wrong :) Dmcq (talk) 17:40, 10 November 2009 (UTC)

• Greg's position appears to be that a statement is, by definition, a concept. This is debatable; but it is also unnecessary here; it suffices to say that a theorem is a species of statement, whatever statements are - to be clarified in Statement (logic).
• Greg's text also omits any difference between theorems and other statements; it is therefore not a definition. Septentrionalis PMAnderson 15:56, 11 November 2009 (UTC)

Yes a statement is an idea or concept. A theorem is also a concept. However a theorem is not necessarily a proposition or statement at all. This is demonstrated by the string of squares and triangles. That is an example of a theorem which is merely an "abstraction". Dmcq, you have to be careful about what is right or wrong. Logicians are always talking about the idea and if the marks on paper do not represent it, the marks are wrong, not the idea and must be reformulated somehow, if possible. Please be advised... I am talking in a metalogical sense. In a mathematical sense we look to the marks on paper to tell us if our "idea" is correct --because the proof of it may be complex and non-obvious. If the idea is simple and obvious, then no amount of complexity and non-obviousness of proof can cause one to deny its validity in someone's mind. That is the type of thing I am talking about. Pontiff Greg Bard (talk) 23:43, 14 November 2009 (UTC)

Merge

I think we should find a way to accommodate the material in formal theorem as a way of elucidating on the topic in theorem. There is material in there about its relationship to tautologies and formal systems, and more which I think readers are expecting to find in "theorem".Pontiff Greg Bard (talk) 23:43, 14 November 2009 (UTC)

The content there is exactly the content that was removed from here. So just redirecting that page to this one would be the best solution I can see. I actually proposed this at WT:WPM, but some people think that maybe formal theorem should be redirected to formal proof instead. Either one is fine with me, but the content that was removed from this article (about abstract objects, etc) really doesn't belong here as far as I can see. — Carl (CBM · talk) 01:25, 15 November 2009 (UTC)

I think you are pretty hung up on that "abstract objects" thing. It isn't even in there. The phrase "idea, concept, or abstraction" is so worded as to avoid POV. I would be content to hone down to "concept." It's just one sentence. To throw the whole rest of the material away because of it is a big mindless waste. If we could be consistent with the way it is at the article set I would be happy. All I am interested in is identifying the topic ontologically at some point.

I certainly do not understand the hostility to the whole rest of it, including material like the relationship between theorems, tautologies, propositions and logical consequence which one would reasonably expect to see in an article about theorem. Perhaps we should move all of this content to "mathematical theorem" and reserve this space for the fundamental concepts which mathematical theorems participate in. Pontiff Greg Bard (talk) 01:45, 15 November 2009 (UTC)

As I said somewhere, I have always thought that a theorem is a statement, either in natural language or in some formal language. There's no benefit to calling a statement an "idea, concept, or abstraction"; at best this is a trivial observation, if one regards everything in mathematics as an idea, concept, or abstraction. At worst, it could be false, if one takes statements to be concrete objects rather than abstract ones.

This article already has a "theorems in logic" section that discusses formal theorems of deduction systems. But I don't see the benefit in adding all this to the lede as well. The study of formal theorems is a very small part of the study of theorems generally, since few mathematicians, physicists, etc. are logicians; so the part of this article devoted to formal theorems should not give them excessive emphasis. — Carl (CBM · talk) 02:01, 15 November 2009 (UTC)

The problem I have is that it is the aspect common to math, physics and logic. You don't see the benefit. You've made that clear. Yes there is a benefit. The most general account is the most useful because it applies to more cases. This is precisely why math and logic are useful at all. If you insist on the narrow scope then you should be open minded to moving the content to mathematical theorem, and let the links to theorem cover the inclusive concept. I think that pushing this material aside is a disservice to the readers. Pontiff Greg Bard (talk) 02:50, 15 November 2009 (UTC)

The thing with theorems is that the informal notion is the more general scope. Natural language theorems are studied in physics, math, economics, etc. Formal theorems, on the other hand, are only studied by a smaller group of people in logic. So making the article focus on formal theorems makes its scope more narrow. — Carl (CBM · talk) 03:02, 15 November 2009 (UTC)

Yes I agree that the informal notion is more general. There are theorems which can be proven in English which cannot be proven in formal languages. However, inevitably, in explaining what a theorem is, some language and some system is required. We are able to use language to describe it, and also make clear that we are using language to describe it rather than say that it is the language. Throwing the formal language account away entirely is just plain irresponsible. Use your words.Pontiff Greg Bard (talk) 03:21, 15 November 2009 (UTC)

Also, Greg, it's frankly very weird that you on the one hand want to call theorems "ideas", and on the other insist on their syntactic nature. Ideas are not syntactic. --Trovatore (talk) 02:04, 15 November 2009 (UTC)

A syntactic rule is an idea also Trov, so there is no contradiction. I do understand your concern over formalism in general. My formulation is that a theorem is an idea which can be formed using a formal language. So I am not hung up on formalism because the way I see it, it is addressed in the first sentence. It doesn't say a theorem is a string... for that very reason. Pontiff Greg Bard (talk) 02:50, 15 November 2009 (UTC)

An individual syntactic rule is not an idea, no. There is an idea of syntactic rules, but that's different. Same with the other things, like sets -- there's an idea of sets, but an individual set is not an idea, it's an object.

But that's a side issue. The point is that you are overemphasizing the formalism. Formal derivations are superstructure, not infrastructure; they're something added after the fact. People were proving theorems long before anyone got around to coding them into strings and reducing the inference rules to syntax. --Trovatore (talk) 05:04, 15 November 2009 (UTC)

Trov, unless you can tell me where a particular "individual syntactic rule" or a particular set is (in space, time, a postal address, something), then you will have to concede that an individual syntactic rule is an idea and so is a set. No, it is not the marks on the paper. That is a particular token of the rule. The idea is the thing that "applies" in cases, or is "found interesting" etcetera; which is not what we would say of the marks on paper. I do not see any problem with explaining theorem in formal terms. We are able to use language to clarify any formalist "pov" issues.

The issue here, is that "theorem" is an important article with a lot of links to it. When people go there they are expecting to see the relationship between tautologies and theorems spelled out, they are expecting something about the fact that they are interpreted as true propositions, they are expecting to see something about logical consequence, etcetera. All of this is lead paragraph material. I think we should merge almost all of the material of the first three paragraphs of "formal theorem" back into this article where it belongs. Pontiff Greg Bard (talk) 22:45, 16 November 2009 (UTC)

You think everything has to be either spatiotemporally located, or else an idea? Why? What about Platonic ideal objects that we are unable to individually ideate (such as non-definable sets)? Are they ideas? (I suppose you could argue that they're ideas, just not our ideas — ideas of God, for example — but I sort of had you pegged as someone who avoids that category.)

In any case this is not the normal usage of the word idea, even in philosophy, I think. Fred: "Hey John, I just had an idea!" John: "What was it"? Fred: "buopwedhweiiur!". Strings are not ideas; they're objects. Where they're located is a red herring. --Trovatore (talk) 22:52, 16 November 2009 (UTC)

Things that aren't located at any particular time and place are commonly considered to be ideas, concepts or abstractions. I would say that round squares, "buopwedhweiiur" and the "ideas in god's mind" all "exist on an intellectual level" which is tantamount to being at least a bad idea (but that's my own view i.e. OR). Think about it. You natural response isn't to think Fred is lying. It depends on what he means. Perhaps it is an abstraction just like " $\blacksquare$ $\bigstar$ $\blacksquare$ $\blacklozenge$ $\blacksquare$ $\blacksquare$ "

But here I've allowed myself to get distracted from the main issue, which is the formalist POV of your contributions. You don't see a problem with explaining theorems in formal terms, but the problem is nevertheless there, and is the main problem, because this is not in fact how theorems are generally conceived. It is fine, certainly, to have a section on formal theorems and their derivations. But to present it as what theorems are, no, that's completely unacceptable. --Trovatore (talk) 22:58, 16 November 2009 (UTC)

It seems to me that your concern is very easily addressed. So why do people feel the need to delete large amounts of text? That doesn't demonstrate very skilled Wikipedia collaboration.Pontiff Greg Bard (talk) 23:17, 16 November 2009 (UTC)

Re Gregbard: several of the things you say people are looking for are already in the article, for example the fact that the conclusion of a theorem is true if its hypotheses are true, and that a theorem is a logical consequence of its hypotheses.

The thing with "tautologies" it less relevant. First, as I have pointed out elsewhere, few people use that word to mean logical validities in general. The word is primarily used in the context of propositional logic. Second, few outside the logic community use the word "tautology" at all. Third, formal theorems are not logically valid if their axioms are not logically valid; there are many formal theorems of Peano Arithmetic that are not logically valid, but rely on axioms from PA.

About your argument that a syntactic formula is an idea: as I said, that argument would reduce everything in mathematics to an idea. In that case it's silly to add "is an idea" to every article on a mathematical topic. It's like writing "A novel is an idea, the tokens of which are printed books." – true from one point of view, but not at all relevant to an article about novels. Moreover, as I have pointed out before, the argument that all syntactic things are ideas also seems to ignore mathematical realism entirely. — Carl (CBM · talk) 11:27, 17 November 2009 (UTC)

Carl, you are failing to see the value in it, not because there isn't any. It's because in your experience you haven't need to address these issues. You need to look beyond your own uses of things if you are going to help expand these articles on this wide open publication. You need to let go of your pre-concieved notions about how important, relevant wp:weight, etcetera because there are other people who are looking for these aspects specifically. Its a basic issue of respect quite frankly. If you don't see why it is important to identify a theorem as an idea, then I could easily take a "philosophosis" attitude and say well YOU JUST DON'T KNOW WHAT YOU ARE TALKING ABOUT... If I had a team of philosophers I could get away with being quite mean about it. However all of my attempts appeal to the idea of subject matter versus pov.

Certainly there is the physical object known as the "bicycle" and then there is the idea of a bicycle which is different than the physical object. It is not appropriate or useful to make a distinction like that in an article like bicycle (and this fact and the reason for it should be obvious) because we do not use the idea of a bicycle we use a bicycle. However in mathematics we use language specifically to represent an idea. Yes everything in mathematics is an idea, however there are a few fundamental ideas which all the other ones boil down to (i.e. set, theorem, formula, relation, et al.) You use language to represent an idea and you seem to think its the marks on paper which identify it. However it is not the same as the bicycle because other than your language representation of it a theorem has no existence other than as an idea. The language cannot be regarded as the primary or fundamental essence of the theorem because it is still in question whether or not language can adequately express all kinds of theorems. The letter "b" followed by an "i" followed by a "c", etcetera on the other hand does express the idea of a bicycle non-controversially. So your determined belief that these distinctions are not important enough to mention is completely presumptuous (I don't mean that harshly, fairly stated you are presuming things) and POV. All articles in mathematical logic should account for all of the metalogical distinctions mentioned in the article metalogic. That isn't POV, it's being a responsible editor and should be called for in the mathematics MOS.

I do not agree with your characterization of tautology either. There are several senses in which the term tautology is used in logic. I understand why you believe that tautology 'is fundamentally within propositional logic' however there are other uses, and there is also the extended sense in first order logic. That, to me says that a proper article will make a general statement first and then specify later. This practice should also be in the math MOS. Be well Carl. Pontiff Greg Bard (talk) 20:51, 24 November 2009 (UTC)

Note 1 Investigation? + constructions and lemmas

Note 1 says "However, both theorems and theories are investigations. See Heath 1897 Introduction, The terminology of Archimedes, p. clxxxii:"theorem (θεὼρνμα) from θεωρεἳν to investigate". They might have derived from the word for an investigation but I don't believe they are that now, or does this note mean something else?

I think the Greeks also referred to as problems what we'd now call constructions, Should there should be a Construction (mathematics) rather like Lemma (mathematics) - or does anyone think should they both be subsumed as a section in this article? Dmcq (talk) 20:53, 15 November 2009 (UTC)

We have ruler and compass for Greek-style geometric constructions and constructivism (mathematics) for constructive mathematics in general. 69.228.171.150 (talk) 22:32, 16 November 2009 (UTC)

Formal Theorem

It was obvious from the preceding discussion that two articles (one clearly a POV fork) were not needed so I have redirected Formal Theorem here. If after further discussion and consensus it's determined that there is material in Formal Theorem not adequately covered here with due weight, it can be added to this article. 166.205.136.246 (talk) 21:39, 13 October 2010 (UTC)

This anonymous editor is unclear on the difference between POV and WEIGHT. It would be helpful is he identified himself so we can address any POV issues that he may manifesting historically. I suspect that is why he is choosing to be anonymous.

As for the claim of POV itself, all of the content of formal theorem is objectively stated subject matter. If there are any particular statements which we could address rather than a blanket characterization, that would be helpful.Greg Bard (talk) 01:32, 14 October 2010 (UTC)

Fine, back as it was166.205.138.83 (talk) 22:53, 14 October 2010 (UTC)

The group has had a year to find a mutually acceptable way to integrate the content in a merge. So far, they demonstrated no inclination or competence in doing so. Separating the content portrays more POV than integrating it for reasons I pointed out at WT:MATH.Greg Bard (talk) 01:00, 15 October 2010 (UTC)

The "merge" now performed is still not acceptable. The articles are about different, but related, concepts. I've attempted to revert the merge, but I'm not sure I've done it correctly. — Arthur Rubin (talk) 09:01, 15 October 2010 (UTC)

Um yeah, Arthur, clearly they are not two different concepts. I think you are going off the deep end with that claim. There is no reasonable claim that a theorem, and a theorem expressed in formal language are different concepts because the whole point is that we are able to express the same concept informally and formally. Face it Arthur, this is a genuine case of you POV getting in the way of you seeing reality.Greg Bard (talk) 14:11, 15 October 2010 (UTC)

On the contrary, they clearly are two different concepts, if we can agree and what "are" means. On the other hand, they are fairly well related, so a single article would be acceptable, if "formalism" is minimized in what was previously in theorem before the merge. (Aside from problems with infinitary logic and proofs, which doesn't seem to be anywhere in the article at the moment, as they weren't there before the merge. They should be there.) — Arthur Rubin (talk) 15:39, 15 October 2010 (UTC)

No, not on the contrary. You are confusing the fact that there are different senses of a term, and two different concepts. It absolutely is you and the the others who are imposing POV, whereas I am covering the same concept from different methodology, which is how articles become comprehensive. You really are off base here Arthur, and it really is your POV that is blinding you to that fact. I don't know how you would minimize the coverage more than placing it below "lore" and the other junk. the section itself is quite concise. Be well,Greg Bard (talk) 18:51, 15 October 2010 (UTC)

Formalism

The section should be corrected to remove formalism from it, and (possibly) some of it should be moved into what used to be in formal theorem, later in the article. As an alternative, the school of formalism could be made an explict option in the section, although I doubt that would be an improvement. — Arthur Rubin (talk) 16:20, 15 October 2010 (UTC)

I certainly am open minded to moving duplicated material down into the "formalized" section. I am not much enamored with any of the sections above the "formalized" section.Greg Bard (talk) 19:33, 15 October 2010 (UTC)

Arthur, I am considering temporarily moving all of the sections between "informal .." and "formalized ...." to a subpage for us to reincorporate in a more organized manner. I hope no one takes great offense. I think we can make a great improvement if we reorganize.Greg Bard (talk) 19:45, 15 October 2010 (UTC)

Interpretation

The text (before the subsection "Example") are about something completely different from an "interpretation", and also appear further up the article, in Relation to proof. The "Example" is just wrong. It could be fixed, but it seems more appropriate to have rules than just an axiom schema, even if one were to desire to use the example. — Arthur Rubin (talk) 16:28, 15 October 2010 (UTC)

Again, I am open minded to your constructive criticism, however I still do not see it as valid at all. If the axiom schema should be replaced with something more explicit, I would be open minded however I do not see that it matters at all. I also do not see anything factually wrong with the section AT ALL. Please do point to a particular sentence or sentences which portray an inaccuracy. To say that theorems can be expressed formally is a fact Arthur. Please do educate me, and consider that you do need to articulate your concern for it to be addressed. Like I said, I am open minded. Greg Bard (talk) 19:33, 15 October 2010 (UTC)

May I remind that factually wrong or right is not what Wikipedia is based on. It is based on summarizing what is written in the literature. Citations would be a good idea thanks. Also I'd have thought an article like this should have a little on the history of the idea. Dmcq (talk) 10:55, 16 October 2010 (UTC)

"Temporary" refactor?

This edit, with the edit summary of a "temporary refactor" appears to have removed entire sections of the article, specifically pertaining to the notion of proof and the relation to science. This content should probably be restored pending further discussion. Sławomir Biały (talk) 13:04, 16 October 2010 (UTC)

The relevance of the relation of theorems to scientific theories is a few steps down the road from this from this article. I thought we could start over a bit and only add back material which is relevant. That whole section needed to be re-thought.Greg Bard (talk) 15:18, 16 October 2010 (UTC)

And all the other stuff that was deleted? I suggest the whole lot be restored to the article and dealt with piecemeal. This makes the editing process more transparent. Sławomir Biały (talk) 15:34, 16 October 2010 (UTC)

Yes I agree, the business of removing stuff to improve it personally and then stick it back smacks of ownership to me. Dmcq (talk) 15:39, 16 October 2010 (UTC)

I've put the stuff back in so everyone can edit it and refactor rather than having to search through archives to find it. If it was worth refactoring it was worth leaving till refactored. Dmcq (talk) 16:04, 16 October 2010 (UTC)

Readability v expository

I do not understand the need to remove the squares and triangles. As a pedagogical tool, it helps to teach someone trying to learn that it is not about some formal language they do not understand, but rather any symbols that they may want to use. The brain manipulates symbols made out of meat. One thing that is very clear about the culture at WP:MATH, is that you do not care one bit about someone trying to learn from the article, but rather whether it satisfies yourself and your advanced mathematician buddies. The example was removed as well, and that goes an enormous way toward help someone understand what is going on here. Please consider readers other than yourselves.Greg Bard (talk) 15:14, 16 October 2010 (UTC)

The "theory" example was removed because it was wrong; it didn't support the claimed theorems. However, I tend to agree with Greg on the symbols. It is important to note that a formal language can have arbitrary symbols, not just what we normally call commonly used "characters". — Arthur Rubin (talk) 18:02, 16 October 2010 (UTC)

Squares and triangles

GregBard has reverted my change of all the $\triangle \,$'s and $\square \,$'s to A and B. Who actually believes triangles and squares make the article more accessible? Plus do we really need ${\mathcal {FS}}\,.$ repeated in practically every single sentence after the context has been established? Dmcq (talk) 15:17, 16 October 2010 (UTC)

The example had solid squares and triangles which were very readable, I would prefer we bring that whole section back for reasons I explain above. Perhaps we could use solid symbols instead of outlined ones.Greg Bard (talk) 15:21, 16 October 2010 (UTC)

Perhaps we go back to A and B thanks. And I actually have a certificate in doing some pedagogy thank you so don't say you're better than me at that. Dmcq (talk) 15:25, 16 October 2010 (UTC)

Certificate or not. Using letters doesn't help in terms of pedagogy. The point is that the principle is sound no matter what symbols you use. You insist on using what is familiar to you, why is that? It doesn't help people understand that the principle applies to the unfamiliar as well. If you want to remain in-the-box with your thinking, that is fine. However imposing that our readers must remain in-the-box is a disservice.

You have reinserted a lot of redundant matierial, which I took the time and effort to incorporate thoughtfully. The "in logic" section is not exactly popular among your bretheren, so I have no idea why that is back. "Lore" Really? Would someone other than me get rid of some of that garbage please. Please take the time to edit thoughtfully, don't just be reactionary. Greg Bard (talk) 16:17, 16 October 2010 (UTC) Greg Bard (talk) 16:10, 16 October 2010 (UTC)

I reinserted the stuff you removed with no justification other than you wanted to go off and edit it yourself. So you were saying it was worth keeping but you went and removed it. And please don't go stuffing me into a 'your brethren' box. Dmcq (talk) 16:26, 16 October 2010 (UTC)

Re the 'in-box'. The whole basis of Wikipedia is that it should be in-box. We are supposed to be summarizing what others have done. Which reminds me, more citations would be a very good idea. Dmcq (talk) 16:31, 16 October 2010 (UTC)

Yeah, you have missed the point here. Yes everyone knows that Wikipedia is an encyclopedia and the content is within an objective box. However the reader should, on their own take what they have learned and be able to apply it out side the box. Squares and triangle do help in that regard. The same old Xs and Ys do not.

Most of that content could be left out entirtely as duplicated or irrelevant. I refactored it to a sub page for the sake of making it easier for everyone to see the mess and use it as a source of readding content thoughtfully. Adding it back does not improve this article AT ALL. "Lore?" Seriously, what are you thinking? Greg Bard (talk) 21:43, 16 October 2010 (UTC)

In regard the symbols; I think it's important that we note that a "formal language" and "formal theory" use arbitrary symbols, not just roman letters, but I would like to point out the Greg's "pedagogy" argument is severely flawed. That is one of the things which made "New Math" inaccessible to the teachers, and hence to the students. — Arthur Rubin (talk) 18:06, 16 October 2010 (UTC)

That is off the deep end again Arthur. We don't need to take it to the extreme of "New Math," I'm just saying that squares and triangles are a neutral (NPOV) way to communicate without math jargon. You also seem inconsistent with your above statement. What exactly are you fair-mindedly agreeing with me on? Greg Bard (talk) 21:43, 16 October 2010 (UTC)

I agree that there is a point to using symbols not normally associated with "formulas" or "mathematics"; but that it is not a good pedagogical tool. Fortunately, Wikipedia's purpose is not pedagogical, but to be informative.

As for "Lore", I would use something like "in popular culture" or "in popular mathematical culture", but it seems an appropriate subheading.

Rather than deleting sections which you think may need to be readded, may I suggest tagging them with {{relevance-section}}, or some other appropriate tag. That could be dealt with in a more sensible manner, as we could all see the topic of discussion. — Arthur Rubin (talk) 22:06, 16 October 2010 (UTC)

Theorem vs. theory

Someone please add a little bit about what the difference is. I am sure many will ask the question. Thanks. 82.43.199.163 (talk) 20:21, 7 March 2013 (UTC)

removing POV tag with no active discussion per Template:POV

I've removed an old neutrality tag from this page that appears to have no active discussion per the instructions at Template:POV:

This template is not meant to be a permanent resident on any article. Remove this template whenever:

1. There is consensus on the talkpage or the NPOV Noticeboard that the issue has been resolved
2. It is not clear what the neutrality issue is, and no satisfactory explanation has been given
3. In the absence of any discussion, or if the discussion has become dormant.

Since there's no evidence of ongoing discussion, I'm removing the tag for now. If discussion is continuing and I've failed to see it, however, please feel free to restore the template and continue to address the issues. Thanks to everybody working on this one! -- Khazar2 (talk) 22:11, 21 July 2013 (UTC)

Classification

Youknowwhatimsayin objected to my classifying a theorem as a mathematical proof and undid an edit of mine that had several other changes. Since there was no rationale for undoing them, I will reinstate the edit and argue for my classification here. Any dictionary definition for "theorem" includes two parts, "statement" and "proof", or their equivalents. These are the defining characteristics, and not much else. We can add Theorem to Category:Statements, but there is no Category:Statements that are proved or the equivalent, and if there were such a category I'm not sure what would be in there besides theorem and lemma. But this article contains 59 uses of the word "proof", so Category:Mathematical proofs seems like the category most likely to contain articles that readers of this article would want to find. RockMagnetist(talk) 23:19, 3 October 2015 (UTC)

A theorem is only the last line of some proof. A theorem *has* a proof, but is not itself a proof. Youknowwhatimsayin (talk) 23:37, 3 October 2015 (UTC)

I didn't think it was necessary for me to state something so obvious. Yes, it is not itself a proof, but it is inseparable from proof; a statement without a proof is just a statement. Hence the rest of my reasoning. RockMagnetist(talk) 00:55, 4 October 2015 (UTC)

Categories aren't for merely related things. They are classification of what the things are. You have removed some appropriate categories (syntax, for instance) and are now putting inappropriate categories in. Youknowwhatimsayin (talk) 01:07, 4 October 2015 (UTC)

So you're claiming that a theorem is syntax but isn't proof? RockMagnetist(talk) 01:16, 4 October 2015 (UTC)

I looked a little closer at Category:Mathematical proofs, and it looks like a highly appropriate category. First, the preamble says "This category includes articles on basic topics related to mathematical proofs, including terminology and proof techniques." In other words, not just examples of proofs. Second, theorems are mentioned throughout the article Mathematical proof, 30 times in all. Compare that to Category:Syntax and Syntax, which have zero mentions. RockMagnetist(talk) 21:47, 4 October 2015 (UTC)

What's written on the category page is of secondary importance. The important thing is whether the categorization is appropriate, given the category's name.

The notion of theorem is related to the notion of proof; no one disputes that. But a theorem is not a proof. Since the "proofs" category is a plural count noun, one expects things categorized by it to be instances of that noun, so it's confusing. The "syntax" category doesn't have the same problem, because "syntax" is not a plural count noun. --Trovatore (talk) 21:57, 4 October 2015 (UTC)

I think an appropriate solution is to rename it Category:Mathematical proof (singular). That sort of thing is often done by speedy renaming to align the names of categories with their topic categories. RockMagnetist(talk) 22:08, 4 October 2015 (UTC)

That's not a bad idea. We could then have a "mathematical proofs" category that's really for articles about individual proofs. --Trovatore (talk) 22:21, 4 October 2015 (UTC)

Indeed, it already exists: Category:Article proofs; and there is also Category:Articles containing proofs. All the more reason to rename their parent category! RockMagnetist(talk) 22:24, 4 October 2015 (UTC)

Huh. "Article proofs" is an even worse name in my estimation (it sounds like galley proofs of articles). "Mathematical proofs" would be a much better name. --Trovatore (talk) 22:31, 4 October 2015 (UTC)

I agree, they are a bit strange. Category:Article proofs is actually for "all pages which provide mathematical proofs of adjunct mathematics and physics articles"; and Category:Articles containing proofs is a hidden maintenance category. It doesn't say how something gets into this category. RockMagnetist(talk) 22:41, 4 October 2015 (UTC)

I have started a discussion of the latter category at WikiProject Mathematics. RockMagnetist(talk) 23:17, 4 October 2015 (UTC)

"Unproven theorems"

In the first line of the article, it says "a theorem is a statement that has been proven ". But, for instance, the conjecture known as "Fermat' Last Theorem" was called a theorem long before it was proven. Shouldn't this widespread but less than stringent use of the word be discussed in the article? Or have I missed it? Wdanbae (talk) 14:06, 5 February 2016 (UTC):

The case of Fermat's last theorem is very specific, because Fermat claimed to have a proof, and the statement has been known as "Fermat's last theorem" a long time before the common use of the word "conjecture". This is briefly discussed in section Terminology. D.Lazard (talk) 15:52, 5 February 2016 (UTC)

I thought there were a few other misnomers around, but I am no pro. Wdanbae (talk) 18:56, 5 February 2016 (UTC)

Just because a statement is called a theorem, doesn't make it a theorem. So although Fermat's last theorem had the word "theorem" as part of its name, it was not in fact a theorem until it had been proven. I doubt there are any other examples of a statement being named a theorem, without there being an accepted proof. Paul August ☎ 19:16, 5 February 2016 (UTC)

Well, at least arguably, it's always been a theorem. Before Wiles, it wasn't known to be a theorem.

As a separate point, I am not sure the word "theorem" has always been used this strictly. The English translation of Hilbert's remarks on his first problem has it:

“ The investigations of Cantor on such assemblages of points suggest a very plausible theorem, which nevertheless, in spite of the most strenuous efforts, no one has succeeded in proving. ”

That's Mary Newson's translation; German sources seem to use Satz, which in a non-mathematical context means "sentence", so it's possible that she just chose a less-than-optimal word here. Still, the word "theorem" suggests an element of a "theory"; that doesn't suggest in and of itself that it must be provable. I would be curious to know how long the word has been generally restricted to statements that have proofs. --Trovatore (talk) 22:17, 5 February 2016 (UTC)

The OED defines theorem as follows: "1a. Chiefly Logic and Math. A statement which has been proved to be true, or asserted as true and capable of being proved." An example of each meaning:

• 1806 C. Hutton Course Math. (ed. 5) I. 2 A Theorem is a demonstrative proposition; in which some property is asserted, and the truth of it required to be proved.
• 2010 Nature 11 Mar. 165/3 Until 2001, the Poincaré conjecture was one of the most famous open problems in maths; now it is one more theorem.

Of course, that is consistent with a change in the meaning over time. RockMagnetist(talk) 23:42, 5 February 2016 (UTC)

Strong and Weak Theorems

I tried to make an edit, and it (rightfully) got undone due to lack of references. I was attempting to define the terms strong theorem and weak theorem, which have multiple definitions and have been used in those different contexts in various other Wikipedia pages. So, I think it would be reasonable to try to work together to find the necessary references to make it all cohesive. The three usages I know of, with examples:

• when neither theorem implies the other, because the "stronger" one has both a stronger hypothesis and a stronger conclusion, so it proves more restrictions are true in a more restrictive special case, as with the law of large numbers.
• when a theorem appears to have a stronger hypothesis or conclusion, but actually is equivalent, as with strong induction.
• when two theorems are similar enough so that one forces the other to be true (but not the other way around), in which the forcing theorem is said to be "stronger" than the other "weak" theorem, as with... well, I struggle to find an example at the moment on Wikipedia itself, but I can find a Math StackExchange reference that supports it. (Note, for instance, that the strong law of large numbers would actually not be a stronger theorem by the accepted definition there. The weak law wouldn't be stronger, either, though; both have propositions which only one of them prove, as neither implies the other.) — Preceding unsigned comment added by Jandew (talk • contribs) 23:12, 23 November 2016 (UTC)

It is true that "strong" and "weak" are sometimes used for qualifying theorems. I may add Hilbert's Nullstellensatz and Goldbach's weak conjecture to your examples. However, these are traditional qualifications, which, as far as I know, have never been formalized in any reliable source. Personally, I doubt that a general definition of these terms is useful, and I consider that it could be confusing as giving a mathematical label to terms that have not any mathematical content. In any case, Wikipedia is not the place for defining terms that are not defined in the literature.

By the way (and this confirms that defining "strong" and "weak" may be confusing) your post above contains several errors: two theorems may not be qualified as equivalent nor non-equivalent (your second item); they are true or wrong. Similarly, a theorem cannot "force" another theorem to be true (third item). D.Lazard (talk) 09:04, 24 November 2016 (UTC)

Four color theorem

Four color theorem has human readable proof.

So shouldn't the picture caption be changed or the example removed all together as pointless? Or it could be replaced with something like: "For years this theorem had only compter derived proof but since ..."?Linkato1 (talk) 16:33, 4 October 2017 (UTC)

References

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Theorem. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20060129095451/http://www.cis.upenn.edu/~wilf/AeqB.html to http://www.cis.upenn.edu/~wilf/AeqB.html

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 11:58, 2 December 2017 (UTC)

Article does not correctly cover theorem in logic

The article as it stands seems to me to be trying to put too much into a single article. The lede describes what mathematicians normally consider to be a theorem in mathematics, but in logic it means something different. In logic, a theory is simply a set of sentences, usually closed under logical consequence, and a sentence that is a member of that set is a theorem of that theory. As such, any sentence can be a theorem of some theory or other. It doesn't have to be true (the theory might be unsound), and it doesn't have to be provable (the theory might be unaxiomatizable). If I am reading the history correctly, this article was merged with a different one about formal theories. I would suggest that this merger has had unfortunate consequences, and it should either be undone, or the article should be split into separate sections. As it stands, the article contradicts the article Theory_(mathematical_logic) Dezaxa (talk) 13:21, 22 September 2021 (UTC)

You must be more accurate and quote the sentences of one article that are contradictory with sentences of the other article. If there are errors in one of the articles, they must be clearly specified. In any case splitting an article is a wrong way for fixing errors.

As far as I understand, you are summarizing a particular point of view on mathematical logic, without any source allowing verifying whether this point of view is a common one (see WP:NPOV). As far as I know, it depends on the context (the logic that is used) whether "theorem" is a synonym of "statement" (well formed formula) or if it is the result of a deductive reasoning (proof). This variability is clearly stated in the article: However, according to Hofstadter, a formal system often simply defines all its well-formed formula[s] as theorems. [...] Different sets of derivation rules give rise to different interpretations of what it means for an expression to be a theorem.

So, I strongly oppose your suggestion of undoing an old merger. Another reason for that is that following your suggestion requires an editor who well knows the rules of Wikipedia, and has a wide knowledge of mathematical logic. I doubt that there is an editor who has these competences and is willing doing this job. D.Lazard (talk) 14:19, 22 September 2021 (UTC)

I don't think Dezaxa is suggesting that all well-formed sentences are theorems, but only a particular subset of them closed under logical consequence. --Trovatore (talk) 16:49, 22 September 2021 (UTC)

No theory closed under logical consequence can be "unaxiomatizable"; you can just take all of the statements of the theory to be axioms. In that case they are all provable, having proofs with one step.

It's true that the axioms don't have to be true in the standard interpretation of the language, if there is one, or even in any interpretation in the case of an inconsistent theory. That's a valid criticism of the opening sentence, which currently suggests that axioms need to be "generally accepted"; there is a strong tradition of using axioms that are believed to be false in the standard interpretation (e.g. axiom of constructibility, axiom of determinacy) as means toward an end.

I think this point is too confusing to treat in detail in the first sentence. It could be treated in the body of the article, with an explanatory footnote added to the first sentence to avoid lies to children. --Trovatore (talk) 16:49, 22 September 2021 (UTC)

The very first sentence of the article Theory_(mathematical_logic) correctly states that a theory is a set of sentences in a formal language. The sentences that make up a theory are its theorems. This is standard stuff that you will find in any textbook of mathematical logic. As such, any wff can be a theorem of some theory or another. It does not have to be true and it does not have to be provable. When I said 'axiomatizable' I should perhaps have said 'recursively axiomatizable' - it is fairly common to say simply 'axiomatizable'. But in any case, an axiom set is required to be decidable, so an undecidable theory does not axiomatize itself.

What counts as a theory does not depend on context, or on the logic that is used. If you close a set of sentences under the consequence relation of a non-classical logic, for example, you just get a different theory.

I agree that demerging the article is not a good option, but the lede should make it clear that it relates only to how the word theorem is used in mathematics, not in logic. The section on logic could then make it clear that within logic, theorem has a much broader sense. The relation between the two seems to be that mathematicians are typically only concerned with theorems that are true and/or interesting. Theories that are unsound and banal also contain theorems. Dezaxa (talk) 21:20, 23 September 2021 (UTC)

"An axiom set is required to be decidable." Hmm? Who says? --Trovatore (talk) 00:57, 25 September 2021 (UTC)

Curiously, some sources require an axiom set to be decidable and some don't. Mendelson has: "Most often one can effectively decide whether a given wff is an axiom, in which case a formal theory is called an axiomatic theory". In any event, though one can say in a trivial sense any theory proves its theorems, we normally think of a proof of a theorem as being some non-trivial derivation proceeding from a recursive set of axioms. In this stronger sense at least, not all theorems are provable, since not all theories are recursively axiomatizable. Also, any inconsistent theory has all wffs as theorems, but we wouldn't normally describe such theorems as having been proved. Dezaxa (talk) 19:27, 26 September 2021 (UTC)

Well, whether they've "been" proved or not, they're certainly provable. This does seem to be going off on a tangent, though.

I think there are two separate issues here. One is that the language in the lead currently requires axioms to be "generally accepted", which isn't always true, as sometimes axioms are added instrumentally or provisionally. The other is the disconnect between theorems as formal strings and theorems as propositions; that is, the meanings of those strings. For example, it's a theorem of Peano arithmetic that every natural number is a sum of four squares, but (after some macro expansion that I'm not going to bother with) one formal theorem of formal PA is the string "$\forall n\exists x\exists y\exists z\exists w(n=x*x+y*y+z*z+w*w)$"

The second issue is probably the original motivation for the formal theorem (or whatever it was called) fork of this article, and in some sense it's a fair point, but that article frankly struck me as a POV fork, and the distinction is not one that mathematicians, or even mathematical logicians, really linger over in practice; the formal theorem is usually just treated as a codified way of expressing the proposition.

I think it would be useful to provide an explanatory footnote to address the first issue. The second issue could possibly be treated somewhere in the body somewhere, but I don't think it's necessary to talk about it in the introduction. --Trovatore (talk) 20:12, 26 September 2021 (UTC)

I have rewritten the beginning of the lead in a more encyclopedic tone, and moved its remainder in a specific section called § Epistemological considerations. IMO, most of this section and of a large part of the article consists of WP:OR and nonneutral point of view, and deserve to be completely rewritten. D.Lazard (talk) 07:26, 28 September 2021 (UTC)

The section on theorems in formal logic still needs a substantial revision. I'll have a go at it over the next couple of days. The section called Derivation of a theorem seems to me to be superfluous. One of the maddening problems with this area is that some writers conflate theory with formal system, which seems to me distinctly unhelpful, if not actually just wrong. I agree that the section on Epistemological considerations is odd. Dezaxa (talk) 08:01, 29 September 2021 (UTC)

Thanks D.Lazard; generally nice work. I have some concerns about a couple of bits:

In the main stream of mathematics, the axioms and the inference rules are implicitly those of Zermelo–Fraenkel set theory with the axiom of choice. Generally, an assertion that is explicitly called a theorem is a proved result that is not an immediate consequence of other known theorems.

I think this over-reifies the informal convention that the assumptions you don't have to mention explicitly are ZFC specifically, and particularly suggests that "main stream mathematicians" (by the way, "mainstream" is just one word) think about ZFC very much. Mathematicians who prefer to think of themselves as formalists will sometimes suppose that they're just generating theorems of ZFC, but they hardly ever call out, say, an instance of the Replacement axiom. Moreover, ZFC was not even formalized until the early 1900s — do we really think that the notion of "theorem" has fundamentally changed since the 19th century? I don't.

And finally, it's not even true in practice. Take Fermat's last theorem — it was initially proved using Grothendieck universes, which can't even be formalized in ZFC (they require a mild large-cardinal assumption). As far as I know no one has yet succeeded in removing this assumption, though I haven't kept up on details. And yet few dispute that it's been proven.

The other bit that I have some issues with is the discussion of conjectures, which assert that FLT was "not a theorem" before the proof was found. But of course it was always a theorem; we just didn't know the proof. --Trovatore (talk) 17:50, 29 September 2021 (UTC)

I agree with Travatore that it is overstating the matter to say that ZFC is implicit. Perhaps we could swap the word 'implicitly' for 'commonly'. The sentence "In logic and other areas of mathematics, an assertion can be called a theorem only if the deductive system and the axioms (that is the logical theory) are explicitely specified, since the possibility of proving the assertion may depend on the used theory." - really does not make much sense. In logic, the set of theorems is the theory. I can modify this when I have done revising the section on theorem in logic.

What I have learned from consulting a number of texts is that there are two distinct ways of defining theory in logic. The more popular camp, which includes Enderton and many others, is that a theory is just a set of sentences, usually closed under logical consequence. The other, which includes Mendelson, conflates theory with formal system, making a theory a structure containing a formal language, a deductive system and a set of non-logical axioms. The relationship between them seems to be that a theory in the first sense is the set of sentences proved by a theory in the second sense, i.e. it is the extension of it. The problem now is that if I give both definitions of theory, this article will become inconsistent with the Theory_(mathematical_logic) article, which goes with the first definition. Looks like I may need to edit that one too. Dezaxa (talk) 20:12, 29 September 2021 (UTC)

To be honest I don't think it's particularly important to distinguish between those two senses; they're pretty much equivalent. The other two questions (whether axioms need to be true or otherwise "accepted", and whether theories are collections of meaningful propositions or simply of uninterpreted strings) are probably more important to treat somehow in this article. --Trovatore (talk) 20:39, 29 September 2021 (UTC)

I can add something about that. In proof theory, at least, theories certainly can be collections of uninterpreted strings, though for ordinary working mathematicians this is not how they would use them. Another slight difference I have noted with different accounts is that some authors consider a theory to be closed under semantic consequence ($\models$), and others under derivability ($\vdash$). The first makes it easier to separate a theory from a formal system, but at the cost of making it so that a theory without a formal semantics does not actually qualify as a theory. The second requires a deductive system. Of course if the underlying logic is sound and complete then the two are extensionally equivalent. Dezaxa (talk) 01:07, 30 September 2021 (UTC)

Recent edits

@D.Lazard - your revision to the lead on 3 October is incorrect, and unless you can give a good reason, I propose to revert it. 1. What is an 'assertion'? Is it the same as a statement or a sentence or what? 2. You are conflating the concept of a formal language and a theory. They are completely different things. A language consists of the rules that determine what qualifies as a wff. A theory is a set of closed wffs (sentences). A theorem is an element of a theory. Theorems are not deduced "from the basic terms of a language". 3. Deduction rules are not "part of" a theory. A theory is a set of sentences, a rule is not a sentence, so a rule cannot be part of a theory. Deduction rules only come into the picture when a theory is closed under a derivability relation. Many accounts of theories define a theory to be closed under semantic consequence, which means they can be defined without reference to a deduction system. 4. The sentence about Gödel's incompleteness theorems does not belong in the lead, and in any case is too inaccurate to be useful. Dezaxa (talk) 05:05, 4 October 2021 (UTC)

The disputed edit consisted of replacing a paragraph recently added by Dezaxa. This Dezaxa's paragraph does not respect the guidelines of WP:LEAD, WP:MATH#Article introduction and WP:TECHNICAL. Also, it does not respect the policy of WP:NPOV.

In other words Dezaxa's paragraph is not written in order to be understandable by readers who are not specialists of logic, and, for people who can understand it, it gives a highly partial view of theorems in mathematical logic. Examples of these issues: A reader of this article is not supposed to know the meaning of "formal" in mathematical jargon; this word is used twice in the first sentence, linked to articles that do not exply this term. The concept of formal language is defined in the linked article, but it is a technical tool that should not be needed here. Moreover, the paragraph is highly biased, as it suggests that the theory of formal languages is the only part of logic that deals with theorems, and that logic does not studies proofs of theorems (statements that are not theorems have not their place in the suggested formalism). Also, the paragraph suggests that logic is concerned only by syntax, and that semantics is outside logic. Also, in the part of the lead that is related to logic, it is essential to mention Gödel's incompleteness theorems, and they do not fit in Dezaxa's paragraph (indeed, as they belong to logic, and they are fundamental theorems about theorems, they must mentioned in the lead of an article about theorems).

About may version: My version can certainly be improved. In particular I agree that "assertion" can be replaced by "statement". Also, I'll slightly modify the current version of the article for being coherent with the linked article. D.Lazard (talk) 08:24, 4 October 2021 (UTC)

@D.Lazard - your revision is still incorrect, and your comments about my paragraph are completely unfounded. My paragraph was no more technical or jargon-laden than the one you replaced it with. In fact it was less so. You complain that I used the word 'formal' twice, when your paragraph uses 'formalized', 'well-formed formulas' and 'formal language'. You say the concept of formal language is not needed here, but you have referenced it yourself. My paragraph does not give a partial or biased view of theorems. In the body of the article I have referenced eight standard textbooks of mathematical logic that support the account I have given. I did not anywhere say that "logic does not study proofs of theorems". Also, I did not say that logic is concerned only with syntax: in fact I said the opposite in the body of the article and left the lead neutral as between syntax and semantics. You removed the point about theories being sets and added the footnote that "this is avoided here for clarity and also for not depending on set theory" even though the second paragraph of the lead, which you wrote, says that the axioms and inference rules used to prove theorems are "almost always those of Zermelo-Fraenkel set theory". I don't believe it is essential to mention Gödel's incompleteness theorems in the lead, but if you are going to do it, they need to be stated correctly. Dezaxa (talk) 17:24, 4 October 2021 (UTC)

The problem is not what you wrote, it is what a non-expert reader understands, and what is suggested to them by the formulation. If you talk only of syntax and if you dont explain the reason for which the syntax has been elaborated (that is proving theorems about theorems), your text will not be useful to anybody who has never followed a course of logic, and will definitively be non convenient for an encyclopedia, even if it is correct for a course introduction.

Similarly, Gödel's theorem are among the results that every mathematician should know of. They must be mentioned and linked to in the lead, but the lead is not the place for their formal statement, specially if the article about them is linked to. Again, WP:Wikipedia is not a textbook.

Well, let wait the opinion of other editors. D.Lazard (talk) 18:16, 4 October 2021 (UTC)

ZFC and Grothendieck universes again

First, let me say that I would love love love for it to turn out that the proof of FLT depends essentially on Grothendieck universes and inaccessible cardinals. If you want to get me something for Christmas, make that be true :-)

But I gather that the folks most in a position to have an opinion think that this is very unlikely. The machinery is developed using Grothendieck universes, and it's bothersome to work around it, which is why no one has technically done it. But that is not particularly surprising, contrary to the footnote that claims it's "astonishing", or at least not particularly more surprising than the already possibly surprising fact that you can find out new things about the natural numbers by reasoning with the real numbers, already a large conceptual leap higher.

The reason that this is an issue at all is the language surrounding ZFC, which as I've mentioned above, I find problematic for other reasons. The notion of "theorem" has not changed all that much since Euclid, but ZFC was only laid out in the 20th century. I think that ZFC is a convenient fallback for mathematicians who want to think of themselves as deriving results purely in an axiomatic system, but don't really want to bother with the details. Don't get me wrong — I'm a set theorist by training, and the formalization of ZFC is a signal accomplishment. But I doubt that it merits calling out as part of the background meaning of "theorem". --Trovatore (talk) 05:58, 5 November 2021 (UTC)

Since this comment was posted, the article has been changed a couple of times so that it now includes a brief treatment of Wiles proof of Fermat's last theorem and the Grothendieck universe, including a recent citation asserting that a work-around was found to avoid depending on the machinery based on the Grothendieck universe. i.e. Wiles revised proof follows from ZFC.

That all appears to be correct, and supported by citations. But to my eye, it seems like an unnecessary distraction this early in the article. Mainstream math is usually based on ZFC, but there's an exception that is not really an exception since someone has found a work-around. It just doesn't make sense to include that material at that point in the article.

Also, my understanding is that a large portion of Algebraic Geometry depends on the Grothendieck universe - that would seem to be a better example of an exception to "mainstream math is based on ZFC" than the non-example of Wiles proof. And if we're going to discuss alternatives or exceptions to ZFC, what about the continuum hypothesis or Godel Bernays set theory?

My take is that the article reads better without all that side discussion:

In mainstream mathematics, the axioms and the inference rules are commonly left implicit, and, in this case, they are almost always those of Zermelo–Fraenkel set theory with the axiom of choice (ZFC), or of a less powerful theory, such as Peano arithmetic. Generally, an assertion that is explicitly called a theorem is a proved result that is not an immediate consequence of other known theorems. Moreover, many authors qualify as theorems only the most important results, and use the terms lemma, proposition and corollary for less important theorems.

If we want to go into all that, my take is to treat it later in the article, although it appears to be well covered elsewhere so I don't really think it's necessary. Mr. Swordfish (talk) 12:21, 17 May 2023 (UTC)

I spoke too soon about it being well covered elsewhere. The Wiles's_proof_of_Fermat's_Last_Theorem article doesn't mention the Grothendieck universe or whether it can be proven from ZFC. Mr. Swordfish (talk) 14:30, 17 May 2023 (UTC)

The side discussion is placed here for explaining "almost always". Nevertheless, I agree that it does not belong to the text of the lead. This is why I have moved a less technical version of the side discussion into an explanatory footnote. D.Lazard (talk) 14:32, 17 May 2023 (UTC)