Является ли логика первого порядка Тьюринг-полной?

Зачем? Он ведь со мной согласен. Ты просто не понимаешь ни формулировки теоремы, ни ее доказательства. Иди почитай учебник по формальным системам и перестань быть дебилом.

Согласен, но утверждал обратное. ок

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

Он не утверждал обратное. Не надо выдумывать за Геделя, он бы откусил свой язык, если бы тот произнес сказанный тобой бред.

Последнее, в отличии от первого, не является парадоксом, не приводит к проитворечия.

Ну че, просто меняем слово «ложно» на «невыводимо», и у нас все ништяк, противоречивая система легким движением руки превращается в неполную.

Это вполне в духе. Я с этим не спорю. Только игра в слова может изменить суть только с точки зрения математика.

ты не знаком с темой, я тут впустую время трачу.

Только игра в слова может изменить суть

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

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

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

с ложностью

Я имел в виду противоречивость(парадоксальность) я просто оговорился

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

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

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

Ну, допустим, у меня машина не работает, не заводится. Я говорю, абра-кадабра, моя машина заводится, просто моя система неполна. Что от этого изменилось? Какая разница, что я говорю об этой системе, что от этого машина тронется?

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

смешно ты рассуждаешь. Я представляю такую картину. Ты стоишь возле МТ и орешь на нее: «останавливайся уже, есть ведь аксиома индукции»

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

Из парадокса лжеца (и любого подобного парадокса, вообще говоря) можно сделать некое другое утвержедние, которое парадоксом уже являться не будет. В случае с парадоксом лжеца это особенно просто, надо лишь «х = ложно(х)» поменять на «х = невыводимо(х)». При этом парадокс снимается т.к. утверждение может спокойно быть невыводимым, но при этом истинным в стандартной интерпретации (одновременно же ложным и истинным оно быть не может). С другой стороны, это утверждение не может быть невыводимым (т.к. в силу семантической полноты оно тогда будет ложным на всех интерпретациях, в том числе на стандартной, а поскольку его стандартаня интерпретация - невыводимость, то отрицание будет выводимость => противоречие). В результате мы записали утверждение которое невыводимо, но истинно (а значит его отрицание - тоже невыводимо).

Дальше вопрос состоит в том, чтобы записать такое утверждение, т.к. самореференций в лпп нет, формальное «x = невыводимо(х)» мы записать не можем. Это делается через спец. костыль - теория погружается сама в себя (именно оттуда требование для теории быть «достаточно сложной» - если теория не достаточно сложна, она не сможет сама себя описать).

а парадокса лжеца в лтт нет, потмоу что он просто не пишется. То есть «x = невыводимо(х)» пишется (пусть и с костылями) а «x = ложно(х)» - ну ваще никак.

Что от этого изменилось? Какая разница, что я говорю об этой системе, что от этого машина тронется?

Правильно. На неполноту совершенно плевать, на самом деле это даже полезное свойство (если бы сложные лтт были полны, они бы поетряли корректность).

Это вещи являются ключевыми, это основная антитеза.

Нету там в теореме никакой антитезы. Не делай вид, что ты ее читал.

это утверждение не может быть невыводимым

не может быть выводимым офк селффикс

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

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

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

Протеворечивые утверждения мы просто объявляем невыводимыми, вот и все.

Нет, это не так. Противоречивые утверждения (вроде парадокса лжеца) не невыводимы. Их нельзя _записать_ (если бы записать было можно - они бы ломали теорию, вне зависимости от их выводимости). А «х = невыводимо(х)» записать можно (точнее, некую его форму записать можно), но при этом ни его ни его отрицание нельзя будет вывести (при том само утвержедние в стандарнтой интерпретации будет наверняка истинным). Противоречивость тут ни при чем (мы естественно полагаем теорию непротиворечивой но лишь затем, что в противоречивой и рассуждать о чем либо смысла нет - у нее нету интерпретации).

Кстати, похоже, все аксиомы, фактически, являются примерами невыводимых и истинных в стандартной интерпретации утверждений.

