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

Теория E1Ords

Теория E1Ords – теория строгого порядка с равенством в языке LE1Ords с алфавитом AE1Os и классом ППТ SST. .

 

Схемы аксиом E1Ords:

  1. Схемы аксиом классической логики высказываний;
  2. (a=b & b=c) a=c;
  3. a=b b=a;
  4. a=a;
  5. a=b ¬a<b ;
  6. (a<b & b<c) a<c;
  7. a<b ¬b<a.

 

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

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

 

Определение класса ППТ SST:
SST={a1, b1, c1, d1, a2, b2, c2, d2, ..., an, bn, cn, dn, ...}.

 

Определение класса ППФ LE1Ords:
1) (a, b є SST) => ((a=b), (a<b) є LE1Ords);
2) (A, B є LE1Ords) => (¬A, (A&B), (AB), (AB), (AB) є LE1Ords).