Может ли доказательство от противоречия работать без закона исключенного среднего?

19

Недавно я думал о достоверности доказательства противоречием. В течение последних нескольких дней я читал материалы по интуиционистской логике и теоремам Годеля, чтобы посмотреть, дадут ли они мне ответы на мои вопросы. Прямо сейчас у меня все еще есть вопросы (возможно, связанные с новым материалом, который я прочитал), и я надеялся получить ответы на некоторые вопросы.

( ВНИМАНИЕ : вы собираетесь приступить к чтению контента с очень запутанными логическими основами, воспринимать все с недоверием, предполагается, что это вопрос, а не ответ, в нем много недоразумений).

Я думаю, что мой главный вопрос: как только мы показали, что не А приводит к некоторому противоречию, поэтому не А должно быть ложным, тогда мы идем и заключаем, что А должно быть правдой. Эта часть имеет смысл (особенно если я принимаю закон исключенного среднего как нечто, что имеет смысл), но меня беспокоит то, как на самом деле происходит доказательство от противоречия. Сначала мы начинаем с А, а затем просто применяем аксиомы и правила умозаключений (скажем, механически) и видим, куда это нас ведет. Это обычно достигает противоречия (скажем, что A истинно или и верно). Мы заключаем, что не A должно быть ложным, поэтому A истинно. Все в порядке. Но мой вопрос в том, какие гарантии у формальных системϕ A¬φϕесли бы я применил тот же процесс, но начал с А, что я бы не получил там противоречия ? Я думаю, что в доказательстве есть какое-то скрытое предположение, противоречащее тому, что если бы аналогичный процесс в А не противоречил , каких у нас гарантий, что бы этого не произошло? Есть ли доказательства, которые невозможно? Другими словами, если бы у меня была Turning Machine (TM) (или super TM), которая работала вечно, она пробовала все логические шаги из каждой аксиомы, начиная с предположительно истинного утверждения , что гарантирует, что оно НЕ ОСТАНОВИТСЯ из-за нахождения противоречия ?A

Затем я связал свой прошлый вопрос с теоремой Гёделя о неполноте, которая выглядит примерно так:

Формальная система F, которая выражает арифметику, не может доказать свою непротиворечивость (в пределах F).

Это в основном дало мне понять, что если это правда, то последовательность, то есть гарантирование того, что A и не A не произойдет, невозможна. Таким образом, оказалось, что доказательство от противоречия просто неявно предполагает, что согласованность каким-то образом гарантирована (в противном случае, почему бы просто пойти дальше и заключить, что A истинно, доказав, что A не возможно, если оно еще не знало, что согласованность и противоречие, где хорошо, для любой пары утверждения A, а не A)? Это неправильно или я что-то упустил?

Тогда я подумал: хорошо, давайте просто включим в наши аксиомы правило исключенного среднего, и тогда все проблемы будут решены. Но потом я понял: подожди, если мы сделаем это, мы просто решаем проблему, а не решаем ее. Если я просто заставляю свою систему быть последовательной по определению, это не обязательно означает, что она на самом деле является последовательной ... верно? Я просто пытаюсь разобраться в этих идеях, и я не совсем уверен, что делать, но это то, что я осознаю после нескольких дней чтения материала и просмотра видео почти во всех аспектах этих концепций, противоречие, исключительная середина, интуиционистская логика, теоремы Годеля о полноте и неполноте ...

В связи с этим, кажется, что фактически невозможно прямо доказать, что что-то ложно, без правила исключенного среднего (или противоречия). Кажется, что системы доказательств хороши в доказательстве истинных утверждений, но, насколько я понимаю, не способны прямо показать, что все ложно. Возможно, то, как они это делают, более косвенно с противоречием (где они показывают, что что-то должно быть ложным, или случается плохое), или с исключенным средним (где знание истинного значения только одного А или нет А дает нам правду другого) или приведение контрпримеров (которые в основном показывают, что верно обратное, поэтому косвенно использует закон исключенного среднего). Наверное, я действительно хочу конструктивное доказательство того, что что-то не так?

