Чисто качественные явления

[epros]

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

Ну вот те возьмите, которые выше. Импликация $a\to b$ определяется как внутренность $\bar a\cup b$, остальное как для решёток множеств по включению.

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

[arseniiv]

Истинное только одно — наибольшее, а все остальные ложные, ну и в определении отрицания используется наименьшее. Формула нулевого порядка тождественно истинна, если для любых значений переменных в любой а. Г. истинна (в классической логике требуется истинность только одной булевой алгебре на $\{0,1\}$, но из неё следует истинность и во всех других*, так что такое обобщение вполне естественно). Остальное аналогично.

* Надеюсь. Понятно, что для булевых алгебр над $\{0,1\}^A$ это работает, но все ли их можно так представить?

[epros]

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

Истинное только одно — наибольшее, а все остальные ложные, ну и в определении отрицания используется наименьшее.

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

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

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

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

[arseniiv]

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

И причём тут отрицание? Отрицание - это значок в синтаксисе.

Это было насчёт интерпретации формулы из этого значка и другой формулы. На всякий случай.

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

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

Давайте только здесь называть это моделью′ (со штрихом).

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

а неразрешимые - по собственному усмотрению (или так, или эдак)

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

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

Как Вы предлагаете их интерпретировать в рамках конструктивной логики? Должны ли доказуемые интерпретироваться как истинные? Должны ли опровержимые интерпретироваться как ложные? А по неразрешимым какие будут предложения?

Все аксиомы интуиционистской логики тождественно истинны, Modus ponens из тождественно истинных выводит такую же. Стало быть, если $\neg A$ доказуема, $A$ имеет какое-то из ложных значений (нельзя однозначно сказать какое).

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

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

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

[epros]

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

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

Да, уточнение принимается.

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

Все аксиомы интуиционистской логики тождественно истинны, Modus ponens из тождественно истинных выводит такую же. Стало быть, если $\neg A$ доказуема, $A$ имеет какое-то из ложных значений (нельзя однозначно сказать какое).

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

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

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

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

[arseniiv]

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

Какая же это интерпретация?

Я привык, что интерпретация определяется индуктивно по структуре формулы (и при этом даны интерпретации всех функциональных и предикатных символов языка), а не через выводимость из данного множества, потому не понял, что речь об этом. Интерпретация тут как в классической, только предикатные символы интерпретируются не как отношения на каком-то $A^n$, а как функции $A^n\to H$, где $H$ — алгебра Гейтинга.

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

Кстати, "множество значений истинности" - не синоним алгебры.

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

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

Какие значения истинности мы в итоге присвоим предложениям: доказуемым, опровержимым и прочим.

Тут просто, по-моему, либо мы идём вашим синтаксическим подходом, но тогда см. ниже, либо мы определяем истинность индуктивно, и она зависит от истинности каких-то других вещей (значений функций $A^n\to H$, сопоставленных предикатам) и не может быть назначена произвольно.

В синтаксическом случае мы тоже не обязаны произвольно что-то назначать неразрешимым формулам. Можно определить значение как класс эквивалентности формул предложений по симметричному затем транзитивному замыканию отношения $(A,B)\mapsto A\vdash B$, и тогда их у нас будет не обязательно два.

-- Вт май 31, 2016 19:35:32 --

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

[epros]

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

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

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

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

только предикатные символы интерпретируются не как отношения на каком-то $A^n$, а как функции $A^n\to H$, где $H$ — алгебра Гейтинга

Какая из алгебр Гейтинга? Кстати, булева алгебра (в том числе, простейшая) - тоже алгебра Гейтинга.

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

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

Как это? А закон исключённого третьего? Ежели я правильно понимаю во всех этих семантиках классического исчисления предикатов первого порядка, предложение $P \vee \neg P$ интерпретируется как истинное тогда и только тогда, когда предложение $P$ истинно или ложно. А ежели $P$ вдруг интерпретируется каким-то другим значением истинности, то $P \vee \neg P$ оказывается невозможным интерпретировать как истинное, что прямо противоречит оному закону.

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

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

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

[arseniiv]

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

То, о чём Вы говорите - это процесс определения интерпретации, но приводит он к тому результату, о котором говорил я.

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

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