они бы ломали теорию, вне зависимости от их выводимости

Да нет же. Именно их (потенциальная) выводимость и ломает теорию(логическую систему), поскольку выводимость таких утверждений ведет к противоречию.

Кстати, похоже, все аксиомы, фактически, являются примерами невыводимых и истинных в стандартной интерпретации утверждений.

Ну естественно. Если аксиома независима от других, конечно.

Да нет же. Именно их (потенциальная) выводимость и ломает теорию

Теорию ломает само их _наличие_. Тот факт что можно их записать. Если бы можно было парадокс лжеца записать в тпп - это бы сразу ее ломало. И плевать выводим он или нет. В этом суть парадокса - теорию ломает его наличие.

Я о полноте. Вопрос ТС об описании - по сути, лишь следствие некоторой фривольности в обращении с языком.
Про FOL давно известно, что нет там полноты.

Ну, вот допустим берем наивную теорию множеств. Жила себе жила теория, пока в ней не нашли противоречие Рассела. Значит ли это, что теория не работала? Она работала. Проблема была в том, что она позволяля сформулировать в ней понятие «множество всех множеств не содержащее само себя». Из того, что система позволяет такое, мы делаем вывод, что она противоречива. Далее мы можем ввести аксиому, которая ограничивает теорию в подобных утверждениях. Система снова *считается* непротиворечивой. Как доказать, в общем случае, что она не содержит в себе еще парадоксы? На чем основано наше утверждение, что она непротиворечива? Тот факт, что мы не нашли противоречий до сей поры не означает что их нет, не так ли?

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

Но это ладно. Дальше что? Где условие останова машины? С чего ты взял, что вычисление остановится? Это у тебя описание или реализация? Если это просто описание, то оно не дает никакого вычислительного профита, а если это реализация, то это будет бесконечный луп, где на каждом шаге определяется новое число.

Иными словами, например, я могу утверждать, что где то во вселенной есть слон. Допустим, ты не видел слона, и отрицаешь его существование. Тогда у тебя есть конкретный механизм вычисления. Ты идешь по планете, и рано или поздно натыкаешься на слона, твой поиск останавливается. Знаем ли мы, что данный алгоритм остановится в общем случае? Нет. Применив этот «общий механизм» к произвольному X(вместо слона) мы не знаем, остановится ли когда либо поиск, поскольку не знаем существует ли X. А если мы это знаем, то нам и искать ничего не надо. Вот это и есть принципиальное отличие описания и исполнения. У алгоритма существует не только описание, но и реализация. Твоя логика может быть реализована, только описание реализации этой логики это не то же самое, что сама логика.

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

Реализация вот тут https://alt-ergo.ocamlpro.com/try.php

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

А, ну да. Только тогда и брейнфак не тьюринг-полный пока его не скормили интерпретатору брейнфака

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

Почти любой современный язык поддерживает конкурентность. МТ не реализует конкурентные системы.

На МТ ты можешь написать эмулятор любого возможного ЯП со всеми этими конкурентностями и прочим.

Скажем так. Не каждый алгоритм, реализуемый в конкурентной системе, может быть в принципе реализован на МТ.

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

Вот тут

http://arxiv.org/pdf/1008.1459.pdf

, на странице 41, ты можешь посмотреть доказательство. Это касается не только обычных, но и недетерминированных МТ

начиная со стр 40

//fixed

Страница 72. Цитирую:

By the Computational Representation Theorem, computations of effective Actor systems on integers are enumerable by a Turing machine. Consequently, every deterministic computable function on integers can be implemented by a Turing machine.

В твоей ПДФ-ке скорее всего идет речь о каком-то сферическом коне в вакууме, который существовать в реальном мире не может. Ну примерно как всякие сверхтьюринговые вычисления, машина Зенона например.

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

Это значит что этот алгоритм вообще нельзя реализовать никаким способом. Ну хотя конечно есть шанс, что ученые откроят какие-то новые законы физики, которые позволят делать эти сверхтьюринговые вычисления, только я пока предпочитаю считать истинным https://ru.wikipedia.org/wiki/Тезис_Чёрча_—_Тьюринга_—_Дойча

