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

[vek88]

AlexDem в сообщении #293055 писал(а):

И вопрос: что гарантирует нам, что если $P < Q$, то $\neg(Q < P$)? То есть - почему возможна частичная упорядоченность по этому отношению, почему не может быть циклических зависимостей вида:

$$P = \frac{a_1 \ominus b}a, Q = \frac{b_1 \ominus a}b$$

? А если они есть, то какой из двух выводов считать И-выводом?

Здесь вообще-то надо было уточнить что такое $a_1, b_1$. Судя по Вашей записи - это выводы, а не слова (поскольку $P, Q$ - выводы). Если так, то вчера я ответил Вам все правильно по этому поводу.

Если же $a_1, b_1$ не выводы, а слова, то $P, Q$ - не выводы, а всего лишь применения каких-то правил Вашей К-системы.

Пример. Пусть $a, b, a_1,b_1$ слова в заданном алфавите и К-система состоит из двух правил

$$\frac{a_1 \ominus b}a, \frac{b_1 \ominus a}b.$$

В этой К-системе вообще нет ни одного вывода. Следовательно, слова $a, b, a_1,b_1$ не имеют вывода и поэтому они ложны.

[AlexDem]

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

Здесь вообще-то надо было уточнить что такое $a_1, b_1$. Судя по Вашей записи - это выводы, а не слова (поскольку $P, Q$ - выводы). Если так, то вчера я ответил Вам все правильно по этому поводу.

vek88, спасибо. Да, я подразумевал, что для слов $a_1, b_1$ существуют какие-нибудь выводы в рассматриваемой К-системе (например, аксиомы), тем более, что их, действительно, можно исключить из примера. Получается, что отсутствие циклов (и неразрешимых слов) гарантировано именно в полных К-системах.

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

Слово ложно в К-системе, если все его выводы являются Л-выводами (или оно вообще не имеет вывода).
К-система, все слова которой разрешимы - истинны или ложны - называется полной.

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

[vek88]

AlexDem в сообщении #293318 писал(а):

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

Слово ложно в К-системе, если все его выводы являются Л-выводами (или оно вообще не имеет вывода).
К-система, все слова которой разрешимы - истинны или ложны - называется полной.

(1) Всё смотрю, что нового дают исключения по сравнению с обычными вариантами логик без них... (2) Вот Вы говорили о полноте и непротиворечивости арифметики в полных К-системах. Я так понимаю, это означает, что существует некоторая полная К-система, такая что каждой выводимой в обычном смысле формуле арифметики можно сопоставить некоторое её истинное слово. При этом все невыводимые в данной К-системе слова алфавита - автоматически ложны, так что оказывается, что невыводимые в арифметике истинные формулы здесь обязательно оказываются выводимы, в том числе и формула, утверждающая непротиворечивость арифметики? (3) А вот формула, утверждающая непротиворечивость самой этой К-системы, тоже выводима?

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

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

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

3. Если мы представили арифметику в полной К-системе, то вопрос непротиворечивости просто не возникает, т.к. по определению К-системы любое слово в алфавите этой К-системы не может быть одновременно истинным и ложным.

P.S. Если я правильно понял из Вашего профиля, Вы - программист. Тогда "глазами программиста" советую Вам просмотреть Главу 8 книги "Представление в ЭВМ ...", в частности:
- раздел 8.3 (Универсальная К-система), в котором фактически выписана конкретная очень полезная "программа", относительная простая по программистским меркам;
- раздел 8.4 (Арифметические множества), в котором как раз и рассмотрено представление арифметики в полной К-системе.

[AlexDem]

Хорошо, посмотрю. На всякий случай, напомню, что я прервал повествование на следующем месте:

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

Для затравки дальнейшего обсуждения вопрос: какая теперь у нас логика?

[vek88]

Итак, продолжим разбираться с логикой - сначала мы рассмотрим логику полных К-систем. Напомню, что в полных К-системах представимы (=определимы) традиционные логические связки $\vee, \wedge$, отрицание $\neg$ и кванторы $\forall, \exists.$ Известно (надеюсь), что можно ограничиться и меньшим количеством связок и кванторов (исключительно для удобства - меньше писанины в тех случаях, когда рассматриваются теоретические вопросы).

Мы далее рассматриваем язык первого порядка $L$, в котором используются

$$\wedge, \neg, \forall.$$

Не вдаваясь в изложение скушных деталей, примем на веру, что любая формула языка $L$ представима в полной К-системе. Следовательно, любая замкнутая формула либо истинна, либо ложна.

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

