Хмм, похоже что является. Определяем Аксиомы Пеано, но чтоб с 0 начиналось а не с 1. Вводим операцию «x + y», операцию «x - y», деления, умножения и остатка от деления определяем, потом операции битового логического сдвига влево и вправо - так можно сдвигами нарезать число от 0 до inf на бесконечный массив байтов по 8 бит каждый — получим ленту для brainfuck и возможность по ней ходить в любую сторону. А сама программа брейнфака, состоящая из 8 инструкций > < + - . , [ ] - делаем отдельный массив для этих инструкций по три бита на инструкцию. Ну а дальше определяем что вот эта инструкция делает такие-то изменения на ленте.

Только я тогда не совсем понимаю, что значит несводимость логики первого порядка к логике второго порядка? Если брейнфак выразим в логике первого порядка, то я могу скомпилить Coq в этот брейнфак — разве это не будет выражение логики одного порядка в логике другого порядка?

скачять реферат безплатно без смс

https://domashke.com/referati/referaty-po-matematike/kursovaya-rabota-nerazre...

3. Вывести неразрешимость логики первого порядка из неразрешимости проблемы остановки.

не уверен, что это то, что тебе нужно, а не обратный результат. в любом случае, см. google://$SUBJ

3. Вывести неразрешимость логики первого порядка из неразрешимости проблемы остановки.

Гёдель это доказал давно, притом без всяких проблем останова зачем про это курсовую писать? Я к тому веду, что я не понимаю, что значит «логика второго порядка невыразима в логике первого порядка», если логикой первого порядка можно выразить что-то Тьюринг-полное, и скомпилять в него что-то что может умеет работать с логикой второго порядка

Не является.

http://arxiv.org/abs/1405.1715

Для начала попробуй определить брейнфак строго в терминах FOL, если получится — полнота доказана.

о! треды о полноте! торт самый ЛОР возвращается!

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

В таких вещах всегда лучше записывать, чтобы найти возможные ошибки.

Если руки все-таки дойдут — кастани :)

Только я тогда не совсем понимаю, что значит несводимость логики первого порядка к логике второго порядка?

Ни логика первого порядка, ни логика второго порядка не являются тьюринг-полными. При этом логика второго порядка шире логики первого (и, с-но, лпп не сводится к лвп).

разве это не будет выражение логики одного порядка в логике другого порядка?

Не будет.

то я могу скомпилить Coq в этот брейнфак

А coq и не является тьюринг-полным. Coq можно скомпилить в брейнфак, а вот брейнфак в coq - нельзя.

Гёдель это доказал давно,

А кто-нибудь понимает вообще, что он там доказал? Его теорема о неполноте сводится к простейшей хрени, типа парадокса лжеца. А проблема останова еще банальней: если бы знал где упасть, соломку бы подстелил:)

Зачем нужны вообще эти клоуны? Пусть живут себе в своем мире первых, 10-х и прочих порядков, нормальным посанам это не нада

Можно ли описать

Кстати, описать не значит выполнить. Тьюринг-полнота — это о вычислителе а не о языке, об этом почему то часто забывают.

Его теорема о неполноте сводится к простейшей хрени, типа парадокса лжеца.

Нет, не сводится.

Если руки все-таки дойдут — кастани :)

Пока покажу промежуточный результат. Я использовал нотацию от SMT-солвера alt-ergo https://paste.debian.net/hidden/ead1da5c/
Протестировать можно тут https://alt-ergo.ocamlpro.com/try.php только лучше поставить это через OPAM потому что так быстрее значительно. Не все те «юнит-тесты» завершаются успешно, но это обусловлено лишь исключительно тем, что солвер не может выбрать стратегию правильную и не пытается очень сильно «разворачивать» сдвиги. Там (если собрать себе этот alt-ergo на локалхост без жабаскриптов) есть возможность посмотреть то, каким образом доказывается верность утверждения

Немного о синтаксисе:

forall - квантор всеобщности. Есть еще квантор существования exists. Оператор -> — импликация. Есть встроенный тип int который принимает значения ... -4 -3 -2 -1 0 1 2 3 4 ... т.е. соответствует множеству целых чисел. Там уже есть встроенные операции умножения сложения деления и нахождения остатка от деления. Остальное должно быть самоочевидным.

через двоичные сдвиги я смогу нарезать инты большие чем или равные 0 на массив из 8-битных unsigned char. И еще нарезать для хранения самого «алфавита» брейнфака < > + - . , [ ]. В alt-ergo есть теория для массивов, но я массивы определю через неотрицательные инты, чтоб не возникало вопросов. Отдельным положительным интом будет хранится положение «указателя» на ленте с инструкциями, и еще одним - положение на ленте с ячейками памяти. Еще один инт будет нужен чтобы проматываться между скобочками [ ]. Далее, можно ввести понятия «шага» брейнфака, чтобы на каждом шаге инкрементировать некую переменную, и тогда можно будет попросить SMT солвер решить «а будет ли на таком-то шаге такое-то состояние у нашей брейнфак-машины?». Вообще это все очень напоминает какое-то функциональное программирование. Скоро доделаю

