Rachunek predykatów drugiego rzędu

Rachunek predykatów drugiego rzędu – rozszerzenie logiki pierwszego rzędu wzbogacone o kwantyfikatory po zmiennych, które przebiegają relacje.

Istnieją odmiany logiki drugiego rzędu w których dopuszczalny zbiór kwantyfikatorów ograniczony jest jedynie do określonych rodzajów relacji, np. monadyczna logika drugiego rzędu jest częścią logiki drugiego rzędu obejmującym jedynie kwantyfikatory nad relacjami unarnymi (zbiorami).

Definicja formalna

Każda formuła atomowa logiki pierwszego rzędu jest formułą logiki drugiego rzędu.

Co więcej:

• Jeśli φ jest formułą logiki drugiego rzędu to ~φ jest formułą logiki drugiego rzędu
• Jeśli φ i ψ są formułami logiki drugiego rzędu to φ ∧ ψ jest formułą logiki drugiego rzędu
• Jeśli φ jest formułą logiki drugiego rzędu to ∃xφ jest formułą logiki drugiego rzędu dla dowolnej zmiennej x
• Jeśli φ jest formułą logiki drugiego rzędu to ∃Rⁿφ jest formułą logiki drugiego rzędu dla dowolnej n-argumentowej zmiennej relacyjnej R

Nieredukowalność do logiki pierwszego rzędu

Istnieją pewne ograniczenia logiki pierwszego rzędu wynikające z twierdzenia Löwenheima-Skolema, które jednocześnie nie dotyczą logiki drugiego rzędu. Na przykład, za pomocą wyrażenia logiki pierwszego rzędu nie jest możliwe scharakteryzowanie relacji osiągalności pomiędzy wierzchołkami grafu skierowanego (relacja G), co staje się możliwe po dopuszczeniu kwantyfikatora nad relacjami binarnymi.

Dowód

Przypuśćmy, że takie wyrażenie istnieje i nazwijmy je φ(x,y). Teraz rozważmy zdanie ψ:

ψ = ψ₀ ∧ ψ₁ ∧ ψ₂

gdzie:

ψ₀ = ∀x∀yφ
ψ₁ = ∀x∃yG(x,y) ∧ ∀x∀y∀z((G(x,y) ∧ G(x,z)) ⇒ y = z)
ψ₂ = ∀x∃yG(y,x) ∧ ∀x∀y∀z((G(y,x) ∧ G(z,x)) ⇒ y = z)

Zdanie ψ₀ mówi, że graf G jest silnie spójny tzn. dla każdej pary wierzchołków x i y istnieje ścieżka prowadząca od wierzchołka x do wierzchołka y, zdanie ψ₁ mówi, że stopień wyjściowy każdego wierzchołka grafu G jest równy 1, zdanie ψ₂ mówi, że stopień wejściowy każdego wierzchołka grafu G jest równy 1. Graf G spełniający koniunkcje tych trzech zdań (ψ) nazywany jest cyklem.

Ponieważ istnieją cykle o dowolnie dużej, skończonej liczbie wierzchołków, oznacza to, że ψ ma dowolnie duży, skończony model. Na podstawie twierdzenia Löwenheima-Skolema wiadomo, że jeśli jakiś zbiór formuł ma modele dowolnych mocy skończonych to ma również model nieskończony. Nazwijmy go G_∞. To prowadzi do sprzeczności, ponieważ w takim wypadku (na mocy zdania ψ₂) istnieje taki element t uniwersum modelu G_∞, że spełniona jest relacja G_∞(t,0) co jednak jest sprzeczne z nieskończoną mocą tego modelu (nie istnieją cykle nieskończone).

W przypadku logiki drugiego rzędu (dla której twierdzenie Löwenheima-Skolema w ogólności nie obowiązuje) wyrażenie φ(x,y) istnieje, np:

φ(x,y) = ~∃R²(∀u∀v∀w(R(u,u) ∧ (G(u,v) ⇒ R(u,v)) ∧ ((R(u,v) ∧ R(v,w)) ⇒ R(u,w))) ∧ ~R(x,y))

Można zauważyć, że skoro R jest zwrotnym, przechodnim domknięciem G (na mocy trzech pierwszych warunków z koniunkcji), to ~R(x,y) implikuje, że nie istnieje ścieżka z x do y. Zatem zanegowanie całego wyrażenia jest szukanym φ(x,y).

Zobacz też

• Rachunek predykatów pierwszego rzędu
• Twierdzenie Löwenheima-Skolema

Bibliografia

• Shawn Hedman: A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity. Oxford University Press, 2004. ISBN 978-0198529811.
• Christos H. Papadimitriou: Computational Complexity. Addison-Wesley, 1994. ISBN 0-201-53082-1.