НГУ

Означает ли это, что можно эффективно отделить это "большинство случаев"?

Пмсм, это `большинство случаев' не то что эффективно, его вообще хоть как-то отделить не получится. Выше я давал ссылку на теоремы теории графов, котороые ни то что в РА, они в ZFC не доказуемы. А как-то хорошо отделить доказуемые и недоказуемые в ZFC утверждения люди пытаются давно и до полной победы далеко. Единственное, что, мне кажется, можно тут сказать, что если закодировать теорию графов в арифметику, то множество её теорем, доказуемых в PA, будет эффективно перечислимо, дополнение этого множества таковым не будет. Более того, в этом дополнении будут как истинные недоказуемые теоремы, так и ложные теоремы (т.е. нетеоремы), а уж об отделимости этих множеств люди мечтают давненько.

_________________
Ненужность матана — не повод его не осилить

Вопрос можно превратить в задачу со строгой формулировкой. Формально 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', которое неразрешимо ещё по одной теореме Гёделя.

Собственно, последний абзац - это доказательство того общего факта, что если T1 - неразрешимая теория и T2 - её подтеория, отличная от неё самой, то T1 \ T2 - тоже неразрешимое множество предложений.