Wynikanie logiczne

Formuła zdaniowa A języka pierwszego rzędu L wynika logicznie ze zbioru formuł zdaniowych X języka L wtw zachodzi: dla każdej interpretacji M języka L: jeżeli wszystkie formuły ze zbioru X są prawdziwe przy interpretacji M, to formuła A jest prawdziwa przy interpretacji M.

Graficznie wynikanie logiczne oznacza się tak:

X ╞ A

Można więc powyższą definicję zapisać tak:

X ╞ A wtw dla każdej interpretacji M: jeżeli X ⊆ Vr(M), to A ∈ Vr(M)

Wynikanie logiczne jest monotoniczne: To, co wynika logicznie z pewnego zbioru formuł, wynika też z każdego „szerszego” zbioru formuł, w którym wyjściowy zbiór jest zawarty.

Jeżeli Y ╞ A oraz Y ⊆ X, to X ╞ A.

Twierdzenie o finitystyczności/zwartości wynikania logicznego

X ╞ A wtw istnieje skończony podzbiór Y zbioru X taki, że Y ╞ A.