Разумеется, мы предполагаем, что во всех конкретных полных К-системах формулы строятся по одним и тем же правилам, причем $\wedge, \neg, \forall.$ определяются одинаковым образом. С учетом этого естественно считать (мы к этому и стремились в рамках полных К-систем), что логическими законами в классе всех полных К-систем будут тавтологии, т.е. тождественно истинные формулы языка $L$.

Более точно, формула языка $L$ тождественно истинна тогда и только тогда, когда она истинна во всех полных К-системах.

И этими логическими законами являются в точности тавтологии классической логики (=классического исчисления предикатов).

Например, формула $\neg(R(a) \wedge \neg R(a))$ истинна в любой полной К-системе независимо от определения предиката $R$ при условии, что это определение полно.

Обратим внимание, что вышесказанное объясняет определенную "размытость" границы между теорией и метатеорией в полных К-системах (и в реальной жизни), поскольку любой логический закон метатеории представим и в теории!

Таким образом, язык $L$ достаточен для формулирования логических законов полных К-систем.

А теперь вернемся к произвольным К-системам. Здесь все значительно сложнее. Следующее утверждение показывает, что истина произвольных К-систем не может быть сформулирована в языке $L$.

Теорема. Пусть $F$ - произвольная формула языка $L$. Существует К-система, в которой эта формула неразрешима (ни истинна, ни ложна).

[vek88]

Идем дальше. Чтобы спасти положение, расширяем язык $L$ до метаязыка $L^*$. При этом, поскольку нам понадобится еще один знак отрицания, договоримся прежнее отрицание (в языке $L$) заменить на знак $\sim$.

Определение. (a) Если $A$ формула языка $L$, то $A$ формула языка $L^*$.

(b) Если $A, B$ формулы языка $L^*$, то

$$(\neg A), (A \wedge B), (A \vee B), (A \rightarrow B), (\forall A), (\exists A)$$

формулы языка $L^*$.

Обратим внимание, что в языке $L^*$ у нас фактически две системы связок. Первая образована связками $\sim, \wedge, \forall$ языка $L.$ Вторая - связками $\neg, \wedge, \vee, \exists, \forall$ языка $L^*$ в соответствии с Определением. Первая система связок применима ко всякой формуле языка $L$, вторая - ко всякой формуле $L^*$.

С учетом сказанного, связки $\wedge, \forall$ применимы и к формулам $L$, и к формулам $L^*$. Поэтому их значение зависит от контекста. Данное обстоятельство могло бы привести к коллизии двух значений этих связок применительно к формулам $L$ (т.к. они являются одновременно и формулами $L^*$), но в дальнейшем мы увидим, что оба этих значения применительно к формулам $L$ совпадают.

[vek88]

Забыл сказать, что мое повествование о логике К-систем основано на статье из Lecture Notes in AI от 1994 г. под названием A Kripke-Kleene Logic over General Logic Programs. Статью можно найти по названию в Google.

Краткое пояснение. В этой статье логические программы рассматриваются в точности в терминах К-систем, но используется язык, принятый в языке Пролог. Вместо понятия истинности в К-системах используется принятая у специалистов по Прологу well-founded semantics (WFS) логических программ, изобретенная, насколько мне известно, в 1990 г.

Замечание. WFS эквивалентна понятию истинности в К-системах, которое опубликовано впервые в 1986 г. (см. ссылку в Представление в ЭВМ ...).

[vek88]

Обратим внимание, что в $L^*$ мы имеем два вида отрицания: $\sim$ и $\neg$. Первое применимо только к формулам $L$, второе - к формулам $L^*$.

Пример. Если $A, B$ формулы $L^*$, то

$$\neg(A \vee B)$$

формула $L^*$. С другой стороны,

$$\sim(A \vee B)$$

в общем случае не является формулой $L^*$, и является таковой только если $(A \vee B)$ формула $L$.

[vek88]

Семантика Крипке

Итак, мы определили синтаксис нашего метаязыка $L^*$. Теперь, следуя Крипке, мы определим семантику этого языка, т.е. припишем смысл формулам этого языка, опираясь на понятие К-системы (в алфавите языка $L$).

Множество всех К-систем, ассоциированных с языком $L$, мы обозначим через $U$. В терминологии Крипке всякое подмножество $U$ называется возможным миром, а множество всех подмножеств $P(U)$ - это универсум возможных миров.

Для возможных миров $X, Y$ мы говорим, что мир $Y$ доступен из мира $X$, если и только если $Y \subseteq X$.

Истиные формулы $L^*$ определяются индуктивно в три шага.

