логика высказываний не нужна

[mclaudt]

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

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

Поведение идентичное, а догмы разные. Как это в программировании называется? Правильно, быдлокодерство. Лишние сущности.

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

Надо сносить все бульдозером и строить заново.

[ewert]

бог мой, что за страсти-то такие. А кто такие таджики?...

[PAV]

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

Но сперва постройте. Почему сразу всех на разрушение тянет?

[mclaudt]

PAV в сообщении #339419 писал(а):

Сначала постройте рядом с существующим свое. Затем убедите общественность, что Ваше лучше, и надо переехать.

То есть не я один вижу эту нестройность?

[PAV]

mclaudt в сообщении #339421 писал(а):

То есть не я один вижу эту нестройность?

Понятия не имею. Разве из моего поста это следует?

[mclaudt]

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

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

Поэтому сложилось представление о ненужности этого раздела. Примерно занимает нишу "логики для философов", по аналогии с "математика для экономиста", "квантовая физика для полных даунов" и "развивающие игры для детей с поражением ЦНС".

Это действительно так, или же на логике высказываний держится что-то важное?



Хотелось послушать, как относятся к логике высказываний сами математики.

[PAV]

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

[mclaudt]

PAV в сообщении #339422 писал(а):

mclaudt в сообщении #339421 писал(а):

То есть не я один вижу эту нестройность?

Понятия не имею. Разве из моего поста это следует?

В контексте математически несовершенных человеческих коммуникаций могло бы следовать. Потому я и уточнил.

[Sonic86]

Давайте мыслить конструктивно. Вот из всего Вашего текста наиболее интересно следующее:

mclaudt писал(а):

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

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

[mclaudt]

Sonic86 в сообщении #339464 писал(а):

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

Так как раз из обсуждения наипримитивнейшей задачки все и пошло.

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

Задача:в рамках исчисления высказываний доказать теорему ((p -> q) -> p) -> p.

ЛВ:

 Есть лемма о том, что из предположений об истинности подформул можно вывести либо саму формулу (если она верная) либо ее отрицание.

1) Гипотеза p

not q, (p->q)->p, p выводится p

2) Гипотеза not p

Множество not q, not p, (p->q)->p противоричиво. Из not p, not q выводится (p->q) а затем и not ((p->q)->p), следовательно по аксиоме A9 из него выводится все что угодно, в том числе и p. 

Логика первого порядка:

((p -> q) -> p) -> p <=> [замена импликации на дизьюнкцию] <=> ((not(p) || q) -> p) -> p <=> [то же самое + де Морган] <=> ((p && not(q)) || p) -> p <=> [закон поглощения] <=> p -> p <=> [тривиально] <=> true

Вопрос о том, то проще - вопрос предпочтений. Но в первом больше юриспруденции.

Однако вопрос был не про простоту, а про то, зачем плодить лишние сущности?

Да, формально на логике высказываний делжится логика первого порядка. Но зачем наплодили одинаково ведущих себя сущностей? Я про импликации в ЛПП и ЛВ. Одна есть функция, а другая - просто закорючка в правилах вывода.

Неужели это неизбежно?

PS Решения не мои, накопипастил не проверяя. Это не важно.

[Sonic86]

Ну так хоть вроде понятно.
Так, я не спец, если что - меня обязательно поправьте, а то вдруг я чушь скажу.

Вроде бы ЛВ - это аксиоматизация ЛПП. Так? Если да, то вроде бы совсем неплохо, если одна теория имеет несколько разных аксиоматизаций. Ну взять ту же геометрию Евклида... Но я, честно говоря, плохо знаю, чем именно ЛВ от ЛПП отличается. М.б. в ЛВ проще и понятнее доказываются какие-то теоремы, или ЛВ как-то очевидным образом обобщается или еще что-то. Вроде бы это стандартный способ проверки качества теории - если ее народ не используется, ну значит она и не нужна особо... То есть - не нравится ЛВ - не пользуйтесь.

-- Пт июл 16, 2010 08:49:37 --

Насчет того, где больше юриспруденции - я не понял. Ни в ЛВ, ни а ЛПП ее вообще вроде бы нету.

[Андрей АK]

mclaudt в сообщении #339421 писал(а):

То есть не я один вижу эту нестройность?

Советую ещё присмотреться ... к "нечеткой логике".
По своим догмам = теоремам/аксиомам - это чистой воды теория вероятностей.

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

[Maslov]

mclaudt в сообщении #339421 писал(а):

То есть не я один вижу эту нестройность?

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

mclaudt в сообщении #339426 писал(а):

Это действительно так, или же на логике высказываний держится что-то важное?

Вся мат. логика и держится.

Ну а прежде, чем предлагать бульдозер, полистайте учебник, например, Клини, Мендельсона или Игошина.

[mclaudt]

Цитата:

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

Просто с текущим уровнем развития информатики держать на бумаге и в головах единое здание математических выводов нерационально до поросячьего визга.

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

Тогда можно будет скормить её компьютеру на предмет поиска "похожестей", причем двух типов:

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

2. Глубокого изоморфизма между на первый взгляд между несвязаными разделами математики. Это намного сложнее. Например, забив в базу определение перестановки и определение конечной группы, программа должна нащупать изоморфизм и на выходе дать теорему Кэли. Это не просто анализ уже внесенных в базу закономерностей, а поиск новых. Это напоминает проекты по автоматическому доказательству теорем (QED и аналоги).

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

-- Пт июл 16, 2010 16:24:17 --

Цитата:

есть формальная аксиматическая теория под названием исчисление (логика) высказываний, и есть её модель -- алгебра высказываний

Если честно, первый раз слышу, чтобы у аксиоматических теорий были модели. Что вообще такое "модель теории", в вашем понимании?

-- Пт июл 16, 2010 16:30:09 --

Цитата:

полистайте учебник, например, Клини, Мендельсона или Игошина.

Картинка удалена как не относящаяся к делу, а также за использование ненормативной английской лексики /Toucan.

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

[Maslov]

mclaudt в сообщении #339532 писал(а):

Если честно, первый раз слышу, чтобы у аксиоматических теорий были модели.

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

mclaudt в сообщении #339532 писал(а):

Что вообще такое "модель теории", в вашем понимании?

Мое понимание самое что ни на есть традиционное:

1. Формальная теория определяется алфавитом, правилом построения формул, набором аксиом и правилами вывода.

2. Интерпретация формальной теории -- это система, состоящая из непустого множества $D$ (область интерпретации) и соответствия, относящего каждой предикатной букве некоторое отношение в $D,$ каждой функциональной букве -- некоторую операцию в $D$ и каждой предметной постоянной -- некоторый элемент из $D$.
Всякая формула формальной теории превращается в данной интерпретации в высказывание, которое может быть истинным или ложным. Открытая формула формальной называется истинной в данной интерпретации, если она превращается в истинное высказывание при любой подстановке предметных констант.

3. Интерпретация называется моделью формальной теории, если в ней истинна любая формула, выводимая в этой формальной теории.

В частности, в алгебре высказываний множество $D$ -- это $\{ T, F\},$ а каждой функциональной букве (логической связке) соответствует операция над элементами $D,$ задаваемая, например, таблицей истинности.

-- Пт июл 16, 2010 18:11:21 --

mclaudt в сообщении #339532 писал(а):

А ты думаешь, что идентичность зависимости между правилами вывода и зависимости между логическими формулами с импликацией мне приснилась?

Если Вас не очень затруднит, обращайтесь ко мне, пожалуйста, "на Вы".