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

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

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

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

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

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

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

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

  1. (A\to (B\to A))
  1. ((A\to B)\to ((B\to C)\to (A\to C)))
  1. (A\to (B\to (A\land B)))
  1. ((A\land B)\to A)
  1. ((A\land B)\to B)
  1. (A\to (A\lor B))
  1. (B\to (A\lor B))
  1. ((A\to C)\to ((B\to C)\to ((A\lor B)\to C)))
  1. ((A\to B)\to ((A\to (\neg B))\to (\neg A)))
  1. (A\to ((\neg A)\to B))

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

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