Примерно тем же, чем римская 60-ричная система счисления :) Громоздко очень и своей громоздкостью затрудняет освоение и провоцирует на ошибки.
[ Импликацию (если р, то q) можно утверждать, только если имеется такое построение, которое, будучи объединено с построением р, автоматически дает построение q ]
То есть, в статье приравняли импликацию к дедуктивному следованию. Это не совсем правильно, но, в принципе, лучше, чем с Раскольниковым :)
[ Услиенно ищу формальную запись аксиом интуиционистской логики ]
могу написать, если интересно :) там всего одна аксиома отличается от системы аксиом КИВ
КИВ: Схемы аксиом (т.е. на место каждой переменной в схеме может быть поставлена любая формула КИВ, но одинаковые формулы на место одинаковых переменных)
Свойства "=>" 1. A => (B => A) 2. (A => B) => ((A => (B => C)) => (A => C) Свойства "~" 3. ~~A => A 4. (A => B) => ((A => ~B) => ~A) - эти 4 аксиомы (или из эквиваленты) обязательны для КИВ. Остальные аксиомы опциональны. Если мы вводим какую-то операцию (например, "&") то должны и добавить соответствующую группу аксиом:
Для "&": (A & B) => A (A & B) => B A => (B => (A & B))
Для "v": A => (A v B) B => (A v B) (A => C) => ((B => C) => ((A v B) => C))
Для "<=>": (A <=> B) => (A => B) (A <=> B) => (A <= B) (A => B) => ((B => A) => (A <=> B))
Для "+" (XOR): (A + B) => (~A => B) (A + B) => (B => ~A) (A => ~B) => ((~B => A) => (A + B))
Плюс правило вывода modus ponens: A, A => B |- B
В интуиционизме делается одна замена. На место игрока номер 3: 3. ~~A => A Приходит другой игрок номер 3: 3. ~A => (A => B)
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2005-12-06 06:07 pm (UTC)Примерно тем же, чем римская 60-ричная система счисления :) Громоздко очень и своей громоздкостью затрудняет освоение и провоцирует на ошибки.
[ Импликацию (если р, то q) можно утверждать, только если имеется такое построение, которое, будучи объединено с построением р, автоматически дает построение q ]
То есть, в статье приравняли импликацию к дедуктивному следованию. Это не совсем правильно, но, в принципе, лучше, чем с Раскольниковым :)
[ Услиенно ищу формальную запись аксиом интуиционистской логики ]
могу написать, если интересно :) там всего одна аксиома отличается от системы аксиом КИВ
no subject
Date: 2005-12-06 06:35 pm (UTC)А еще интересно, что, похоже вы сегодня не первый раз меня ловите на заблуждениях, тока я пока в этом не признаюсь :)
no subject
Date: 2005-12-06 07:12 pm (UTC)Схемы аксиом (т.е. на место каждой переменной в схеме может быть поставлена любая формула КИВ, но одинаковые формулы на место одинаковых переменных)
Свойства "=>"
1. A => (B => A)
2. (A => B) => ((A => (B => C)) => (A => C)
Свойства "~"
3. ~~A => A
4. (A => B) => ((A => ~B) => ~A)
- эти 4 аксиомы (или из эквиваленты) обязательны для КИВ. Остальные аксиомы опциональны. Если мы вводим какую-то операцию (например, "&") то должны и добавить соответствующую группу аксиом:
Для "&":
(A & B) => A
(A & B) => B
A => (B => (A & B))
Для "v":
A => (A v B)
B => (A v B)
(A => C) => ((B => C) => ((A v B) => C))
Для "<=>":
(A <=> B) => (A => B)
(A <=> B) => (A <= B)
(A => B) => ((B => A) => (A <=> B))
Для "+" (XOR):
(A + B) => (~A => B)
(A + B) => (B => ~A)
(A => ~B) => ((~B => A) => (A + B))
Плюс правило вывода modus ponens:
A, A => B |- B
В интуиционизме делается одна замена. На место игрока номер 3:
3. ~~A => A
Приходит другой игрок номер 3:
3. ~A => (A => B)