925:@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.
840:@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.
1204:
noting explicitly that theories do not necessarily contain all their theorems, but in general only contain the closed theorems - those which are closed formulas, sentences. Sorry for the nitpicking, if i came to this page it is because the page on
Presburger arithmetic uses the undefined term "nontheorem" to define "decidable", and that leads in that page to a nonnegligible ambiguity about the notion of decidable theory - which does not have to be complete, but the PrA page left this ambiguity and that on "nontheorem" unsettled as PrA is complete, so i added a note near "nontheorem" to clarify.
330:
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
95:
85:
64:
31:
174:
22:
1003:
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". --
612:(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.
816:). 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.
303:
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.
741:
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
1199:
by use of the rule of inference (some finite number of times). » Theorems according to
Enderton's book thus include wff which are not sentences, ie which have free variables, thus since Enderton uses the same definition of "theory" as here there exist a theory which does not contain all its theorems,
1132:
This defines a theory in mathematical logic and says that all members of a theory are theorems of that theory, but it does not define logical theorems - though in the following sentence it is explained that « Usually a theory is understood to be closed under the relation of logical consequence. » but
473:
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
439:
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
302:
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
1207:
There are surely better presentations than i suggest. It may be useful to survey classic logic textbooks and present all the definitions they use, ideally with a short presentation of pros, cons, and typical use cases of each notion - like why a theory is usually defined as a set of closed formulas.
1002:
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
887:
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
760:
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
495:
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
287:
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
1018:
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
994:
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
708:
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
878:
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
431:
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
363:
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
Knowledge (XXG), and has a wide knowledge of mathematical logic. I doubt that there is an editor who has these competences and is
329:
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
1203:
I thus suggest defining the formal concept of theorem in logic directly, and separately defining "theory" in logic. I suggest using
Enderton's definitions - which apply to all quantified logics, with the already present caveat that logical consequence can be replaced by semantic consequence - and
1029:
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
775:
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
712:
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
1128:
one expects a definition of a theorem in logic but it seems that that is missing and that the presentation may be misleading. One finds the informal sentence: «In mathematical logic, a formal theory is a set of sentences within a formal language. A sentence is a well-formed formula with no free
740:
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
732:
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
666:
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
397:
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
432:
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.
249:
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.
257:. It's not true that "many specialists think that it is possible ". 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.
943:
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
888:
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
348:
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
356:). 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:
1101:
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.
1200:
in particular a theory which is not the set of its theorems. The informal definition in this wiki page seems to correspond to Enderton's definition: a theorem is any logical consequence of a set of formulas, it may contain free variables.
615:
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.
745:
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.
500:
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
358:
However, according to Hofstadter, a formal system often simply defines all its well-formed formula as theorems. Different sets of derivation rules give rise to different interpretations of what it means for an expression to be a
245:
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.
603:
716:
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.
910:
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.
1133:
this does not define "theory" or "theorem". In fact the last part seems unconventional and conflicting with the rest of this wiki page: Enderton in his textbook on logic, p110 defines « Then for a set of formulas
435:
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
468:
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
394:
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.
151:
409:
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
1280:
704:
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"
1242:
999:
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.
733:
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
991:
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 :-)
1197:
352:
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
1048:. 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
1270:
794:
440:
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.
1171:
1151:
814:
1069:
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.
939:
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
35:
1285:
474:
are recursively axiomatizable. Also, any inconsistent theory has all wffs as theorems, but we wouldn't normally describe such theorems as having been proved.
1265:
951:
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,
273:
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.
1295:
952:
378:
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. --
141:
1084:
504:
266:
117:
1275:
667:
system, which seems to me distinctly unhelpful, if not actually just wrong. I agree that the section on Epistemological considerations is odd.
1022:
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.
698:. Generally, an assertion that is explicitly called a theorem is a proved result that is not an immediate consequence of other known theorems.
1290:
1036:
In mainstream mathematics, the axioms and the inference rules are commonly left implicit, and, in this case, they are almost always those of
310:
289:
108:
69:
288:
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.
889:
1024:
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
1037:
691:
1260:
44:
639:
I have rewritten the beginning of the lead in a more encyclopedic tone, and moved its remainder in a specific section called
398:
accepted"; there is a strong tradition of using axioms that are believed to be false in the standard interpretation (e.g.
254:
1129:
variables. A sentence that is a member of a theory is one of its theorems, and the theory is the set of its theorems. »
428:
331:
228:
399:
883:; this word is used twice in the first sentence, linked to articles that do not exply this term. The concept of
207:
314:
293:
50:
306:
1092:
1074:
195:
190:
1176:
868:
742:
709:
we really think that the notion of "theorem" has fundamentally changed since the 19th century? I don't.
270:
116:
on Knowledge (XXG). If you would like to participate, please visit the project page, where you can join
892:, and they do not fit in Dezaxa's paragraph (indeed, as they belong to logic, and they are fundamental
94:
403:
21:
1008:
880:
766:
722:
621:
459:
418:
383:
278:
1209:
1107:
963:
916:
656:
369:
213:
100:
84:
63:
947:
Similarly, Gödel's theorem are among the results that every mathematician should know of. They
1088:
1070:
690:
In the main stream of mathematics, the axioms and the inference rules are implicitly those of
872:
864:
860:
779:
648:
353:
1213:
1156:
1136:
1045:
930:
845:
821:
799:
751:
672:
479:
445:
410:
338:
209:
173:
1041:
884:
695:
644:
1087:
article doesn't mention the Grothendieck universe or whether it can be proven from ZFC.
737:
the theory. I can modify this when I have done revising the section on theorem in logic.
253:
Moreover, the sentence is almost entirely false, see for example all the discussions in
1004:
762:
718:
617:
609:
455:
414:
379:
274:
255:
https://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof
1254:
1103:
959:
912:
683:
652:
365:
1026:. It just doesn't make sense to include that material at that point in the article.
926:
856:
841:
817:
747:
668:
598:{\displaystyle \forall n\exists x\exists y\exists z\exists w(n=x*x+y*y+z*z+w*w)}
475:
441:
334:
113:
90:
1120:
Possibly missing (and conflicting partial) definition of a theorem in logic
1033:
My take is that the article reads better without all that side discussion:
643:. IMO, most of this section and of a large part of the article consists of
761:
strings) are probably more important to treat somehow in this article. --
1019:
on the Grothendieck universe. i.e. Wiles revised proof follows from ZFC.
1125:
855:
The disputed edit consisted of replacing a paragraph recently added by
713:
haven't kept up on details. And yet few dispute that it's been proven.
640:
995:
footnote that claims it's "astonishing", or at least not particularly
1030:
ZFC, what about the continuum hypothesis or Godel Bernays set theory?
686:; generally nice work. I have some concerns about a couple of bits:
1233:
templates on this page, but the references will not show without a
211:
488:
Well, whether they've "been" proved or not, they're certainly prov
454:"An axiom set is required to be decidable." Hmm? Who says? --
1217:
1111:
1096:
1078:
1012:
967:
934:
920:
849:
825:
770:
755:
726:
676:
660:
625:
483:
463:
449:
422:
387:
373:
342:
318:
297:
282:
214:
167:
15:
859:. This Dezaxa's paragraph does not respect the guidelines of
608:
The second issue is probably the original motivation for the
1083:
I spoke too soon about it being well covered elsewhere. The
492:. This does seem to be going off on a tangent, though.
900:, they must mentioned in the lead of an article about
1281:
Knowledge (XXG) level-4 vital articles in Mathematics
1179:
1159:
1139:
802:
782:
507:
112:, a collaborative effort to improve the coverage of
1052:only the most important results, and use the terms
1191:
1165:
1145:
808:
788:
597:
325:Article does not correctly cover theorem in logic
1173:will be the formulas which can be obtained from
776:theory to be closed under semantic consequence (
265:I removed the sentence "A notable exception is
1271:Knowledge (XXG) vital articles in Mathematics
1044:(ZFC), or of a less powerful theory, such as
958:Well, let wait the opinion of other editors.
222:This page has archives. Sections older than
8:
706:(by the way, "mainstream" is just one word)
871:. Also, it does not respect the policy of
651:, and deserve to be completely rewritten.
304:
58:
1178:
1158:
1138:
801:
781:
506:
427:The very first sentence of the article
126:Knowledge (XXG):WikiProject Mathematics
60:
19:
1266:Knowledge (XXG) level-4 vital articles
1085:Wiles's_proof_of_Fermat's_Last_Theorem
357:
267:Wiles's proof of Fermat's Last Theorem
232:when more than 5 sections are present.
1286:B-Class vital articles in Mathematics
7:
1192:{\displaystyle \Gamma \cup \Lambda }
982:First, let me say that I would love
978:ZFC and Grothendieck universes again
953:WP:Knowledge (XXG) is not a textbook
106:This article is within the scope of
1221:
49:It is of interest to the following
1186:
1180:
1160:
1140:
796:), and others under derivability (
532:
526:
520:
514:
508:
14:
1296:Top-priority mathematics articles
226:may be automatically archived by
879:know the meaning of "formal" in
641:§ Epistemological considerations
172:
129:Template:WikiProject Mathematics
93:
83:
62:
29:
20:
890:Gödel's incompleteness theorems
146:This article has been rated as
1276:B-Class level-4 vital articles
1227:<ref group=lower-alpha: -->
1218:21:23, 13 September 2024 (UTC)
826:01:07, 30 September 2021 (UTC)
771:20:39, 29 September 2021 (UTC)
756:20:12, 29 September 2021 (UTC)
727:17:50, 29 September 2021 (UTC)
677:08:01, 29 September 2021 (UTC)
661:07:26, 28 September 2021 (UTC)
626:20:12, 26 September 2021 (UTC)
592:
538:
496:as propositions; that is, the
484:19:27, 26 September 2021 (UTC)
464:00:57, 25 September 2021 (UTC)
450:21:20, 23 September 2021 (UTC)
423:16:49, 22 September 2021 (UTC)
388:16:49, 22 September 2021 (UTC)
374:14:19, 22 September 2021 (UTC)
343:13:21, 22 September 2021 (UTC)
1:
1235:{{reflist|group=lower-alpha}}
120:and see a list of open tasks.
1291:B-Class mathematics articles
1064:for less important theorems.
1013:05:58, 5 November 2021 (UTC)
865:WP:MATH#Article introduction
1038:Zermelo–Fraenkel set theory
968:18:16, 4 October 2021 (UTC)
941:you dont explain the reason
935:17:24, 4 October 2021 (UTC)
921:08:24, 4 October 2021 (UTC)
850:05:05, 4 October 2021 (UTC)
692:Zermelo–Fraenkel set theory
429:Theory_(mathematical_logic)
332:Theory_(mathematical_logic)
1312:
1126:Theorem#Theorems in logic
406:) as means toward an end.
400:axiom of constructibility
240:
145:
78:
57:
1112:14:32, 17 May 2023 (UTC)
1097:14:30, 17 May 2023 (UTC)
1079:12:21, 17 May 2023 (UTC)
789:{\displaystyle \models }
649:nonneutral point of view
364:willing doing this job.
319:05:49, 17 May 2023 (UTC)
298:22:50, 16 May 2023 (UTC)
283:12:52, 16 May 2023 (UTC)
241:Grothendieck's universes
152:project's priority scale
1166:{\displaystyle \Gamma }
1146:{\displaystyle \Gamma }
809:{\displaystyle \vdash }
109:WikiProject Mathematics
1261:B-Class vital articles
1193:
1167:
1147:
810:
790:
599:
271:Grothendieck universes
261:Removed by me as WP:OR
229:Lowercase sigmabot III
1194:
1168:
1148:
811:
791:
600:
269:, which involves the
43:on Knowledge (XXG)'s
36:level-4 vital article
1177:
1157:
1137:
800:
780:
505:
404:axiom of determinacy
132:mathematics articles
881:mathematical jargon
1241:template (see the
1189:
1163:
1153:, the theorems of
1143:
908:About may version:
806:
786:
595:
101:Mathematics portal
45:content assessment
707:
321:
309:comment added by
236:
235:
201:
200:
166:
165:
162:
161:
158:
157:
1303:
1248:
1247:
1246:
1240:
1236:
1232:
1228:
1198:
1196:
1195:
1190:
1172:
1170:
1169:
1164:
1152:
1150:
1149:
1144:
1046:Peano arithmetic
815:
813:
812:
807:
795:
793:
792:
787:
705:
604:
602:
601:
596:
411:lies to children
231:
215:
187:
186:
176:
168:
134:
133:
130:
127:
124:
103:
98:
97:
87:
80:
79:
74:
66:
59:
42:
33:
32:
25:
24:
16:
1311:
1310:
1306:
1305:
1304:
1302:
1301:
1300:
1251:
1250:
1238:
1234:
1230:
1226:
1224:
1222:
1175:
1174:
1155:
1154:
1135:
1134:
1124:In the section
1122:
1042:axiom of choice
980:
885:formal language
838:
798:
797:
778:
777:
696:axiom of choice
503:
502:
327:
263:
243:
227:
216:
210:
181:
131:
128:
125:
122:
121:
99:
92:
72:
40:
30:
12:
11:
5:
1309:
1307:
1299:
1298:
1293:
1288:
1283:
1278:
1273:
1268:
1263:
1253:
1252:
1220:
1188:
1185:
1182:
1162:
1142:
1121:
1118:
1117:
1116:
1115:
1114:
1099:
1067:
1066:
1065:
1031:
1027:
1020:
979:
976:
975:
974:
973:
972:
971:
970:
956:
945:
905:
876:
837:
834:
833:
832:
831:
830:
829:
828:
805:
785:
738:
731:
729:
714:
710:
702:
701:
700:
681:
679:
637:
636:
635:
634:
633:
632:
631:
630:
629:
628:
613:
610:formal theorem
606:
594:
591:
588:
585:
582:
579:
576:
573:
570:
567:
564:
561:
558:
555:
552:
549:
546:
543:
540:
537:
534:
531:
528:
525:
522:
519:
516:
513:
510:
493:
437:
433:
407:
395:
392:
391:
390:
361:
350:
326:
323:
311:132.230.196.70
290:110.174.47.229
262:
259:
242:
239:
234:
233:
221:
218:
217:
212:
208:
206:
203:
202:
199:
198:
193:
183:
182:
177:
171:
164:
163:
160:
159:
156:
155:
144:
138:
137:
135:
118:the discussion
105:
104:
88:
76:
75:
67:
55:
54:
48:
26:
13:
10:
9:
6:
4:
3:
2:
1308:
1297:
1294:
1292:
1289:
1287:
1284:
1282:
1279:
1277:
1274:
1272:
1269:
1267:
1264:
1262:
1259:
1258:
1256:
1249:
1244:
1219:
1215:
1211:
1205:
1201:
1183:
1130:
1127:
1119:
1113:
1109:
1105:
1100:
1098:
1094:
1090:
1089:Mr. Swordfish
1086:
1082:
1081:
1080:
1076:
1072:
1071:Mr. Swordfish
1068:
1063:
1059:
1055:
1051:
1047:
1043:
1039:
1035:
1034:
1032:
1028:
1025:
1021:
1017:
1016:
1015:
1014:
1010:
1006:
1000:
998:
992:
990:
989:
985:
977:
969:
965:
961:
957:
954:
950:
946:
944:introduction.
942:
938:
937:
936:
932:
928:
924:
923:
922:
918:
914:
909:
906:
903:
899:
895:
891:
886:
882:
877:
874:
870:
866:
862:
858:
854:
853:
852:
851:
847:
843:
835:
827:
823:
819:
803:
783:
774:
773:
772:
768:
764:
759:
758:
757:
753:
749:
744:
739:
736:
730:
728:
724:
720:
715:
711:
703:
699:
697:
693:
688:
687:
685:
680:
678:
674:
670:
665:
664:
663:
662:
658:
654:
650:
646:
642:
627:
623:
619:
614:
611:
607:
589:
586:
583:
580:
577:
574:
571:
568:
565:
562:
559:
556:
553:
550:
547:
544:
541:
535:
529:
523:
517:
511:
499:
494:
491:
487:
486:
485:
481:
477:
472:
467:
466:
465:
461:
457:
453:
452:
451:
447:
443:
438:
434:
430:
426:
425:
424:
420:
416:
412:
408:
405:
401:
396:
393:
389:
385:
381:
377:
376:
375:
371:
367:
362:
360:
355:
351:
347:
346:
345:
344:
340:
336:
333:
324:
322:
320:
316:
312:
308:
300:
299:
295:
291:
285:
284:
280:
276:
272:
268:
260:
258:
256:
251:
247:
238:
230:
225:
220:
219:
205:
204:
197:
194:
192:
189:
188:
185:
184:
180:
175:
170:
169:
153:
149:
143:
140:
139:
136:
119:
115:
111:
110:
102:
96:
91:
89:
86:
82:
81:
77:
71:
68:
65:
61:
56:
52:
46:
38:
37:
27:
23:
18:
17:
1239:{{notelist}}
1237:template or
1223:Cite error:
1206:
1202:
1131:
1123:
1061:
1057:
1053:
1049:
1023:
1001:
996:
993:
987:
986:
983:
981:
948:
940:
907:
901:
897:
893:
869:WP:TECHNICAL
839:
836:Recent edits
734:
689:
638:
497:
489:
470:
328:
305:— Preceding
301:
286:
264:
252:
248:
244:
237:
223:
178:
148:Top-priority
147:
107:
73:Top‑priority
51:WikiProjects
34:
1058:proposition
123:Mathematics
114:mathematics
70:Mathematics
1255:Categories
1225:There are
1243:help page
1062:corollary
1040:with the
1005:Trovatore
763:Trovatore
743:extension
719:Trovatore
694:with the
618:Trovatore
471:axiomatic
456:Trovatore
415:Trovatore
380:Trovatore
275:Erxnmedia
196:Archive 2
191:Archive 1
39:is rated
1229:tags or
1104:D.Lazard
1050:theorems
960:D.Lazard
913:D.Lazard
902:theorems
898:theorems
894:theorems
684:D.Lazard
653:D.Lazard
498:meanings
366:D.Lazard
359:theorem.
307:unsigned
224:365 days
179:Archives
1231:{{efn}}
873:WP:NPOV
861:WP:LEAD
682:Thanks
436:theory.
354:WP:NPOV
349:errors.
150:on the
41:B-class
1210:Plm203
927:Dezaxa
896:about
857:Dezaxa
842:Dezaxa
818:Dezaxa
748:Dezaxa
669:Dezaxa
476:Dezaxa
442:Dezaxa
335:Dezaxa
47:scale.
1054:lemma
645:WP:OR
28:This
1214:talk
1108:talk
1093:talk
1075:talk
1060:and
1009:talk
997:more
988:love
984:love
964:talk
949:must
931:talk
917:talk
867:and
846:talk
822:talk
767:talk
752:talk
723:talk
673:talk
657:talk
647:and
622:talk
490:able
480:talk
460:talk
446:talk
419:talk
413:. --
384:talk
370:talk
339:talk
315:talk
294:talk
279:talk
142:Top
1257::
1245:).
1216:)
1187:Λ
1184:∪
1181:Γ
1161:Γ
1141:Γ
1110:)
1095:)
1077:)
1056:,
1011:)
966:)
933:)
919:)
904:).
863:,
848:)
824:)
804:⊢
784:⊨
769:)
754:)
735:is
725:)
717:--
675:)
659:)
624:)
616:--
587:∗
575:∗
563:∗
551:∗
533:∃
527:∃
521:∃
515:∃
509:∀
482:)
462:)
448:)
421:)
402:,
386:)
372:)
341:)
317:)
296:)
281:)
1212:(
1106:(
1091:(
1073:(
1007:(
962:(
955:.
929:(
915:(
875:.
844:(
820:(
765:(
750:(
721:(
671:(
655:(
620:(
605:"
593:)
590:w
584:w
581:+
578:z
572:z
569:+
566:y
560:y
557:+
554:x
548:x
545:=
542:n
539:(
536:w
530:z
524:y
518:x
512:n
501:"
478:(
458:(
444:(
417:(
382:(
368:(
337:(
313:(
292:(
277:(
154:.
53::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
