Правила вывода:
2. Г├ ( Á & B) Þ Г├ Á (удаление &)
3. Г├ ( Á & B) Þ Г├ B (удаление &)
Правила вывода:
2. Г├ ( Á & B) Þ Г├ Á (удаление &)
3. Г├ ( Á & B) Þ Г├ B (удаление &)
4. Г├ B Þ Г├ (Á È B) (введение È )
5. Г├ Á Þ Г├ (Á È B) (введение È )
6. Г1 ├ (Á È B); Г2 , Á ├ Ã ;Г3 , B ├ Ã Þ Г 1 ,Г 2 , Г3 + Ã (удаление È )
7. Г , Á ├ B Þ Г ├ (Á É B) ( введение É )
8. Г1 ├ ( Á É B ); Г2 + Á Þ Г1 , Г2 ├ В (удаление É )
9. Г, Á ├ Þ Г├ ù Á (введение ù )
10. Г1 ├ Á ; Г2 ├ ┐Á Þ Г1 , Г2 ├ (сведение к противоречию)
11. Г, ┐Á ├ Þ Г ├ Á (удаление ù )
12. Г ├ Þ Г ├ Á ( утончение )
13. Г├ Á Þ Г, В ├ Á ( расширение)
14. Г1, Á , В, Г2+ Ã Þ Г1, В, Á , Г2+ Ã ( перестановка)
15. Г1, Á , Á , Г2+ Ã Þ Г1, Á , Г2+ Ã ( сокращение).
Аксиомой называется выражение, получающееся из схемы аксиом подстановкой вместо символа Á конкретной формулы.
Выводом в ИС называется конечная последовательность секвенций S 1,…, S п такая, что для каждого i ( 1 £ i £ n) S i есть либо аксиома, либо непосредственное следствие предыдущих секвенций по правилам 1—15.
Секвенция S называется выводимой в ИС , если существует вывод в ИС, оканчивающийся S . Правило 
называется допустимым в ИС, если из выводимости в ИС секвенций S 1,…, S п следует выводимость секвенции S .
Определим исчисление ИВ. Схемами аксиом исчисления ИВ являются следующие выражения:
Исчисление ИВ имеет следующее правило вывода ( modus ponens):
.
Аксиомой (или вариантом схемы аксиом) называется выражение, полученное из данной схемы аксиом подстановкой вместо символов Á , B , Ã конкретных формул. Формула В называется непосредственным следствием формул Á и (Á Ì B ).
Выводом в ИВ называется конечная последовательность формул Á 1,…, Á п такая, что для каждого i ( 1 £ i £ n) Á i есть либо аксиома, либо непосредственное следствие предыдущих формул.
Вывод на множестве формул Г есть последовательность Á 1,…, Á п такая, что для каждого i ( 1 £ i £ n) Ái есть либо аксиома, либо одна из формул Г, либо непосредственное следствие предыдущих формул.
Будем писать ├ Á ( Г├ Á ), если существует вывод (вывод из Г), оканчивающийся формулой Á . Формула Á в этом случае называется выводимой в ИВ (выводимой из Г).
Множество формул Г назовем противоречивым, если существует такая формула Á , что Г├ Á и Г├ ┐Á . В противном случае Г назовем непротиворечивым.
Интуиционистским исчислением высказываний ИИВ называется исчисление, схемами аксиом которого являются схемы аксиом 1—9 исчисления ИВ и формулы вида (┐Á É (Á É В)), правилом вывода – modus ponens. Определение выводимости в ИИВ аналогично соответствующему определению для ИВ. ├И Á(Г├И Á ) означает, что Á выводима в ИИВ (Á выводима в ИИВ из Г).
Логической матрицей называется система Â = á M; D, &, Ú , É , ù ñ , где М – непустое множество, D Í M, &, Ú , É -- двуместные, ù -- одноместная функция на М. Формула Á называется общезначимой в Â , если при любых значениях переменных в множестве М значение формулы Á входит в D.
Говорим, что формула Á зависит от системы формул D , если существует конечная последовательность формул В1,…, Вп, где Вп = Á и для любого i ( 1 £ i £ n) Вi есть непосредственное следствие предыдущих формул по modus ponens. В противном случае Á называется независимой от D . Система формул Dнезависимой, если каждая формула Á из D независима от D \{Á }. называется
Система схем аксиом называется независимой, если для каждой схемы аксиом существует ее вариант, независимый от множества вариантов остальных схем аксиом.