Основания математики - элементарное рассмотрение

[vek88]

Если сравнить два номера сообщений, то замечаем, что они разные. Но это мелочи. Реально я хотел сказать, что в названии рассмотренной сематники (и логики) фигурирует Клини, т.е. трехзначная логика (детали см. в цитируемой статье).

На все остальные мысли Вашего сообщения вряд ли смогу ответить - уж очень их много. А вот относительно трехзначной и непрерывной логики выскажусь, что все хорошо на своем месте. Например, мозги человека - это аналог непрерывной К-системы, в которой истиностные значения описываются действительными числами из интервала $[0,1]$ с очевидным определением истиности. Это особенно актуально в случае нечетких плохо формализованных методов и теорий (см. нечеткие логики).
Так что Вы правы.

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

[infoliokrat]

vek88 в сообщении #311510 писал(а):

...
На все остальные мысли Вашего сообщения вряд ли смогу ответить - уж очень их много. А вот относительно трехзначной и непрерывной логики выскажусь, что все хорошо на своем месте. Например, мозги человека - это аналог непрерывной К-системы, в которой истиностные значения описываются действительными числами из интервала $[0,1]$ с очевидным определением истиности. Это особенно актуально в случае нечетких плохо формализованных методов и теорий (см. нечеткие логики).
Так что Вы правы.

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

На все - даже инфолионереально, хотябы на 1 или 2, можно. Прошу поверить, что мнение века88 В нынешний век по поводу нулевой вероятности наличия всеобщего ноля (абстрактого, объективного и субъективного) - это интересно (может не только 1 мне), и про 1математику - тоже.
Заглянул в тему Случайность (почти не случайно), решил что и там простейшей (примитивной двузначной) логике есть где разгуляться. Понимаю, что совсем её хоронить (как коммунизм) пока нельзя, особенно пока монологика есть в повседневной жизни, а не
"в математике - здесь мы привыкли именно к классической логике. И я не вижу причин отказываться от нее"

[epros]

vek88 в сообщении #284163 писал(а):

Но мы не можем в них определить логическое отрицание!?

Для коллег, сомневающихся в этом, следующая задача.

Задача 4. Определите отрицание в канонической системе.

А заглянем-ка сюда. Читаем:

- Формула $\neg P$ определяется как $P \to \bot$, таким образом, доказательством её является функция $f$, которая преобразует доказательство $P$ в доказательство $\bot$.
- $\bot$ - это абсурд, он не должен быть доказуем.

Можно также почитать раздел "Что такое абсурд?". Из приведённых там примеров (типа $0=1$ для арифметики) можно видеть, что это нечто, рассматриваемое как по определению недопустимое в теории.

[vek88]

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

vek88 в сообщении #284163 писал(а):

Но мы не можем в них определить логическое отрицание!?

Для коллег, сомневающихся в этом, следующая задача.

Задача 4. Определите отрицание в канонической системе.

А заглянем-ка сюда. Читаем:

- Формула $\neg P$ определяется как $P \to \bot$, таким образом, доказательством её является функция $f$, которая преобразует доказательство $P$ в доказательство $\bot$.
- $\bot$ - это абсурд, он не должен быть доказуем.

Можно также почитать раздел "Что такое абсурд?". Из приведённых там примеров (типа $0=1$ для арифметики) можно видеть, что это нечто, рассматриваемое как по определению недопустимое в теории.

Не понял, к чему Вы это написали. У меня же сказано, что мы не можем в них определить логическое отрицание!?

Или Вас смутила Задача 4? Дык ведь она и дана для того, чтобы читатель убедился в этой самой невозможности.

Или я что-то не понял в Вашем посте?

[epros]

vek88 в сообщении #355098 писал(а):

...чтобы читатель убедился в этой самой невозможности

Тогда вопрос: чем это с Вашей точки зрения не определение логического отрицания?

[vek88]

epros

Действительно, я поспешил с ответом, не вникнув в суть Вашей ссылки. Посмотрел более внимательно. Итак, Ваша ссылка - на интерпретацию интуиционистской логики. В частности, на интерпретацию отрицания в интуиционизме. Другими словами, BHK interpretation разъясняет смысл интуиционистской логики вообще и интуиционистского отрицания в частности.

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

Цитата:

It is not in general possible for a logical system to have a formal negation operator such that there is a proof of "not" P exactly when there isn't a proof of P ; see Gödel's incompleteness theorems. The BHK interpretation instead takes "not" P to mean that P leads to absurdity, designated , so that a proof of ¬P is a function converting a proof of P into a proof of absurdity.

Кстати, по поводу логики К-систем см. post293513.html#p293513 и далее, включая пост post294896.html#p294896 (о связи логики К-систем с интуиционистской логикой).

[epros]

vek88 в сообщении #355125 писал(а):

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

