ДОКАЗОВОЮ І ІСТИННІСТЬ

Нехай М - деяка формальна теорія, aip - довільна модель цієї теорії. Тоді якщо F - формула теорії М, то апріорі ця формула або доказова (є теоремою), або не доказова (НЕ-теорема). Інтерпретація ф (/ ^г ) цієї формули є або істиною, тобто y (F) = 1, або брехнею, т. е. ф (С) = 0. Так що для довільної формули Стеоріі М і довільної моделі ф є чотири варіанти взаємин доказовою і істинності:

• (Г ₀ ). F - теорема і ф (/) - помилкове твердження,
• (Г,). F - теорема і ФС / ⁷ ) - істинне твердження,
• (Т ₀ ): F - Ні-теорема і ф (F) - помилкове твердження,
• (Г,): F - Ні-теорема і ф (F) - істинне твердження.

Для довільної формальної теорії М і будь-який її моделі ф символом Т ₀ будемо позначати клас формул теорії М , задовольняють умові (7),), символом 7) будемо позначати клас формул теорії М, удовлетворяю- цщх умові (Г,), символом Т ₀ - клас формул, які відповідають умові (ТД, і Г | - клас формул, які відповідають умові (Г,). Тоді множина всіх формул теорії М, взагалі кажучи, являє собою об'єднання цих чотирьох класів формул

Найбільш доцільним є виконання умов

які означають, що всі теореми інтерпретуються моделлю ф як істинні твердження, а не-теореми - як помилкові. В цьому випадку можна сказати, що формальна теорія М адекватно формалізує предметну область D моделі ф, для якої виконуються ці умови. Якщо Т ₀ Ф 0, то в теорії М є теореми F, для яких ф (F) - помилкове твердження. Така ситуація, ф (F) = 0, вказує на необхідність коригування теорії М для того, чтобь ^ в ній все теореми інтерпретувалися істинними твердженнями. Якщо Т _{ ф0, то в теорії М мають не-теореми F, які все ж є істинними твердженнями. Ситуація Т ₁ ф0 може означати необхідність доповнення теорії М новими аксіомами. Ще більш неприємним є той факт (теорема Тарського), що є формальні системи, в яких клас Г, не є порожнім ні за якої інтерпретації.

Наведемо приклад ситуації Т _х ф0 для формальної системи ( JP ), тобто підберемо для цієї формальної системи інтерпретацію (модель) <р, для якої мають не-теореми, що інтерпретуються як істинні твердження. Розглянемо модель ф, в якій символам алфавіту {a, b, ?} Формальної системи ( JP ) приписані значення: а - твердження «Сократ смертний»,

Ь - фраза «Невірно, що"; позначає заперечення твердження,

? - фраза «еквівалентно тому що»; позначає еквівалентність тверджень.

Тоді аксіома АПА інтерпретується так:

«Сократ смертний еквівалентно тому, що Сократ смертний», а теорема ЬаПЬа означає

«Сократ безсмертний еквівалентно тому, що Сократ безсмертний»,

якщо вважати, що фрази «Невірно, що Сократ смертний» і «Сократ безсмертний» мають ідентичний зміст.

Але для формули ЬЬаПа, що не є теоремою формальної системи (JP ), її інтерпретація є істинним твердженням:

«Неправильно, що Сократ безсмертний еквівалентно тому, що Сократ смертний».

Так що формула F = bbaDa є не-теоремою, що інтерпретується як істинне твердження, тобто F е Т _х .

Розглянемо іншу модель формальної системи ( JP ): а - це число нуль, т. Е. Замість а будемо писати саме число О, b - знак, який вказує на подальше натуральне число, тобто запис Ьа читається як «натуральне число, наступне за числом 0»; коротше кажучи, запис Ьа позначає число 1; запис bba позначає число 2 і т.д.,

? - знак рівності двох натуральних чисел, тобто замість знака? писатимемо знак =.

Для цієї інтерпретації виконуються зазначені вище умови:

Дійсно, аксіома А2А означає 0 = 0. Теорема, наприклад, ЬЬЬаПЬЬЬа означає 3 = 3. А от не-теорема ЬЬаПа означає невірне рівність 2 = 0.