Определение класса ППТ SST:
SST={a1, b1, c1, d1, a2, b2, c2, d2, ..., an, bn, cn, dn, ...}.
Определение класса ППФ LOrds:
1) (a, b є SST => (a<b є LOrds);
2) (A, B є LOrds) => (¬A, (A&B), (AB), (AB), (AB) є LOrds).
Алфавит AOs языка LOrds
Элементарные константные термы:
a1, b1, c1, d1, a2, b2, c2, d2, ..., an, bn, cn, dn, ... – символы для простых сингулярных термов.
Предикаторы:
< – предикатор строгого порядка.
Пропозициональные связки:
1) ¬ – отрицание;
2) & – конъюнкция;
3) – дизъюнкция;
4) – импликация;
5) – эквивалентность.
Технические знаки:
( – левая и
) – правая скобки.