Сначала мы определяем отношение "возможный мир $X$ вынуждает (forces - за перевод не уверен) формулу $A$ языка $L$", обозначаемое $X \vdash A$. Грубо говоря, это отношение означает, что формула $A$ истинна или является "логическим законом" во всем возможном мире $X$. Затем мы расширяем отношение вынуждения на формулы $L^*$, приписывая связкам языка $L^*$ семантику возможных миров. И окончательно мы определим истину - формула $L^*$ истинна, если она вынуждается в мире всех К-систем.

В следующем сообщении мы приведем формальное определение семантики, которое является очевидной адаптацией известных работ Крипке (см. ссылки [7, 8] в упомянутой статье).

PS. Вообще говоря, традиционно, работы Крипке выходят за рамки элементарного рассмотрения. Однако мы ограничимся рассмотрением сути, которая ИМХО элементарна и легко усваивается на уровне элементарного здравого смысла.

[vek88]

Определение. Пусть $X, Y \subseteq U.$

(1) Пусть $A$ - формула языка $L.$ $X \vdash A$ iff $A$ истинна во всякой К-системе $P \in X.$

(2) Пусть $A, B$ - формулы языка $L^*.$

(a) $X \vdash A \wedge B$ iff $X \vdash A$ и $X \vdash B.$
(b) $X \vdash A \vee B$ iff $X \vdash A$ или $X \vdash B.$
(c) $X \vdash A \rightarrow B$ iff, для всех $Y \subseteq X$, если $Y \vdash A$, то $Y \vdash B.$
(d) $X \vdash \neg A$ iff $Y \nvdash A$ для любого непустого $Y \subseteq X.$
(e) $X \vdash (\forall x)A(x)$ iff, для всех $x$, $X \vdash A(x).$
(f) $X \vdash (\exists x)A(x)$ iff существет $x$ такой, что $X \vdash A(x).$

(3) Формула языка $L^*$ истинна iff $U \vdash A.$

Далее нам осталось рассмотреть:
- несколько простых примеров, иллюстрирующих построенную логику;
- связь построенной логики с классической и интуиционистской логиками.

[vek88]

Пример 1. Напомним, что связки $\wedge, \forall$ используются и в $L$ и в $L^*$. Например, если $A, B$ формулы $L$, то связка $\wedge$ в формуле $A \wedge B$ может рассматриваться либо как элемент $L$, либо как элемент $L^*$. Покажем, что значение (=смысл) выражения $X \vdash A \wedge B$ не зависит от этого выбора.

В первом случае $X \vdash A \wedge B$ означает, что $A \wedge B$ истинно в К-системе $P$ для всякой $P \in X$. Во втором - что $X \vdash A $ и $X \vdash B .$ Поскольку $A, B$ формулы $L$, по определению (1) оба значения совпадают.

Аналогично можно показать, что то же самое имеет место для квантора $\forall$ - если $A(x)$ формула $L$, то оба значения выражения $X \vdash (\forall x) A(x)$ совпадают.

-- Чт мар 04, 2010 23:33:32 --

Пример 2. Приведем пример истинной формулы. Пусть $A$ формула $L^*$. Очевидно, что, для всех $X \subseteq U$, если $X \vdash A$, то $X \vdash A$. Тогда по определению (2c)

$$U \vdash A \rightarrow A$$

и значит по определению (3) формула

$$A \rightarrow A$$

истинна.

-- Чт мар 04, 2010 23:40:59 --

Пример 3. Пусть $A$ формула $L$. Поскольку формула языка $L$

$$A \wedge \sim A$$

не является истинной в любой К-системе, формула

$$\neg (A \wedge \sim A)$$

истинна по определению (2d).

Эта формула утверждает, что "противоречие в смысле отрицания $\sim$" невозможно в К-системе.

[vek88]

Пример 4. Пусть $A$ формула языка $L$. Тогда, для всех $X \subseteq U$, если $X \vdash \sim A$, то $X \vdash \neg A$. Таким образом, по определению (2c)

$$ U \vdash \sim A \rightarrow \neg A $$

и, следовательно, по определению (3) формула

$$ \sim A \rightarrow \neg A $$

истинна.

Эта формула утверждает, что "если факт ложен в К-системе, то этот факт не может быть истинным". Заметим, что обратное не имеет места - формула

$$ \neg A \rightarrow \sim A $$

не является истинной в нашей логике (если факт не является истинным в К-системе, он не обязательно ложен).

Теперь несколько слов о связи построенной логики с интуиционизмом и классической логикой.

Определение. Если формула языка $L^*$ не содержит знака $\sim$, она называется интуиционистской формулой.

Теорема 1. Интуиционистская формула истинна (в нашей логике) iff она выводима в интуиционистском исчислении предикатов.

