Русская Википедия:Интуиционистская логика

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

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

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

Схемы аксиом 1-10 и правило «модус поненс» задают интуиционистское исчисление высказываний. Все 12 схем аксиом и все 3 правила вывода задают интуиционистское исчисление предикатов. Интуиционистское исчисление предикатов отличается от классического тем, что в последнем вместо схемы аксиом 10 используется схема аксиом <math>(\neg \neg A) \to A</math>..

Логические символы

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

Схемы аксиом

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

1. <math>(A\to (B\to A))</math>
2. <math>((A\to B)\to ((B\to C)\to (A\to C)))</math>
3. <math>(A\to (B\to (A\land B)))</math>
4. <math>((A\land B)\to A)</math>
5. <math>((A\land B)\to B)</math>
6. <math>(A\to (A\lor B))</math>
7. <math>(B\to (A\lor B))</math>
8. <math>((A\to C)\to ((B\to C)\to ((A\lor B)\to C)))</math>
9. <math>((A\to B)\to ((A\to (\neg B))\to (\neg A)))</math>
10. <math>((\neg A)\to (A \to B))</math>
11. <math>\forall x A(x) \to A(y)</math>
12. <math>A(y) \to \exists x A(x)</math>

Правила вывода

1. Modus ponens: <math>\frac{A,\;(A\to B)}{B}</math>.
2. <math>\frac{C \to A(x)}{C \to \forall x A(x)}</math> если <math>x</math> не является свободной переменной в <math>C</math>.
3. <math>\frac{A(x) \to C}{\exists x A(x) \to C}</math>если <math>x</math> не является свободной переменной в <math>C</math>.

См. также

• Интуиционизм

Литература

• Гейтинг А. Интуиционизм. — М., 1965.
• Клини С. К. Введение в метаматематику. — М., 1957.
• Новиков П. С. Конструктивная математическая логика с точки зрения классической. — М., 1977.
• Драгалин А. Г. Математический интуиционизм. Введение в теорию доказательств. — М., 1979.
• Шаблон:НФЭ