Логика и методология математики.

[epros]

Феликс Шмидель в сообщении #952082 писал(а):

То что нет изменений это плохо, потому что я признаю всю предыдущую критику правильной. Что конкретно Вы указали, и я не исправил?

Хм, а что исправили? Вам сказали, что без рассказа о том, что такое метатеория, все объяснения про логику и про формализацию теорий будут профанацией. Вы где-то рассказываете про метатеории, метаязык? Я заметил Вам, что раз уж Вы отличаете «первоначальные» понятия, то следует чётко указать на формальные отличия в способах их определения в теории. Я этого не вижу. Вижу только общие слова про «первоначальность». Ещё я Вам замечал, что «обоснование» аксиом с формальной точки зрения является какой-то бессмыслицей. Тем не менее, Вы продолжаете строить вокруг этого какую-то непонятную мне философию...

А про схемы аксиом Вы поняли? Что схему можно записать предложением метатеории первого порядка? Было бы мудро привести пример предложения второго порядка и для сравнения — тут же соответствующее метапредложение первого порядка. Чтобы читатель увидел разницу: Где есть квантор по предикатам, а где — только по строкам в алфавите языка теории.

Феликс Шмидель в сообщении #952082 писал(а):

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

А правильно ли будет мне навязывать Вам своё понимание, которое тоже не бесспорно? Ваше изложение ведь содержит не только формально строго определённые вещи, но и изрядную долю философии. А здесь возможны различные интерпретации слов. Например, «доказательство» в формальном смысле — это просто конечная последовательность предложений, получаемых в результате применения правил вывода. Но есть более широкое значение слова «доказательство», употребляемое в естественном языке, которое Вы обсуждаете в своём тексте. С моей точки зрения было бы мудро продемонстрировать, что всякое доказательство в естественном смысле можно неким способом свести к формальному доказательству. Но будет ли правильным мне предлагать свою точку зрения на всю эту философию, раз у Вас есть своя?

[Феликс Шмидель]

epros в сообщении #952127 писал(а):

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

Рассказать про метатеорию ещё не пришло время - это только первый параграф. Я понял, что схемы-аксиом являются не утверждениями теории, а выражениями метатеории. Соответственно, входящие в них переменные являются метапеременными. Моё понимание аксиом-схем изменилось в результате Вашей критики, так как раньше я считал аксиомы-схемы и входящие в них переменные принадлежащими теории.

epros в сообщении #952127 писал(а):

Я заметил Вам, что раз уж Вы отличаете «первоначальные» понятия, то следует чётко указать на формальные отличия в способах их определения в теории. Я этого не вижу. Вижу только общие слова про «первоначальность».

Я сказал, что общепринятое название первоначальных понятий - неопределяемые понятия, что эти понятия определяются системой аксиом, что это особый вид определения.
Какие формальные отличия Вы имеете ввиду?

epros в сообщении #952127 писал(а):

Ещё я Вам замечал, что «обоснование» аксиом с формальной точки зрения является какой-то бессмыслицей. Тем не менее, Вы продолжаете строить вокруг этого какую-то непонятную мне философию...

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

epros в сообщении #952127 писал(а):

А про схемы аксиом Вы поняли? Что схему можно записать предложением метатеории первого порядка? Было бы мудро привести пример предложения второго порядка и для сравнения — тут же соответствующее метапредложение первого порядка. Чтобы читатель увидел разницу: Где есть квантор по предикатам, а где — только по строкам в алфавите языка теории.

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

epros в сообщении #952127 писал(а):

А правильно ли будет мне навязывать Вам своё понимание, которое тоже не бесспорно? Ваше изложение ведь содержит не только формально строго определённые вещи, но и изрядную долю философии. А здесь возможны различные интерпретации слов. Например, «доказательство» в формальном смысле — это просто конечная последовательность предложений, получаемых в результате применения правил вывода. Но есть более широкое значение слова «доказательство», употребляемое в естественном языке, которое Вы обсуждаете в своём тексте. С моей точки зрения было бы мудро продемонстрировать, что всякое доказательство в естественном смысле можно неким способом свести к формальному доказательству. Но будет ли правильным мне предлагать свою точку зрения на всю эту философию, раз у Вас есть своя?

