Просто об интуиционистской логике
Есть классическое исчисление высказываний (КИВ), а есть "легендарное" интуиционистское исчисление, 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)
В результате получается забавное исчисление... в нем обходятся некоторые трудности, зато нет некоторых интересных результатов. Это что-то типа неевклидовой геометрии: там тоже заменили одну аксиому и получили новые виды геометрий.
Выскажу сугубо личное мнение: в отличии от геометрии КИВ - не очень полезная логика ВНЕ математики. Как следствие, и интуиционистская логика - малополезна ВНЕ математики. Единственное практическое применение, которое мне видится - это тренировка студентов в умении выводить теоремы в сугубо абстрактных условиях.
Вот аксиомы КИВ:
Аксиом в КИВ (точнее, в одном из вполне обычных вариантов КИВ) бесконечно много. Но все бесконечное число аксиом сводится к небольшому числу "схем аксиом". На место каждой переменной в схеме может быть поставлена любая формула КИВ (в том числе и другая аксиома), но одинаковые формулы должны вставать на место одинаковых переменных.
Все схемы я разделил на группы. Каждая группа определяет свойства определенной логической операции. Первая и вторая группы должны быть в любом варианте КИВ или же должны быть вместо них другие похожие аксиомы, из которых выводятся эти. Остальные группы необязательны. Например, схемы 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)
В результате получается забавное исчисление... в нем обходятся некоторые трудности, зато нет некоторых интересных результатов. Это что-то типа неевклидовой геометрии: там тоже заменили одну аксиому и получили новые виды геометрий.
Выскажу сугубо личное мнение: в отличии от геометрии КИВ - не очень полезная логика ВНЕ математики. Как следствие, и интуиционистская логика - малополезна ВНЕ математики. Единственное практическое применение, которое мне видится - это тренировка студентов в умении выводить теоремы в сугубо абстрактных условиях.
no subject
no subject
А точнее надо Клини перечитывать :)