Я думаю, если бы я мог знать, что если я докажу, что А не является ложным (скажем, я принимаю противоречие), то это действительно нормально, и мне не нужно бесконечно применять все правила вывода и аксиомы к А, и я гарантирую, что А выиграл не достичь противоречия. Если бы это было правдой, то, я думаю, я мог бы легче принять доказательство от противоречия. Это правда или гарантия второй незавершенности Годеля - я не могу этого иметь? Если я не могу иметь этого тогда, то, что меня озадачивает, как это возможно из-за того, что математики столько лет занимались математикой, что мы не нашли несоответствия? Нужно ли полагаться на эмпирические доказательства последовательности? Или, например, я prof F последовательный, показывая, что superF доказывает F, но, поскольку мне никогда не понадобится superF и просто F, я не могу быть доволен тем, что действительно работает?


Я только что заметил, что моя жалоба также распространяется на прямые доказательства. Итак, если бы я сделал прямое доказательство А, то я знаю, что А это правда ... но откуда мне знать, что если бы я сделал прямое доказательство не А, то я бы также не получил правильное доказательство? Вроде тот же вопрос, только немного другой акцент ....

Чарли Паркер
источник
1
Комментарии не для расширенного обсуждения; этот разговор был перенесен в чат .
DW
Интуиционистская логика отвергает общее утверждение об исключенном исключении среднего / двойного отрицания, но может иметь место для конкретных предложений. В лучшем случае доказательство двойного отрицания в интуиционистской логике просто означает, что поиск положительного доказательства не бесполезен.
Карл Дамгаард Асмуссен

Ответы:

30

Вы спросили (я делаю ваш вопрос немного четче): «Какая формальная гарантия того, что не может случиться, что оба и приводят к противоречию?» Вы, кажется, беспокоитесь, что если логика противоречива, то доказательство от противоречия проблематично. Но это совсем не так.р¬pp

Если логика непоследовательна, то доказательство с помощью противоречия все еще остается действительным правилом рассуждения, но как и ее отрицание, а также правило, которое гласит, что из мы можем сделать вывод, что вы следующий папа. Несоответствие в логике ничего не делает недействительным: напротив, оно проверяет все !1+1=2

Есть еще один возможный источник путаницы: название вашего вопроса может быть истолковано как подразумевающее, что закон исключенного среднего говорит о том, что логика последовательна. Это неверно. Последовательность логики сводится к «это не тот случай, когда и утверждение, и его отрицание имеют доказательства», а исключенное среднее - это правило, которое позволяет нам доказывать утверждения вида .p¬p


Дополнение: я не понимаю, почему этот вопрос вызывает столько дискуссий. У меня проблемы с пониманием того, что на самом деле является дилеммой, и, насколько я могу судить, вопрос возникает из-за какого-то недопонимания. Если кто-то может прояснить вопрос, я буду благодарен. Также я просто хотел бы обратить внимание на следующие моменты:

  1. Доказательство от противного и исключенное среднее эквивалентны друг другу, поэтому название, как написано, бессмысленно. Конечно, мы не можем иметь одно без другого, они эквивалентны.

  2. Из того, что я могу понять из продолжительной дискуссии в этом вопросе, ОП, кажется, говорит или беспокоится, что несогласованность в логике делает доказательство недействительным. Это неверно, как я указал выше. Я был бы признателен за ответ от ОП: может ли ОП увидеть, как несоответствие в логике (т. Е. Возможность доказать все) не лишает законной силы какие-либо доказательства?

  3. Я нахожу вероятным, но не могу сказать наверняка, что ФП считает, что закон исключенных средних состояний не может оба параметра: и (с формулой: ). Это не исключено середина. Его иногда называют законом непротиворечия, и он доказуем (без исключенного среднего).¬ p ¬ ( p ¬ p )p¬p¬(p¬p)

  4. ФП считает, что «невозможно прямо доказать, что что-то не так, без исключенной середины». Он сбивает с толку доказательство отрицания и доказательство противоречием, что не одно и то же . Связанный пост имеет множество примеров конструктивных доказательств того, что что-то не так. Фактически, большинство доказательств того, что что-то является ложным в учебниках, уже конструктивно.

  5. Незавершенность Геделя затягивается по причине, которую я могу различить. Неполнота Гёделя дает такое предложение , что ни ни доказуемы. Это не означает, что недоказуемо (то есть простым приложением исключенной середины)! Это также не означает, что имеет место, или что-то подобное. Итак, как здесь важна незавершенность Геделя?G ¬ G G ¬ G ¬ G ¬ ¬ GGG¬GG¬G¬G¬¬G