Речь не идёт о навязывании, наоборот я хочу знать Вашу точку зрения. Я тоже об этом думал: что всякое доказательство в естественном смысле можно свести к формальному доказательству по той причине, что любую теорему классической математики можно доказать в теории множеств. Как Вы предлагаете это продемонстрировать?

[epros]

Феликс Шмидель в сообщении #952221 писал(а):

Речь не идёт о навязывании, наоборот я хочу знать Вашу точку зрения.

В итоге Вы меня раскрутите на писание собственного эссе.

Феликс Шмидель в сообщении #952221 писал(а):

Рассказать про метатеорию ещё не пришло время

Хм, а вот я бы с этого начал. Логика такая: Вот Вы рассказываете о всяких понятиях логики первого порядка. А откуда это всё взялось? Именно задачей метатеории является определение всех этих понятий и правил работы с ними.

Феликс Шмидель в сообщении #952221 писал(а):

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

А в чём конкретно заключается их особенность? Такая недосказанность характерна для философских текстов...

Феликс Шмидель в сообщении #952221 писал(а):

Какие формальные отличия Вы имеете ввиду?

Это уж как Вы определите. Я, например, могу понять отличия между понятием, для которого выделен символ в языке теории (плюс в арифметике Пеано) или не выделен (минус в той же теории). Но такое отличие не всегда существенно.

Феликс Шмидель в сообщении #952221 писал(а):

Я оставил обоснование того, что "первоначальные истины доказать невозможно". Это нужно убрать?

Ну, если Вы в состоянии чётко определить что такое «первоначальные истины» и считаете это важным... По моим понятиям аксиомы не тянут на это высокое звание.

Феликс Шмидель в сообщении #952221 писал(а):

Я не понимаю, что утверждает схема-аксиом - если это формула метатеории, то она должна что-то утверждать о теории. Для меня это просто выражение, в которое подставляют формулы теории вместо метапеременной.

Да, именно так: строка, подставляемая вместо метапеременной.

Феликс Шмидель в сообщении #952221 писал(а):

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

Это и есть квантор по строкам в алфавите языка теории. Например, где-то так:
$\forall \varphi \, \text{isFormula}(\varphi) \to A \vdash
где записанное в синтаксисе метатеории выражение $A \vdash означает утверждение о выводимости строки $\text{string}$ в теории $A$, а точками обозначена конкатенация.

Собственно, это формализация схемы индукции.

Феликс Шмидель в сообщении #952221 писал(а):

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

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

[Феликс Шмидель]

У Вас могут быть более важные дела, чем написание эссе.
Нужно разбавить мой философский текст примерами, чтобы было понятнее о чём речь.
Фразу о "первоначальных истинах" нужно изменить, потому что сегодня они первоначальные, а завтра, глядишь, и непервоначальные, а бывает и наоборот.
Бывает и так, что вместо аксиомы принимают её отрицание и ничего не случается, в том числе и в теории множеств.
В евклидовой геометрии есть строгое доказательство, что сумма углов треугольника равна 180 градусам, а в неевклидовой строгое доказательство отрицания этого утверждения.
Это нуждается в объяснении, которого в моём тексте нет.
Я бы не хотел подробно говорить о метатеории, можно только упомянуть её в связи с аксиомными схемами.
Я же ставлю целью не введение в математическую логику, а введение в практическое обоснование обычной математики.
Так что, я почти во всём с Вами согласен, но не во всём.
Я пишу эти версии для удовольствия, вряд ли я что-нибудь закончу.
Большое спасибо за критику, надеюсь получать её и дальше.

[epros]

Феликс Шмидель в сообщении #952651 писал(а):

В евклидовой геометрии есть строгое доказательство, что сумма углов треугольника равна 180 градусам, а в неевклидовой строгое доказательство отрицания этого утверждения.
Это нуждается в объяснении, которого в моём тексте нет.

