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

Теория QE1Ords

Теория QE1Ords – кванторная теория строгого порядка с равенством в языке LQE1Ords с алфавитом AQE1Os и классом ППТ VST. .

 

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

  1. Схемы аксиом классической логики предикатов;
  2. xyz(x<y & y<z x<z);
  3. xy(x<y ¬y<x);
  4. xyz(x=y & y=z x=z);
  5. xy(x=y y=x);
  6. x(x=x);
  7. xy(x=y ¬x<y).

 

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

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

 

Определение класса ППТ VST:
VST={x1, y1, z1, x2, y2, z2, ..., xn, yn, zn, ...}.

 

Определение класса ППФ LQE1Ords:
1) (x, y є VST) => ((x<y), (x=y) є LQOrds);
2) (A, B є LQE1Ords) => (¬A, (A&B), (AB), (AB), (AB) є LQE1Ords);
3) (A(x) є LQE1Ords) => (xA(x), xA(x) є LQE1Ords).