PS Прошу прощения за предыдущую версию дополнения, которая была грубой.

Андрей Бауэр
источник
1
Комментарии не для расширенного обсуждения; этот разговор был перенесен в чат .
Рафаэль
Что касается # 5, я думаю, что проблема заключается в следующем: plus видимому, подразумевает, что однако на самом деле верен. И это, конечно, странно. На самом деле это то, чего я не понимаю, и искал ответ, когда натолкнулся на этот вопрос. Не могли бы вы ответить на это, пожалуйста? G ¬ G ¬ G ¬ GGG¬G¬G¬G
Squirtle
Я считаю, что решение таково: линия рассуждений такова, что plus подразумевает by Modus Tollendo Ponens; Однако, у нас есть , который не то же самое , как . Хорошим примером Modus Tollendo Ponens были бы и следовательно, (который является избыточным). ИЛИ и поэтому . Конечно, эти первые утверждения ( и илиG ¬ G ¬ G G ¬ G ¬ G G ¬ G ¬ G ¬ ¬ G G ¬ G G ¬ G ¬ ¬ G GGG¬G¬GG¬G¬GG¬G¬G¬¬GG¬GG¬G¬¬GG ) точно исключены теоремой Гёделя о неполноте.
Squirtle
8

Я думаю, что ваш вопрос сводится к тому, что «при формальной проверке с использованием какой-либо формальной логики, какая у меня гарантия, что логика последовательна?». И ответ: нет. Это то, что вы должны предположить. Формальная проверка не устраняет все предположения; это просто поможет вам лучше понять, что вы предполагаете, и, возможно, поможет вам начать с предположений, которые кажутся разумными.

Если вы работаете в рамках стандартной логики, как правило, большинство людей рады предположить, что логика последовательна, даже если у них нет доказательства этого факта. Это правда, что мы можем когда-нибудь обнаружить, что логика на самом деле противоречива ... но большинство людей считают, что это не очень вероятно.

В некоторых случаях можно доказать, что логика непротиворечива, но это требует использования другой, более мощной логики, где мы должны предположить, что вторая логика непротиворечива, поэтому нам все еще приходится делать некоторые предположения (предположим, что некоторая логика непротиворечива) ). Это может быть принято как свидетельство того, что первая логика, вероятно, последовательна, если вы считаете, что вторая логика, вероятно, последовательна, но рассуждение должно где-то обосноваться - есть некоторые вещи, которые мы должны просто принять и не можем доказать.

См., Например, вторую проблему Гильберта и это обсуждение согласованности ZFCэто, и это, и это, и, вероятно, еще много).

DW
источник
Немного вводит в заблуждение утверждение, что «у вас нет гарантии согласованности», потому что это звучит так, будто вся логика взлетает в воздух. Конечно, существуют доказательства согласованности формальных систем, но они, так сказать, не «уменьшают веру», потому что такие доказательства требуют еще большей веры в согласованность более сильных систем. Тем не менее, весьма полезно иметь доказательства последовательности.
Андрей Бауэр
1
@AndrejBauer Это никогда не вопрос веры, а того, согласны ли вы с аксиомами. Формальные системы делают аксиомы явными.
Рафаэль
1
Я не понимаю вашу точку зрения @Raphael. Вы говорите, что мнение об аксиомах лучше, чем вера в аксиомы? Это слова, выражающие общеизвестный факт о прочности последовательности. И, как говорят слова, они не особенно полезны или полезны. Я указывал, что не очень педагогично делать общие заявления об отсутствии доказательств последовательности, вот и все.
Андрей Бауэр
@AndrejBauer Я чувствовал, что ни «[согласованность] - это то, что вы должны принять», ни «вера в согласованность» не достигли цели. Вы можете (иногда) доказать непротиворечивость, но в конечном итоге все доказательства «в воздухе» на ходулях аксиом. (Кроме того, я хотел назвать «аксиому», которую, как мне казалось, здесь не хватало.)
Рафаэль
@AndrejBauer, хорошо, достаточно честно. Я отредактировал свой ответ, чтобы быть более ясным об этом. Надеюсь, теперь это выглядит лучше. К сожалению, это не устраняет необходимость допущений. Это просто меняет то, какая логика мы считаем последовательной. В конечном счете, это основывается на некоторой логике, которую вы должны считать последовательной.
DW
8

Есть много интересных философских моментов, которые затрагивает ваш пост.

