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 [1].

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) [2].

Definicja formalnaEdytuj

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

Co więcej: [1]

  • 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 ∃Rnφ jest formułą logiki drugiego rzędu dla dowolnej n-argumentowej zmiennej relacyjnej R

Nieredukowalność do logiki pierwszego rzęduEdytuj

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 [3].

DowódEdytuj

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

ψ = ψ0 ∧ ψ1 ∧ ψ2

gdzie:

ψ0 = ∀x∀yφ
ψ1 = ∀x∃yG(x,y) ∧ ∀x∀y∀z((G(x,y) ∧ G(x,z)) ⇒ y = z)
ψ2 = ∀x∃yG(y,x) ∧ ∀x∀y∀z((G(y,x) ∧ G(z,x)) ⇒ y = z)

Zdanie ψ0 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 ψ1 mówi, że stopień wyjściowy każdego wierzchołka grafu G jest równy 1, zdanie ψ2 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 [4]. Nazwijmy go G. To prowadzi do sprzeczności, ponieważ w takim wypadku (na mocy zdania ψ2) 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) = ~∃R2(∀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żEdytuj

PrzypisyEdytuj

  1. a b Hedman 2004 ↓, s. 388.
  2. Hedman 2004 ↓, s. 392.
  3. Papadimitriou 1994 ↓, s. 112-114.
  4. Papadimitriou 1994 ↓, s. 111.

BibliografiaEdytuj

  • 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.