множество выводимых формул исчисления предикатов 1-го порядка
Мне вот это нравится, доказательство проще получится. Обозначим это множество
Что значит, что формула выводима? Это значит, что существует доказательство этой формулы.
Как это можно записать формально?
Что это такое? Это проекция. Осталось еще сказать, что свойство "
есть корректное доказательство" разрешимо.
С остальными примерами можно сделать что-то похожее ("Существует конечное вычисление МТ на своем коде", "Существует целый корень многочлена" и т.п.).
-- Пн янв 11, 2010 18:27:42 --Напомню определение примитивно-рекурсивной функции: ф-я примитивно-рекурсивна, если она м.б.получена из базовых с помощью суперпозиции и примитивной рекурсии.
А определение частично рекурсивной функции добавляет еще одну операцию - операцию минимизации
:
есть по определению минимальное
такое, что
, и
определено для всех
.
Так вот, проекция ("существует
такое, что
") и минимизация("найти
такое, что
") похожи.
Так что попробуйте свести минимизацию к проекции.
Еще можно доказать, что те разрешимые свойства, о которых я говорил до этого (насчет второй задачи), примитивно рекурсивны.