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

Теория BM

Теория BM – формализация фрагмента Этики Спинозы в языке LBM с алфавитом ABM и классом ППТ VST. .

 

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

  1. Схемы аксиом классической логики предикатов;
  2. xyz(x=y & y=z x=z);
  3. xy(x=y y=x);
  4. x(x=x);
  5. x(Cxx Nx);
  6. x(Kx y(Kxy & Lyx & ¬x=y));
  7. x(Sx Ixx);
  8. x(Sx Dxx);
  9. x(Sx ¬ y (Dxy & ¬y=x));
  10. xy(Axy (Sy & Exy));
  11. xy(Sx Ayx);
  12. xy(Mxy (Sy & Ixy & ¬x=y & Dxy));
  13. x(Gx (Sx & Hx));
  14. x(Qx (Nx & Cxx));
  15. x(Ex Nx);
  16. x(Ixx y(¬x=y & Ixy));
  17. xy((¬x=y & ¬Dxy) Dxx);
  18. x(yCxy zTzx) & x(yTxy zCzx);
  19. xy(Cxy z(Uzy Uzx));
  20. xy(¬zWxyz (v(Uvx & ¬Uvy) & v(Uvy & ¬Uvx) & ¬Dxy & ¬Dyx));
  21. þA A;
  22. x(Nx y(Eyx z(Azy u(z=u))));
  23. xy((¬x=y & Dxy) Pyx);
  24. x(Dxx Cxx);
  25. xy((Dxy Dyx) wWxyw);
  26. xyuv((Eux & Evy) (x=y u=v));
  27. x(Qx ¬yLyx).

 

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

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

 

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

 

Определение класса ППФ LBM:
1) (x, y, z є VST) => (A(x,y), C(x,y), D(x,y), E(x), E(x,y), F(x), H(x), I(x,y), K(x), K(x,y), L(x,y), M(x,y), N(x), P(x,y), Q(x), S(x), T(x,y), U(x,y), W(x,y,z) є LBM);
2) (A, B є LBM) => (¬A, (A&B), (AB), (AB), (AB) є LBM);
3) (A є LBM) => (þA є LBM);
4) (A(x) є LBM) => (xA(x), xA(x) є LBM).

 

Библиография по BM

1. Blum A., Malinovich S. A Formalization of a Segment of Part I of Spinoza´s Ethics // Metalogicon. Roma: L.E.R., 1993.С. 1-14.
2. Malatesta M. On the Inconsistency of Spinoza´s Metaphysics // Metalogicon. Roma: L.E.R., 1993.С. 15-121.
3. Блюм А., Малинович С. Формализация фрагмента Первой части "Этики" Спинозы. Internet: www.theo.ru, 2005.