Согласованность булевой логики

Проблема согласованности теории доказательств в классической логике не так страшна, как вы ее себе представляете. Это в основном сводится к следующему:

Мы можем определить логическую логику как совокупность функций логических операций над значениями истинности 1и 0. Но откуда мы это знаем 0≠1?

(обратите внимание, что я просто использую 0и 1как абстрактные символы для двух значений истинности; в частности, я не предполагаю здесь никакого понятия целого числа)

Мы, конечно, не знаю , что 0и 1другие. Но булева логика настолько смехотворно проста, что отказ от этой возможности является крайним уровнем скептицизма.

Но классическая логика высказываний сводится к этому. Напомним, что мы можем присвоить логические значения атомным предложениям любым способом, и это распространяется на присвоение значения всем предложениям, которые можно построить из атомарных.

Утверждение «из Pвас можно вывести Q» буквально просто упорядочивающее отношение; это означает то же самое, что и утверждение, которое « v(P) ≤ v(Q)справедливо для каждой функции, vприсваивающей истинностные значения атомарным суждениям».

Правила вывода логики высказываний как раз и являются свойствами для работы с упорядочением . Доказательством от противного, в частности, является наблюдение, что если P ≤ 0, то P = 0.

И возвращаясь к вашей проблеме ... если бы мы знали и то P ≤ 0и другое ¬P ≤ 0, то после включения значений истины мы в конечном итоге пришли бы к выводу 0=1; что истина и ложь означают одно и то же.

Итак, если вы уверены, что «истина» и «ложь» означают разные вещи, то вы должны быть одинаково уверены в непротиворечивости логической логики.

Доказательство от противоречия в интуиционистской логике

Следует обратить особое внимание на то, что доказательство от противного лучше сформулировать так:

  • Если вы можете извлечь противоречие из P, а затем заключить¬P

Фактически, можно прямо определить отрицание как связь с этим свойством. Например, в алгебре Хейтинга вы обычно видите ¬P, определенное как среднее значение P → 0.

Обратите внимание, в частности, на особый случай

  • Если вы можете извлечь противоречие из ¬P, а затем заключить¬¬P

То, что вы назвали «доказательством от противоречия», происходит от идентификации ¬¬Pс P. Интуиционистская логика не предполагает, что они эквивалентны.

Согласованность как официальный контракт

Есть больше вычислительных формализмов для кодирования логики; см. простейшее лямбда-исчисление, зависимые типы и, в частности, парадигму «предложения как типы».

Не вдаваясь в детали, противоречие в основном рассматривается как формальный договор. Есть тип, который я буду называть 0, и есть контракт «эти функции нельзя использовать для создания элемента типа 0».

Если такая система настолько смелая, что позволяет вам построить функцию T → 0, то, если она действительно придерживается контракта, это означает, что аналогичным образом невозможно создать какие-либо объекты типа T. Это вычислительная точка зрения на то, что означает доказательство от противного.

В конечном счете это не сильно отличается от, например, функции C, которая возвращает указатель, обещающий не возвращать нулевой указатель, или функции C ++, обещающей не генерировать исключение.

И возвращаясь к классической логике, мы действительно делаем это.

Нам предлагают формальные контракты, такие как «из аксиом Пеано, правила вывода не позволят вам вывести противоречие». Если этот контракт действительно соблюдается, то, если вы смогли показать, что ¬Pподразумевает противоречие, то Pтакже не может подразумевать противоречие.

И если бы можно было нарушить договор, мы бы просто сказали: «Аксиомы Пеано противоречивы».


