Просто об интуиционистской логике
Dec. 6th, 2005 10:13 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
psilogicЕсть классическое исчисление высказываний (КИВ), а есть "легендарное" интуиционистское исчисление, 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)
В результате получается забавное исчисление... в нем обходятся некоторые трудности, зато нет некоторых интересных результатов. Это что-то типа неевклидовой геометрии: там тоже заменили одну аксиому и получили новые виды геометрий.
Выскажу сугубо личное мнение: в отличии от геометрии КИВ - не очень полезная логика ВНЕ математики. Как следствие, и интуиционистская логика - малополезна ВНЕ математики. Единственное практическое применение, которое мне видится - это тренировка студентов в умении выводить теоремы в сугубо абстрактных условиях.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2005-12-07 08:20 am (UTC)Эту же задачу пытались решить в стандарте IDEF 2 (стандарт математического моделирования), но на базе классической математики. Не вышло по той причине, что по мат. модели не всегда можно построить функциональную модель (из которой уже возможны автоматические построения программ).
no subject
Date: 2005-12-07 08:47 am (UTC)там математики пишут или философы?
no subject
Date: 2005-12-07 11:05 am (UTC)no subject
Date: 2005-12-07 10:11 am (UTC)А раскрыть?
no subject
Date: 2005-12-07 10:24 am (UTC)Точнее так: берем произвольную формулу булевой алгебры (произвольную - но с учетом выбранной системы аксиом КИВ, т.е. если нет группы аксиом для операции "<=>", то формулы с "<=>" ене считаются). Далее, если эта формула всегда (при всех значениях переменных) дает в булевой алгебре true, то она 100% может быть доказана в КИВ. Это, собственно, полнота. Если эта формула всегда дает в булевой алгебре false, то она 100% может быть опровергнута в КИВ (т.е. может быть доказано ее отрицание). Наконец, если эта формула может давать и true, и false, то ни доказать, ни опровергнуть ее в КИВ не получится.
no subject
Date: 2005-12-07 10:50 am (UTC)no subject
Date: 2005-12-07 11:14 am (UTC)А точнее надо Клини перечитывать :)
no subject
Date: 2005-12-07 11:09 am (UTC)no subject
Date: 2005-12-07 11:22 am (UTC)no subject
Date: 2005-12-09 09:50 am (UTC)no subject
Date: 2005-12-09 09:53 am (UTC)no subject
Date: 2005-12-07 11:32 am (UTC)[ в отличии от геометрии КИВ - не очень полезная логика ВНЕ математики. ]
[ Как следствие, и интуиционистская логика - малополезна ВНЕ математики. ]
Строго говоря, второе не следует из первого. Если одно исчисление оказалось малополезным, это не значит, что похожее, но более слабое исчисление тоже будет малополезным. В приведеном примере с IDEF именно это и произошло: ослабив логику, удалось добиться соответствия мат. модели и функциональной модели. Чтобы не быть голословным (стараюсь теперь на эти грабли не наступать :), показано это здесь:
http://www.logic.ru/Russian/LogStud/03/LS_3_r_Pupyshev.pdf
no subject
Date: 2005-12-07 11:57 am (UTC)Да, это как бы описание "неясного жопного чувства", не более того :)
no subject
Date: 2005-12-08 03:16 pm (UTC)Где-то правую скобку потеряли.
=======
Спасибо. Восполняю недостатки образования. =)
Для не-двузначных логик есть ли какие-нибудь тонкости в данном наборе аксиом?
no subject
Date: 2005-12-08 03:25 pm (UTC)насколько я понимаю, в КИВ и в интуиционистской логике вообще не используется понятие дву- или не дву- значности. Там для формул другое деление: не на истинные и ложные, а на аксиомы, теоремы и недоказанные. Иногда, правда, вводят мисволы true и false, но опят-таки, не как истинность, а просто как символы, с которыми надо играть по этим правилам. Т.е. например, нельзя взять и заменить в формуле ~true на false.
no subject
Date: 2005-12-08 03:44 pm (UTC)в свое время меня очень поразила алгебра сплетений.
no subject
Date: 2005-12-08 04:48 pm (UTC)no subject
Date: 2005-12-12 12:34 pm (UTC)http://www.mccme.ru/prasolov/