Закон исключенного третьего

[knizhnik]

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

[arseniiv]

Как-как, у интуиционистской логики ведь тоже есть интерпретации — только там не булевы алгебры, а алгебры Гейтинга (Heyting). Если формула истинна во всех интерпретациях, она, как обычно, зовётся тождественно истинной.

[knizhnik]

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

Если формула истинна

Для начала нужно понять, какая формула. Формул бесконечно много. Как их описать? Как проверить каждую конкретную?

[arseniiv]

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

[knizhnik]

Что-то я не понял.

Ладно, вот формула $((p\to (q\to r))\to ((p\to q)\to (p\to r)))$. Как определить, выводима ли она в интуиционистских ИВ? Дайте любой способ.

[Anton_Peplov]

knizhnik в сообщении #1206529 писал(а):

Как определить, выводима ли она в интуиционистских ИВ?

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

[knizhnik]

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

[Anton_Peplov]

Ах, Вам нужен алгоритм, который за обозримое время останавливается? Это я поддерживаю и одобряю. Мне он тоже нужен. Как и алгоритм, который за обозримое время найдет доказательство или опровержение любого поданного на вход утверждения (ладно, кроме тех, для которых это запрещает герр Гедель). Как и ключ от квартиры, где деньги лежат.
Только вот я понимаю, что волшебных палочек не бывает. А Вы?

[Xaositect]

Определение интуиционистской выводимости - PSPACE-полная задача: https://www.sciencedirect.com/science/a ... 7579900069

[mihaild]

knizhnik в сообщении #1206529 писал(а):

Дайте любой способ.

Перебираем интуиционистские доказательства и одновременно конечные шкалы Крипке. Рано или поздно наткнемся либо на доказательство, либо на шкалу, в которой формула не выполнена.

[knizhnik]

Anton_Peplov в сообщении #1206539 писал(а):

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

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

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

Определение интуиционистской выводимости - PSPACE-полная задача: https://www.sciencedirect.com/science/a ... 7579900069

Что-то не получилось. A problem was encountered providing the content you requested
Please try again later or contact our Customer Service team providing the below reference number.

mihaild, я не знаю, что такое шкалы Крипке. Может вы можете предложить статьи или учебные материалы, которые мне помогут?

[Anton_Peplov]

knizhnik в сообщении #1206547 писал(а):

Это однозначный метод проверки с всегда конечным числом действий.

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

knizhnik в сообщении #1206547 писал(а):

Одно ясно - вы в этом не разбираетесь

Я уже покраснел и ушел плакать.

[mihaild]

knizhnik, Верещагин, Шень "Языки и исчисления", 2.4.

[knizhnik]

Anton_Peplov в сообщении #1206555 писал(а):

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

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

Anton_Peplov в сообщении #1206555 писал(а):

Я уже покраснел и ушел плакать.

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

[Xaositect]

knizhnik в сообщении #1206547 писал(а):

Что-то не получилось. A problem was encountered providing the content you requested
Please try again later or contact our Customer Service team providing the below reference number.

Странно, у меня работает. Попробуйте другие ссылки: https://scholar.google.de/scholar?clust ... as_sdt=0,5