Теорема 2. Пусть $A$ формула языка $A.$ $A$ является (классической) тавтологией iff формула $\neg \sim A$ истинна (в нашей логике).

Грубо говоря, это означает, что наша логика содержит каждую классическую тавтологию с префиксом $\neg \sim $.

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

[infoliokrat]

AlexDem в сообщении #293446 писал(а):

Хорошо, посмотрю. На всякий случай, напомню, что я прервал повествование на следующем месте:

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

Для затравки дальнейшего обсуждения вопрос: какая теперь у нас логика?

:)

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

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

Но можно!?
А в троичной логике (ДА, неопределено, НЕТ), на ваш взгляд уютнее?

[vek88]

infoliokrat в сообщении #310641 писал(а):

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

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

Но можно!?
А в троичной логике (ДА, неопределено, НЕТ), на ваш взгляд уютнее?

Минутку!? Но ведь Клини - это и означает трехзначную логику (см. выше). Только для третьего значения использовался термин "неразрешимо". См. сообщение #294016.

[infoliokrat]

Кликнув по ссылке попал на это:

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

Обратим внимание, что в $L^*$ мы имеем два вида отрицания: $\sim$ и $\neg$. Первое применимо только к формулам $L$, второе - к формулам $L^*$.

Пример. Если $A, B$ формулы $L^*$, то

$$\neg(A \vee B)$$

формула $L^*$. С другой стороны,

$$\sim(A \vee B)$$

в общем случае не является формулой $L^*$, и является таковой только если $(A \vee B)$ формула $L$.

Не заблудился? Только по поиску "трехзначная логика" Правка-найти
туда не попадал. По "неразрешимо", - туда можно дойти. Но так как я древний (пенсионер), то в голове сидит Да, Неопределено, Нет (или 0, *, 1 - когда-то в 75-м году мне пришлось сопровождать в производстве УПД-2, в котором ИМС серии "Тропа" истиной считали НОЛЬ- отсутствие сигнала, т.е. "землю", а 1- ложно), а также четверичная ДА, Да с-, НЕТ с+, НЕТ. (Тут очевидно * далее делится на Нет+ Да- ). Понравился пример: в точке на небе есть звезда, нет, * (светит "сгоревшая", свет от "молодой" ещё не дошел, а для 5-ричной логики опять добавляется *). К четверичной и тп. это тоже так легко формально применимо для вас? Так что прошу простить великодушно: в бане (из-за пара) не всё видно.. Ещё:

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

Вот еще камень ... есть интуитивная арифметика. А есть ее финитная формализация. ... Гедель своей теоремой лишь доказал ограниченность финитных формализаций.
А что с наивной теорией множеств? Ведь ее, из-за своих человечьих ошибок мышления, люди затоптали в грязь и выбросили на помойку!?
Так вот, с моей точки зрения, интуитивная теория множеств жива и будет жить вечно. Более того, для нее аналогично арифметике любая финитная формализация неполна (надеюсь, это всем очевидно). Следовательно, любая ее финитная аксиоматика "обедняет" теорию множеств. А народу это не нужно.
...
И как был прав Гильберт, сказав: "Никто не изгонит нас из рая, созданного Кантором!"
А чтоб никто больше не порочил нашу любимую теорию множеств, мы контролируем полноту всех используемых определений множеств, т.е. проверяем полноту этих определений в К-системах.
Кто-нибудь еще против наивной теории множеств? Тогда мы идем к вам.

(Ту-то и "сермяжная правда", Мое мнение о ней следующее. Как абстрактный математический факт - эта логика для меня интересна. )
Чем наивнее, тем эффетивнее (может быть) И Велихов, и Лихачёв о взаимосвязи сложного и простого говорили.
Как по мне, то "непрерывная" чаще людьми используется, чем двоичная. И только лишь когда оппоненты хотят "своего", они от собеседника требуют ответа: так ты мне скажи ДА или НЕТ?
"Грубо говоря, это означает, что наша логика содержит каждую классическую тавтологию с префиксом ."
...жить и работать в такой логике, на мой взгляд, очень неудобно.
Добавлю: терпеть почти ненавижу (хотя даже в щахматы люблю проигрывать), когда самым весомым логическим обоснованием чего-либо является: да какая разница?, требуя, чтобы сделали не так, как положено.
И очень интересно мнение Века (как Пеано) об арифметике, в которой 0 (всеобщий) исключить.. Ну недостижим он, и всё! Что касается того, что за каждым числом идет очередное - тоже не факт. (Если дискретную плоскость - из "пчелинных сот " прономеровать одной координатой - по кривой, по спирали ... Но это уже другая история)