» Искусственный интеллект. Фантастика? Нет! Реальноасть!!!

Ладно, продолжаем беседу.

Мне кажется, что varjag путает недоказуемость, непротиворечивость и т.д. Естественно, что в рамках теории невозможно доказать аксиомы. Они потому и называются аксиомами, поскольку принимаются без доказательства. Далее, насколько я помню Рассела, он изучал НЕПРОТИВОРЕЧИВОСТЬ, а не НЕПОЛНОТУ математики. Действительно, находясь внутри теории невозможно доказать ее непротиворечивость.

По поводу теоремы Геделя о неполноте. Есть ведь еще и теорема Геделя о полноте. Она гласит о том, что каждое тождественно истинное утверждение в исчислении предикатов может быть доказано. Я не помню точно, есть ли ее аналог для арифметики Пеано, но, по-моему есть.

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

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

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

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

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

veprus

Цитата:

формализовать процесс мышления. И в математике это сделано

опять же, имхо, но формализован не "процесс мышления" , а "процесс решения" - а это совершенно разные вещи...
...постановка задачи подразумевает до 80% решения... и чем сложнее задача, тем меньше логики и больше интуиции на этапе постановки задачи... а вот этап решения можно формализовать, но это в большинстве случаев вторичная задача...
Можно формализовать движение рук рабочего на конвеере, но ни как не движения руки художника...

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

А математика (теоретическая) - это искусство чистого ума, я и говорю о том, что в ней машина никогда не заменит человека.

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

Ну почему именно *машину*?
Вот как звучит т. Геделя о неполноте:
If a proof system for arithmetic is sound (meaning that only true formulas are provable) then there must be a true formula that is not provable.
"Если система доказательств для арифметики непротиворечива (означая что только истинные формулы доказуемы) то должна сущестовать истинная, но недоказуемая формула.
И все!
Где вы видите упоминание машины? Человек с таким же успехом ничего доказать не сможет.

Добавлено
Tim72

> мне кажется, что чисто математический подход к данному вопросу - напоминает попытку написать музыку простым перебором вариантов...

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

Почему я использую слово "машина". Потому что доказательство этой теоремы существенно использует теорию рекурсивных функций и машин Тьюринга.

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

Загвоздка заключается в том, что невозможно написать алгоритм для придумывания новых систем доказательств и потому машина НИКОГДА не заменит человека.

> Потому что доказательство этой теоремы существенно использует теорию рекурсивных функций и машин Тьюринга.

1) Теорема не использует формализм Тьюринга, т.к. появилась на несколько лет раньше.
2) Я не вижу, как из использования рекурсивных функций следует что человек обладатет большими возможностями в формальной арифметике, нежели машина.

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

Неверно.

> невозможно написать алгоритм для придумывания новых систем доказательств и потому машина НИКОГДА не заменит человека.

Откуда это следует?

Цитата:

> Потому что доказательство этой теоремы существенно использует теорию рекурсивных функций и машин Тьюринга.

1) Теорема не использует формализм Тьюринга, т.к. появилась на несколько лет раньше.

Но то доказательство, что знаю я - использует.

[/q]2) Я не вижу, как из использования рекурсивных функций следует что человек обладатет большими возможностями в формальной арифметике, нежели машина. [/q]

Это не из рекурсивных функций следует.

[/q]> Но все дело в том, что мы можем придумать потенциально бесконечно много систем доказательств, таким образом, потенциально, можно доказать любое утверждение.

Неверно.[/q]

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

[/q]> невозможно написать алгоритм для придумывания новых систем доказательств и потому машина НИКОГДА не заменит человека.

Откуда это следует?[/q]

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

Резюме. Машина ТОЧНО не способна доказать все истинные утверждения формальной арифметики. Неспособность человека до сих пор не доказана. По-видимому, в рамках человеческого мышления, она и не может быть доказана, как в рамках арифметики не может быть доказана ее полнота.

> Оно лишь недоказуемо, но и опровержения для него не существует.

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

> Далее, просто добавляем данную машину Тьюринга в нашу систему доказательств, получаем противоречие с теоремой Геделя.

В чем заключается противоречие?

> Неспособность человека до сих пор не доказана.

Доказана. Теоремой Геделя.
Возможно, человек может доказывать истинные, но недоказуемые утверждения, используя пророческий дар, силу внушения, святую воду или зелье мишек Гамми.
Но не в рамках математики.

Цитата:

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

