El teorema de Laver , en teoría del orden , establece que la incrustabilidad de órdenes totales numerables es un buen cuasiordenamiento . Es decir, para cada 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 conjetura de Fraïssé , en honor a Roland Fraïssé , quien la conjeturara en 1948; [1] Richard Laver demostró la conjetura en 1971. De manera más general, Laver demostró el mismo resultado para incrustaciones de orden de uniones numerables de órdenes dispersos . [2] [3]
En matemáticas inversas , la versión del teorema para órdenes contables se denota FRA (por Fraïssé) y la versión para uniones contables 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 encuentra en algún punto entre los dos sistemas más fuertes, -CA 0 y ATR 0 , y es más débil que -CA 0 . Sin embargo, sigue abierto si es equivalente a ATR 0 o estrictamente entre estos dos sistemas en fuerza. [5]