Т.е. если мы интерпретируем все аксиомы как истинные, то Ваш процесс индуктивного определения интерпретации по структуре формулы непременно приведёт к тому, что все выводимые предложения интерпретируются как истинные (конечно, если аксиоматика непротиворечива).

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

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

Какая из алгебр Гейтинга? Кстати, булева алгебра (в том числе, простейшая) - тоже алгебра Гейтинга.

Последнее я знаю и, кажется, тоже здесь упоминал. Какая — так понимаю, любая, и дополнительно параметризует интерпретации. Не вижу как можно было бы сделать интерпретацию независимой от неё (можно взять все интерпретации с разными $H$ и одинаковыми интерпретациями сигнатуры, но что потом с ними делать? Значения формул будут из разных $H$, чтобы их пытаться как-то объединить).

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

Как это? А закон исключённого третьего? Ежели я правильно понимаю во всех этих семантиках классического исчисления предикатов первого порядка, предложение $P \vee \neg P$ интерпретируется как истинное тогда и только тогда, когда предложение $P$ истинно или ложно. А ежели $P$ вдруг интерпретируется каким-то другим значением истинности, то $P \vee \neg P$ оказывается невозможным интерпретировать как истинное, что прямо противоречит оному закону.

В любой булевой алгебре по определению $a\vee\neg a = 1$.

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

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

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

[epros]

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

В любой булевой алгебре по определению $a\vee\neg a = 1$.

Это Вы сейчас применяете закон исключённого третьего. А если применять то самое "индуктивное" определение интерпретации по структуре формулы, то:
1) $\neg P$ интерпретируется как истинное тогда и только тогда, когда $P$ ложно.
2) $P \vee Q$ интерпретируется как истинное тогда и только тогда, когда $P$ или $Q$ истинно.
Отсюда:

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

$P \vee \neg P$ интерпретируется как истинное тогда и только тогда, когда предложение $P$ истинно или ложно.

Если $P$ - не предложение, а формула со свободными переменными, то она, разумеется, интерпретируется не значением истинности, а отношением. Но при нулевом количестве свободных переменных это вырождается как раз в значение истинности (одно из двух). Т.е. интерпретация обязана присвоить каждому предложению одно из двух значений истинности, а всё-таки не любое значение "из большей, чем простейшая, булевой алгебры". Я правильно понимаю?

P.S. Я вообще-то за всю эту т.н. "семантику" совершенно не ручаюсь.

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

-- Вт май 31, 2016 22:34:54 --

Добавлю: Я имею в виду конкретный пример, а не "возьмите какую-нибудь алгебру Гейтинга". Скажем, возьмём арифметику Гейтинга (теорию в конструктивном исчислении предикатов первого порядка) и в какой-нибудь её "конструктивной модели" рассмотрим значения истинности нескольких предложений. Например, $0 = 0$ - истинно, $0 = 1$ - ложно. "Существует нечётное совершенное число" - ?

[arseniiv]

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

Это Вы сейчас применяете закон исключённого третьего.

Не думаю, что для произвольной булевой алгебры эту аксиому стоит так называть. Например, $\neg(0,1) = (1,0)$ и $(0,1)\vee(1,0)=(1,1)$, но это не отменяет того, что значений в соответствующей булевой алгебре не меньше трёх.

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

А если применять то самое "индуктивное" определение интерпретации по структуре формулы, то:
1) $\neg P$ интерпретируется как истинное тогда и только тогда, когда $P$ ложно.
2) $P \vee Q$ интерпретируется как истинное тогда и только тогда, когда $P$ или $Q$ истинно.

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

$$\begin{align*} I(\neg A) &= \neg I(A) \equiv I(A)\to0, \\ I(A\vee B) &= I(A)\vee I(B), \\ I(A\wedge B) &= I(A)\wedge I(B), \\ I(A\to B) &= I(A)\to I(B), \\ \end{align*}$$

где $I$ имеет значения в а. Г., и соответствующие $\to,\vee,\wedge$ — это операции из неё.

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

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

А у них, считается, есть ещё какой-то?

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

Тем не менее, поскольку классическая логика утверждает, что конструктивная логика имеет счётное множество значений истинности

