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

Теория E1

Теория E1 – бескванторная теория равенства в языке LE1 с алфавитом AE1 и классом ППТ SST. .

 

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

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

 

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

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

 

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

 

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