Knowlus logo
Intellect for rent

Доказательство в логике предикатов первого порядка

Говорят "истина относительна", "истины не существует". Эти утверждения ложны. Истина существует. Легко можно придумать неограниченное число истинных утверждений. "Марсиане нападут на Землю или марсиане не нападут на Землю" - истина, независимо от того, существуют марсиане или нет, и утверждение останется истинным, даже если не существует ни Земли, ни Марса, и сами мы подключены к Матрице.

Сервис доказательства на платформе Knowlus позволяет Вам доказать любое принципиально доказуемое утверждение1.

Как спорить

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

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

Сначала надо определиться, относится ли спорная посылка к субъективным или объективным суждениям. Субъективные суждения отражают личные предпочтения или личные обстоятельства. Если соперник называет кефир вкусным напитком, а Вы с этим не согласны, искать компромисс бесполезно. Если у соперника нету дома, пожары ему не страшны то и правильное расположение огнетушителя его (соперника, а не дом) не интересует. Спорить с субъективными утверждениями бесполезно и не верно.

Объективные суждения описывают окружающий мир, вселенную: "пропускная способность одной полосы дороги не превышает 100 машин в минуту", "зимой идут дожди", "легализация ношения короткоствола снижает число преступлений насильственного характера", "светло", "Гундяев - примерный христианин". Для конструктивного спора не обязательно иметь строгое доказательство объективных посылок, достаточно согласия об их истинности с оппонентом. Иногда имеет смысл согласиться и с посылкой, которую Вы считаете ложной. Например, в случае, если Вы видите, что выводы оппонента ложны даже в его системе ценностей и аксиом. Указав на ошибки в рассуждениях, Вы подтолкнете оппонента к переоценке его взглядов или аксиом. Это безусловно считается победой в споре. А сторона, признавшая ошибочность своих выводов, достойна уважения. Далеко не многие способны скорректировать свои взгляды даже под давлением четкой логической аргументации.

Если же вы имеете противоположные представления об истинности посылки со своим оппонентом, попробуйте обосновать свою посылку из более очевидных предположений. Может потребоваться несколько итераций, прежде чем вы найдете утверждения, с которыми вы оба согласны. Например, "Общественное благосостояние больше, если больше благосостояние каждого член общества", "P≠NP" (если речь не идет о доказательстве самого утверждения), "В ВОВ погибло более 27 млн. советских людей" (при этом вы можете расходиться в более точных оценках).

Вкратце:

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

Как пользоваться

Новое доказательство

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

Предикаты

Предикат определяется именем и арностью - числом мест для термов. Предикат может принимать одно из двух значений: ИСТИНА и ЛОЖЬ.

Предикатам и константам можно давать произвольные имена, в том числе включающие пробелы, если заключить их в кавычки: "Сегодня отмечается"("День конституции РФ"). Но теперь кавычки - часть имени предиката или константы. "красный" и красный - разные константы. Использование кавычек для имен переменных и функций, не являющихся константами, не допускается.

На данный момент поддерживается инфиксная форма записи бинарных предикатов. Не забудьте вставить пробелы между предикатом и термами, иначе a>b распознается как нуль-местный предикат с именем a>b. С пробелами a > b распознается как двухместный предикат > c термами a и b.

Сложнее обстоит дело с формализацией обещаний и утверждений человека. Мы можем ввести посылку Обещал(Обещалкин, "отремонтировать все дороги в области"). Объект обещания хотелось бы формализовать с помощью квантора общности, но кванторы применяются только к переменным, а "отремонтировать все дороги в области" в нашей посылке константа. Поэтому лучшее, что мы можем сделать, обернуть его предикатом истинности Выполнено("отремонтировать все дороги в области") и попытаться вставить в дополнительные условия как целое.
0Обещал($x, $y) ∧ ¬Выполнено($y)→¬"Выполняет обещания"($x) premise
1(∃ $r Дорога($r) ∧ ¬Отремонтирована($r))→¬Выполнено("отремонтировать все дороги в области") premise
2Обещал(Обещалкин, "отремонтировать все дороги в области") premise
Добавив сведения о реальном состоянии дорог можно провести следующий вывод:
0Обещал($x, $y) ∧ ¬Выполнено($y)→¬"Выполняет обещания"($x) premise
1(∃ $r Дорога($r) ∧ ¬Отремонтирована($r))→¬Выполнено("отремонтировать все дороги в области") premise
2Обещал(Обещалкин, "отремонтировать все дороги в области") premise
3Дорога(Окружная) premise
4¬Отремонтирована(Окружная) premise
5Дорога(Окружная) ∧ ¬Отремонтирована(Окружная) conjunction introduction [3, 4]
6∃ $r Дорога($r) ∧ ¬Отремонтирована($r) existential introduction [5]
$r/Окружная
7¬Выполнено("отремонтировать все дороги в области") modus ponens [6, 1]
8Обещал(Обещалкин, "отремонтировать все дороги в области") ∧ ¬Выполнено("отремонтировать все дороги в области") conjunction introduction [2, 7]
9Обещал(Обещалкин, "отремонтировать все дороги в области") ∧ ¬Выполнено("отремонтировать все дороги в области")→¬"Выполняет обещания"(Обещалкин) substitution [0]
Обещалкин/$x, "отремонтировать все дороги в области"/$y
10¬"Выполняет обещания"(Обещалкин) modus ponens [8, 9]

