palaisien писал(а):
Означает ли это, что можно эффективно отделить это "большинство случаев"?
Вопрос можно превратить в задачу со строгой формулировкой. Формально PA и ZFC - теории в разных языках, хотя по смыслу PA является частью ZFC. Чтобы сделать это формально верным, можно добавить в язык ZFC предикат N(x) для множества натуральных чисел и операции сложения и умножения на этом множестве, получив теорию ZFC'. Поскольку этот предикат и операции выразимы формулами в исходном ZFC, такая добавка ничего по существу не изменит (мы получим т.н. консервативное расширение ZFC), то есть ZFC и ZFC' будут по сути одной и той же теорией. В частности, будет существовать очевидный алгоритм, сводящий вопрос об истинности предложения в одной теории к вопросу об истинности в другой.
Далее, можно немного переделать аксиомы PA так, чтобы они относились к множеству N(x) со сложением и умножением, получив теорию PA'. Вновь теории PA и PA' будут по сути одной и той же теорией. Теперь PA' будет уже формальной подтеорией ZFC', и исходную задачу можно свести к вопросу о сложности множества предложения языка PA', лежащих в ZFC' \ PA'.
Легко показать, что оно будет неразрешимо, то есть не будет существовать алгоритма, который бы, получая на вход предложение, мог бы ответить, лежит оно в этом множестве или нет. Чтобы доказать это, можно взять предложение Con(PA') языка PA', выражающее, что PA' непротиворечиво. Мы знаем, что оно лежит в ZFC', и не лежит в PA' по теореме Гёделя. Затем можно рассмотреть отображение, которое предложению B языка PA' сопоставит предложение B & Con(PA'). Если B лежит в ZFC', то второе предложение попадёт в ZFC' \ PA', если не лежит, то не попадёт. Тем самым мы сведём к нашему множеству множество следствий из ZFC' в языке PA', которое неразрешимо ещё по одной теореме Гёделя.