Teorema de Laver

El teorema de Laver , en teoría del orden , establece que la incrustación de órdenes totales numerables es un cuasiordenamiento bien definido . Es decir, para toda secuencia infinita de conjuntos numerables totalmente ordenados , existe una incrustación de orden desde un miembro anterior de la secuencia a un miembro posterior. Este resultado se conocía anteriormente como la conjetura de Fraïssé , en honor a Roland Fraïssé , quien la conjeturó en 1948; ^{[ 1 ]} Richard Laver demostró la conjetura en 1971. De forma más general, Laver demostró el mismo resultado para las incrustaciones de orden de uniones numerables de órdenes dispersos . ^{[ 2 ] [ 3 ]}

En matemáticas inversas , la versión del teorema para órdenes numerables se denota FRA (por Fraïssé) y la versión para uniones numerables de órdenes dispersos se denota LAV (por Laver). ^{[ 4 ]} En términos de los "cinco grandes" sistemas de aritmética de segundo orden , se sabe que FRA se sitúa en fuerza en algún punto entre los dos sistemas más fuertes,${\displaystyle \Pi _{1}^{1}}$-CA ₀ y ATR ₀ , y ser más débil que${\displaystyle \Pi _{1}^{1}}$-CA ₀ . Sin embargo, queda abierto si es equivalente a ATR ₀ o si se encuentra estrictamente entre estos dos sistemas en cuanto a fuerza. ^{[ 5 ]}

• Teorema de Dushnik-Miller