Definicje dotyczace logik modalnych pierwszego rzedu z staa dziedzina nad sygnatura bez funkcji

Formuy w takich logikach sa zbudowane z symboli staych, zmiennych, symboli relacyjnych, klasycznych spójników, unarnych spójników modalnych $\Box$ i $\Diamond$, kwantyfikatorów $\forall$ i $\exists$, oraz nawiasów, w zwyky sposób. Termem jest symbol stay lub zmienna. Klasycznym atomem nazywamy $R_i(t_1, \ldots, t_n)$, gdzie R_i jest symbolem relacyjnym arnosci n a t₁, ..., t_n sa termami.

Definiujemy gebokosc modalnosci formuy $\phi$ jako maksymalne zagniezdzenie modalnosci (tzn. $\Box$ i $\Diamond$) w $\phi$.

Definicja Modelem Kripkego pierwszego rzedu nad sygnatura bez funkcji $\Sigma$ jest struktura $M = \langle D, W, \tau, R, m \rangle$, gdzie D jest zbiorem zwanym dziedzina, $\langle W, \tau, R\rangle$ jest struktura Kripkego, a m jest interpretacja symboli staych i relacyjnych. Dla symbolu c_i, m(c_i) jest elementem D, oznaczonym równiez przez c_i^M. Dla symbolu relacyjnego R_j arnosci n i swiata $w \in W$, m(w)(R_j) jest relacja arnosci n na D, oznaczona równiez przez R_j^M,w.

Relacja spenialnosci jest zdefiniowana w zwyky sposób (zobacz Definicje 5.1.3).

Niech L oznacza nazwe pewnej normalnej logiki modalnej, np. KD. Logika modalna pierwszego rzedu L jest zdefiniowana przez ograniczenie jej klasy dopuszczalnych interpretacji do klasy modeli Kripkego pierwszego rzedu z L-struktura.

Pojecia L-spenialnosc i L-model dla normalnej logiki modalnej pierwszego rzedu L sa zdefiniowane w zwyky sposób.

Dla zbioru formu X i formuy $\phi$, piszemy $X \models_L \phi$ aby oznaczac, ze $\phi$ jest speniona w kazdym L-modelu pierwszego rzedu speniajacym X.