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

Теория SE₁Ordn

Теория SE₁Ordn – теория нестрогого порядка на множествах в языке LSE₁Ons с алфавитом ASE₁Ons и классом ППТ CST. .

Правила вывода:

Правило modus ponens (правило отделения): ((AB), A) => B.

Определение класса ППТ CST:
CST={S₁, P₁, Q₁, M₁, S₂, P₂, Q₂, M₂, ..., S_n, P_n, Q_n, M_n, ...}.

Определение класса ППФ LSE₁Ons:
1) (t₁, t₂ є CST) => ((t₁=t₂), (t₁t₂) є LPO;
2) (A, B є LPO) => (¬A, (A&B), (AB), (AB), (AB) є LPO).