Правила исключения ∧ E 1 и ∧ E 2 выбирают либо левое, либо правое соединение; таким образом, доказательства представляют собой пару проекций — первую (fst) и вторую (snd).
| π доказательство ─────────── первое- F первое π доказательство | Γ ⊢ π : A ∧ B ───────────── ∧ E 1 Γ ⊢ первое число π : A | |
| π доказательство ─────────── snd - F snd π доказательство | Γ ⊢ π : A ∧ B ───────────── ∧ E 2 Γ ⊢ snd π : B |
Что касается импликации, форма введения локализует или связывает гипотезу, записанную с использованием λ ; это соответствует удаленной метке. В правиле " Γ , u : A " обозначает совокупность гипотез Γ вместе с дополнительной гипотезой u .
| π доказательство ──────────── λ - F λu . π доказательство | Γ , u : A ⊢ π : B ───────────────── ⊃ I Γ ⊢ λ u . π : A ⊃ B | |
| 1 доказательство 2 доказательства ─────────────────── приложение- F доказательство 1 2 | Γ ⊢ π 1 : A ⊃ B Γ ⊢ π 2 : A ──────────────────────────── ⊃ E Γ ⊢ π 1 2 : B |
Имея доказательства, доступные явно, можно манипулировать доказательствами и рассуждать о них. Ключевой операцией при доказательствах является замена одного доказательства предположением, используемым в другом доказательстве. Это широко известно как теорема о подстановке и может быть доказано с помощью индукции относительно глубины (или структуры) второго суждения.
Теорема о подстановке
Если Γ ⊢ π 1 : A и Γ , u : A ⊢ π 2 : B , то Γ ⊢ [ π 1 / u ] 2 : B .
До сих пор суждение " Γ ⊢ π : A " имело чисто логическую интерпретацию. В теории типов логическое представление заменяется более вычислительным представлением объектов. Предложения в логической интерпретации теперь рассматриваются как типы, а доказательства - как программы в лямбда-исчислении . Таким образом, интерпретация " π : A " такова: "программа π имеет тип A ". Логические связки также читаются по-разному: конъюнкция рассматривается как произведение (×), импликация - как стрелка функции (→) и т.д. Однако различия носят лишь косметический характер. Теория типов представлена методом естественной дедукции в терминах правил формирования, введения и исключения; фактически, читатель может легко реконструировать то, что известно как простая теория типов, из предыдущих разделов.
Разница между логикой и теорией типов заключается прежде всего в смещении фокуса с типов (предложений) на программы (доказательства). Теорию типов в основном интересует конвертируемость или редуцируемость программ. Для каждого типа существуют канонические программы этого типа, которые являются неприводимыми; они известны как канонические формы или значения. Если каждую программу можно привести к канонической форме, то теория типов называется нормализующей (или слабо нормализующей). Если каноническая форма уникальна, то говорят, что теория сильно нормализуется. Нормализуемость - редкая особенность большинства теорий нетривиальных типов, что является большим отклонением от логического мира. (Напомним, что почти каждый логический вывод имеет эквивалентный нормальный вывод.) Вкратце объясню причину: в теориях типов, допускающих рекурсивные определения, возможно писать программы, которые никогда не сводятся к значению; таким циклическим программам обычно можно присвоить любой тип. В частности, циклическая программа имеет тип ⊥ , хотя логического доказательства " ⊥ истинно" не существует. По этой причине предложения как типы; доказательства как программы парадигма работает только в одном направлении, если вообще работает: интерпретация теории типов как логики обычно дает противоречивую логику.