84:
74:
53:
22:
518:
Probably, intended meaning here was something like this. Considered theories in first order arithmetical languages, have standard axiomatizations by schemes, where parameters ranges over some classes of formulas. Languages of such theories could be extended by family of unary predicates and schemes
211:
There are several ways of defining "proof theoretic strength". One way is to say that T is stronger than S if T proves Con(S). Another is the say T is stronger than S if the ordinal of T is larger than S. These are very related but not identical. But if there is no better place for "proof theoretic
374:
The article claims that something called
Rudimentary Function Arithmetic has ordinal omega^2. But there's no citation of where that information comes from, Knowledge doesn't have an article on that system of arithmetic, and if you Google the phrase "Rudimentary Function Arithmetic", you only get
188:
Hi. I am curious about the redirect from proof-theoretic strength. I don't see why it is here. Sure, they are closely related, but from what I've seen, the proof-theoretic strength is not usually defined by the proof-theoretic ordinal. Rather, one logic is stronger than another if it proves more
267:
Hmm. Maybe it is worth starting an article on that topic, then. Do you have anything in mind for large cardinal axioms except that they tend to be linearly ordered by consistency strength? Because the consistency strength of subsystems of artithmetic is equally interesting in that case. — Carl
511:-sentences. But number of theories in the list actually are theories in the language of first-order arithmetic or extensions of this language by some functional symbols. So one would need to consider conservative extensions of this theories in order to talk about provable Π
782:) to be an excellent new development in ordinal analysis, but since it is currently a preprint from late last year, is it too soon to add to Knowledge? If it is found to be appropriate, the "?" in the "Ordinal" column of the table of ordinal analyses can be replaced by
328:
I don't understand this well enough to add anything to the article about it yet, but it looks relevant. It is an approach to ordinal analysis on very weak (e.g. polynomially bounded) arithmetic systems for which the usual approach is too coarse.
519:
could be extended by extending classes of formulas by allowing new predicates in atomic formulas. But because I am not familiar with calculations of proof-theoretic ordinal of some mentioned weak theories (for example IΔ
825:
733:
140:
680:
635:
546:"Small Rathjen Ordinal", only Google results are Lihachevss and a Googology Wiki blog post which attributes the name to the former. And Lihachevss is known to contain incorrect info
162:
This page would be greatly improved if there were a specific citation for the ordinal of each of the listed theories (e.g. where one can find the proof that I\Sigma_1 is w^w, etc).
711:
302:
ordinal analysis. The interesting thing here is that his analysis shows that a theory, say PA, has a different ordinal than PA + Con(PA), two theories which the more traditional Π
776:
355:
Is that really right? I can see how they might be related to each other but a little more explanation would be helpful (maybe in the ELEMENTARY article). Thanks.
855:
130:
850:
413:, and while I know about rudimentary functions from set theory the connection isn't obvious. The person who added the term to the article (in
106:
732:
The table contains links to reference footnotes, up to reference number sixteen. However, under notes, there is no reference number sixteen.
169:
524:
330:
307:
196:
382:
737:
356:
97:
58:
465:
785:
33:
722:
713:) isn't as large as some ordinals before it in the table, so it's probably a good idea to move it further up the table
836:
643:
598:
528:
334:
173:
311:
200:
21:
576:
569:
422:
386:
242:
360:
685:
39:
83:
378:
348:
I see that "elementary function arithmetic", a proof system with ordinal strength ω, is linked to to
234:
192:
165:
250:
828:
714:
584:
105:
on
Knowledge. If you would like to participate, please visit the project page, where you can join
489:
430:
418:
89:
73:
52:
832:
718:
588:
326:
754:
298:
concept). Lev
Beklemishev has introduced and explored a finer (as in less coarse) notion of Π
238:
397:
Good question, I'd like to know this as well. I imagine it's some minor variation on IΔ
405:), but the term does not appear, let alone any ordinal analysis, in Hájek and Pudlák's
246:
290:
It also might be worth noting that the proof-theoretic ordinals defined here are the Π
844:
485:
426:
275:
219:
401:(and perhaps a "rudimentary" function is one that can be proved to be total in IΔ
549:
Edit: Also a
Googology Wiki talk page, but this was a suggestion for a name of ψ
102:
640:
I asked someone who made a list of proof-theoretic ordinals and they said that
349:
79:
507:-ordinal. It works fine with theories for which we can talk about provable Π
741:
532:
493:
434:
390:
364:
338:
315:
280:
254:
224:
204:
177:
375:
references to this
Knowledge article. So can we get a source for this?
271:
215:
583:
I will need to search in other places to see if I've missed any sources
479:-predicates augmented by an axiom asserting that exponentiation is total
503:
The current definition of proof-theoretic ordinal in the article is Π
542:
Some of these names appear to have no reliable external source:
15:
459:+ exp" on separate lines, implying that they're different:
212:
strength" to redirect it may as well redirect here. — Carl
594:
820:{\displaystyle \psi _{\Omega }(\mathbb {I} _{\omega })}
779:
451:
414:
353:
788:
757:
688:
646:
601:
515:-sentences. So some clarifications are needed here.
101:, a collaborative effort to improve the coverage of
819:
770:
746:
705:
674:
629:
575:"Small Stegert Ordinal", so far this article and
568:"Large Rathjen Ordinal", so far this article and
461:
8:
19:
675:{\displaystyle \psi (\Omega _{M+\omega })}
630:{\displaystyle \psi (\Omega _{M+\omega })}
47:
808:
804:
803:
793:
787:
762:
756:
747:Arai's recent analysis of Pi_n-collection
697:
691:
690:
687:
657:
645:
612:
600:
407:Metamathematics of First-Order Arithmetic
425:), so it's probably best to ask him. --
370:What is Rudimentary Function Arithmetic?
189:(when the other is interpreted in it).
734:2001:1A81:7327:7900:2502:7D8E:8500:AA5F
294:ordinals (since well-foundedness is a Π
49:
475:+ exp, arithmetic with induction on Δ
7:
95:This article is within the scope of
706:{\displaystyle {\textrm {KPM}}^{+}}
352:, a computational complexity class.
38:It is of interest to the following
794:
759:
654:
609:
14:
856:Mid-priority mathematics articles
499:Ordinals of arithmetical theories
115:Knowledge:WikiProject Mathematics
851:Start-Class mathematics articles
118:Template:WikiProject Mathematics
82:
72:
51:
20:
563:) using Extended Buchholz's OCF
523:), I not completely sure here.
135:This article has been rated as
814:
799:
742:16:27, 15 September 2022 (UTC)
723:21:44, 18 September 2021 (UTC)
669:
650:
624:
605:
466:elementary function arithmetic
435:10:50, 30 September 2013 (UTC)
391:15:55, 29 September 2013 (UTC)
1:
339:00:43, 7 September 2009 (UTC)
306:analysis cannot distinguish.
109:and see a list of open tasks.
533:14:37, 15 October 2015 (UTC)
494:09:25, 8 January 2015 (UTC)
365:07:36, 27 August 2010 (UTC)
872:
751:I find Arai's analysis of
281:01:09, 17 March 2009 (UTC)
255:00:57, 17 March 2009 (UTC)
225:03:06, 16 March 2009 (UTC)
205:00:29, 16 March 2009 (UTC)
837:08:05, 15 June 2024 (UTC)
241:; and is also related to
178:10:02, 5 April 2008 (UTC)
134:
67:
46:
771:{\displaystyle \Pi _{n}}
322:dynamic ordinal analysis
316:21:02, 22 May 2010 (UTC)
184:proof-theoretic strength
141:project's priority scale
577:Large countable ordinal
570:Large countable ordinal
243:large cardinal property
98:WikiProject Mathematics
821:
778:-collection (added in
772:
707:
676:
631:
482:
441:EFA not the same as IΔ
28:This article is rated
822:
773:
708:
677:
632:
827:by its theorem 1.4.
786:
755:
686:
644:
599:
579:are the only results
572:are the only results
235:consistency strength
121:mathematics articles
455:lists "EFA" and "IΔ
817:
768:
728:Missing references
703:
672:
627:
90:Mathematics portal
34:content assessment
694:
538:Names of ordinals
484:Is that correct?
381:comment added by
279:
223:
195:comment added by
180:
168:comment added by
155:
154:
151:
150:
147:
146:
863:
826:
824:
823:
818:
813:
812:
807:
798:
797:
777:
775:
774:
769:
767:
766:
712:
710:
709:
704:
702:
701:
696:
695:
692:
681:
679:
678:
673:
668:
667:
636:
634:
633:
628:
623:
622:
454:
393:
269:
213:
207:
163:
123:
122:
119:
116:
113:
92:
87:
86:
76:
69:
68:
63:
55:
48:
31:
25:
24:
16:
871:
870:
866:
865:
864:
862:
861:
860:
841:
840:
802:
789:
784:
783:
758:
753:
752:
749:
730:
689:
684:
683:
653:
642:
641:
638:
608:
597:
596:
562:
561:
560:
552:
540:
522:
514:
510:
506:
501:
478:
474:
458:
452:current article
450:
447:
444:
409:or in Pohler's
404:
400:
376:
372:
346:
324:
305:
301:
297:
293:
239:equiconsistency
190:
186:
170:130.226.132.226
160:
120:
117:
114:
111:
110:
88:
81:
61:
32:on Knowledge's
29:
12:
11:
5:
869:
867:
859:
858:
853:
843:
842:
816:
811:
806:
801:
796:
792:
765:
761:
748:
745:
729:
726:
700:
671:
666:
663:
660:
656:
652:
649:
637:
626:
621:
618:
615:
611:
607:
604:
593:
581:
580:
573:
566:
565:
564:
558:
556:
554:
550:
539:
536:
525:83.149.209.253
520:
512:
508:
504:
500:
497:
481:
480:
476:
472:
469:
456:
446:
442:
439:
438:
437:
402:
398:
371:
368:
345:
342:
331:67.122.211.205
323:
320:
308:174.29.174.220
303:
299:
295:
291:
288:
287:
286:
285:
284:
283:
260:
259:
258:
257:
228:
227:
197:68.188.164.248
185:
182:
159:
156:
153:
152:
149:
148:
145:
144:
133:
127:
126:
124:
107:the discussion
94:
93:
77:
65:
64:
56:
44:
43:
37:
26:
13:
10:
9:
6:
4:
3:
2:
868:
857:
854:
852:
849:
848:
846:
839:
838:
834:
830:
809:
790:
781:
763:
744:
743:
739:
735:
727:
725:
724:
720:
716:
698:
664:
661:
658:
647:
619:
616:
613:
602:
592:
590:
586:
578:
574:
571:
567:
548:
547:
545:
544:
543:
537:
535:
534:
530:
526:
516:
498:
496:
495:
491:
487:
470:
467:
463:
462:
460:
453:
440:
436:
432:
428:
424:
420:
419:Ben Standeven
416:
412:
408:
396:
395:
394:
392:
388:
384:
383:69.248.140.74
380:
369:
367:
366:
362:
358:
354:
351:
343:
341:
340:
336:
332:
327:
321:
319:
317:
313:
309:
282:
277:
273:
266:
265:
264:
263:
262:
261:
256:
252:
248:
244:
240:
237:redirects to
236:
232:
231:
230:
229:
226:
221:
217:
210:
209:
208:
206:
202:
198:
194:
183:
181:
179:
175:
171:
167:
157:
142:
138:
132:
129:
128:
125:
108:
104:
100:
99:
91:
85:
80:
78:
75:
71:
70:
66:
60:
57:
54:
50:
45:
41:
35:
27:
23:
18:
17:
750:
731:
639:
582:
541:
517:
502:
483:
448:
411:Proof Theory
410:
406:
377:— Preceding
373:
357:67.119.3.248
347:
325:
318:logicmuffin
289:
233:Notice that
187:
161:
137:Mid-priority
136:
96:
62:Mid‑priority
40:WikiProjects
191:—Preceding
164:—Preceding
112:Mathematics
103:mathematics
59:Mathematics
30:Start-class
845:Categories
350:ELEMENTARY
780:this edit
415:this edit
247:JRSpriggs
595:Size of
486:Melchoir
427:Gro-Tsen
379:unsigned
193:unsigned
166:unsigned
158:Untitled
829:C7XWiki
715:C7XWiki
585:C7XWiki
139:on the
445:+ exp?
36:scale.
682:(for
464:EFA,
417:) is
833:talk
738:talk
719:talk
589:talk
529:talk
490:talk
449:The
431:talk
423:talk
387:talk
361:talk
335:talk
312:talk
276:talk
251:talk
220:talk
201:talk
174:talk
693:KPM
559:...
344:EFA
272:CBM
216:CBM
131:Mid
847::
835:)
810:ω
795:Ω
791:ψ
760:Π
740:)
721:)
665:ω
655:Ω
648:ψ
620:ω
610:Ω
603:ψ
591:)
553:(Ω
531:)
492:)
471:IΔ
433:)
389:)
363:)
337:)
314:)
274:·
253:)
245:.
218:·
203:)
176:)
831:(
815:)
805:I
800:(
764:n
736:(
717:(
699:+
670:)
662:+
659:M
651:(
625:)
617:+
614:M
606:(
587:(
557:Ω
555:Ω
551:0
527:(
521:0
513:1
509:1
505:1
488:(
477:0
473:0
468:.
457:0
443:0
429:(
421:(
403:0
399:0
385:(
359:(
333:(
310:(
304:1
300:n
296:1
292:1
278:)
270:(
249:(
222:)
214:(
199:(
172:(
143:.
42::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