Не совсем понятно, что имеется в виду.

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

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

Эм… Мы сначала берём интерпретацию $X$, смотрим на значения формул теории в ней, и когда убеждаемся, что они все 1, тогда и называем её моделью. Интерпретация сигнатуры языка этой теории при этом могла быть мало ли какая. • Как идти в обратную сторону и искать модели какой-то теории, насколько я знаю, в общем случае сложная задача даже в классической логике. Тут я ничем помочь не могу — не знаю. Итак, в одну сторону вы ведь и так знаете, а в другую сложновато — так что я наверняка снова не понял, что спрашивалось.

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

Добавлю: Я имею в виду конкретный пример, а не "возьмите какую-нибудь алгебру Гейтинга". Скажем, возьмём арифметику Гейтинга (теорию в конструктивном исчислении предикатов первого порядка) и в какой-нибудь её "конструктивной модели" рассмотрим значения истинности нескольких предложений. Например, $0 = 0$ - истинно, $0 = 1$ - ложно. "Существует нечётное совершенное число" - ?

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

По поводу сразу всего: не нашёл у себя никакой литературы по обсуждаемым вещам. Без поддержки толку мало, завтра поищу что-нибудь. Или кто-то ещё придёт и рассортирует всё, но название темы и раздел могут отпугивать. Наверно, уже давно надо было отделиться…

[epros]

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

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

Ну, традиция. Именно аксиому в такой записи так называть.

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

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

А она была, польза-то? Я имею в виду не алгебраистам (им-то конечно интересно), а логикам?

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

А у них, считается, есть ещё какой-то?

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

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

Не совсем понятно, что имеется в виду.

Ну, есть какая-то теорема на этот счёт.

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

Наверно, уже давно надо было отделиться…

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

Суть моего первоначального замечания как раз заключалась в том, что значения истинности - это не суть логики, о довесок к ней, иногда лишний. Поэтому интерпретации, которые нужны как раз для назначения предложениям значений истинности, тоже излишество. Суть логики, по моему, заключается в манипулировании утверждениями. Т.е. важно только то, что некоторые из предложений не просто существуют в языке, а утверждаются теорией. Это - единственная модальность или, если хотите, "значение истинности", без которой (которого) нельзя обойтись. Остальные же модальности можно выразить посредством доработки языка. Даже отрицание (т.е. утверждение о ложности предложения) выразимо синтаксическими средствами. А уж всякие более хитрые модальности (типа утверждений о возможности, о желательности или о предположительности) - и подавно лучше выражать дополнительными словами в языке, чем придумывать для каждого из них логические значения.

[arseniiv]

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

А она была, польза-то? Я имею в виду не алгебраистам (им-то конечно интересно), а логикам?

Не знаю, что говорят логики, но это один из способов прийти к интерпретации.

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

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

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

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

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

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

Ну, есть какая-то теорема на этот счёт.

Я что-то в этом ключе слышал, но наверняка у той теоремы есть более точные посылки — имелось в виду это. Может, они весьма специфические. Сразу не видно, почему рассматривать более чем счётные а. Г. уже не нужно.

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

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

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

Хотите закончить — OK. Я сам ничего нового уже не добавлю. Если бы кто-то присоединился, было бы другое дело.

[epros]

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

Сразу не видно, почему рассматривать более чем счётные а. Г. уже не нужно.

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

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

А вообще непонятно, чем два значения истинности лучше не двух. (Понятно, чем они лучше одного.)

Кстати, по-моему, одно логическое значение всё же лучше двух. См. мой предыдущий пост.

[arseniiv]

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

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

Для классической мне это хотя бы (если только я не неправ там выше об изоморфности любой булевой алгебры алгебре булевых функций из чего-нибудь в $\{0,1\}$) очевидно, а тут…

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

Кстати, по-моему, одно логическое значение всё же лучше двух. См. мой предыдущий пост.

Одно значение должно присваиваться всем предложениям, так что это всё равно что не присваивать им никакого. Отделить одни предложения от других оно не сможет. Какая ж тут польза.

[epros]

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

Одно значение должно присваиваться всем предложениям, так что это всё равно что не присваивать им никакого. Отделить одни предложения от других оно не сможет. Какая ж тут польза.

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