и что доказывает воя цитата, собственно? Там написано, что любая детерминированно-вычислимая функция с числами может быть реализована МТ

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

А что собственно доказывается там на странице стр 40? Что «Смотрите, мы построили некую гипотетическую теоретическую модель вычислений на акторах, нереализуемую на реальных вычислительных устройствах, которая оказывается еще и нереализуема на МТ»? Какой от этого вообще толк? Столько же толку и от какой-нибудь машины Зенона.

Пойду лучше аксиомы допишу для брейнфака на alt-ergo

с чего ты взял, что она не реализуема на реальных устройствах? Она давно реализована в реальных устройствах, но на МТ не реализуема.

И где можно посмотреть реализацию? Ну вот предположим что это реализовали на x86-64 архитектуре используя Haskell или еще что-то вроде этого. И что мне мешает сделать эмулятор x86-64 на брейнфаке и запустить там собранный через GHC бинарник, который реализует эту модель вычислений?

да ты не читал нифига текст. Это алгоритм, который возвращает неопределенное число в диапазоне от 1 до бесконечности. Обычный random это реализует. Есть реализация рандома? Только не псевдо, а настоящего?

Это алгоритм, который возвращает неопределенное число в диапазоне от 1 до бесконечности. Обычный random это реализует.

Нет, это нереализуемо вообще никак. Матожидание такого рандома будет равно бесконечности, а бесконечности не существует вообще (нельзя вывести бесконечное число за конечное время. Да и за бесконечное тоже нельзя). За конечное время ты никогда не выведешь число от 1 до бесконечности

бесконечности не существует вообще

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

Ладно, отстань от этой реальности. Даже если рассматривать только модели, МТ не может реализовать подобный алгоритм:

Step 1: Either print 1 on the next square of tape or execute Step 3.
Step 2: Execute Step 1.
Step 3: Halt.

According to the definition of Nondeterministic Turing Machines, the above machine might never halt.

Матожидание такого рандома будет равно бесконечности

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

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

Ну насчет МТ у меня еще есть сомнения, может там физики откроют какие-то законы физики, которые позволяют получить квантовую ерунду c бесконечной памятью, логически эквивалентную МТ(еще непонятно, можно ли проквантовать пространство). А вот про то чтобы получить случайное число от 1 до бесконечности - у меня нет никаких сомнений, что это невозможно вообще никак, даже чисто исходя из теории вероятности. Вот смотри, если ты возвращаешь целое число от 1 до 2 то вероятность каждого исхода у тебя 1/2 или 50% т.к. возможных возвращаемых значений 2. Если возвращать число от 1 до 5 то соотвественно у тебя будет уже 1/5 и 20%. А если ты возвращаешь случайное число от 1 до бесконечности, то вероятность что оно вернет любое конечное число равно 1/∞ что вообще говоря равно 0 и 0% вероятности получить какое-либо число от такого алгоритма.

Даже если рассматривать только модели, МТ не может реализовать подобный алгоритм:

Да ладно, вот я на Си реализовал, неужели МТ не справится?

#include <sys/types.h>
#include <sys/stat.h>
#include <fcntl.h>

#include <stdio.h>

int main(void)
{
  int randomData = open("/dev/random", O_RDONLY);
  unsigned char randchar;
  unsigned char tape[10000] = {};
  unsigned int tape_pos = 0; 
  
step1:  // Either print 1 on the next square of tape or execute Step 3.
  read(randomData,&randchar,1);
  randchar = randchar % 2;
  if(randchar) goto step3;
  printf("write to tape position %u\n", tape_pos);
  tape[tape_pos] = 1;
  tape_pos++;
  
step2: // Execute Step 1.
  goto step1;
  
step3: // Halt.
  printf("Halt.\n");
  return 0;
}

According to the definition of Nondeterministic Turing Machines, the above machine might never halt.

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