Информационная система по формальным теориям

Язык LBM с классом ППТ VST и алфавитом ABM

Определение класса ППТ VST:
VST={x₁, y₁, z₁, x₂, y₂, z₂, ..., x_n, y_n, z_n, ...}.

Определение класса ППФ LBM:
1) (x, y, z є VST) => (A(x,y), C(x,y), D(x,y), E(x), E(x,y), F(x), H(x), I(x,y), K(x), K(x,y), L(x,y), M(x,y), N(x), P(x,y), Q(x), S(x), T(x,y), U(x,y), W(x,y,z) є LBM);
2) (A, B є LBM) => (¬A, (A&B), (AB), (AB), (AB) є LBM);
3) (A є LBM) => (þA є LBM);
4) (A(x) є LBM) => (xA(x), xA(x) є LBM).

Алфавит ABM языка LBM

Элементарные переменные термы:
x₁, y₁, z₁, x₂, y₂, z₂, ..., x_n, y_n, z_n, ... – индивидные переменные термы.

Предикаторы:
1) A² – двухместный предикатор "... атрибут ...";
2) C² – двухместный предикатор "... причина ...;
3) D² – двухместный предикатор "... зависит от ...";
4) E¹ – одноместный предикатор "... вечено";
5) E² – двухместный предикатор "... сущность ...";
6) F¹ – одноместный предикатор "... конечно";
7) H¹ – одноместный предикатор "... абсолютно бесконечно";
8) I² – двухместный предикатор "... содержится в ...";
9) K¹ – одноместный предикатор "... конечно в своем роде" (in suo genere finita);
10) K² – двухместный предикатор "... и ... имеют одну и ту же природу";
11) L² – двухместный предикатор "... ограничивает ...";
12) M² – двухместный предикатор "... модус (состояние) ..." (mode);
13) N¹ – одноместный предикатор "... иметь необходимое существование";
14) P² – двухместный предикатор "... первее ...";
15) Q¹ – одноместный предикатор "... свободно";
16) S¹ – одноместный предикатор "... субстанция";
17) T² – двухместный предикатор "... действие ...";
18) U² – двухместный предикатор "... знает (познает) ...";
19) W³ – трехместный предикатор " ... и ... общее ...";
20) = – предикат равенства.

Кванторы
1) – квантор всеобщности;
2) – квантор существования.

Пропозициональные связки:
1) ¬ – отрицание;
2) & – конъюнкция;
3) – дизъюнкция;
4) – импликация;
5) – эквивалентность.

Модальные операторы:
þ – оператор истинности.

Технические знаки:
( – левая и
) – правая скобки.