Интуиционистское исчисление высказываний

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Интуиционистское исчисление высказываний — формальная система, отражающие некоторые способы рассуждений, приемлемые с точки зрения интуиционизма. Предложена А. Гейтингом в 1930.

Основное отличие от привычного исчисления высказываний заключается в том, что отсутствует закон исключённого третьего.

Логические символы[править | править вики-текст]

\land (знак конъюнкции), \lor (знак дизъюнкции), \to (знак импликации) и \neg (знак отрицания).

Схемы аксиом[править | править вики-текст]

Далее через A, B и C обозначаются произвольные пропозициональные формулы.

  1. (A\to (B\to A))
  2. ((A\to B)\to ((B\to C)\to (A\to C)))
  3. (A\to (B\to (A\land B)))
  4. ((A\land B)\to A)
  5. ((A\land B)\to B)
  6. (A\to (A\lor B))
  7. (B\to (A\lor B))
  8. ((A\to C)\to ((B\to C)\to ((A\lor B)\to C)))
  9. ((A\to B)\to ((A\to (\neg B))\to (\neg A)))
  10. (A\to ((\neg A)\to B))

Правила вывода[править | править вики-текст]

Modus ponens: \frac{A,\;(A\to B)}{B}.