Совпадение теорем

[arseniiv]

(Мета)

Sinoid в сообщении #1150166 писал(а):

Быть может, вам будет удобно начать новую тему?

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

Sinoid в сообщении #1150174 писал(а):

а arseniiv'у уже это длинное обсуждение доставляет дискомфорт

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

[Someone]

Sinoid, Вы окончательно всех запутали.
Вы явно путаете предметную теорию и метатеорию. Предметная теория ничего не знает ни о таблицах истинности, ни об их строках, ни вообще об истинности или ложности. Эти понятия относятся к метатеории, точнее, к той её части, которая называется "теория моделей".

Когда мы в предметной теории говорим "Если $A$, то $B$", то мы не имеем в виду никаких таблиц истинности. Мы имеем в виду, что если в (некоторой) модели предметной теории выполняется $A$, то в ней выполняется и $B$.

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

[Sinoid]

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

Итак, есть теорема "Если число делится на 6, то оно делится и на 3". Но это только краткая форма записи определенной мысли. Запишем эту мысль в полном виде: Предложение "Если истина то, что число делится на 6, то будет истина и то, что оно делится на 3" - истина.

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

[mihaild]

Sinoid в сообщении #1150366 писал(а):

Но это только краткая форма записи определенной мысли. Запишем эту мысль в полном виде

Нет, это две разных "мысли". Первая была утверждением в теории (видимо, какой-то арифметической). Вторая - уже утверждение метатеории.
Вторая не является "полным видом" первой, это просто разные утверждения в разных теориях.

UPD: на самом деле, зависит от формализации "если истино $X$", где $X$ - конкретная формула. Это можно формализовать и как утверждение метатеории (которая умеет говорить об истинности произвольных утверждений теории - и, в частности, об истинности $X$), и как утверждение теории (просто как $X$ - т.к. формула конкретная).

[arseniiv]

Ещё можно добавить, что «теорема $A$» значит, что $A$ выводима (где-то там), а не то, что $A$ истинна (где-то там), и Someone выводимости не упоминал.

[Sinoid]

arseniiv в сообщении #1150373 писал(а):

Ещё можно добавить, что «теорема $A$» значит, что $A$ выводима (где-то там), а не то, что $A$ истинна (где-то там), и Someone выводимости не упоминал.

Так значит, когда мы писали

Sinoid в сообщении #1150366 писал(а):

Итак, есть теорема "Если число делится на 6, то оно делится и на 3".

мы в эти слова вкладывали смысл, что если выводимо (им аксиом или уже доказанных теорем), что число ($a$) делится на 6, то из тех же теорем выводимо и то, что это же число делится и на 3?

[mihaild]

Sinoid в сообщении #1150377 писал(а):

я в эти слова вкладывал смысл, что если выводимо (им аксиом или уже доказанных теорем), что число ($a$) делится на 6, то из тех же теорем выводимо и то, что это же число делится и на 3?

Я не знаю, что вы вкладывали в эти слова:-) Но вообще они обычно означают "в теории выводится, что $\forall a: 6|a \rigtharrow 3 | a$" (FIX: $\forall a: 6|a \rightarrow 3 | a$) (это уже утверждение метатеории, т.к. говорит про выводимость в теории). С Вашей интерпретацией могут быть проблемы в том, что в теории не обязательно выразимы все объекты модели этой теории, так что непонятно, как формулировать "доказано, что $a$ делится на $6$". Если ограничиться только выразимыми объектами - то получившееся утверждение ("для любого выразимого $a$, если $\vdash P(a)$, то $\vdash Q(a)$"), вообще говоря, слабее, чем "$\vdash \forall a: P(a) \rightarrow Q(a)$".

[Sinoid]

mihaild в сообщении #1150378 писал(а):

Я не знаю, что вы вкладывали в эти слова:-)

я исправил у себя
А вот тут

mihaild в сообщении #1150378 писал(а):

$\forall a: 6|a \rigtharrow 3 | a$

ничего не забыли? Просто выглядит как-то необычно.

[mihaild]

Sinoid в сообщении #1150381 писал(а):

А вот тут

mihaild в сообщении #1150378 писал(а):

$\forall a: 6|a \rigtharrow 3 | a$

ничего не забыли? Просто выглядит как-то необычно.

right неправильно написал (в TeX видно)

[Sinoid]

