В теории алгоритмов есть теорема гласящая что не существует алгоритма опредляющего для любой пары (alg, state), где alg — запись некоторого алгоритма, state — его входные параметры, завершится ли выполнение alg или нет.
Доказательство теоремы ароводят от противного. Полагают что такой алгоритм A существует и подают ему на вход другой алгоритм B. При этом B конструируют с использованием A.
Можно ли провести это доказательство не передавая некоему алгоритму на вход самого себя?
Здравствуйте, cvetkov, Вы писали:
C>В теории алгоритмов есть теорема гласящая что не существует алгоритма опредляющего для любой пары (alg, state), где alg — запись некоторого алгоритма, state — его входные параметры, завершится ли выполнение alg или нет.
C>Доказательство теоремы ароводят от противного. Полагают что такой алгоритм A существует и подают ему на вход другой алгоритм B. При этом B конструируют с использованием A.
C>Или в более общей постоновке. Можно ли доказать эту теорему в Конструктивистской логике?
Это не тот вид доказательства от противного, который не работает в конструктивной логике.
Т.е. нам нужно доказать !Q, где Q — утверждение о существовании такого алгоритма.
!Q = Q -> 0 , где 0 — тождественная ложь.
Мы предполагаем, что Q верно и выводим противоречие:
Q -> .... -> 0
всё получается, даже в конструктивной логике
Здравствуйте, SergH, Вы писали:
SH>Здравствуйте, ω, Вы писали:
ω>>Это не тот вид доказательства от противного, который не работает в конструктивной логике.
SH>А какой тогда не работает?
((A -> 0) -> 0) -> A
т.е. снимать два отрицания нельзя
в данном случае, когда A = (Q -> 0), снимать два из трёх отрицаний можно:
(((Q -> 0) -> 0) -> 0) -> (Q -> 0)
Djinn> ? f :: (((q -> Void) -> Void) -> Void) -> (q -> Void)
f :: (((q -> Void) -> Void) -> Void) -> q -> Void
f a b = void (a (\ c -> c b))
Здравствуйте, SergH, Вы писали:
SH>Что-то я сомневаюсь, что _не_ существование чего-либо в принципе можно доказать конструктивно.
да, для меня этот вопрос тоже не ясен.
я бы удовлетворился конструктивно построенным алгоритмом, относительно которого мы могли бы доказать что для него невозможно доказать конечен он или нет.
Здравствуйте, cvetkov, Вы писали:
C>я бы удовлетворился конструктивно построенным алгоритмом, относительно которого мы могли бы доказать что для него невозможно доказать конечен он или нет.
А единственность этого алгоритма как доказать?
Видимо, понятие "конструктивная логика" всё же немного шире бытовых представлений о ней, на что нам и намекнул тов. Омега.
Здравствуйте, SergH, Вы писали:
SH>Здравствуйте, cvetkov, Вы писали:
C>>я бы удовлетворился конструктивно построенным алгоритмом, относительно которого мы могли бы доказать что для него невозможно доказать конечен он или нет.
SH>А единственность этого алгоритма как доказать?
а она меня не интересует SH>Видимо, понятие "конструктивная логика" всё же немного шире бытовых представлений о ней, на что нам и намекнул тов. Омега.
да, тяжело не скатиться к логике интуиционалистской
Здравствуйте, cvetkov, Вы писали:
C>а она меня не интересует
А, сорри, я неправильно тебя понял, теперь прочитал внимательно. Да, так можно было бы.
Кажется, диофантовы уравнения начиная с некоторой степени в общем виде не разрешимы. Так что алгоритм поиска решения (хоть перебором) подходит. Другое дело, что доказательства неразрешимости диофантовых уравнений имеет тот же характер, что и проблема останова.
Здравствуйте, cvetkov, Вы писали:
C>Здравствуйте, ?, Вы писали: C>?>Мы предполагаем, что Q верно и выводим противоречие:
C>а это предположение не вызывает у вас подозрений? C>закон исключения третьего в конструктивистской логике не работает.
Я совершенно не спец. в intuitionistic logic, но с первого взгляда я не вижу проблемы.
Как уже писал omega, в этой логике есть проблемы с док-ом от противного, но(!) только при выводе положительных утверждений (поскольку мы не можем снять двойное отрицание). Однако, учитывая, что (A -> 0) -> !A — это тавтология (просто по определению отрицания в int. logic), я не вижу проблем с док-ом отрицания существования алгоритма.
Здравствуйте, cvetkov, Вы писали:
C>закон исключения третьего в конструктивистской логике не работает.
Доказательство утверждения «Алгоритм A решает задачу остановки ⇒ противоречие» вполне конструктивно. Разве отсюда не следует «ни один алгоритм не решает задачу остановки»?
Здравствуйте, Roman Odaisky, Вы писали:
RO>Доказательство утверждения «Алгоритм A решает задачу остановки ⇒ противоречие» вполне конструктивно. Разве отсюда не следует «ни один алгоритм не решает задачу остановки»?
Можно конструктивно показать эквивалентность (∀x:X).¬P и ¬(∃x:X).P. Т.е. если любой решающий проблему остановки алгоритм приводит к противоречию, то не существует такого, который бы ее решал.
Здравствуйте, cvetkov, Вы писали:
C>В теории алгоритмов есть теорема гласящая что не существует алгоритма опредляющего для любой пары (alg, state), где alg — запись некоторого алгоритма, state — его входные параметры, завершится ли выполнение alg или нет.
Вообще, эту теорему можно сформулировать в положительном ключе: если дана программа H, решающая проблему останова для некоторого множества S пар (alg, state), и не останавливающаяся для всех остальных пар, то мы можем явным образом сконструировать программу H', решающую проблему останова для более широкого множества S' пар (alg, state), и не останавливающуюся для всех остальных пар ("более широкого" значит, что S является подмножеством S', не совпадающим с S').
C>я бы удовлетворился конструктивно построенным алгоритмом, относительно которого мы могли бы доказать что для него невозможно доказать конечен он или нет.
это 2 разных теоремы: то что не существует единого алгоритма, который дает ответ остановится ли данный алгоритм на данных данных. И то что существует конкретный алгоритм и конкретные данные для которых не существует доказательства остановки или неостановки. В классической математике верны обе. В конструктивной верна первая, но неизвестно верна ли вторая.
Кстати заметим, что даже в классической математике из первой вывести вторую просто, но не совсем тривиально. А из второй первую вообще не очень понятно как вывести, потому что из того что нет доказательства не следует что нет алгоритма -- алгоритм может просто "угадать" ответ.
Здравствуйте, cvetkov, Вы писали:
C>я бы удовлетворился конструктивно построенным алгоритмом, относительно которого мы могли бы доказать что для него невозможно доказать конечен он или нет.
Для каждого из этих "доказать" важно уточнить, о доказательствах в каких формальных системах (теориях) идет речь. После такого уточнения соответсвующий пример может быть несложно построить.
Например, в арифметике Пеано, дополненной аксиомой о непротиворечивости арифметики Пеано (по видимому, эта теория доказывает только утверждения, соответствующие действительности; ее аксиомы могут быть доказаны в ZF — теории множеств Цермело-Френкеля) можно доказать, что в арифметике Пеано отсутствуют доказательства об остановке и неостановке алгоритма, который ищет противоречение, перебирая все теоремы арифметики Пеано, и который остановился бы только если бы он его нашёл.
Тут есть несколько важных правил (они касаются систем, на которые наложены минимальные требования: они должны позволять формализовать понятие алгоритма, и должны быть способны доказывать простейшие арифметические истины, для которых не требуется даже принципа индукции, наподобие 2+2=4):
* если в системе T можно доказать, что в системе T что-либо нельзя доказать, что этим система T доказывает свою непротиворечивость, а значит, она противоречива (по второй теореме Гёделя).
* если в системе T нельзя доказать, что алгоритм останавливается, то он не останавливается (т.к. если алгоритм останавливается, то можно выписать полную последовательность состояний машины, выполняющей его, каждые два последовательных из которых связаны простейшими арифметическими соотношениями).
* если в системе T можно доказать, что алгоритм не останавливается, а он останавливается, то теория T противоречива.
* а вот если в системе T можно доказать, что алгоритм останавливается, а он не останавливается, то теория T может и не быть противоречивой. Но всё равно это очень плохая теория, так как она доказывает некоторые ложные утверждения. По видимому, примером такой теории является арифметика Пеано, дополненная аксиомой о противоречивости арифметики Пеано.
Здравствуйте, nikov, Вы писали:
N>Тут есть несколько важных правил (они касаются систем, на которые наложены минимальные требования: они должны позволять формализовать понятие алгоритма, и должны быть способны доказывать простейшие арифметические истины, для которых не требуется даже принципа индукции, наподобие 2+2=4)
А, вот ещё одно:
* Если в системе T можно доказать, что алгоритм не останавливается, то в системе T можно доказать, что в системе T можно доказать, что этот алгоритм не останавливается ("навешивание доказуемости").
Здравствуйте, cvetkov, Вы писали:
C>В теории алгоритмов есть теорема гласящая что не существует алгоритма опредляющего для любой пары (alg, state), где alg — запись некоторого алгоритма, state — его входные параметры, завершится ли выполнение alg или нет.
C>Доказательство теоремы ароводят от противного. Полагают что такой алгоритм A существует и подают ему на вход другой алгоритм B. При этом B конструируют с использованием A.
C>Можно ли провести это доказательство не передавая некоему алгоритму на вход самого себя?
C>Или в более общей постоновке. Можно ли доказать эту теорему в Конструктивистской логике?
Мне кажется, что когда мы доказываем от противного высказывания о всеобщности (для любого или для всех) мы допускаем какую-то ошибку иерархического характера. Вообще, доказывая истинность высказывания мы выходим на новый семантичский уровень. (Альфред Тарский. Семантическая концепция истины и основания семантики). Не буду повторять его рассуждения (это каждый может сделать самостоятельно). Приведу, собственное понимание парадокса лжеца. Это когда Критянин утверждает "Все Критяне лжецы". Даже на бытовом уровне понятно, что его высказывание не может служить основанием для конструирования противоречия. Это конструирование происходит на другом семантическом уровне. Мы так и воспринимаем в реальной жизни. Еще одним примером является высказывание "Существует минимальное число, которое нельзя представить меньше чем пятюдесятью словами на русском языке". Дальше конструируем противоречие. Если такого числа не существует, то само это высказывание является его определением потому как содержит меньще 50 русских слов. Недопустимость пользоваться этим определением становится очевидной если мы заменим слова "На русском языке" на "на английском языке". Отсюда само высказывание и его доказательство находятся на разных семантических уровнях.
Потому как сегодня праздник не хочется вникать в дебри. Но, я с большим подозрением отношусь к доказательствам такого типа. Когда берем алгортим, допускаем отрицание. Запускаем это отрицание через него.. и т.п.
