Lavers teorem

Lavers sats , i ordningsteori , säger att ordningsinbäddning av räknebara totala beställningar är en väl kvasi-ordning . Det vill säga, för varje oändlig sekvens av totalt ordnade räknebara uppsättningar finns det en ordning som bäddas in från en tidigare medlem av sekvensen till en senare medlem. Detta resultat var tidigare känt som Fraïssés gissning , efter Roland Fraïssé, som förmodade det 1948; Richard Laver bevisade gissningen 1971. Mer allmänt bevisade Laver samma resultat för beställningsinbäddningar av countable fackföreningar av spridda beställningar .

₀₀₀₀ I omvänd matematik betecknas versionen av satsen för countable orders FRA (för Fraïssé) och versionen för countable unions av spridda order betecknas LAV (för Laver). När det gäller de "fem stora" systemen för andra ordningens aritmetik , är FRA känt för att falla i styrka någonstans mellan de två starkaste systemen, $\Pi _{1}^{1}$ -CA och ATR , och att vara svagare än $\Pi _{1}^{1}$ -CA . Det är dock fortfarande öppet om det är likvärdigt med ATR eller strikt mellan dessa två system i styrka.

Se även

• Dushnik-Millers teorem