Итак, соберем все в одно место. Когда в книге написана теорема "Если число делится на 6, то оно делится и на 3", авторы имели ввиду не истинность теоремы, а

mihaild в сообщении #1150378 писал(а):

в теории выводится, что $\forall a: 6|a \rigtharrow 3 | a$" (FIX: $\forall a: 6|a \rightarrow 3 | a$) (это уже утверждение метатеории, т.к. говорит про выводимость в теории).

употребляемая здесь импликация принадлежит метатеории и не принадлежит предметной теории. Правильно?

[mihaild]

Sinoid в сообщении #1150388 писал(а):

Когда в книге написана теорема "Если число делится на 6, то оно делится и на 3", авторы имели ввиду не истинность теоремы

Нельзя говорить об "истинности" теоремы без указания конкретной модели. Можно говорить об истинности утверждения в модели, или о его выводимости в теории. Почти всегда все рассуждения идут внутри некоторой конкретной теории $T$, и в итоге доказывается теорема $A$ этой теории.

Sinoid в сообщении #1150388 писал(а):

употребляемая здесь импликация принадлежит метатеории и не принадлежит предметной теории

Говорить о принадлежности связки теории нехорошо.
Нет, утверждение "$\forall a \ldots$ - это утверждение теории. А вот утверждение $T \vdash \forall a \ldots$ - уже утверждение метатеории.

[Someone]

mihaild в сообщении #1150370 писал(а):

UPD: на самом деле, зависит от формализации "если истино $X$", где $X$ - конкретная формула. Это можно формализовать и как утверждение метатеории (которая умеет говорить об истинности произвольных утверждений теории - и, в частности, об истинности $X$), и как утверждение теории (просто как $X$ - т.к. формула конкретная).

Тут есть одна пакость: в предметной теории невозможно выразить истинность формулы. Эта теория ничего об истинности не знает. Особенно удивляться этому не следует, так как, вообще говоря, есть формулы, истинность которых зависит от модели (правда, не во всякой теории; в арифметике Пеано такие формулы точно есть, а в исчислении высказываний их нет). Поэтому как утверждение теории истинность формулы формализовать нельзя.

Sinoid в сообщении #1150388 писал(а):

Когда в книге написана теорема "Если число делится на 6, то оно делится и на 3", авторы имели ввиду не истинность теоремы, а

выводимость формулы $\forall a(6\mid a\rightarrow 3\mid a)$.

Sinoid в сообщении #1150388 писал(а):

употребляемая здесь импликация принадлежит метатеории и не принадлежит предметной теории. Правильно?

Неправильно. Написанная формула принадлежит языку предметной теории. А метатеории принадлежит утверждение о выводимости этой формулы, то есть, другая формула: $\vdash\forall a(6\mid a\rightarrow 3\mid a)$. В частности, символ "$\rightarrow$" принадлежит алфавиту предметной теории.

[mihaild]

Someone в сообщении #1150392 писал(а):

есть формулы, истинность которых зависит от модели (правда, не во всякой теории; в арифметике Пеано такие формулы точно есть, а в исчислении высказываний их нет)

Модель - это интерпретация переменных? Тогда истинность формулы $a$ зависит от модели.

Someone в сообщении #1150392 писал(а):

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

А что развалится, если мы будем под "$X$ истинно" понимать как синоним $X$? (в смысле, это всё равно было синтаксически бессмысленное высказывание)

[Someone]

mihaild в сообщении #1150398 писал(а):

Модель - это интерпретация переменных?

Не любая интерпретация. Только такая, в которой все аксиомы истинны.

Someone в сообщении #1150392 писал(а):

есть формулы, истинность которых зависит от модели (… в исчислении высказываний их нет)

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

mihaild в сообщении #1150398 писал(а):

А что развалится, если мы будем под "$X$ истинно" понимать как синоним $X$?

А вдруг $X$ ложно?

[mihaild]

Someone в сообщении #1150406 писал(а):

Не любая интерпретация. Только такая, в которой все аксиомы истинны.

Теорема о корректности же утверждает, что аксиомы общезначимы (или вы про модели конкретных теорий в исчислении высказываний?).

Someone в сообщении #1150406 писал(а):

А вдруг $X$ ложно?

И что?
У нас есть конкретное высказывание $X$ в теории $T$. Мы хотим формализовать высказывание "$X$ истинно" в какой-нибудь теории. Почему нельзя его формализовать как $X$ в самой $T$?