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

Теория Sa2

Теория Sa2 – теория связки a в языке LS_a с алфавитом AS_a и классом ППТ CST. .

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

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

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

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