psilogic: (Default)
psilogic ([personal profile] psilogic) wrote2005-12-06 10:13 pm

Просто об интуиционистской логике

Есть классическое исчисление высказываний (КИВ), а есть "легендарное" интуиционистское исчисление, aka интуиционистская логика. Подробно о ней можно прочитать у Клини. А почему легендарная? Да потому, что слухи о ней слегка преувеличены.

Вот аксиомы КИВ:


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

Все схемы я разделил на группы. Каждая группа определяет свойства определенной логической операции. Первая и вторая группы должны быть в любом варианте КИВ или же должны быть вместо них другие похожие аксиомы, из которых выводятся эти. Остальные группы необязательны. Например, схемы 11-16 часто пропускают (и, соответственно, в таких вариантах КИВ нет операций <=> и XOR, либо они используются просто как сокращения).

Свойства "=>"
1. A => (B => A)
2. (A => B) => ((A => (B => C)) => (A => C))

Свойства "~"
3. ~~A => A
4. (A => B) => ((A => ~B) => ~A)

Свойства "&":
5. (A & B) => A
6. (A & B) => B
7. A => (B => (A & B))

Свойства "v":
8. A => (A v B)
9. B => (A v B)
10. (A => C) => ((B => C) => ((A v B) => C))

Свойства "<=>":
11. (A <=> B) => (A => B)
12. (A <=> B) => (A <= B)
13. (A => B) => ((B => A) => (A <=> B))

Свойства "+" (XOR):
14. (A + B) => (~A => B)
15.(A + B) => (B => ~A)
16. (A => ~B) => ((~B => A) => (A + B))

Плюс правило вывода modus ponens:
A, A => B |- B



Так вот, в интуиционизме делается одна замена. На место аксиомы номер 3:
3. ~~A => A
ставится другая:
3. ~A => (A => B)

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

Выскажу сугубо личное мнение: в отличии от геометрии КИВ - не очень полезная логика ВНЕ математики. Как следствие, и интуиционистская логика - малополезна ВНЕ математики. Единственное практическое применение, которое мне видится - это тренировка студентов в умении выводить теоремы в сугубо абстрактных условиях.

[identity profile] firtree.livejournal.com 2005-12-07 10:50 am (UTC)(link)
Так, а как насчёт чем наоборот, интуиционизм хорош, или минимум интересен?

[identity profile] psilogic.livejournal.com 2005-12-07 11:14 am (UTC)(link)
Хорош тем, что демонстрирует: можно составить развитую логическую систему, для которой даже найти какие-то применения (как раз из области алгоритмики, как тут говорили) - но притом неклассическую.

А точнее надо Клини перечитывать :)