источник
есть пункт, который я думаю, я не понимаю, как противоречие так же, как наблюдение ? Я бы подумал, что это больше похоже на , но, конечно, это должно быть неправильно, потому что мое предположение не совпадает сP = 0 P = 1 P 0P0P=0P=1P0
Чарли Паркер
@CharlieParker: - тождественно ложное суждение; в синтаксисе, где у вас есть символ для этого, это часто называют «противоречием». оказывается пропозицией, эквивалентной . P ¬ P 00P¬P0
1
Кроме того, ... это неуклюжий оператор. Вы имеете в виду, что обозначает логическую ? Тогда . Но если вы имели в виду как утверждение « равно », то это не утверждение (это металогическое); на самом деле не имеет смысла говорить, что аргумент, использующий правила вывода из логики высказываний, может вывести его, поскольку вы даже не можете сказать это на языке высказываний. = ( P 0 P 1 ) = ( ¬ P P ) = 0 P = 0 P 0P=0P=1=(P0P1)=(¬PP)=0P=0P0
Это интересно. Я обычно не приравниваю Ложь к противоречию обязательно. Например, допустим, мы знали, что ложно, а истинно. Тогда я не могу сделать вывод, что я папа от всего этого. Однако, если истинно, тогда я могу использовать принцип взрыва, чтобы сделать вывод, что я папа. Не уверен, что я ошибаюсь, но тот факт, что - False, не устанавливает эквивалентности между каждой ложью. Эти две лжи разные ... или я что-то упустил? A A ¬ A P ¬ P¬AAA¬AP¬P
Чарли Паркер
1
@CharlieParker: Как правило, противоречие используется так же, как тавтология в булевой логике, за исключением того, что противоречие относится к чему-то идентично ложному, а тавтология к чему-то идентично истинному. Это удобно выражать и в синтаксисе, где у вас есть такие символы; по какой-то странной причине классическая логика обычно не представлена ​​в таком синтаксисе; таким образом, является удобной заменой, поэтому он часто вставляется в место, где необходимо противоречие. 1 P ¬ P01P¬P
1

При использовании для гарантии истинности формального утверждения все доказательства неявно предполагают согласованность системы, в которой они основаны. Это потому, что если система несовместима, целостность системы нарушается, и вся работа, которую мы сделали в этой системе в основном мусор.

Поскольку мы не можем доказать, что какая-либо система (или, по крайней мере, любая сложная система) является последовательной в пределах этой системы, мы должны воспринимать ее как эмпирическую истину, а не формально доказуемую истину. По сути, если математики тратят много времени на работу с формальной системой, а противоречия никогда не обнаруживаются, то это эмпирическое доказательство в пользу согласованности системы. Кроме того, мы можем использовать более мощную систему для доказательства согласованности системы, с которой мы работаем (хотя согласованность этой более мощной системы все равно будет эмпирической - доллар где-то останавливается).

По своей сути, ситуация в математике идентична ситуации в науке. Мы строим математику на основе теорий, которые кажутся правильными, основываясь на всей имеющейся у нас информации об этих теориях, и, как и в науке, вы не можете доказать, что теория верна; Вы можете только доказать, что это неверно.

Когда мы впервые начали пытаться основывать математику в теории множеств, мы фактически обнаружили, что наши первые формулировки теории множеств были непоследовательны, потому что они допускали такие вещи, как «пусть будет множеством всех множеств, которые не содержат себя». Мы должны были выбросить эти формулировки.S

Независимо от того, на какой системе аксиом мы выберем математику, всегда существует опасность, что мы обнаружим противоречие в этой системе. Именно поэтому математики не вводят новые аксиомы в математику: у каждой новой аксиомы есть шанс быть несовместимой с уже используемыми аксиомами, и вся работа, которая использует новую аксиому, должна быть полностью переоценена.

Приложение: Когда я говорю о том, что утверждение является верным для данной системы, я имею в виду, что оно не может быть опровергнуто в этой системе, если эта система является последовательной.

Х. Антонио Перес
источник
2
Ложно, что «все доказательства предполагают последовательность». Правильное доказательство действует независимо от последовательности.
Андрей Бауэр
Если я использую аксиомы ZFC, чтобы доказать что-то, мое доказательство предполагает, что ZFC непротиворечив. Если ZFC противоречив, то мое доказательство больше не гарантирует правды того, что я доказал
Х. Антонио Перес
1
Это просто ложь. Если ZFC несовместим, тогда все утверждения доказуемы, и ваше доказательство все еще является доказательством. Единственное, что меняется с несогласованностью, это то, что ZFC становится довольно бесполезной теорией, которая не имеет моделей (и поэтому ваше доказательство все еще показывает, что ваше утверждение верно во всех моделях).
Андрей Бауэр
Я исправил свой ответ
Х. Антонио Перес
2
К сожалению, вы не можете просто составить определения принятых слов. «True» означает «действителен в модели». Найдите другое слово, или даже лучше, просто признайте, что ошибаетесь. Я также прошу прощения за то, что был немного резким, но я забочусь о том, чтобы держать вещи прямо в логике.
Андрей Бауэр