![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Просто об интуиционистской логике
Есть классическое исчисление высказываний (КИВ), а есть "легендарное" интуиционистское исчисление, 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
Эту же задачу пытались решить в стандарте IDEF 2 (стандарт математического моделирования), но на базе классической математики. Не вышло по той причине, что по мат. модели не всегда можно построить функциональную модель (из которой уже возможны автоматические построения программ).
no subject
там математики пишут или философы?
no subject