Sufficient conditions for the existence of undecidable indirectly reflective sentences.pdf Формула F языка теории первого порядка T называется неразрешимой в T, если ни сама формула F, ни её отрицание - F не являются теоремами этой теории. Арифметика Пеано PA является одной из хорошо известных теорий первого порядка и играет важную роль в логике. В теории PA можно построить неразрешимое в этой теории предложение. Нелогическими символами PA являются константа 0, унарный функциональный символ S (который обозначает функцию следования) и два бинарных функциональных символа + и х. Для любого неотрицательного целого n терм SS...S0 (S повторяется n раз) будем обозначать п. Такие термы называются нумералами. Курт Гёдель первым построил неразрешимое предложение для теории PA. Он сделал это посредством процедуры, которая сейчас называется арифметизацией. Пусть U есть объединение трех множеств: множества символов теории T, множества всех выражений (термов и формул) T и множества всех конечных последовательностей выражений T. Пусть N - множество целых неотрицательных чисел и функция g: U ^ N инъективна. Функция g называется арифметизацией теории T, если выполнены следующие условия: (1) g эффективно вычисляема; (2) существует алгоритм, который определяет, принадлежит ли данное положительное целое m множеству значений функции g и, если это так, то алгоритм находит объект x е U такой, что g(x) = m. Функция g определяется стандартным способом [1, 2]. Число g(x) называется гёделевым номером объекта x. Если g(x) = n, мы определяем Tx! как нумерал п. Это позволяет заменить утверждения о формальной теории эквивалентными теоретико-числовыми предложениями и затем выразить такие предложения в самой формальной теории. В работе [3] изучались косвенно рефлексивные предложения в PA (в предположении, что данная теория ю-непротиворечива [1]), говорящие о доказуемости и/или опровержимости. Рассматривались некоторые совокупности таких предложений, и доказывалось, что среди них существуют неразрешимые предложения. Настоящая работа является продолжением и обобщением [3]. Мы формулируем общие условия и доказываем, что они достаточны для существования неразрешимых косвенно рефлексивных предложений. Исходным утверждением является следующая теорема о косвенной рефлексивности, доказанная в [3]. Теорема 1. Пусть m - положительное целое число и B1, B2, ..., Bm - формулы теории PA, для которых свободные переменные содержатся в списке x1, x2, ..., xm. Тогда существуют такие формулы G1, G2, Gm, что |- G1 ~ B^GA fel, ..., TGml), |- G2 ~ B2(fG1l, Gl, ..., TGml), |- Gm ~ Bm^G^, rG2l, TGml) в теории PA. Как известно [1], отношение Provable(n, m): «формула с гёделевым номером n является выводимой (доказуемой) в PA и ее доказательство имеет номер m» выразимо в PA некоторой формулой Pr(x, y), т.е.: 1) если Provable(n, m) истинно, то |- Pr(n, m), 2) если Provable(n, m) ложно, то |-i Pr(n, m). Формула P(n) = 3y Pr(n, y) выражает следующее свойство: «формула с гёделе-вым номером n является выводимой (доказуемой) в PA». Из теоремы 1 при m = 1 получаем известную лемму о рефлексии. Пусть B(x) произвольная формула формальной арифметики, имеющая единственную свободную переменную x. Тогда можно построить замкнутую формулу A, такую, что |- A ~ B(TaI). Формула A рефлексивна и «говорит о себе», что она обладает свойством B. В частности, имеется формула G, для которой |- G ~ -P(TgI), т.е. G «говорит о себе», что она недоказуема в PA. Гёдель, неявно используя лемму о рефлексии, получил формулу G и доказал, что она неразрешима в PA (предполагая, что ^ является ю -непротиворечивой теорией). Определение ш-непротиворечивости [1, с. 158]. Пусть T - теория первого порядка с теми же самыми символами, что и PA. Теория T называется ю-непро-тиворечивой, если для всякой формулы

Скачать электронную версию публикации