Термы

Терм - это либо переменная, либо функция, либо константа.

Переменные

Переменные обозначаются знаком доллара и именем переменной, например, $x, $сотрудник. Использование кавычек не допускается.

Функции и константы

К именам функций и констант предъявляются такие же требования, как и к предикатам. Система отличает их от предикатов по положению в структуре формулы. Функции и константы могут быть только внутри предикатов, и ни один предикат не может быть внутри функции. После имени функции, в скобках следует список термов, через запятую. Если функция не зависит от термов (нуль-местная функция, также называемая константой), то скобки можно опустить.

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

Константа - частный случай функции, а именно, нуль-местная функция. Соответственно константа не зависит от переменных.

Логика предикатов ничего не знает о числах. Вы спокойно можете добавлять утверждения Больше(10, 100), Произведение(2, 2, 5), (1>2) ∧ (2>1).

Посылки

Посылки отражают факты и законы внешнего мира. Введенная посылка предполагается истинной. Поэтому, если Вы хотите добавить отрицательное утверждение, поставьте знак отрицания перед утверждением: ~(начало(лекция, "9:00") & заведен(будильник, "9:00") ).
Поддерживаются формулы исчисления высказываний и логики предикатов первого порядка.

Следствия

Список правил вывода в логике предикатов (англ.).

Коммутативность и ассоциативность конъюнкции и дизъюнкции заложены в реализацию. Так конъюнкция конъюнкций рассматривается как одна большая конъюнкция множества подформул. Также в кванторах не имеет значения порядок переменных и одинаковые кванторы объединяются.

∀ $x ∀ $y $z P($x, $y, $z) ⇔ ∀ $x $y $z P($x, $y, $z)

Но порядок чередования кванторов общности и существования, сохраняется.

Предположения

Противоречия

Ограничения

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

ЧАВО

Что означает значок на логотипе?

⊨ - в логике этот символ ставится перед общезначимой формулой. Общезначимая формула истинна независимо от интерпретации предикатов и термов.

Какие символы можно использовать для обозночения логических связок?

'exist' | '\exist' | '\E' | '∃' '\u8707' | '\u2203'
'forall' | '\forall' | '\A' | '∀' | '\u8704' | '\u2200'
'=>' | '->' | 'impl' | '\u2283' | '\u2192' | '\u21D2' | '→'
'AND' | '&' | 'and' | 'And' | '\u2227'
'OR' | '|' | 'or' | 'Or' | '\u2228'
¬ '~' | '-' | 'not' | 'Not' | 'NOT' | '¬' | '\u00AC'
False 'false' | 'FALSE' | 'False'
True 'true' | 'TRUE' | 'True'
Кавычки печатать не надо.

Какой приоритет логических операторов?

Я добавил импликацию, а она воспринимается как один предикат, или не распознается совсем

В именах предикатов и констант можно использовать символы '>', '<', '=', '_', '@', '#', '%', '^', '*'. Поэтому, если знак импликации не отделен пробелом, он воспринимается как часть имени предиката. Добавьте пробел перед и после знака импликации.

Я хочу добавить логическое следствие формул, но система не предлагает мой вариант следствия

Валидность логического следствия зависит не только от выбранных формул, но и от контекста: посылок и активных предположений. Например, из формулы P(const) следует формула ∀ $x P($x), если терм const не входит ни в одну посылку или предположение, и не следует, если входит.

Почему кнопка редактирования описания доступна только для посылок?

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

Примечания

1 Можно доказать любую выводимую формулу в логике предикатов первого порядка, т.е. формулы могут содержать квантификацию по переменным, а квантифация по предикатам не допускается.

en_US © 2012-2016 Ilya Ashikhmin
Request result: