#ЛогическиеЗадачи
Приходит время каникул, и можно отвлечься от образовательных задач для того, чтобы отдохнуть, решая логические головоломки. Логические задачи на выяснение вопроса: «Кто есть кто?» Предметная область данных задач - персонажи, отвечающие на вопросы Главного Героя (решающего задачу) или сообщающие информацию о предметной области. Причем ответы должны быть односложными (строго да либо нет), а сообщения - высказываниями. Каждому из объектов рассматриваемой предметной области присваивается собственное имя: А, Б, В и так далее.

Каждый из персонажей имеет одно из свойств: 1) отвечая на любые вопросы всегда говорить только правду, т.е. произносить только истинные высказывания – людей, имеющих это свойство обычно называют рыцарями; 2) отвечая на любые вопросы всегда лгать, т.е. произносить только ложные высказывания – людей, имеющих это свойство обычно называют лжецами; 3) отвечая на любые вопросы иногда говорить правду, а иногда лгать – таких персонажей обычно называют нормальными людьми.

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

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

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

Например, выводя формулу В из формул А и Если А, то В по модусу поненс (Modus Ponens), т.е. по единственному правилу вывода для исчисления высказываний, мы получаем её как результат вывода, но формула В сама по себе вовсе не обязательно будет теоремой исчисления высказываний.
Иными словами, формула В окажется выводимой в исчислении высказываний, но не будет считаться доказуемой, или теоремой.

В вышеуказанном случае формула В может оказаться и теоремой, но тогда и только тогда, когда формулы А и Если А, то В тоже окажутся теоремами.

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