Потенциально можно доказать любое истинное утверждение ФОРМАЛЬНОЙ АРИФМЕТИКИ. А мое утверждение ни коим образом к формальной арифметике не относится.


Цитата:

В чем заключается противоречие?

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

Кстати, ее формулировка на русском.

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

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



Цитата:

Доказана. Теоремой Геделя.

Теорема Геделя относится лишь к формальным системам, каковой человеческое мышление на данный момент не является. По крайней мере формализации для него еще не придумано.

> Потенциально можно доказать любое истинное утверждение ФОРМАЛЬНОЙ АРИФМЕТИКИ.

В рамках непротиворечивой системы - НЕЛЬЗЯ. Прочтите еще раз формулировку теоремы.

> Противоречие заключается в том, что получаем систему доказательств, в которой формальная арифметика остается непротиворечивой и при этом становится полной.

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

> Под формальной системой доказательств понимается набор правил вывода, записанный на языке предикатов.

Неверно. Исчисление предикатов - одна из многих формалльных систем.

> Теорема Геделя относится лишь к формальным системам, каковой человеческое мышление на данный момент не является.

Математическое рассуждение - формально. Вопросы вне математики теорема Геделя не затрагивает.

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

Уважаемые, я вот почитал, и подумал, что за ... пишут.
А как сами теоремы о недоказуемости доказывают?
Может кто ссылку кинет на сайты с математикой... а то что то Вы меня совсем запутали.

Я не поленился найти в интернете утверждение теоремы Геделя и привести его здесь, поскольку Ваша формулировка содержит изъяны. Подчеркиваю, что ВСЕ условия в формулировке существенны.

Если мы ФИКСИРУЕМ арифметику Пеано и ФИКСИРУЕМ систему доказательств, то для ДАННОЙ системы доказательств ДАННАЯ арифметика не будет одновременно непротиворечивой и полной. Но ничто не мешает нам выбрать ДРУГУЮ систему доказательств, в которой арифметика останется непротиворечивой. Это ничему не противоречит. И ниоткуда не следует, что множество недоказуемых утверждений второй системы будет содержать множество недоказуемых утверждений первой системы. А потому ничто не мешает нам предположить, что при этом количество недоказуемых утверждений уменьшится. Пусть даже на одно. Вообще количество утверждений счетно. Потому ничто не мешает нам предположить, меняя сколь угодно много раз систему доказательств, мы можем, в конце концов, доказать ЛЮБОЕ истинное утверждение.

Все дело в том, что процесс ВЫБОРА системы доказательств не является формализованным (по крайней мере, до сих пор формализации нет), а потому из теоремы Геделя не следует, что существуют истинные утверждения, которые не может доказать человек.

Приведенные выше рассуждения не являются ДОКАЗАТЕЛЬСТВОМ того, что ИИ невозможет. Они лишь показывают, за счет чего человек может превзойти машину. Ни доказать, ни опровергнуть их в математике нельзя, поскольку процесс ВЫБОРА системы доказательств в математике не формализован.

Я читал различные источники и лично общался с весьма авторитетными людьми, которые считали, что машина НИКОГДА не сможет заменить человека даже в математике. Но я не использую их мнение, а привожу аргументированное суждение. Прошу Вас поступать также. Я так и не услышал внятного опровержения того факта, что процесс ВЫБОРА системы доказательств нельзя реализовать на машине. Опровержением будет лишь его реализация или доказательство соответствующего теоретического результата, а я о них пока не слышал.

И в конце, просто для справки. У меня в университете логику читал Палютин. Я помню, что после этой теоремы мы его спросили:"Что, значит, существуют теоремы арифметики, которые человек не может доказать?" На что он ответил:"Существуют утверждения, которые не может доказать машина." После этого он привел какую-то аргументацию в защиту человека. Я ее не помню (давно это было), но подозреваю, что он сказал нечто подобное тому, что написано мной. Если Вы изучали логику, то должны знать такую фамилию. К сожалению, не могу сослаться также на Ершова, поскольку с ним мы об этом никогда не говорили.

Прошу отвечать аргументированно!!!

> А как сами теоремы о недоказуемости доказывают?

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

Добавлено
> Но ничто не мешает нам выбрать ДРУГУЮ систему доказательств, в которой арифметика останется непротиворечивой.

В этой ДРУГОЙ системе доказательств всегда будут свои, недоказуемые, но истинные высказывания.

> Потому ничто не мешает нам предположить, меняя сколь угодно много раз систему доказательств, мы можем, в конце концов, доказать ЛЮБОЕ истинное утверждение.

Ни одна из этих систем не сможет доказать ВСЕ истинные утверждения ОДНОВРЕМЕННО. Поэтому пользы от такого подхода - ноль.

> Приведенные выше рассуждения не являются ДОКАЗАТЕЛЬСТВОМ того, что ИИ невозможет.

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

Цитата:

Уважаемые, я вот почитал, и подумал, что за ... пишут.
А как сами теоремы о недоказуемости доказывают?
Может кто ссылку кинет на сайты с математикой... а то что то Вы меня совсем запутали.

Доказательство, которое рассказывали мне (в общих чертах). Предположим, что любое истинное утверждение можно доказать. Поскольку все формализованно и фиксированно, можно ввести нумерацию доказательств, утверждений и т.д. Таким образом, все можно записать с помощью частично-рекурсивных функций. Утверждение о доказуемости означает, что существует функция, которая на любом истинном утверждении выдает ответ, скажем, 1, а на ложном либо 0, либо не останавливается. Поскольку эта функция конкретна, она зависит от конечного набора переменных. Но при этом доказывается, что в непротиворечивой системе существуют функции, которые зависят от сколь угодно большого количества переменных и при этом не могут быть реализованы в качестве функций с меньшим количеством переменных. Понять это очень легко. Предположим, что Fn - множество функций от n переменных. Поскольку все здесь счетно, мы можем ввести нумерацию на этих функциях и рассмотреть функцию G с условием, что G(x1,...,xn,y)=Fy(x1,...,xn). Непротиворечивость арифметики влечет, что данная функция не может быть реализована над меньшим количеством переменных.

Добавлено

Цитата:

Ни одна из этих систем не сможет доказать ВСЕ истинные утверждения ОДНОВРЕМЕННО. Поэтому пользы от такого подхода - ноль.

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

Это аналогично тому, что множество натуральных чисел бесконечно, но добавляя по единице мы в конце концов дойдем до любого натурального числа. Нужно объяснить, почему количество ВСЕХ (а не только истинных) утверждений счетно и почему для них проходит это рассуждение?

Добавлено

Цитата:

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

Я и не сказал, что они что-то доказывают. Я просто объяснил, почему из теоремы Геделя не следует, что человек не может доказать все истинные утверждения.

Добавлено
Забыл добавить. Мы не просто меняем систему доказательств. Мы ее каждый раз добавляем, уменьшая множество недоказуемых утверждений.

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

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

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

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

Добавлено
> Мы ее каждый раз добавляем, уменьшая множество недоказуемых утверждений.

А вот так не получится - система станет противоречивой.

Цитата:

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

Мы не меняем формальную систему. Это все та же арифметика.


Цитата:

А вот так не получится - система станет противоречивой.

В логике доказано, что объединение непротиворечивых систем остается непротиворечивой системой.

Добавлено
Читайте внимательней. Я же подчеркивал, что меняется лишь система доказательств, но не арифметика.


Цитата:

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

Аналогия заключается в процессе исчерпания счетного множества. Это существенно, что множество счетно, так как для континуума такое рассуждение уже не проходит.

Добавлено
Контраргументов пока нет.

> Мы не меняем формальную систему.

Если мы меняем множество аксиом и/или правил вывода, то мы меняем формальную систему.

> В логике доказано, что объединение непротиворечивых систем остается непротиворечивой системой.

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

Цитата:

Если мы меняем множество аксиом и/или правил вывода, то мы меняем формальную систему.

Правила вывода не входят в формальную систему. Равно как и набор аксиом. В формальную систему входит язык с заданными правилами формирования утверждений. Аксиомы арифметики включены в язык.


Цитата:

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

Я говорю о ПРЕДЕЛЕ. Мы не можем его достичь, но можем подойти сколь угодно близко. Потому рано или поздно любое истинное утверждение будет доказано.

Извиняюсь за нескромный вопрос, а Вы сами чем занимаетесь. Слишком нематематическая у Вас аргументация.

> В формальную систему входит язык с заданными правилами формирования утверждений.

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

> Извиняюсь за нескромный вопрос, а Вы сами чем занимаетесь.

В данный момент - я системный аналитик.
Математику нам читали хорошо.

> Слишком нематематическая у Вас аргументация.

В чем это заключается?

Цитата:

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

НЕТ!!! Я уже писал определения здесь и повторять не буду. Чтобы убедить Вас в том, что это разные вещи приведу простой контрпример. Если бы правила вывода и правила формирования утверждений совпадали, то любое утверждение было бы истинным, поскольку любое утверждение, которое можно вывести, является истинным. Спорить было бы не о чем.


Цитата:

В чем это заключается?

Заключается это в том, что Вы придираетесь к отдельным словам, не отвечая по сути. Так поступают профессиональные ораторы. И это означает, что либо Вы не понимаете о чем я вам говорю, а потому не математик, либо Вы не умеете корректно формулировать доказательство, а потому Вы тоже не математик. Надеюсь, без обид?

Добавлено
Да, возможен еще третий вариант. Я объясняю плохо. Но тогда вы должны задавать точные наводящие вопросы, чего тоже не наблюдается.

> Если бы правила вывода и правила формирования утверждений совпадали, то любое утверждение было бы истинным, поскольку любое утверждение, которое можно вывести, является истинным.

В непротиворечивой системе, любое выводимое утверждение является истинным. Но не любое истинное утверждение выводимо.

> Вы придираетесь к отдельным словам, не отвечая по сути.

Я отвечаю по сути, но вы глухи к аргументам.
Каюсь, не надо было мне поминать Тьюринга. С другой стороны, переход на личности - тоже плохой аргумент в споре.

> Надеюсь, без обид?

Знаете, я занимаюсь разработкой компиляторов, поэтому теорию формальных систем волей-неволей пришлось изучить. И, вероятно, я знаю о ней не меньше студента-математика. Без обид?

Цитата:

> Если бы правила вывода и правила формирования утверждений совпадали, то любое утверждение было бы истинным, поскольку любое утверждение, которое можно вывести, является истинным.

В непротиворечивой системе, любое выводимое утверждение является истинным. Но не любое истинное утверждение выводимо.

Где я сказал о ВЫВОДИМОМ утверждении. Я говорю просто об УТВЕРЖДЕНИИ. А множество утверждений никак не зависит от правил вывода. Читайте внимательней. Это как раз то, почему о чем я говорил - не математические рассуждения. Я говорю одно, а Вы отвечаете совсем другое.


Цитата:

Знаете, я занимаюсь разработкой компиляторов, поэтому теорию формальных систем волей-неволей пришлось изучить. И, вероятно, я знаю о ней не меньше студента-математика. Без обид?

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

Добавлено

Цитата:

Я отвечаю по сути, но вы глухи к аргументам.
Каюсь, не надо было мне поминать Тьюринга. С другой стороны, переход на личности - тоже плохой аргумент в споре.

Я не переходил на личности. Просто было интересно, угадал я или нет.

Далее, по теме. Либо мы пользуемся разными определениями, либо... я даже не знаю, что подумать.

Итак. Определения утверждения я уже давал. См. мой пост на стр. 6 данного топика.

Определение правил вывода.

Символ "Т на боку" используется формально, он не входит в язык.

Аксиомы - это КОНЕЧНЫЙ набор схем типа Ф"Т на боку" f(Ф), где f - это некоторое слово, в нашем языке, получаемое из слова Ф.

Правила вывода - это КОНЕЧНЫЙ набор схем типа

f(Ф1,...,Фk)"Т на боку"g(Ф1,...,Фk) "следует" h(Ф1,...Фk)"Т на боку" k(Ф1,...,Фk).

Именно их мы меняем, расширяем и т.д. Все это вместе дает нам систему доказательств.

Добавлено
Система называется непротиворечивой, если в ней невыводима формула вида Ф и "не"Ф. Формула называется истинной, если она дает тождество на нашей системе относительно выбранной интерпретации (ее мы тоже фиксируем). Формула называется выводимой относительно данной системы правил вывода, если если существует дерево доказательств, все начальные вершины которого аксиомы.

Добавлено

Цитата:

Правила вывода - это КОНЕЧНЫЙ набор схем типа

f(Ф1,...,Фk)"Т на боку"g(Ф1,...,Фk) "следует" h(Ф1,...Фk)"Т на боку" k(Ф1,...,Фk).

Извиняюсь, должно быть так:
f(Ф1,...,Фk)"Т на боку"g(Ф1,...,Фk) "следует"Ф, где Ф-формула.

Добавлено
Мы меняем правила вывода. Система, утверждения и истинность от этого НЕ МЕНЯЮТСЯ. Т.о. мы можем расширять и расширять правила вывода, не меняя системы.

Добавлено

Цитата:

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

Теперь понятно, что написано некорректное утверждение?


Цитата:

Если мы меняем множество аксиом и/или правил вывода, то мы меняем формальную систему.

