з з загальнозначущих формул дають загальнозначущі формули => будь-яка теорема - общезначима.
Утв.: (Гедель)
Будь-який розділ математики може бути описаний як теорія 1-го порядку.
Приклад теорії 1-го порядку, аксіоматична арифметика. Теорема Геделя про неповноту
Нехай задана довільна теорія 1-го порядку. Якщо до її алфавітом додати предикат "рівність": P (x, y) = (з опр.) "X = y" і в число власних аксіом ввести 2 аксіоми:
(AP 1 ): " x (x = x)
(AP 2 ): (x = y) Г (A (x) Г A (y))
при будь-якому предикате А, то отримана теорія зв. теорією 1-го порядку з рівністю.
Розглянемо МП 1-го порядку з рівністю. {Це т. зв. аксіоматика Пеано}
Додамо в алфавіт символ const 0 - "нуль", функціональний символ '- "штрих"
x '- це (х + 1),
і довільний набір функціональних символів (+, *) (ф-й), і додаємо аксіоми:
1) x = y Г (y = z Г x = z)
2) Г№ (x '= 0)
) x = y Г x '= y' 3 ') x' = y ' Г x = y
) x + 0 = x
) x + y ' Г (x + y ) '
) x * 0 = 0
) x * y '= x * y + x
)
для будь-якого предиката А здійснимо:
9) [A (0) & ( " x (A (x) Г A (x ')))] Г A (x), A (0) - базис індукції, ( " x (A (x) Г A (x '))) - індуктивний крок.
Ця аксіома визначає метод математичної індукції.
Арифметика - основа всієї математики. Вона вкл. в будь-який розділ математики.
Теорема Геделя про повноту:
Будь формальна аксіоматична теорія, вкл-я в себе формальну арифметику неповна, тобто в ній є змістовно істинні затв-я, недоведені в рамках цієї теорії.
Слідство:
1) будь-яку теорію, яка містить арифметику, не можна поповнити так, щоб вийшла система була сповнена щодо загальнозначущих формул.
2) така аксіоматична теорія нерозв'язна.
) несуперечливість формальної арифметики не можна встановити, користуючись засобами самої арифметики.
попереджання нормальна форма
Визначення 3.68. Формула називається попереджання нормальною формою, якщо вона має вигляд
x1Q2x2. . . QkxkA, (3.28)
де Qi ? { ? < span align = "justify">, ? }, а формула A не містить кванторів. Зауважимо, що для попереджання нормальної форми виконується умова розділеності змінних.
Теорема 3.69. Для будь-якої формули існує еквівалентна їй попереджання нормальна форма. p align="justify"> Доказ теореми 3.69 використовує індукцію з побудови формули. Для індуктивного кроку нам потрібно набір пар еквівалентних формул, який забезпечується наступною лемою. p align="justify"> Лемма 3.70. Нехай A, B - формули обчислення предикатів, причому B не містить змінної x. p align="justify"> Тоді наступні пари формул еквівалентні
| ?