Спасибо, посмотрю.

Язык является средством описания симуляции

Далее, можно ввести понятия «шага» брейнфака, чтобы на каждом шаге инкрементировать некую переменную, и тогда можно будет попросить SMT солвер решить «а будет ли на таком-то шаге такое-то состояние у нашей брейнфак-машины?»

Ты же понимаешь, что умение вычислять МТ до некоторого конечного n, не ведет к полноте по тьюрингу?

Для n можно использовать квантор существования т.е. можно сформулировать это как «Существует такой шаг n на котором состояние м.т. при вот таком-то начальном состоянии ленты является таким-то»

Но это не дает тьюринг-полноты.

вообще никакая непротиворечивая лт не может быть тьюринг-полной. Для тьюринг-полноты надо уметь зависать - то есть выводить nonsense.

Но это не дает тьюринг-полноты.

Дает.

вообще никакая непротиворечивая лт не может быть тьюринг-полной. Для тьюринг-полноты надо уметь зависать - то есть выводить nonsense.

А описанная в логике первого порядка машина тьюринга тоже будет уметь зависать.

Дает.

Не дает. На не тьюринг-полном ЯП можно написать ф-ю которая вычисляет любую мт до любого шага на любых данных.

А описанная в логике первого порядка машина тьюринга тоже будет уметь зависать.

Описать-то в лпп (точнее, в какой-нибудь в теории первого порядка, например ZFC) МТ можно легко - формальное определение МТ именно таким описанием и является. Это, однако, не делает указанную теорию (и лежащую в основе логику) тьюринг-полной.

Не дает. На не тьюринг-полном ЯП можно написать ф-ю которая вычисляет любую мт до любого шага на любых данных.

