Построение непротиворечивой математики как процедуры логического вывода. Использование в качестве универсума собственного класса для обеспечения наибольшей надёжности процедуры логического вывода

ОАО «ГСКБ «Алмаз-Антей», г. Железнодорожный

Для обеспечения наибольшей надёжности процедуры логического вывода целесообразно в качестве универсума использовать собственный класс, то есть данная процедура логического вывода будет работать для аксиоматических систем, включающих в себя понятие собственного класса. Примеры различных аксиоматических систем, как включающих в себя понятие собственного класса, так и не включающих в себя это понятие, приведены в фундаментальной монографии А.А. Френкеля и И. Бар-Хиллела [1].

С учётом вышесказанного поставленная в заголовке статьи задача может быть решена следующим образом.

Ǝ!n ((2^{א n} = א_n ) → ((ω_n × ω_n = ω_n) symbol position: mathematics )) →

( unsigned long semantic = 16384;

unsigned char level_3f[semantic];

unsigned char level_3e[64][semantic];

unsigned char level_3d[64][64][semantic];

unsigned char level_3c[64][64][64][semantic];

unsigned char level_3b[64][64][64][64][semantic];

unsigned char level_3a[64][64][64][64][64][semantic];

unsigned char level_39[64][64][64][64][64][64][semantic];

unsigned char level_38[64][64][64][64][64][64][64][semantic];

unsigned char level_37[64][64][64][64][64][64][64][64][semantic];

unsigned char level_36[64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_35[64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_34[64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_33[64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_32[64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_31[64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_30[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_2f[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_2e[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_2d[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_2c[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_2b[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [semantic];

unsigned char level_2a[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [semantic];

unsigned char level_29[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_28[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_27[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_26[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_25[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_24[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_23[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_22[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_21[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_20[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semanti c];

unsigned char lev- el_1f[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][sem antic];

unsigned char lev- el_1e[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64]

[semantic];

unsigned char lev- el_1d[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64]

[64][semantic];

unsigned char lev- el_1c[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64]

[64][64][semantic];

unsigned char lev- el_1b[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64]

[64][64][64][semantic];

unsigned char lev- el_1a[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64]

[64][64][64][64][semantic];

unsigned char lev- el_19[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64]

[64][64][64][64][64][semantic];

unsigned char lev- el_18[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64]

[64][64][64][64][64][64][semantic];

unsigned char lev- el_17[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][semantic];

unsigned char lev- el_16[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_15[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_14[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_13[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64] [semantic];

unsigned char lev- el_12[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64] [semantic];

unsigned char lev- el_11[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_10[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_0f[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][ 64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_0e[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_0d[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_0c[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_0b[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_0a[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_09[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_08[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_07[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_06[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_05[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_04[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_03[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_02[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char lev- el_01[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64] [64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic];

unsigned char level_00[64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][ 64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][64][semantic]; )

Рассмотрим две различные задачи.

• 1.    Исключение логических противоречий из базы данных, построенной без применения процедуры логического вывода.

• 2.    Построение непротиворечивой математики как процедуры логического вывода.

Во втором случае не требуется проведения большой предварительной работы, однако при этом размер базы данных должен быть больше, благодаря чему увеличивается вероятность возникновения противоречия между потребным размером базы данных и физическими ограничениями, определяющими максимальный возможный размер базы данных.