То, что Вы написали относительно этого самого исчисления Поста в сообщении #283784, является ничем иным, как описанием доказательства в произвольной формальной теории, которое = процедуре (алгоритму) разрешения вопроса об истинности высказывания. Это - подход конструктивизма: интерпретировать истинность процедурным образом, т.е. рассматривать в качестве истинного то и только то, что доказано. То, что в рамках этого подхода неопределимо отрицание, совершенно некорректно. Но этот подход несовместим с классическим представлением об истинности, в частности - с законом исключённого третьего. Это - совсем другой разговор. Классическое представление об истинности не является процедурным и связано с доказуемостью только косвенно - через состоятельность и полноту теории.

[vek88]

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

(1) То, что Вы написали относительно этого самого исчисления Поста в сообщении #283784, является ничем иным, как описанием доказательства в произвольной формальной теории, (2) которое = процедуре (алгоритму) разрешения вопроса об истинности высказывания.

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

1. Это мне понятно. Кстати, это я даже не пишу, а заимствую у Мартин-Лёфа.

2. А это я никак не могу понять. ИМХО понятие доказательства и/или доказуемости не равно понятию разрешающего алгоритма. Более того, существует неразрешимая каноническая система Поста, т.е. такая, для которой не существует разрешающего алгоритма, позволяющего определить доказуемость или недоказуемость в ней произвольного слова в ее алфавите. См. post284210.html#p284210 .
Это, если не ошибаюсь, теорема Чёрча - см. post278622.html#p278622 .

Или я что-то не понял в Вашем посте? Или у Поста?

[epros]

vek88 в сообщении #355225 писал(а):

ИМХО понятие доказательства и/или доказуемости не равно понятию разрешающего алгоритма. Более того, существует неразрешимая каноническая система Поста, т.е. такая, для которой не существует разрешающего алгоритма, позволяющего определить доказуемость или недоказуемость в ней произвольного слова в ее алфавите.

Я не говорил о разрешимости процедуры, я говорил о процедуре разрешения. Доказательство в формальной теории с точки зрения конструктивизма является процедурой разрешения вопроса об истинности высказывания. Это не значит, что таковая процедура обязательно существует и имеет точку останова. Вы именно с изложения этой точки зрения и начали изложение Вашего понимания "основ математики" (которое потом непонятным для меня образом попытались расширить "за пределы конструктивизма"). И на этом этапе (т.е., как я понимаю, пока ещё находясь "в пределах конструктивизма") Вы вдруг заявляете о каких-то проблемах с определением отрицания. Так вот я Вам и говорю, что у конструктивизма нет проблем с определением отрицания. У него есть проблема с законом исключённого третьего. И эта последняя проблема в рамках процедурной интерпретации истинности (когда истинное = доказуемое) неразрешима.

Оставшуюся-то (непроцитированную Вами) часть моего предыдущего поста Вы поняли?

[vek88]

epros

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

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

А в канонической системе (или в любой финитной формальной системе) отрицание определяется элементарно - слово ложно iff оно не выводимо.

Так что Вы говорите все правильно.

Но я говорю о другом - об определении отрицания в канонической системе средствами самой же канонической системы. Разумеется, мне следовало бы сказать это явно - виноват, забыл. См. примеры определений в канонической системе: post284028.html#p284028,
post284163.html#p284163. Кстати, если у Вас остались сомнения, попробуйте решить Задачу 4.

См. также далее К-систему post284210.html#p284210.

В К-системе уже можно определить отрицание (средствами же К-системы) для подкласса полных К-систем (он включает в себя все финитные формальные системы). См. post284468.html#p284468.

Надеюсь, мне удалось прояснить ситуацию?

[epros]

vek88 в сообщении #355360 писал(а):

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

Я явно чего-то не понимаю. Наверное, не хватает терпения вникнуть в Ваше изложение. Но я не вижу проблем определить отрицание в самой формальной теории. Например, в арифметике можно использовать такой закон: $(P \to 0=S(0)) \to \neg P$. Всё, пожалуйста, можно выводить высказывания с символом отрицания. Например, из аксиомы $\exists x [S(x)=0] \to 0=S(0)$ (здесь нет символа отрицания) выводится $\neg \exists x [S(x)=0]$ (отрицательное высказывание).

Или Ваше утверждение апеллирует к теореме Тарского о неопределимости предиката истинности в теории? Так это не мешает определить отрицание...

[vek88]

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

Попробую пояснить на примере. Вот я определяю в канонической системе связку $\vee$ посредством правил вывода

$$\frac{x}{x\vee y},$$

$$\frac{y}{x\vee y}.$$

Это означает следующее. Пусть дана произвольная каноническая система $E$, не содержащей в алфавите знака $\vee$. Строим новую каноническую систему приписыванием к $E$ этих двух правил.

Тогда для этой канонической системы справедливо утверждение: для любых двух слов $a,b$ слово $a\vee b$ выводимо iff выводимо слово $a$ или выводимо слово $b$.

Определить подобным образом отрицание невозможно. Т.е. мы не можем написать правил, определяющих связку $\neg$ так, чтобы добавлением этих правил к произвольной канонической системе мы могли бы сказать, что в полученной системе слово $\neg a$ выводимо iff слово $a$ не выводимо.