И это утверждение тоже некорректно.


Цитата:

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

Еще раз повторюсь, я говорю о ПРЕДЕЛЕ. Мы НИКОГДА не построим такой системы. Но это не значит, что есть утверждения, которые мы НИКОГДА не докажем.

> А множество утверждений никак не зависит от правил вывода.

Да, но от правил вывода зависит выводимо ли утверждение. А продукции (правила вывода) ЯВЛЯЮТСЯ частью формальной системы.

> Мы меняем правила вывода. Система, утверждения и истинность от этого НЕ МЕНЯЮТСЯ.

Т.е. если в системе мы меняем правило a -> b на a ->с, формальная система не меняется?

> Но это не значит, что есть утверждения, которые мы НИКОГДА не докажем.

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

Добавлено
P.S. Знак "->" в примере выше означает порождение, т.е. правило перезаписи.

Добавлено
P.P.S. Не думайте только что я доказываю возможность human-level AI: я прекрасно вижу практические препятствия, и допускаю что потенциально могут быть и теоретические ограничения. Но теорема о неполноте - не одно из них: по этому поводу в computer sicence есть коненсус на протяжении последних нескольких десятилетий.

Цитата:

Да, но от правил вывода зависит выводимо ли утверждение. А продукции (правила вывода) ЯВЛЯЮТСЯ частью формальной системы.

Я же только что привел все определения. Неужели и после этого не понятно, что алгебраическая система (это так правильно называется) и система доказательств (правила вывода плюс аксиомы) это разные вещи???!!


Цитата:

Т.е. если в системе мы меняем правило a -> b на a ->с, формальная система не меняется?

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


Цитата:

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

Мы расширяем не формализм, не формальную систему, а систему доказательств. Не надо путать и подменять одни понятия другими. Такого термина, как формализм, я нигде не использовал. Попрошу использовать лишь те понятия, для которых даны определения.

1) Вернёмся к самому началу этого топика... Человек - это всего-навсего сложная машина. Он мыслит так же, как и современные компьтеры, при помощи электромагнитных импульсов. Только разрядность мозга человека во много тысячь... миллионов... а может и миллиардов раз больше.
2)

Цитата:

Теорема Геделя относится лишь к формальным системам, каковой человеческое мышление на данный момент не является.

Как я понял из вашего спора мышление машины формально. Из этого утверждения и пункта 1) следует, что мышление человека формально.
3) Математика рассматривает обстрактные прцессы, не имеющие никакого отношения к реальным процессам. Возмём к примеру n-мерные пространства и геометрию в них, что может быть обстрактнее? Пожай только Машине Дьюринга. Так что ваши познания в математике похвальны, но при создании ИИ математик имеет равные шансы с историком добиться успеха. Я не прав? Беседуйте дальше, мне очень интересна ваша беседа, благодаря ей я заполняю свои прорехи в матеметике. Всё очень интересно, только немного не относится к ИИ.

ОК, veprus, давайте опредилимся с терминологией.
Итак:

1) Формальный алфавит - конечная дискретная система сущностей. Сущности обычно называют символами, хотя, строго говоря, они абстрактные сущности, поименованные символами.

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

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

4) Формальная система - абстрактная система сущностей и отношений, которая может быть описана указанием формального алфавита, формального языка на этом алфавите, и формальных правил для порождения высказываний этого формального языка.

То есть, модифицируя правила, мы модифицируем систему.

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

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

В конце-концов, прочитайте первый абзац статьи Геделя с доказательством:
http://www.ddc.net/ygg/etext/godel/godel3.htm

На всякий случай процитирую:
"It may therefore be surmised that these axioms and rules of inference are also sufficient to decide all mathematical questions which can in any way at all be expressed formally in the systems concerned. It is shown below that this is not the case, and that in both the systems mentioned there are in fact relatively simple problems in the theory of ordinary whole numbers4 which cannot be decided from the axioms."

Т.е. невозможно создать формальную систему (в т.ч. и та, которую пытался построить Рассел), которая сможет ответить на все вопросы математики. Заметьте, речь идет о том, что *никто* не сможет построить такую систему - ни машина, ни человек. В начале 30-х о возможности ИИ еще не задумывались.

Добавлено
Prizrak
> Возмём к примеру n-мерные пространства и геометрию в них, что может быть обстрактнее?

Есть вещи и поабстрактнее - теория категорий, например.

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

Цитата:

И еще - реальный мир подчиняется математическим правилам...

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

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