Зачем? Что тут нужно объяснять? Разные теории с разными аксиоматиками предназначены для разных применений. Понятие «теории» ведь можно низвести до конкретной задачи. Например, есть более или менее общая физическая теория, согласно которой скорость является производной перемещения по времени. Если дополнить её аксиомами: «Скорость автобуса на всём пути равна 60 км/ч» и «Расстояние до пункта прибытия составляет 30 км», то мы получим условия конкретной задачи на нахождение времени прибытия. Причем задачу можно трактовать как вариант теории, а решение — как вывод в этой теории. Соответственно, какой смысл придавать указанным двум аксиомам статус каких-то «первоначальных истин» и пытаться их как-то «объяснить»? Аксиомы всего лишь соответствуют конкретной задаче.

Или Вы пытаетесь найти заложенное в основания математики «абсолютное знание»? Так оно вряд ли существует.

Феликс Шмидель в сообщении #952651 писал(а):

Я бы не хотел подробно говорить о метатеории, можно только упомянуть её в связи с аксиомными схемами.

Дело не только в схемах. Без понимания того, что за процессом определения теории на заднем плане всегда маячит метатеория — никуда. Возьмем к примеру Ваше любимое правило вывода modus ponens. Как оно записывается в теории? Да никак. Зато оно прекрасно записывается утверждением метатеории.

Феликс Шмидель в сообщении #952651 писал(а):

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

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

[Феликс Шмидель]

epros в сообщении #952972 писал(а):

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

Я имел ввиду другое: на практике математика обычно обосновывается теорий множеств $ZFC$.
К этому можно добавить простое объяснение логики первого порядка, формального метода и общей концепции оснований математики.

Я обязательно прислушаюсь к Вашим словам о метатеории.

[Феликс Шмидель]

epros в сообщении #952972 писал(а):

Разные теории с разными аксиоматиками предназначены для разных применений. Понятие «теории» ведь можно низвести до конкретной задачи. Например, есть более или менее общая физическая теория, согласно которой скорость является производной перемещения по времени. Если дополнить её аксиомами: «Скорость автобуса на всём пути равна 60 км/ч» и «Расстояние до пункта прибытия составляет 30 км», то мы получим условия конкретной задачи на нахождение времени прибытия. Причем задачу можно трактовать как вариант теории, а решение — как вывод в этой теории. Соответственно, какой смысл придавать указанным двум аксиомам статус каких-то «первоначальных истин» и пытаться их как-то «объяснить»? Аксиомы всего лишь соответствуют конкретной задаче.

Согласен. Но аксиомы в вашем примере отличаются от аксиом Пеано или даже постулатов Евклида (кроме постулата о параллельных).
Аксиомы в Вашем примере не очевидны: скорость автобуса может быть 60 км/час, а может быть и 80.
Такие аксиомы относятся не только к основаниям теории, но и влияют на рассуждения в этой теории.
В то время, как аксиомы Пеано относятся к основаниям арифметики, но арифметические доказательства могут вполне обходиться без этих аксиом.
То же самое можно сказать и о геометрии Евклида.
В геометрических доказательствах, Евклид ссылается на аксиомы и постулаты, где аксиомы - очевидные утверждения общего характера, а постулаты - то, что мы называем геометрическими аксиомами.
В доказательствах используются и другие очевидные утверждения, поэтому если бы не было ссылок на аксиомы, доказательства бы не пострадали.
Но в этом случае, мы не узнали бы из "Начал" Евклида о важном методе обоснования математики.
Впрочем один постулат не казался Евклиду достаточно очевидным, и на него стоило ссылаться.
Неудачные попытки на протяжении 2-ух тысяч лет доказать его привели в 19-ом веке к созданию неевклидовой геометрии.

[epros]

Феликс Шмидель в сообщении #953134 писал(а):

на практике математика обычно обосновывается теорий множеств $ZFC$.

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

-- Сб дек 27, 2014 21:56:56 --

Феликс Шмидель в сообщении #953186 писал(а):

Такие аксиомы относятся не только к основаниям теории, но и влияют на рассуждения в этой теории.

Не понимаю о чём Вы сейчас говорите. Аксиомы, как аксиомы.

Феликс Шмидель в сообщении #953186 писал(а):

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

