Схемы аксиом SE1Ords:
- Схемы аксиом классической логики высказываний;
- (S=M & M=P)
S=P;
- S=P P=S;
- S=S;
- (S
M & MP) SP;
- SP ¬PS;
- S=P ¬SP.
Теория SE1Ords – теория строгого порядка на множествах с равенством в языке LSE1Os с алфавитом ASE1Os и классом ППТ CST. .
Схемы аксиом SE1Ords:
S=P; P=S;M & MP) SP;P ¬PS; ¬SP.
Правила вывода:
Правило modus ponens (правило отделения): ((AB), A) => B.
Определение класса ППТ CST:
CST={S1, P1, Q1, M1, S2, P2, Q2, M2, ..., Sn, Pn, Qn, Mn, ...}.
Определение класса ППФ LSE1Os:
1) (t1, t2 є CST) => ((t1=t2), (t1t2) є LE1Os;
2) (A, B є LE1Os) => (¬A, (A&B), (A
B), (AB), (A
B) є LE1Os).