Недавно я спросил, являются ли аксиомы тавтологиями , и получил комментарии, которые показались мне весьма подозрительными. А именно, что вы всегда можете доказать аксиому из самой себя, что вы можете тривиально сказать А, следовательно, А, например
«Аксиомы недоказуемы снаружи системы, но внутри нее они (тривиально) доказуемы».
И другим человеком,
Каждая аксиома имеет доказательство. Если А является аксиомой, ее доказательством является А. Однострочник.
Насколько я понимаю, ни одна система не может доказать свою собственную достоверность, не становясь при этом несовместимой по Гёделю .
Во-первых, если мы примем тривиальные доказательства для различных аксиом, не ошибемся ли мы в итоге? Во-вторых, как насчет, как заметил другой комментатор, аксиомы идентичности? Поскольку один лайнер в основном A = A, не можем ли мы доказать эту аксиому из нее самой? Возможно, можно тривиально доказать, что А, следовательно, А для других аксиом, но разве эта возможность не предоставляется аксиомой, которая утверждает, что А = А? Как это может быть действительным?
Разве по крайней мере одна аксиома не должна по существу утверждать, что все тавтологии верны? И действительно ли можно доказать это самому себе? И ошибаюсь ли я, говоря, что одно из следствий теории Гёделя состоит в том, что такие вещи не могут быть доказаны сами по себе без того, чтобы система не была непротиворечивой?
Да, аксиомы тривиально доказывают себя. Ваш последний вывод, однако, неверен: «А=А» не может быть заменено на А, потому что последнее является символом в формальной системе, а первое является ее объектом. Вы вольны постулировать закон тождества применительно к символам или законам, конечно, в дополнение только к закону тождества для объектов, но это отдельный метазакон. Я думаю, что интуиция ОП может быть чем-то вроде универсалистской концепции логики, которую представляли себе логисты , где все должно быть оправдано изнутри системы, и, следовательно, некоторые аксиомы должны быть в основе и «недоказуемы». Это, конечно, сильно отличается от современной теории формальных систем., где (вслед за Гильбертом) металингвистические манипуляции «молча допускаются», не аксиоматизируя их в самой системе. При необходимости для этой цели может быть введен отдельный метаязык.
Путаница понятна, поскольку в гильбертовских терминах универсалистская концепция смешивает объектный язык формальной системы с метаязыком, используемым для обсуждения утверждений этого языка, см. семантическую теорию истины . Они были разделены Тарским именно для того, чтобы избежать парадоксов самореференции после того, как результаты Гёделя о неполноте сделали универсалистский логицизм непривлекательным. Тарский доказал, что формальная теория первого порядка, содержащая арифметику Пеано и способная выражать утверждения об истинности своих предложений, обязательно несостоятельна. Это его теорема о неопределимости истины , и это может быть «одно из следствий Гёделя», упомянутое в ОП:
Это предполагает серьезное ограничение объема «саморепрезентации». Формулу True(n), расширением которой является T, можно определить, но только с помощью метаязыка, чья выразительная сила выходит за пределы L. Например, предикат истинности для арифметики первого порядка может быть определен в арифметике второго порядка.Однако эта формула может определить предикат истинности только для предложений в исходном языке L. Чтобы определить предикат истинности для метаязыка, потребуется еще высший «метаметазык» и т. д. » .
Необходимая башня метаязыков известна как иерархия Тарского . Именно эта иерархия препятствует формальному выражению таких вещей, как фраза Лжеца «Я неправда».
Теперь перейдем к другому «следствию Гёделя», теореме Лёба, которая, согласно более раннему вопросу ОП, выводит A из A, «может быть показано, нарушает» . Конечно, ничего подобного показать нельзя, но не помогает и то, что «формулировка» теоремы Лёба в Википедии вводит в заблуждение:
" в любой формальной системе F с арифметикой Пеано (РА) для любой формулы P, если в F доказуемо, что "если P доказуемо в F, то P истинно", то P доказуемо в F" .
Не может быть «доказуемо в F», что «если P доказуемо в F, то P истинно», потому что такая вещь потребовала бы, чтобы F содержало свой собственный предикат истинности и, следовательно, было бы несовместимо с Неопределимостью Истины. SEP дает точную формулировку теоремы Лёба и объясняет, почему версия Википедии с «неубедительными терминами» неубедительна:
Чтобы правильно понять теорему Лёба, полезно сначала рассмотреть так называемые «принципы отражения». Выше основное внимание уделялось выражению внутри формальной системы того, что система непротиворечива, т. е. Cons(F) ...Но, естественно, теория должна быть не только непротиворечивой, но и здравой, т. е. доказывать только истинные предложения.Как должна быть выражена обоснованность системы, т. е. утверждение, что все выводимое в системе истинно? это на языке самой системы, это не может быть сделано с помощью одного высказывания, говорящего это, потому что в силу неопределимости истины в языке нет подходящего предиката истинности. выраженные в виде схемы, так называемые Принципы Рефлексии...
Какие именно экземпляры схемы отражения действительно доказуемы в системе? Теорема Лёба дает точный ответ на этот вопрос (при условии, что Prov_F(x) удовлетворяет условиям выводимости). [...] случаи обоснованности (принцип отражения), доказуемые в системе, - это в точности те, которые касаются предложений, которые сами по себе доказуемы в системе. "
пользователь4894
Мауро АЛЛЕГРАНСА
Мауро АЛЛЕГРАНСА
Мауро АЛЛЕГРАНСА