Если есть штука, которая будет нечто доказывать, пользуясь аксиомами, описанными логикой первого порядка, то она вполне может быть(может делать вычисления) полной по тьюрингу. Проблему останова можно тоже сформулировать, что вот при таком-то состоянии ленты МТ у нас никогда не будет выполнено условие останова(отрицание квантора существования https://ru.wikipedia.org/wiki/Квантор)

Это, однако, не делает указанную теорию (и лежащую в основе логику) тьюринг-полной.

А что делает?

что вот при таком-то состоянии ленты МТ у нас никогда не будет выполнено условие останова(отрицание квантора существования

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

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

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

что вот при таком-то состоянии ленты МТ у нас никогда не будет выполнено условие останова(отрицание квантора существования

да какая ошибка, если ты вообще не понимаешь о чем говоришь? Допустим есть алгоритма который «призван доказать или опровергнуть» утверждение о бесконечности натурального ряда. Алгоритм заключается в реализации индуктивного шага n-next = n + 1. Есть утверждение, что не существует такого n, что машина остановится. Докажем это, запустив нашу машину. Но машина не остановится, следовательно ничего никогда не будет доказано.

вообще никакая непротиворечивая лт не может быть тьюринг-полной. Для тьюринг-полноты надо уметь зависать - то есть выводить nonsense.

«зависанеие», если ты говоришь о бесконечном вычислении, это не вывод. Мы (машина) не можем делать утверждение о вычислимости, так как не знаем закончится ли когда-нибудь процесс вычисления (остановится ли машина).

Допустим есть алгоритма который «призван доказать или опровергнуть» утверждение о бесконечности натурального ряда.

Да, есть. Но это доказывается не перебором до бесконечности, а напрямую следует из определения натурального числа и аксиомы индукции. Число 1 - натуральное. Любое число, следующее за натуральным - натуральное.

(Аксиома индукции.) Если какое-либо предложение доказано для 1 (база индукции) и если из допущения, что оно верно для натурального числа n, вытекает, что оно верно для следующего за n натурального числа (индукционное предположение), то это предложение верно для всех натуральных чисел.

Алгоритм заключается в реализации индуктивного шага n-next = n + 1.

Можно математически доказать, что этот алгоритм никогда не завершится т.к. любое натуральное число+1 это натуральное число

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

У тебя в голове каша.

А что делает?

Делает вычислительная эквивалентность МТ. Если твоя логика не может повиснуть (вывести противоречие), то она слабее МТ.

Вот тебе на alt-ergo

goal inf_proff:
  forall x : int.
  x >= 1 -> (* все натуральные числа больше либо равны 1 *) 
  (x+1 >= 1) (* всякое натуральное число, если к нему прибавить 1, будет натуральным *)

«зависанеие», если ты говоришь о бесконечном вычислении, это не вывод.

Вывод - это терм. Если терм повис - то тип содержит жопу. Жопа - это противоречивое утверждение. С-но, если МТ содержит виснущие термы, то тьюринг-полная логика, эквивалентная (в смысле изоморфизма Карри-Говарда) позволяет вывести ложное утверждение.

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

Че то сейчас подумал, и вот что я скажу. Логика и вычислитель(в том числе МТ) вообще имеют разную природу. Принципиальное отличие заключается в том, что вычислитель задает правила вычисления, а логика сама является этим набором правил. Вычислитель вообще ничего не должен доказывать, он должен обеспечивать(если надо) соблюдение этих правил, и осуществление их. Причем, правила могут быть абсолютно любые, не обязательно логические. К примеру, мы можем реализовать вывод «если не А и не Б то С» какая тут логика? да никакой(хотя, формально это, типа импликация). Просто мы так захотели. Или нам так надо. Никакая логика не может не то что реализовать, но и описать данное вычисление, так как нет логических оснований для него.

Алсо, зыбкость логики феерично показал Льюис Керрол в «Черепахе и Аххилесе». Доказательство — это пустой звук, по большому счету. Просто отражение работы человеческого мышления, не более того. Самостоятельного значения она не имеет. Не случайно, до сих пор определение слова «доказательство» весьма туманно, если вообще существует:)

Если твоя логика не может повиснуть (вывести противоречие), то она слабее МТ.

А кто-то разве утверждал, что в логике порядка нельзя сформулировать невыводимую и неопровержимую формулу? https://ru.wikipedia.org/wiki/Теорема_Гёделя_о_неполноте

Первая теорема утверждает, что если формальная арифметика непротиворечива, то в ней существует невыводимая и неопровержимая формула.

Если терм повис

Кто будет делать вывод о его зависании? Нет этой сущности. Если МТ не закончила вычисление, значит она либо его закончит, либо нет. Что из этих 2 — никто не знает, на любом шаге вычисления. Поэтому нет никакого зависания.

А кто-то разве утверждал, что всякое утверждение в логике порядка нельзя сформировать невыводимая и неопровержимая формула?

Прекрати бросаться баззвордами, которых не понимаешь.

1. Теорема Геделя не относится к лпп, она относится к теориям первого порядка (которые являются расширениями лпп). Сама лпп как раз является полной. И многие ее расширения (которые не являются достаточно сложными для погружения в себя) - тоже являются полными, например арифметика Пресбургера. Так что, да, в лпп не существует формулы, которая была бы не выводима в лпп вместе со своим отрицанием.

2. Речь не о невыводимой-неопровержимой формуле, а о формуле, которая выводится вместе со своим противоречием (то есть обратная ситуация). Чтобы твоя лоника была «тьюринг-полной», в ней должна быть возможность вывести А и не-А одновременно.

Кто будет делать вывод о его зависании?

Вывод о его зависании делать не надо. Это просто факт, терм повис, нормальной формы у него нет.

Что из этих 2 — никто не знает

Я знаю, потому что я это доказал. for(int i = 0; 1; i++); - зависает в соответствии с семантикой языка. Чтобы в этом убедиться, запускать программу не нужно.

Че то сейчас подумал, и вот что я скажу. Логика и вычислитель(в том числе МТ) вообще имеют разную природу.

Но мы легко можем превращать одно - в другое:

https://en.wikipedia.org/wiki/Curry–Howard_correspondence

по-этому на самом деле разницы нет.

Не случайно, до сих пор определение слова «доказательство» весьма туманно

Да нет, у этого слова четкое, формально строгое математическое определение. Это вполне конкретный математический объект, вполне определенного вида.

Отличной иллюстрацией теоремы Геделя является парадокс Лжеца (она и есть парадокс Лжеца, переведенный на язык математики). Пусть лжец говорит «я лгу» лжет ли он? Допустим лжет. Но он и утверждает, что он лжет. значит он говорит правду. Но если он говорит правду — то он не лжец.

Имхо, решение этого парадокса тривиально. Такая фраза из уст лжеца попросту невозможна по-определению, так же как невозможно существование Расселовского множества. Эти хреноплеты просто перемудрили сами себя, не более того. Можно породить кучу пародоксов на пустом месте. Например, «прыгающий хохол не прыгает» Если он прыгающий, как же он может не прыгать? А если он прыгает, значит он не прыгающий. Парадокс!

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

Приведи его.

Но мы легко можем превращать одно - в другое:

Я уже привел пример, где мы не можем превратить одно в другое. Если бы мы могли превращать одно в другое всегда — другое дело.

Это последовательность правил вывода.

Если бы мы могли превращать одно в другое всегда

Ты все верно понял. Мы можем ВСЕГДА.

Отличной иллюстрацией теоремы Геделя является парадокс Лжеца (она и есть парадокс Лжеца, переведенный на язык математики).

Не является. Не есть. Невыводимая с отрицанием формула у Геделя это не «данное утверждение ложно» а «данное утверждение невыводимо». Последнее, в отличии от первого, не является парадоксом, не приводит к проитворечия.

На самом деле все эти логические изыскания кажутся обывателю такими сложными

Так ты и есть обыватель. И ты этих рассуждений не понимаешь. Но смеешь мнение иметь.

в огороде бузина --> в киеве дядька

логично?

Ты вроде утеверждал, что существует общепринятое четкое определение. Тогда зачем же ты отсебятину постишь?

Не является. Не есть.

Угу, поспорь с самим Геделем

логично?

Что?

Ты вроде утеверждал, что существует общепринятое четкое определение.

И я тебе его дал. Общепринятое, формально строгое математическое определение.

нет

дай ка пруфец