Akademik

формула к.-л. (логико-математического) исчисления, одновре- менно не доказуемая и не опровержимая средствами этого исчисления. (Соответственно формула, доказуемая или опровержимая в исчислении, наз. разрешимой в нем.) Термин "Н. ф." прилагается, как правило, лишь по отношению к замкнутым формулам, что объясняется трудностями, связанными с возможностью различных интерпретаций, открытых (незамкнутых) формул. Напр., при наиболее распространенной интерпретации, т.н. интерпретации всеобщности, формула А(х) интерпретируется так же, как и ее замыкание ∀хА(х), так что формула Α(x), – интерпретируемая в этом случае как ∀xA(x), – не выражает отрицания предложения, выражаемого формулой А(х), и в применении к таким формулам понятие Н. ф. оказывается довольно бессодержательным. (Подробнее об интерпретациях формул со свободными переменными см. в ст. Предикатов исчисление.)

Наличие в исчислении Н. ф. означает, по определению, его (простую) неполноту. Наиболее известными примерами Н. ф. служат формулы, выражающие свою собственную недоказуемость, доказательство существования к-рых составляет предмет разл. модификаций знаменитой теоремы Гёделя о неполноте формальной арифметики. Неразрешимость (одновременная недоказуемость и неопровержимость) к.-л. формулы не означает, вообще говоря, невозможности установления истинности (или ложности) выражаемого ею предложения к.-л. cодержат. образом. Так, Н. ф., фигурирующие в доказательствах теоремы Гёделя, как раз являются (в предположении непротиворечивости системы, содержащей Н. ф.) содержательно истинными. Желая подчеркнуть именно формальный характер понятий доказуемости и опровержимости, часто говорят о формально Н. ф. (соответственно о формально разрешимых). С др. стороны, эпитет "неразрешимое" прилагают и непосредственно к предложениям к.-л. теории; именно так этот термин был впервые (1931) введен в основополагающей работе К. Гёделя. О методологич. и филос. (гносеологич.) значениях понятия Н. ф., см. Полнота, Метатеория и лит. при этих статьях.