Operacja konsekwencji

Z Wikipedii, wolnej encyklopedii

Niech J będzie językiem sformalizowanym. Oznaczmy przez FORMJ zbiór wszystkich poprawnie zbudowanych formuł języka J. Funkcję C: 2FORMJ |→ 2FORMJ (tj. funkcję, której argumentami i wartościami są zbiory poprawnie zbudowanych formuł języka J) nazywamy operacją konsekwencji w języku J wtw dla dowolnych podzbiorów X, Y zbioru FORMJ spełnione są następujące warunki:

  1. X ⊆ C(X),
  2. C(C(X)) ⊆ C(X),
  3. jeżeli X ⊆ Y, to C(X) ⊆ C(Y).


Gdy ponadto dla dowolnego A ∈ FORMJ spełniony jest warunek:

A ∈ C(X) wtw istnieje skończony podzbiór Z zbioru X taki, że A ∈ C(Z),

to C nazywamy finitystyczną operacją konsekwencji w J.