Как это обходиться без аксиом? Всё равно любое доказательство на что-то опирается. Хотя про это могли забыть сказать явно и у читателя создаётся иллюзия, что оно убедительно «само по себе», независимо ни от каких аксиом.

[Феликс Шмидель]

epros в сообщении #953188 писал(а):

Как это обходиться без аксиом? Всё равно любое доказательство на что-то опирается. Хотя про это могли забыть сказать явно и у читателя создаётся иллюзия, что оно убедительно «само по себе», независимо ни от каких аксиом.

Разве Евклид, доказывая теорему о бесконечности последовательности простых чисел думал об аксиомах Пеано? Или он думал об аксиомах $ZFC$? Нет, конечно.

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

[Someone]

Феликс Шмидель в сообщении #953134 писал(а):

на практике математика обычно обосновывается теорий множеств $ZFC$

Вот только не надо сводить всю математику к ZFC. Ничего ZFC не обосновывает, её саму дай бог обосновать. Это просто очень удобный инструмент. Но не всюду.

[arseniiv]

Феликс Шмидель в сообщении #953220 писал(а):

Математические понятия являются абстракциями реальности

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

Феликс Шмидель в сообщении #953220 писал(а):

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

Кстати, и логика ведь тоже не единственна, об этом вы ещё не упоминали в тексте.

[Феликс Шмидель]

После заявлений, что от $ZFC$ нулевая польза, и что она ничего не обосновывает, я полностью сбит с толку.
Хотелось бы понять, какая вообще польза от оснований математики и в чём их цель?

[epros]

Феликс Шмидель в сообщении #953220 писал(а):

Разве Евклид, доказывая теорему о бесконечности последовательности простых чисел думал об аксиомах Пеано? Или он думал об аксиомах $ZFC$?

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

Феликс Шмидель в сообщении #953220 писал(а):

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

Что аксиомы — это что-то «очевидное», это здорово устаревшая точка зрения. Инвариантность скорости света не очевидна. А многие очевидные вещи, такие, как абсолютность времени во всей Вселенной, являются неправомерными обобщениями ограниченного опыта субъекта и по этой причине — ложны.

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

Феликс Шмидель в сообщении #953220 писал(а):

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

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

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

Феликс Шмидель в сообщении #953382 писал(а):

После заявлений, что от $ZFC$ нулевая польза, и что она ничего не обосновывает, я полностью сбит с толку.
Хотелось бы понять, какая вообще польза от оснований математики и в чём их цель?

А в чём Вы видите эти основания? Вот есть такое направление — reverse mathematics, которое занимается именно исследованиями оснований математики. Но там постановка проблемы звучит более конкретно: Для получения каких математических результатов какая аксиоматика минимально необходима.

А если Вы ищите абсолютное знание, то математика вряд ли в этом поможет.

[Xaositect]

Феликс Шмидель в сообщении #953382 писал(а):

Хотелось бы понять, какая вообще польза от оснований математики и в чём их цель?

Цель была в том, чтобы построить формальную систему, в которую можно вложить любую математическую теорию. Получилось, в принципе, неплохо: вся математика начала века в теорию множеств влезла, теория множеств сама по себе оказалась интересной математической структурой, теория ординальных и кардинальных чисел в частности оказалась очень полезной. Соответственно, была установлена некая платформа, к которой можно обращаться в случае, когда какие-то утверждения в теории зависят от особенностей этой объемлющей структуры. Иногда, правда, вылезают артефакты этой системы в виде неизмеримых множеств и прочих неприятных вещей, но к ним привыкли.

[Феликс Шмидель]

Xaositect в сообщении #953437 писал(а):

Цель была в том, чтобы построить формальную систему, в которую можно вложить любую математическую теорию.

Построили:

Xaositect в сообщении #953437 писал(а):

вся математика начала века в теорию множеств влезла

А потом приходит уважаемый epros и говорит, что польза от этого нулевая:

epros в сообщении #953188 писал(а):

Феликс Шмидель в сообщении #953134 писал(а):

на практике математика обычно обосновывается теорий множеств $ZFC$.

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

И как прикажете это понимать?