Из чего это следует? Да хоть из теоремы Чёрча (существует неразрешимое РП множество).

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

[epros]

vek88 в сообщении #284210 писал(а):

Разумеется, всем очевидно, что для любого натурального числа $n$ выражение $\neg (n \in A)$ истинно тогда и только тогда, когда $n \notin A$.

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

Тоже непонятное заявление. С моей точки зрения $\neg (n \in A)$ и $n \notin A$ - это просто синонимы. Какое это имеет отношение к рекурсивности (или к рекурсивной перечислимости) множества? Получается, что Вы рассматриваете какие-то разные виды отрицания. Я встречал упоминания разных видов отрицания у некоторых авторов. Например, можно ввести понятие "слабого" отрицания как синоним "невыводимости в данной теории", это будет отличаться от определения отрицания, даваемого в BHK interpretation. Однако если Вы говорите о чём-то подобном, то следовало бы сначала уточнить о чём именно.

-- Чт сен 23, 2010 16:01:37 --

vek88 в сообщении #355433 писал(а):

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

Это слишком сильное требование: "любой" канонической системой может оказаться нечто такое, в котором рассматривать любые логические связки будет бессмысленно. Ваш пример с определением дизъюнкции это тоже хорошо иллюстрирует (см. ниже). Разумеется, чтобы определить отрицание в смысле BHK, необходимо иметь две вещи: 1) понятие о выводимости и 2) понятие об абсурде.

vek88 в сообщении #355433 писал(а):

Попробую пояснить на примере. Вот я определяю в канонической системе связку $\vee$ посредством правил вывода

$$\frac{x}{x\vee y},$$

$$\frac{y}{x\vee y}.$$

Это означает следующее. Пусть дана произвольная каноническая система $E$, не содержащей в алфавите знака $\vee$. Строим новую каноническую систему приписыванием к $E$ этих двух правил.

Угу. И если в этой произвольной канонической системе $E$ выводится пустое слово, то получаем в качестве выводов такие вещи, как $\vee \vee$ или $\vee \vee\vee$, что вообще неизвестно что означает.

vek88 в сообщении #355433 писал(а):

Тогда для этой канонической системы справедливо утверждение: для любых двух слов $a,b$ слово $a\vee b$ выводимо iff выводимо слово $a$ или выводимо слово $b$.

А вот и неправда Ваша. В арифметике Пеано первого порядка невыводимо ни утверждение "теорема Гудстейна истинна", ни утверждение "теорема Гудстейна ложна", однако утверждение "теорема Гудстейна истинна"$\vee$"теорема Гудстейна ложна" выводимо тривиально из закона исключённого третьего.

vek88 в сообщении #355433 писал(а):

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

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

[vek88]

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

vek88 в сообщении #284210 писал(а):

Разумеется, всем очевидно, что для любого натурального числа $n$ выражение $\neg (n \in A)$ истинно тогда и только тогда, когда $n \notin A$.

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

Тоже непонятное заявление. С моей точки зрения $\neg (n \in A)$ и $n \notin A$ - это просто синонимы. Какое это имеет отношение к рекурсивности (или к рекурсивной перечислимости) множества? Получается, что Вы рассматриваете какие-то разные виды отрицания. Я встречал упоминания разных видов отрицания у некоторых авторов. Например, можно ввести понятие "слабого" отрицания как синоним "невыводимости в данной теории", это будет отличаться от определения отрицания, даваемого в BHK interpretation. Однако если Вы говорите о чём-то подобном, то следовало бы сначала уточнить о чём именно.

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

А в следующем абзаце говорится элементарная вещь (уверен, что это для Вас абсолютно элементарно) о существовании неразрешимого РП множества. И пока еще ничего отсюда не "получается".

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

Короче, у меня предложение - если Вам интересно, то просмотрите более внимательно мои записки. При этом обратите внимание на основные теоремы и не очень придирайтесь (раньше времени) ко всяким поясняющим комментариям. В частности, когда Вы дойдете до Крипке-Клини семантики, то увидите, что в логике К-систем действительно возникают два отрицания, и что в этой логике "спрятаны" и интуиционистская логика и классическая. За деталями отсылаю к книге "Представление в ЭВМ неформальных процедур" и к статье из сообщения post294016.html#p294016.

Предварительно советую прочитать сообщение post283539.html#p283539, чтобы не было ко мне претензий о нестрогости изложения.

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

А если Вам все это не интересно, то давайте не будем тратить время на обсуждение пустяков.

С уважением,
vek88

ЗЫ. Пока писал ответ, Вы тут еще много чего написали в том же духе. А с пустым слово просто начудили. Так вот, заниматься полемикой ради полемики я не намерен.

[epros]

vek88 в сообщении #355454 писал(а):

Я даже понять не могу, как Вам удалось связать это с РП.

Оба на... Это, вроде, Вы связали. Или я неправильно понял, что слова: "Однако все не столь очевидно" относились именно к равносильности двух упомянутых строчкой выше выражений?

vek88 в сообщении #355454 писал(а):

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

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

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