¿La teoría de primer orden de una estructura finita tiene un rango cuantificador acotado?

11

Deje que sea ​​cualquier estructura finita. ¿Su teoría de primer orden tiene un rango cuantificador acotado, en el sentido de que hay un tal que para todos con hay un con y ?AT:=TH(A)q∈Nφ∈Tqr(φ)>qφ′∈Tqr(φ′)≤qφ′≡φ

co.combinatorics lo.logic relational-structures D. Rusin
fuente
¿No es esta una pregunta para Mathoverflow en lugar de la teoría de CS?
Andrej Bauer
66
@Andrej, la teoría de modelos finitos y la complejidad descriptiva también se consideran parte de TCS.
Kaveh
1
Excelente, así que es como dijo Bob Harper una vez: las matemáticas son un caso especial de la informática.
Andrej Bauer
La informática también es un caso especial de matemáticas, y ambos son también casos especiales de lógica, y viceversa.
fhyve

Respuestas:

12

La teoría de cualquier estructura finita es el modelo completo. De hecho, es fácil ver que cualquier fórmula es equivalente a una fórmula existencial con un cuantificador por cada elemento de la estructura, después de lo cual todos los cuantificadores de la fórmula original pueden simularse mediante conjunciones y disyunciones. En particular, el número de cuantificadores (por lo tanto, el rango del cuantificador) está limitado por el tamaño de la estructura.

Emil Jeřábek
fuente
En realidad, se necesita un cuantificador universal adicional, que permita expresar que no hay más elementos. En todas las respuestas hay una suposición que debe hacerse explícita: la presencia de la calidad, es decir, que x = y es una fórmula atómica permitida.
Thomas S
No se necesita un cuantificador adicional. Recuerde que no estamos tratando de axiomatizar la teoría de la estructura, sino de encontrar una fórmula equivalente a un módulo dado de la teoría. Y la presencia de igualdad es el estándar universal para la lógica clásica de primer orden. Su ausencia necesitaría ser declarada.
Emil Jeřábek
Ah Tienes razón. "Teoría del módulo". Con respecto a la igualdad: como estamos tratando de explicar cosas fáciles a personas de fuera de Logic, no está de más hacer explícito el marco. Una observación más: reemplazar cuantificadores por conjunciones y disyunciones es perfectamente bueno. Sin embargo, existen alternativas: dado que una fórmula con, digamos, m variables libres define una relación m-aria de A, la nueva fórmula puede, después de adivinar todos los elementos y verificar cuál es cuál (módulo automorfismos), también "enumerar" explícitamente todos tuplas, para las cuales la antigua fórmula produce "verdadero".
Thomas S
3

Para hacer lo que Emil dijo un poco más concreto: considere la fórmula que expresa la existencia de k objetos distintos. Eso muestra que necesitamos un número ilimitado de cuantificadores.

Ahora tiene una fórmula con q cuantificadores y su modelo tiene k objetos. Puede expresar la fórmula indicando que existen k objetos distintos y que la relación entre ellos puede expresarse como un CNF.

Kaveh
fuente