Интуиционистична логика

2023 Автор: Noah Black | [email protected]. Последно модифициран: 2023-08-25 04:38

Навигация за влизане

• Съдържание за участие
• библиография
• Академични инструменти
• Friends PDF Preview
• Информация за автора и цитирането
• Върнете се в началото

Интуиционистична логика

За първи път публикуван сря 1 септември 1999; съществена ревизия вт. септември 4, 2018

Интуиционистичната логика обхваща общите принципи на логическото разсъждение, които са били абстрахирани от логиците от интуиционистичната математика, разработени от LEJ Brouwer в неговите [1907] и [1908]. Тъй като тези принципи важат и за руската рекурсивна математика и конструктивния анализ на Е. Бишоп и неговите последователи, интуиционистичната логика може да се счита за логическа основа на конструктивната математика. Въпреки че интуиционистичният анализ противоречи на класическия анализ, интуиционистичният аритметичен Heyting е подсистема на класическата аритметика на Peano. От това следва, че интуиционистичната логика на предложенията е подходяща подсистема на класическата логика на предложенията, а чистата интуиционистка предикатна логика е правилна подсистема от чиста класическа предикатна логика.

Философски, интуиционизмът се различава от логизма, като третира логиката като част от математиката, а не като основа на математиката; от финитизъмкато позволяват конструктивни разсъждения за неизчислими структури (например, монотонна лентова индукция върху дървото на потенциално безкрайни последователности от естествени числа); и от платонизма, като разглеждате математическите обекти като ментални конструкции без независимо идеално съществуване. Формалистичната програма на Хилберт, за да оправдае класическата математика, като я свежда до формална система, чиято последователност трябва да бъде установена чрез финистични (следователно конструктивни) средства, беше най-мощният съвременен съперник на развиващия се интуиционизъм на Броувър. В своето есе от 1912 г. Интуиционизмът и формализмът Браувър правилно предсказа, че всеки опит за доказване на последователността на пълната индукция на естествените числа ще доведе до порочен кръг.

Броуер отхвърли формализма сам по себе си, но призна потенциалната полезност на формулирането на общи логически принципи, изразяващи интуиционистично правилни конструкции, като modus ponens. Официалните системи за интуиционистична логика на предсказание и предикат и аритметика са изцяло разработени от Heyting [1930], Gentzen [1935] и Kleene [1952]. Гьодел [1933] доказа еквиконсистенцията на интуиционистичните и класическите теории. Бет [1956] и Крипке [1965] предоставиха семантика, по отношение на която интуиционистичната логика е правилна и пълна, въпреки че доказателствата за пълнота на интуиционистичната предикатна логика изискват някои класически разсъждения.

• 1. Отхвърляне на Tertium Non Datur

• 2. Интуиционистична предикатна логика от първи ред

  • 2.1 Официалните системи (mathbf {H – IPC}) и (mathbf {H – IQC})
  • 2.2 Алтернативни формализми и теорема за дедукция
• 3. Интуиционистка теория на числата (Хейтинг Аритметика) (mathbf {HA})

• 4. Основна теория за доказване

  • 4.1 Превеждане на класическо в интуиционистична логика
  • 4.2 Допустими правила на интуиционистичната логика и аритметика

• 5. Основна семантика

  • 5.1 Семантика на Крипке за интуиционистична логика
  • 5.2 Семантика на реализируемост за аритметика на Heyting

• 6. Допълнителни теми и допълнително четене

  • 6.1 Субинтуиционистична и междинна логика
  • 6.2 Разширени теми
  • 6.3 Препоръчително четене
• библиография
• Академични инструменти
• Други интернет ресурси
• Свързани записи

1. Отхвърляне на Tertium Non Datur

Интуиционистичната логика може да бъде кратко описана като класическа логика без аристотелевския закон на изключената средна:

) маркер {LEM} A / vee / neg A)

или класическия закон за премахване на двойното отрицание:

) маркер {DNE} neg / neg A / rightarrow A)

но със закона за противоречие:

[(A / rightarrow B) rightarrow ((A / rightarrow / neg B) rightarrow / neg A))

и ex falso sequitur quodlibet:

) neg A / rightarrow (A / rightarrow B).)

Brouwer [1908] отбелязва, че LEM е абстрахиран от крайни ситуации, след което се разширява без оправдание до твърденията за безкрайните колекции. Например, нека (x, y) варира над естествените числа (0, 1, 2, / ldots) и нека (B (y)) съкрати ((primepred (y) oldand) primepred (y + 2))), където (primepred (y)) изразява „(y) е просто число.“Тогава (forall y (B (y) vee / neg B (y))) се държи интуитивно и класически, защото за да определим дали дадено естествено число е първостепенно, трябва само да проверим дали това е или не има делител строго между себе си и 1.

Но ако (A (x)) съкращава (съществува y (y / gt x / old и B (y))), тогава, за да се твърди (forall x (A (x) vee / neg Интуиционистично (x))) ще ни е необходим ефективен (вж. Тезата на Църквата-Тюринг), за да определим дали има двойка близнаци, по-големи от произволно естествено число (x), и досега не е известен такъв метод. Очевиден полуефективен метод е да се изброят чифтовете на основните числа, като се използва прецизиране на ситото на Ератостен (генериране на естествените числа едно по едно и зачертаване на всяко число (y), което не успява да удовлетвори (B (y))) и ако има двойка близнаци, по-големи от (x), този метод в крайна сметка ще намери първия. Въпреки това, (forall x A (x)) изразява Конвенцията на Twin Primes, която все още не е доказана или опровергана,така че в настоящото състояние на нашите знания не можем да твърдим нито (forall x (A (x) vee / neg A (x))), нито (forall x A (x) vee / neg / forall x А (х)).

Човек може да възрази, че тези примери зависят от факта, че Конвенцията на Близнаците не е уредена. Редица оригинални „контрапримери“на Брауър зависеха от проблеми (като последната теорема на Фермат), които оттогава са били решени. Но за Brouwer общият LEM беше еквивалентен на априорното предположение, че всеки математически проблем има решение - предположение, което той отхвърли, очаквайки теоремата за непълнота на Gödel за четвърт век.

Отхвърлянето на LEM има далечни последици. От една страна,

• Интуиционистично, reductio ad absurdum доказва само отрицателни твърдения, тъй като (neg / neg A / rightarrow A) не е общо взето. (Ако беше така, LEM ще последва модус ponens от интуиционистично доказаното (neg / neg (A / vee / neg A)).)
• Интуиционистичната логика на предложенията няма ограничена интерпретация на таблицата с истината. Има безкрайно много различни аксиоматични системи между интуиционистичната и класическата логика.
• Не всяка формула на предложение има интуиционистично еквивалентна дизюнктивна или конюнктивна нормална форма, изградена от основни формули и техните отрицания, като се използват само (vee) и (oldand).
• Не всяка формула на предикатите има интуиционистично еквивалентна нормална форма на пренекс, с всички количествени характеристики отпред.
• Докато (forall x / neg / neg (A (x) vee / neg A (x))) е теорема за интуиционистичната предикатна логика, (neg / neg / forall x (A (x) vee / neg A (x))) не е; така (neg / forall x (A (x) vee / neg A (x))) е в съответствие с интуиционистичната логика на предиката.

От друга страна,

• Всяко интуиционистично доказателство за затворено изявление на формата (A / vee B) може ефективно да се трансформира в интуиционистично доказателство на (A) или интуиционистично доказателство на (B) и подобно на затворените екзистенциални изявления.
• Интуиционистичната логика на предложенията е ефективно решаваща, в смисъл, че един ограничен конструктивен процес се прилага еднакво към всяка формула на предложението или произвежда интуиционистично доказателство на формулата или показва, че такова доказателство не може да съществува.
• Отрицателният фрагмент от интуиционистичната логика (без (vee) или (съществува)) съдържа верен превод на класическата логика и подобно на интуиционистичната и класическата аритметика.
• Интуиционистичната аритметика може последователно да се разширява чрез аксиоми, които противоречат на класическата аритметика, което позволява официалното изучаване на рекурсивната математика.
• Противоречивият интуиционистичен анализ на Броувър, който противоречи на LEM, може да бъде формализиран и показан последователен спрямо класическа и интуиционистично правилна подтеория.

2. Интуиционистична предикатна логика от първи ред

Формализираната интуиционистка логика естествено се мотивира от неформалното обяснение на Брауър-Хейтинг-Колмогоров на интуиционистичната истина, очертано в записите за интуиционизма във философията на математиката и развитието на интуиционистичната логика. Конструктивната независимост на логическите операции (oldand, / vee, / rightarrow, / neg, / forall, / съществува) контрастира на класическата ситуация, където например, (A / vee B) е еквивалентна на (neg (neg A / oldand / neg B)), и (съществува xA (x)) е еквивалентно на (neg / forall x / neg A (x)). От гледна точка на BHK, изречение от формата (A / vee B) твърди, че или доказателство за (A), или доказателство за (B) е конструирано;докато (neg (neg A / oldand / neg B)) твърди, че е изграден алгоритъм, който ефективно ще преобразува всяка двойка конструкции, доказващи съответно (neg A) и (neg B), в доказателство за известно противоречие.

2.1 Официалните системи (mathbf {H – IPC}) и (mathbf {H – IQC})

Следва формализъм в стил Хилберт (mathbf {H – IQC}) от Kleene [1952] (вж. Troelstra и van Dalen [1988]) за интуиционистична логика на предикат от първи ред. Езикът (L) на (mathbf {H – IQC}) има предикативни букви (P, Q (.), / Ldots) на всички артерии и отделни променливи (x, y, z, / ldots) (със или без абонати (1, 2, / ldots)), както и символи (oldand, / vee, / rightarrow, / neg, / forall, / съществува) за логическите съединители и квантори и скоби (,). Атомните (или първичните) формули на (L) са изрази като (P, Q (x), R (x, y, x)), където (P, Q ({.}), R ({.} {.} {.})) са (0) - ари, (1) - ари и (3) - ари предикатни букви съответно; тоест резултатът от попълването на всяко празно писмо в предикатна буква от индивидуален символ на променлива е основна формула.(Добре оформените) формули на (L) се определят индуктивно, както следва.

• Всяка атомна формула е формула.
• Ако (A) и (B) са формули, значи са ((A / oldand B), (A / vee B), (A / rightarrow B)) и (neg A).
• Ако (A) е формула и (x) е променлива, тогава (forall xA) и (съществува xA) са формули.

Като цяло използваме (A, B, C) като метаизменни за добре оформени формули и (x, y, z) като метаизменни за отделни променливи. Предвиждайки приложения (например за интуиционистична аритметика), ние използваме (s, t) като метаизменни за термини; в случай на чиста предикатна логика, термините са просто индивидуални променливи. Появата на променлива (x) във формула (A) е обвързана, ако тя е в обхвата на количествения елемент (forall x) или (съществува x), в противен случай свободен. Интуиционистично като класически, ((A / leftrightarrow B)) съкращава (((A / rightarrow B) oldand (B / rightarrow A))) и скобите ще бъдат пропуснати, когато това не предизвиква объркване.

Има три правила за извод:

Modus Ponens

От (A) и (A / rightarrow B), заключете (B).

(forall) - Въведение

От (C / rightarrow A (x)), където (x) е променлива, която не се появява свободна в (C), заключи (C / rightarrow / forall x A (x)).

(съществува) - премахване

от (A (x) rightarrow C), където (x) е променлива, която не се появява свободна в (C), заключи (съществува x A (x) права прашка C).

Аксиомите са всички формули на следните форми, където в последните две схеми подформулата (A (t)) е резултат от заместване на възникване на термина (t) за всяко свободно възникване на (x) в (A (x)) и нито една променлива, свободна в (t), не се обвързва в (A (t)) в резултат на замяната.

) започнем {array} {l} A / rightarrow (B / rightarrow A) (A / rightarrow B) rightarrow ((A / rightarrow (B / rightarrow C)) rightarrow (A / rightarrow C)) / A / rightarrow (B / rightarrow (A / oldand B)) (A / oldand B) rightarrow A \(A / oldand B) rightarrow B \\ A / rightarrow (A / vee B) / B / rightarrow (A / vee B) (A / rightarrow C) rightarrow ((B / rightarrow C) rightarrow ((A / vee B) rightarrow C)) (A / rightarrow B) rightarrow ((A / rightarrow / neg B) rightarrow / neg A) / \ neg A / rightarrow (A / rightarrow B) / \ forall xA (x) rightarrow A (t) / A (t) rightarrow / съществува xA (x) end {array})

Доказателство е всяка крайна последователност от формули, всяка от които е аксиома или непосредствена последица, чрез правило на извод, на (една или две) предходни формули на последователността. Казано е всяко доказателство, което доказва последната му формула, която се нарича теорема или доказуема формула на интуиционистичната предикатна логика от първи ред. Производство на формула (E) от колекция (F) от предположения е всяка последователност от формули, всяка от които принадлежи на (F) или е аксиома или непосредствено следствие от правило на извода от предходни формули на последователността, така че (E) е последната формула на последователността. Ако такова производно съществува, ние казваме, че (E) може да се извлече от (F).

Интуиционистичната логика на предложенията (mathbf {H – IPC}) е подсистемата на (mathbf {H – IQC}), която води до ограничаване на езика до формули, изградени от буквите на предложението (P, Q, R, / ldots) като се използват предложенията за съединители (oldand, / vee, / rightarrow) и (neg), като се използват само предложените постулати. Следователно последните две правила за извод и последните две схеми на аксиома отсъстват от предложената подсистема.

Ако в дадения списък на схеми на аксиоми за интуиционистична предсказателна логика или предикатна логика от първи ред, законът, изразяващ ex falso sequitur quodlibet:

) neg A / rightarrow (A / rightarrow B))

се заменя с класическия закон за премахване на двойно отрицание DNE:

) neg / neg A / rightarrow A)

(или еквивалентно, ако интуиционистичният закон за въвеждане на отрицание:

[(A / rightarrow B) rightarrow ((A / rightarrow / neg B) rightarrow / neg A))

се заменя с LEM), формална система (mathbf {H – CPC}) за класическа логика на предложението или (mathbf {H – CQC}) за класически резултати от предикатна логика. Тъй като ex falso и законът за противоречие са класически теореми, интуиционистичната логика се съдържа в класическата логика. В известен смисъл класическата логика се съдържа и в интуиционистичната логика; вижте раздел 4.1 по-долу.

Важно е да се отбележи, че докато LEM и DNE са еквивалентни като схеми над (mathbf {H – IPC}), последицата

[(neg / neg A / rightarrow A) rightarrow (A / vee / neg A))

не е теорема схема на (mathbf {H – IPC}). За теории (mathbf {T}), базирани на интуиционистична логика, ако (E) е произволна формула на (L (mathbf {T})), тогава по дефиниция:

(E) е разрешимо в (mathbf {T}), ако и само ако (mathbf {T}) докаже (E / vee / neg E).

(E) е стабилен в (mathbf {T}), ако и само ако (mathbf {T}) докаже (neg / neg E / rightarrow E).

(E) е тестируем в (mathbf {T}), ако и само ако (mathbf {T}) докаже (neg E / vee / neg / neg E).

Решимостта предполага стабилност, но не и обратното. Съединението на стабилност и доказателство е еквивалентно на решимостта. Самият Брауър доказа, че „абсурдността на абсурда на абсурда е еквивалентна на абсурда“(Brouwer [1923C]), така че всяка формула на формата (neg A) е стабилна; но в формулите (mathbf {H – IPC}) и (mathbf {H – IQC}) и техните отрицания не могат да се определят, както е показано в раздел 5.1 по-долу.

2.2 Алтернативни формализми и теорема за дедукция

Системата в стил Хилберт (mathbf {H – IQC}) е полезна за метаматематически проучвания на интуиционистичната логика, но принудителното й линеаризиране на удръжките и предпочитанието му към аксиоми над правилата я правят неудобен инструмент за установяване на производна. Естествена дедукционна система (mathbf {N – IQC}) за интуиционистична предикатна логика е резултат от дедуктивната система (mathbf {D}), представена в раздел 3 от записа на класическата логика в тази енциклопедия, като се пропусне символът и правилата за идентичност и заменя класическото правило (DNE) на двойно елиминиране на отрицание с интуиционистичното правило за премахване на отрицанието, изразяващо ex falso:

(INE) Ако (F) означава (A) и (F) означава (neg A), тогава (F) означава (B)

Ключовете за доказване на това, че (mathbf {H – IQC}) е еквивалентно на (mathbf {N – IQC}) са modus ponens и обратното,:

Теорема за приспадане

Ако (B) се извлича от (A) и евентуално от други формули (F), като всички променливи, свободни в (A), остават постоянни в деривацията (тоест, без да се използва втората или трето правило на извода за която и да е променлива (x), възникваща свободно в (A), освен ако предположението (A) не възникне при извеждането преди въпросния извод), тогава (A / правна ставка B) се извлича от (F).

Този основен резултат, грубо изразяващ правилото ((rightarrow I)) на (mathbf {I}), може да бъде доказан за (mathbf {H – IQC}) чрез въвеждане на определението на деривация. Останалите правила на (mathbf {I}) важат за (mathbf {H – IQC}) по същество от modus ponens, което съответства на ((rightarrow E)) в (mathbf {N -IQC}); и всички аксиоми на (mathbf {H – IQC}) са доказуеми в (mathbf {N – IQC}).

За да илюстрираме полезността на теоремата за приспадане, помислете за (очевидно тривиалната) схема на теоремата ((A / правилна A)). Правилното доказателство в (mathbf {H – IPC}) заема пет реда:

• 1. (A / правда (A / правда A))
• 2. ((A / rightarrow (A / rightarrow A)) rightarrow ((A / rightarrow ((A / rightarrow A) rightarrow A)) rightarrow (A / rightarrow A)))
• 3. ((A / rightarrow ((A / rightarrow A) rightarrow A)) rightarrow (A / rightarrow A))
• 4. (A / rightarrow ((A / rightarrow A) rightarrow A))
• 5. (A / правда A)

където 1, 2 и 4 са аксиоми и 3, 5 идват от по-ранни редове от modus ponens. Въпреки това, (A) може да се извлече от (A) (като предположение) в една очевидна стъпка, така че теоремата за приспадане ни позволява да заключим, че съществува доказателство за (A / правилна стрелка A). (Всъщност официалното доказателство за току-що представеното (A / rightarrow A) е част от конструктивното доказателство на теоремата за приспадане!)

Важно е да се отбележи, че при дефиницията на производно от предположения в (mathbf {H – IQC}) формулите на предположения се третират така, сякаш всичките им свободни променливи са универсално количествено определени, така че (forall x A (x)) произлиза от хипотезата (A (x)). Обаче променливата (x) ще се променя (не се поддържа постоянна) в това производно, като се използва правилото на (forall) - въвеждане; и така теоремата за приспадане не може да бъде използвана, за да се заключи (невярно), че (A (x) rightarrow / forall x A (x)) (и следователно чрез (съществува) - премахване, (съществува x A (x) rightarrow / forall x A (x))) са доказуеми в (mathbf {H – IQC}). Като пример за правилното използване на теоремата за приспадане за логиката на предиката, помислете за въздействието (съществува x A (x) rightarrow / neg / forall x / neg A (x)). За да покажете, че това е доказано в (mathbf {H – IQC}),първо извличаме (neg / forall x / neg A (x)) от (A (x)) с всички свободни променливи, държани постоянни:

• 1. (forall x / neg A (x) rightarrow / neg A (x))
• 2. (A (x) rightarrow (forall x / neg A (x) rightarrow A (x)))
• 3. (A (x)) (предположение)
• 4. (forall x / neg A (x) rightarrow A (x))
• 5. ((forall x / neg A (x) rightarrow A (x)) rightarrow ((forall x / neg A (x) rightarrow / neg A (x)) rightarrow / neg / forall x / neg A (x)))
• 6. ((forall x / neg A (x) rightarrow / neg A (x)) rightarrow / neg / forall x / neg A (x))
• 7. (neg / forall x / neg A (x))

Тук 1, 2 и 5 са аксиоми; 4 идва от 2 и 3 от modus ponens; и 6 и 7 идват от по-ранни редове от modus ponens; така че не са променяни променливи. Теоремата за приспадане ни казва, че има доказателство (P) в (mathbf {H – IQC}) на (A (x) rightarrow / neg / forall) x (neg A (x)) и едно приложение на (съществува) - елиминирането превръща (P) в доказателство за (съществува x A (x) rightarrow / neg / forall x / neg A (x)). Обратното не е доказано в (mathbf {H – IQC}), както е показано в раздел 5.1 по-долу.

Други важни алтернативи на (mathbf {H – IQC}) и (mathbf {N – IQC}) са различните последователни изчисления за интуиционистичната логика на предсказанието и предиката. Първият такъв анализ е определен от Gentzen [1934–5], вж. Kleene [1952]. Последователни системи, които доказват абсолютно същите формули като (mathbf {H – IQC}) и (mathbf {N – IQC}), проследяват изрично всички предположения и заключения при всяка стъпка на доказателство, заменяйки modus ponens (което елиминира междинна формула) чрез правило за рязане (което може да се покаже като допустимо правило (вж. раздел 4.2) за подсистемата, останала, когато тя е пропусната).

Когато подробностите за формализма не са важни, оттук нататък следваме Троелстра и ван Дален [1988], като оставяме "(mathbf {IQC})" или "(mathbf {IPC})" формална система за интуиционистична предикатна или предложена логика съответно и по подобен начин „(mathbf {CQC})” и „(mathbf {CPC})” за класическа предикативна и предложна логика.

И двете (mathbf {IPC}), и (mathbf {IQC}) отговарят на интерполационните теореми, напр.: Ако (A) и (B) са формули за предложение, които имат поне едно писмо на предложението, и ако (A / rightarrow B) е доказуем в (mathbf {IPC}), тогава има формула (C), съдържаща само букви за предложения, които се срещат и в (A), и (B), така че и (A / rightarrow C), и (C / rightarrow B) са доказуеми. Тези теми са разгледани в Kleene [1952] и Troelstra и Schwichtenberg [2000].

Докато идентичността може разбира се да се добави към интуиционистичната логика, за приложения (например, за аритметика) символът за равенство обикновено се третира като разграничена предикатна константа, удовлетворяваща аксиомите за еквивалентна връзка (рефлексивност, симетрия и транзитивност) и допълнителни нелогични аксиоми (напр., примитивните рекурсивни дефиниции на събиране и умножение). Идентичността е решаваща, интуиционистично, както и класически, но интуиционисткото разширение на равенството не винаги е решаващо; вижте дискусията за аксиомите за непрекъснатост на Брууър в раздел 3 от записа на интуиционизма във философията на математиката.

3. Интуиционистка теория на числата (Хейтинг Аритметика) (mathbf {HA})

Интуиционистичната (Heyting) аритметика (mathbf {HA}) и класическата (Peano) аритметика (mathbf {PA}) споделят един и същи език от първи ред и същите нелогични аксиоми; само логиката е различна. В допълнение към логическите съединители, квантори и скоби и отделните променливи (x, y, z, / ldots) (използвани също като метаизменни), езикът (L (mathbf {HA})) на аритметиката има двоичен предикатен символ (=), индивидуална константа (0), константа на унарната функция (S) и безкрайно много или безкрайно много допълнителни константи за примитивни рекурсивни функции, включително добавяне и умножение; точният избор е въпрос на вкус и удобство. Термините са изградени от променливи и (0) с помощта на функционалните константи; по-специално,всяко естествено число (n) се изразява на езика чрез числото (mathbf {n}), получено чрез прилагане на (S) (n) пъти към (0) (например, (S (S (0))) е числото за (2)). Основните формули са във формата ((s = t)), където (s, t) са термини, а съставните формули се получават от тях, както обикновено.

Логичните аксиоми и правила на (mathbf {HA}) са тези от първокласна интуиционистка логика на предикатите (mathbf {IQC}). Нелогичните аксиоми включват рефлексивните, симетрични и преходни свойства на (=):) forall x (x = x),)) forall x / forall y (x = y / rightarrow y = x),)) forall x / forall y / forall z ((x = y / oldand y = z) rightarrow x = z);) аксиомата, характеризираща (0) като най-малкото естествено число:

) forall x / neg (S (x) = 0),)

аксиомата, характеризираща (S) като функция "едно към едно":

) forall x / forall y (S (x) = S (y) rightarrow x = y),)

аксиома на разширителното равенство за (S):

) forall x / forall y (x = y / rightarrow S (x) = S (y));)

примитивните рекурсивни определящи уравнения за всяка постоянна функция, по-специално за добавяне:) forall x (x + 0 = x),)) forall x / forall y (x + S (y) = S (x + y));) и умножение:) forall x (x / cdot 0 = 0),)) forall x / forall y (x / cdot S (y) = (x / cdot y) + x);) и (универсално затваряне на) схемата на математическата индукция за произволни формули (A (x)):

[(A (0) oldand / forall x (A (x) rightarrow A (S (x)))) rightarrow / forall x A (x).)

Аксиомите за разширяване на равенството за всички функционални константи са извлечени чрез математическа индукция от аксиомата за равенство за (S) и аксиомите на примитивната рекурсивна функция.

Отношението на естествения ред (x / lt y) може да бъде определено в (mathbf {HA}) чрез (съществува z (S (z) + x = y)), или от количественото число без формула (S (x) точка {-} y = 0), ако символът и примитивните рекурсивно определящи уравнения за предшественика: [Pd (0) = 0,)) forall x (Pd (S (x)) = x)) и изваждане на отрязване:) forall x (x / dot {-} 0 = 0),)) forall x (x / dot {-} S (y) = Pd (x / dot {-} y))) присъстват във формализма. (mathbf {HA}) доказва сравнителния закон

) forall x / forall y (x / lt y / vee x = y / vee y / lt x))

и интуиционистична форма на принципа с най-малко число за произволни формули (A (x)):

) forall x) forall y (y / lt x / rightarrow (A (y) vee / neg A (y))) rightarrow \(съществува y ((y / lt x / oldand A (y)) oldand / forall z (z / lt y / rightarrow / neg A (z))) vee \\ / forall y (y / lt x / rightarrow / neg A (y))].)

Хипотезата е необходима, тъй като не всички аритметични формули могат да се решат в (mathbf {HA}). Обаче, (forall x / forall y (x = y / vee / neg (x = y))) може да бъде доказано директно чрез математическа индукция и т.н.

Основните формули (и следователно всички формули без квантификатори) са разрешими и стабилни в (mathbf {HA}).

Ако (A (x)) е разрешимо в (mathbf {HA}), тогава чрез индукция на (x), така са (forall y (y / lt x / rightarrow A (y))) и (съществува y (y / lt x / oldи A (y))). следователно

Формулите, в които са ограничени всички количествени характеристики, са разрешими и стабилни в (mathbf {HA}).

Събирането (Delta_0) на аритметични формули, в които са ограничени всички квантори, е най-ниското ниво на класическа аритметична йерархия, основаващо се на модела на редуване на квантори във формула на предварителен приклад. В (mathbf {HA}) не всяка формула има пренекс форма, но Бър [2004] откри проста интуиционистична аритметична йерархия, съответстваща на ниво на класическата. Само за целите на следващите две дефиниции, (forall x) обозначава блок от крайно много универсални квантови числа и подобно (съществува x) означава блок от крайно много екзистенциални количествени числа. С тези конвенции класовете на Бър (Phi_n) и (Psi_n) се определят от:

• (Phi_0 = / Psi_0 = / Delta_0),
• (Phi_1) е класът на всички формули на формата (forall x A (x)), където (A (x)) е в (Psi_0). За (n / ge 2), (Phi_n) е класът на всички формули на формата (forall x [A (x) rightarrow / съществува y B (x, y)]) където (A (x)) е в (Phi_ {n-1}) и (B (x, y)) е в (Phi_ {n-2}),
• (Psi_1) е класът на всички формули на формата (съществува x A (x)), където (A (x)) е в (Phi_0). За (n / ge 2), (Psi_n) е класът на всички формули на формата (A / rightarrow B), където (A) е в (Phi_n) и (B) е в (Phi_ {n-1}).

Съответните класически класове за предварително определение са дефинирани по-просто:

• (Pi_0 = / Sigma_0 = / Delta_0),
• (Pi_ {n +1}) е класът на всички формули на формата (forall x A (x)), където (A (x)) е в (Sigma_n),
• (Sigma_ {n +1}) е класът на всички формули на формата (съществува x A (x)), където (A (x)) е в (Pi_n).

Арифметиката на пеано (mathbf {PA}) идва от Heyting arithmetic (mathbf {HA}) чрез добавяне на LEM или (neg / neg A / rightarrow A) към списъка на логическите аксиоми, т.е. използвайки класическата вместо интуиционистична логика. Следните резултати са валидни дори във фрагментите на (mathbf {HA}) и (mathbf {PA}), като схемата на индукция е ограничена до формули (Delta_0).

Теорема на Бър:

• Всяка аритметична формула е доказуемо еквивалентна в (mathbf {HA}) на формула в един от класовете (Phi_n).
• Всяка формула в (Phi_n) е доказуемо еквивалентна в (mathbf {PA}) на формула в (Pi_n) и обратно.
• Всяка формула в (Psi_n) е доказуемо еквивалентна в (mathbf {PA}) на формула в (Sigma_n) и обратно.

(mathbf {HA}) и (mathbf {PA}) са теоретично еквивалентни на доказателство, както ще бъде показано в раздел 4. Всеки може да изрази (по цифри) своя собствен доказателствен доказател. По известната теорема за непълнота на Гьодел, ако (mathbf {HA}) е последователна, нито (mathbf {HA}), нито (mathbf {PA}) не могат да докажат своята последователност.

4. Основна теория за доказване

4.1 Превеждане на класическо в интуиционистична логика

Основен факт за интуиционистичната логика е, че тя има същата сила на консистенция като класическата логика. За логиката на предложението това за първи път е доказано от Гливенко [1929].

Теорема на Гливенко Доволната

формула на предложение (A) е класически доказуема, ако и само ако (neg / neg A) е интуитивно настроена.

Теоремата на Гливенко не се разпростира до логиката на предиката, въпреки че произволна предикатна формула (A) е класически доказама, ако и само ако (neg / neg A) е доказуема в интуиционистичната предикатна логика плюс схемата на "двойно отхвърляне на отрицанието".

) маркер {DNS} forall x / neg / neg B (x) rightarrow / neg / neg / forall x B (x))

По-сложният отрицателен превод на класическите в интуиционистичните теории, дължащ се независимо на Гьодел и Гентцен, свързва с всяка формула (A) на езика (L) друга формула (g (A)) (с не (vee) или (съществува)), така че

• (I) Класическата логика на предикатите доказва (A / leftrightarrow g (A)).
• (II) Интуиционистичната предикатна логика доказва (g (A) leftrightarrow / neg / neg g (A)).
• (III) Ако класическата предикатна логика докаже (A), тогава интуиционистичната предикатна логика доказва (g (A)).

Доказателствата са направени от следното индуктивно определение на (g (A)) (използвайки директния превод на импликацията на Гентцен, а не на Gödel по отношение на ((neg) и (oldand)):

) начало {подравняване *} g (P) & / текст {е} neg / neg P, / текст {ако} P / текст {е първичен}. \\ g (A / old и B) & / текст { е} g (A) oldand g (B). \\ g (A / vee B) & / text {is} neg (neg g (A) oldand / neg g (B)). \\ g (A / rightarrow B) & / text {is} g (A) rightarrow g (B). \\ g (neg A) & / text {is} neg g (A). \\ g (forall xA (x)) & / text {is} forall xg (A (x)). \\ g (съществува xA (x)) & / text {is} neg / forall x / neg g (A (x)). / Край {подравняване *})

За всяка формула (A), (g (A)) е доказуемо интуиционистично, ако и само ако (A) е доказуемо класически. По-специално, ако (B / oldand / neg B) са класически доказуеми за някаква формула (B), тогава (g (B) oldand / neg g (B)) (което е (g (B / oldand / neg B))) от своя страна би била интуитивно настроена. следователно

(IV) Класическата и интуиционистичната предикатна логика са равностойни

Отрицателният превод на класическата в интуиционистичната теория на числата е още по-опростен, тъй като основните формули на интуиционистичната аритметика са стабилни. Така (g (s = t)) може да се приеме, че е (s = t), а останалите клаузи са непроменени. Отрицателният превод на всеки случай на математическа индукция е друг случай на математическа индукция, а другите нелогични аксиоми на аритметиката са собствени отрицателни преводи, така че

(I), (II), (III) и (IV) важат и за теорията на числата

Гьодел [1933e] интерпретира тези резултати като показа, че интуиционистичната логика и аритметика са по-богати от класическата логика и аритметика, тъй като интуиционистката теория отличава формули, които са класически еквивалентни и имат същата сила на консистенция като класическата теория. По-специално теоремите за непълнота на Гьодел се прилагат за (mathbf {HA}), както и за (mathbf {PA}).

Директните опити за разширяване на отрицателната интерпретация до анализа се провалят, защото отрицателният превод на изброената аксиома на избор не е теорема за интуиционистичен анализ. Въпреки това, той е в съответствие с интуиционистичния анализ, включително противоречивия принцип на Броувър, чрез функционалната версия на рекурсивната реализируемост на Kleene (вж. Раздел 6.2 по-долу). От това следва, че интуиционистичната математика, която може да бъде изразена само с помощта на всички стандартни логически съединители и количествени характеристики, е в съответствие с верния превод на класическата математика, като се избягват (vee) и (съществува).

Това е важно, защото интуиционистичният анализ на Броувър е в противоречие с LEM. Ако обаче (A) е някаква отрицателна формула (без (vee) или (съществува)), тогава (neg / neg A / rightarrow A) може да се докаже с помощта на интуиционистична логика. Съвпадение на интуиционистичния и класически анализ по тези линии, вдъхновено от идеята на Крипке за последователност на избор, е предложено в Moschovakis [2017].

4.2 Допустими правила на интуиционистичната логика и аритметика

Гьодел [1932] отбелязва, че интуиционистката логика на предложение има свойството на дизюнкция:

(DP) Ако (A / vee B) е теорема, тогава (A) е теорема или (B) е теорема

Gentzen [1935] установява свойството на дизюнкция за затворени формули на интуиционистичната предикатна логика. От това следва, че ако интуиционистката логика е последователна, тогава (P / vee / neg P) не е теорема, ако (P) е атомна формула. Kleene [1945, 1952] доказа, че интуиционистичната теория на числата от първи ред също има свързаното (вж. Фридман [1975]) свойство на съществуване:

(EP) Ако (съществува x A (x)) е затворена теорема, тогава за някакъв затворен термин (t), (A (t)) е теорема

Свойствата на дизъюнкцията и съществуването са специални случаи на общо явление, характерно за некласическите теории. Допустимите правила на една теория са правилата, при които теорията е затворена. Например Харроп [1960] наблюдава, че правилото

Ако (neg A / rightarrow (B / vee C)) е теорема, така е ((neg A / rightarrow B) vee (neg A / rightarrow C))

е допустим за интуиционистичната логика на предложения (mathbf {IPC}), защото ако (A), (B) и (C) са някакви формули, такива, че (neg A / rightarrow (B / vee C)) е доказуемо в (mathbf {IPC}), тогава също ((neg A / rightarrow B) vee (neg A / rightarrow C)) е доказуемо в (mathbf {IPC }). Правилото на Harrop не може да се извлече в (mathbf {IPC}), защото ((neg A / rightarrow (B / vee C)) rightarrow (neg A / rightarrow B) vee (neg A / rightarrow C)) не е доказано интуитивно. Друг важен пример за допустимо немислимо правило на (mathbf {IPC}) е правилото на Мінц:

Ако ((A / rightarrow B) rightarrow (A / vee C)) е теорема, така е (((A / rightarrow B) rightarrow A) vee ((A / rightarrow B) rightarrow C))).

Двузначната интерпретация на таблицата за истинност на класическата логика на предложенията (mathbf {CPC}) поражда просто доказателство, че всяко допустимо правило на (mathbf {CPC}) може да се получи: в противен случай някакво присвояване на (A), (B) и т.н. би направила хипотезата вярна, а заключението невярно и като замести напр. (P / rightarrow P) за буквите, присвоени "true" и (P / oldand / neg P) за тези, които са назначени „неверни“, би имала доказаема хипотеза и недоказано заключение. Фактът, че интуиционистичната ситуация е по-интересна, води до много естествени въпроси, на някои от които наскоро са дадени отговори.

Като обобщи правилото на Mints, Visser и de Jongh идентифицират рекурсивно изброяваща последователност от последователно по-силни допустими правила („правила на Visser”), които, те предположиха, създават основа за допустимите правила на (mathbf {IPC}) в смисъл че всяко допустимо правило може да се извлече от свойството на разединението и едно от правилата на последователността. Въз основа на работата на Ghilardi [1999], Iemhoff [2001] успя да докаже своите предположения. Рибаков [1997] доказа, че събирането на всички допустими правила на (mathbf {IPC}) е решимо, но няма ограничена основа. Visser [2002] показа, че неговите правила са също така допустимите предложения за правила на (mathbf {HA}) и на (mathbf {HA}), разширени от принципа на MP на Марков (дефиниран в раздел 5.2 по-долу). Съвсем наскоро,Jerabek [2008] намери независима основа за допустимите правила на (mathbf {IPC}), със свойството, което никое правило в основата не произвежда друго.

Много по-малко се знае за допустимите правила на интуиционистичната предикатна логика. Pure (mathbf {IQC}), без отделни константи или предикати, има следното забележително допустимо правило за (A (x)) без променливи, но (x):

Ако (съществува x A (x)) е теорема, така е (forall x A (x)).

Не всяко допустимо правило за предикат на (mathbf {IQC}) е допустимо за всички формални системи, базирани на (mathbf {IQC}); например, (mathbf {HA}) очевидно нарушава току-що посоченото правило. През 1999 г. Visser доказа, че свойството да бъде допустимо предикатно правило на (mathbf {HA}) е (Pi_2) пълно, а през 2002 г., че (mathbf {HA}) (+) MP има същите допустими правила за предикат като (mathbf {HA}). Плиско [1992] доказа, че предикативната логика на (mathbf {HA}) (+) MP (множеството изречения на езика на (mathbf {IQC}), всички чиито единици в случай на заместване в езикът на аритметиката е доказаем в (mathbf {HA}) (+) MP) е (Pi_2) пълен; Visser [2006] разшири този резултат до някои конструктивно интересни последователни разширения на (mathbf {HA}), които не се съдържат в (mathbf {PA}).

Въпреки че те не са напълно класифицирани, известните допустими правила на интуиционистичната предикатна логика са известни с това, че включват Правилото на Марков за решаващи предикати:

Ако (forall x (A (x) vee / neg A (x)) oldand / neg / forall x / neg A (x)) е теорема, така е (съществува x A (x)).

и следното правило за независимост на помещението (където се приема, че (y) не се появява свободно в (A (x))):

Ако (forall x (A (x) vee / neg A (x)) oldand (forall x A (x) rightarrow / съществува y B (y))) е теорема, така е (съществува y (forall x A (x) rightarrow B (y))).

И двете правила са допустими и за (mathbf {HA}). Съответните импликации (съответно MP и IP), които не се доказват интуитивно, се проверяват от интерпретацията на Гьодел „Dialectica“на (mathbf {HA}) (вж. Раздел 6.3 по-долу). И така, импликацията (CT) съответства на едно от най-интересните допустими правила на аритметиката на Хейтинг, нека го наречем правилото на Църквата-Клайн:

Ако (forall x / съществува y A (x, y)) е затворена теорема от (mathbf {HA}), тогава има число (n) такова, че, доказващо се в (mathbf {HA}), частичната рекурсивна функция с номер на Гьодел (n) е тотална и преброява всяко (x) в a (y), удовлетворяващо (A (x, y)) (и освен това (A (mathbf {x}, / mathbf {y})) е доказуемо, където (mathbf {x}) е числото за естественото число (x) и (mathbf {y}) е числото за (y)).

Комбинирането на правилото на Марков с отрицателния превод дава резултат, че класическата и интуиционистичната аритметика доказват същите формули на формата (forall x / съществува y A (x, y)), където (A (x, y)) е квантор-безплатно. Като цяло, ако (A (x, y)) е доказуемо решим в (mathbf {HA}) и ако (forall x / съществува y A (x, y)) е затворена теорема на класическа аритметика (mathbf {PA}), заключението на правилото на Църквата-Клайн важи дори в интуиционистичната аритметика. Защото, ако (mathbf {HA}) докаже (forall x / forall y (A (x, y) vee / neg A (x, y))), тогава от правилото на Church-Kleene характерната функция от (A (x, y)) има номер на Гьодел (m), доказуемо в (mathbf {HA}); така (mathbf {HA}) доказва (forall x / съществува y A (x, y) leftrightarrow / forall x / съществува y / съществува z B (mathbf {m}, x, y, z)) където (B) е без количествен показател,и съседните екзистенциални количествени характеристики могат да бъдат договорени в (mathbf {HA}). От това следва, че (mathbf {HA}) и (mathbf {PA}) имат едни и същи доказано рекурсивни функции.

Ето доказателство, че правилото "Ако (forall x (A / vee B (x))) е теорема, така е и (A / vee / forall x B (x))" (където (x) не е свободен в (A)) не е допустим за (mathbf {HA}), ако (mathbf {HA}) е последователен. Номерирането на Гьодел предоставя формула без количествен номер (G (x)), която (числово) изразява предиката „(x) е кодът на доказателство в (mathbf {HA}) на ((0 = 1)). “Чрез интуиционистичната логика с разрешимостта на аритметичните формули без квантификатори (mathbf {HA}) доказва (forall x (съществува y G (y) vee / neg G (x))). Ако обаче (mathbf {HA}) се докаже (съществува yG (y) vee / forall x / neg G (x)), тогава от свойството на разединяване, (mathbf {HA}) трябва докажете или (съществува yG (y)), или (forall x / neg G (x)). Първият случай е невъзможен,от свойството съществуване с предположението за съгласуваност и факта, че (mathbf {HA}) доказва всички истински изречения без количествени изречения. Но вторият случай е невъзможен и от втората теорема за непълнота на Гьодел, тъй като (forall x / neg G (x)) изразява последователността на (mathbf {HA}).

5. Основна семантика

Интуиционистичните системи са вдъхновили различни интерпретации, включително таблицата на Бет, топологичните модели на Расиова и Сикорски, алгебри на Хейтинг, формули като типове, рекурсивните реализации на Клейн, наклоните на Клейн и Аксел и моделите, базирани на снопове и топои. От всички тези интерпретации на възможната световна семантика [1965] на Крипке, по отношение на която интуиционистичната предикатна логика е пълна и последователна, най-много прилича на теорията на класическия модел. Рекурсивните интерпретации за реализация, от друга страна, се опитват ефективно да приложат обяснението на BHK на интуиционистичната истина.

5.1 Семантика на Крипке за интуиционистична логика

Структура на Kripke (mathbf {K}) за (L) се състои от частично подреден набор (K) от възли и функция на домейн D, приписваща се на всеки възел (k) в (K) обитаем набор (D (k)), така че ако (k / le k '), тогава (D (k) subseteq D (k')). Освен това (mathbf {K}) има принудително отношение, определено както следва.

За всеки възел (k) нека (L (k)) е езикът, простиращ се (L) с нови константи за всички елементи на (D (k)). Към всеки възел (k) и всеки (0) - арикатна предикативна буква (всяка буква на предложение) (P), или присвойте (f (P, k) =) вярно, или оставете (f (P, k)) неопределена, съответстваща на изискването, че ако (k / le k ') и (f (P, k) =) е вярно, тогава (f (P, k') =) true също. Кажи това

(k) (vDash) (P), ако и само ако (f (P, k) =) е вярно.

Към всеки възел (k) и всеки ((n + 1)) - сурова буква предикат (Q (ldots)), задайте (евентуално празен) набор (T (Q, k)) на ((n + 1)) - сборници от елементи на (D (k)) по такъв начин, че ако (k / le k '), тогава (T (Q, k) subseteq T (Q, k ')). Кажи това

(k) (vDash) (Q (d_0, / ldots, d_n)), ако и само ако ((d_0, / ldots, d_n) в T (Q, k)).

Сега дефинирайте (k) (vDash) (E) (което може да се чете "(k) сили (E)") за сложни изречения (E) на (L (k)) индуктивно, както следва:

(k) (vDash) ((A / old и B))	ако (k) (vDash) (A) и (k) (vDash) (B).
(k) (vDash) ((A / vee B))	ако (k) (vDash) (A) или (k) (vDash) (B).
(k) (vDash) ((A / правда B))	ако за всеки (k '\ ge k), ако (k') (vDash) (A), тогава (k ') (vDash) (B),
(k) (vDash) (neg A)	ако за не (k '\ ge k) прави (k') (vDash) (A).
(k) (vDash) (forall x A (x))	ако за всеки (k '\ ge k) и всеки (d / в D (k')), (k ') (vDash) (A (d)).
(k) (vDash) (съществува x A (x))	ако за някои (d / в D (k)), (k) (vDash) (A (d)).

Всяка такава принудителна връзка е последователна:

За никакво изречение (A) и не (k) случаят ли е, че и (k) (vDash) (A), и (k) (vDash) (neg A).

и монотонен:

Ако (k / le k ') и (k) (vDash) (A), тогава (k') (vDash) (A).

Теоремите за звучност и пълнота на Крипке установяват, че изречение от (L) е доказано в интуиционистичната логика на предиката, ако и само ако е принудено от всеки възел от всяка структура на Крипке. По този начин, за да покажем, че (neg / forall x / neg P (x) rightarrow / съществува x P (x)) е интуиционистично недоказано, достатъчно е да се разгледа структура на Kripke с (K = {k, k '},) (k / lt k',) (D (k) = D (k ') = {0 }), (T (P, k)) празно, но (T (P, k ') = {0 }). А за да се покаже обратното, е интуиционистично доказано (без всъщност да се доказва доказателство), човек се нуждае само от свойствата на последователност и монотонност на произволни модели на Крипке, с определението на (vDash).

Крипке моделите за езици с равенство могат да интерпретират (=) на всеки възел от произволно съотношение на еквивалентност, при условие на монотонност. За приложения към интуиционистичната аритметика са достатъчни нормални модели (тези, при които равенството се интерпретира чрез идентичност на всеки възел), тъй като равенството на естествените числа е решаващо.

Пропозиционната семантика на Крипке е особено проста, тъй като произволна предложна формула е интуитивно настроена, ако и само ако е принудена от корена на всеки модел на Крипке, чийто кадър (множеството (K) от възли заедно с тяхното частично подреждане) е ограничен дърво с най-малко елемент (коренът). Например, моделът на Крипке с (K = {k, k ', k' '}, k / lt k') и (k / lt k ''), и с (P) вярно само в (k '), показва, че и (P / vee / neg P), и (neg P / vee / neg / neg P) са недоказуеми в (mathbf {IPC}), Всеки терминален възел или лист на модел на Крипке е класически модел, защото лист форсира всяка формула или нейното отрицание. Само тези букви с предложение, които се срещат във формула (E), и само тези възли (k '), такива, че (k / le k'), са релевантни за решаването дали силите (k) (Е). Такива съображения ни позволяват да се свържем ефективно с всяка формула (E) на (L (mathbf {IPC})) краен клас от крайни крипке структури, които ще включват контрамодел на (E), ако такъв съществува. Тъй като класът на всички теореми на (mathbf {IPC}) е рекурсивно изброяващ, заключаваме, че

(mathbf {IPC}) е ефективно решение. Има рекурсивна процедура, която определя за всяка формула на предложение (E) дали или не (E) е теорема на (mathbf {IPC}), завършваща или с доказателство за (E) или (краен) контрамодел на Крипке.

Решимостта на (mathbf {IPC}) е получена за първи път от Гентцен през 1935 г. Неопределяемостта на (mathbf {IQC}) следва от неопределяемостта на (mathbf {CQC}) от отрицателната интерпретация, Познатите неинтуиционистични логически схеми съответстват например на структурните свойства на крипке моделите

• DNS притежава във всеки модел Kripke с ограничена рамка.
• ((A / rightarrow B) vee (B / rightarrow A)) има във всеки модел на Kripke с линейна подредена рамка. Обратно, всяка формула на предложение, която не може да бъде извлечена в (mathbf {IPC} + (A / rightarrow B) vee (B / rightarrow A)), има контрамодел на Kripke с линейно подредена рамка (вж. Раздел 6.1 по-долу).
• Ако (x) не е свободен в (A), тогава (forall x (A / vee B (x)) rightarrow (A / vee / forall x B (x))) има във всяка Kripke модел (mathbf {K}) с постоянен домейн (така че (D (k) = D (k ')) за всички (k, k') в (K)). Същото важи и за депутата.

Моделите на Крипке и моделите на Бет (които се различават в детайли от моделите на Крипке, но са интуиционистично еквивалентни) са мощен инструмент за установяване на свойствата на интуиционистичните формални системи; cf. Troelstra и van Dalen [1988], Smorynski [1973], de Jongh и Smorynski [1976], Ghilardi [1999] и Iemhoff [2001], [2005]. Въпреки това, няма чисто интуиционистично доказателство, че всяко изречение, което е валидно във всички модели на Крипке и Бет, е доказано в (mathbf {IQC}). След наблюдение на Гьодел, Kreisel [1958] потвърди, че пълнотата на интуиционистичната предикатна логика за семантиката на Бет е еквивалентна на принципа на MP на Марков, който Brouwer отхвърля.

Нещо повече, Дайсън и Крейсел [1961] показаха, че ако (mathbf {IQC}) е слабо завършен за семантиката на Бет (тоест, ако не съществува непротиворечиво изречение във всеки модел на Бет), то следва следствието от MP: [tag {GDK} forall / alpha_ {B (alpha)} neg / neg / съществува x R (alpha, x) rightarrow / neg / neg / forall / alpha_ {B (alpha)} съществува x R (alpha, x),), където (x) варира над всички естествени числа, (alpha) варира над всички безкрайни последователности от естествени числа, (B (alpha)) съкращения (forall x (alpha (x) leq 1)), а (R) изразява примитивно рекурсивно отношение на (alpha) и (x). Обратно, GDK води до слабата пълнота на (mathbf {IQC}). Този интересен принцип, който би оправдал негативното тълкуване на форма на теорията на вентилатора на Броувър,е по-слаб от MP, но недоказан в съвременните системи на интуиционистичен анализ. Kreisel [1962] предположи, че GDK евентуално може да бъде доказано въз основа на все още неоткритите свойства на интуиционистичната математика.

Променяйки дефиницията на модел на Крипке, за да позволи "експлодиращи възли", които налагат всяко изречение, Вълдман [1976] намери доказателство за пълнота, използвайки само интуиционистична логика, но постави под въпрос дали моделите на Крипке с взривяващи се възли са интуиционистично значими математически обекти.

5.2 Семантика на реализируемост за аритметика на Heyting

Един от начините за прилагане на обяснението на BHK на интуиционистичната истина за аритметиката е да се свърже с всяко изречение (E) на (mathbf {HA}) някаква колекция от цифрови кодове за алгоритми, които биха могли да установят конструктивната истина на (E). След Kleene [1945], число (e) реализира изречение (E) на аритметичния език чрез индукция върху логическата форма на (E):

(e) реализира (r = t)	ако (r = t) е вярно.
(e) реализира (A / oldand B)	ако (e) кодира двойка ((f, g)), така че (f) реализира (A) и (g) реализира (B).
(e) реализира (A / vee B)	ако (e) кодира двойка ((f, g)), така че ако (f = 0) тогава (g) реализира (A), и ако (f / gt 0) тогава (g) реализира (B).
(e) осъзнава (A / правда B)	ако всеки път, когато (f) реализира (A), тогава (e)-тата частична рекурсивна функция се дефинира при (f) и нейната стойност реализира (B).
(e) реализира (neg A)	ако не (f) реализира (A).
(e) реализира (forall x A (x))	ако за всеки (n), частичната рекурсивна функция е дефинирана при (n) и нейната стойност реализира (A (mathbf {n})).
(e) реализира (съществува x A (x))	ако (e) кодира двойка ((n, g)) и (g) реализира (A (mathbf {n})).

Произволна формула е реализируема, ако някакво число реализира универсалното си затваряне. Обърнете внимание, че не и двете (A), и (neg A) са реализируеми за всяка формула (A). Основният резултат е

Теорема на Нелсън [1947]

Ако (A) се извлича в (mathbf {HA}) от реализуеми формули (F), тогава (A) е реализируем.

Някои неинтуиционистични принципи могат да се окажат реализируеми. Например Принципът на Марков (за формули, които се решават) може да се изрази чрез схемата

(MP) (forall x (A (x) vee / neg A (x)) oldand / neg / forall x / neg A (x) rightarrow / съществува x A (x))

Макар и недоказуем в (mathbf {HA}), MP е реализируем чрез аргумент, който използва принципа на Марков неофициално. Но осъществимостта е фундаментално некласическо тълкуване. В (mathbf {HA}) е възможно да се изрази аксиома на рекурсивен избор CT (за „Теза на Църквата“), която противоречи на LEM, но е (конструктивно) осъществима. Следователно от теоремата на Нелсън, (mathbf {HA}) (+) MP (+) CT е последователна.

Kleene използва вариант на реализируемост на числата, за да докаже, че (mathbf {HA}) удовлетворява правилото на Църква-Клейн; същият аргумент работи за (mathbf {HA}) с MP или CT и за (mathbf {HA}) (+) MP (+) CT. В Kleene and Vesley [1965] и Kleene [1969] функциите заменят числата като реализиращи обекти, установявайки съгласуваността на формализирания интуиционистичен анализ и неговото затваряне във версия от втория ред на правилото Church-Kleene.

Теоремата на Нелсън установява недоказуемостта в (mathbf {IQC}) на някои теореми на класическата предикатна логика. Ако към всяка (n) - поставете предикатната буква (P (ldots)), формула (f (P)) на (L (mathbf {HA})) с (n) се задават свободни променливи и ако формулата (f (A)) на (L (mathbf {HA})) идва от формулата (A) на (L) чрез замяна на всяка основна формула (P (x_1, / ldots, x_n)) от (f (P) (x_1, / ldots, x_n)), тогава (f (A)) се нарича аритметична инстанция на заместване на (А). Например, ако формула от (L (mathbf {HA})), изразяваща (x), кодира доказателство в (mathbf {HA}) на формулата с код (y)”Е присвоено на (P (x, y)), получената арифметична заместваща инстанция на (forall y (съществува x P (x, y) vee / neg / съществува x P (x, y))) е нереализируем и следователно недоказан в (mathbf {HA}), и това е двойното му отрицание. От това следва, че (neg / neg / forall y (съществува x P (x, y) vee / neg / съществува x P (x, y))) не е доказано в (mathbf {IQC}).

Де Йонг [1970] комбинира реализируемостта с моделирането на Крипке, за да покаже, че интуиционистичната логика на предложенията (mathbf {IPC}) и фрагмент от (mathbf {IQC}) са аритметично пълни за (mathbf {HA}). Достатъчно е да се докаже еднакво разпределение на прости екзистенциални формули за предсказване на букви

Теорема на Де Йонг (за IPC) [1970]

Ако формула на предложение (A) на езика (L) не е доказуема в (mathbf {IPC}), тогава някой аритметичен екземпляр на заместване на (A) не е доказаем в (mathbf {HA}).

Доказателството за тази версия на теоремата на де Йонг не се нуждае от осъзнаваемост; cf. Сморински [1973]. Като пример, формата на Розер от теоремата за непълнота на Гьодел предоставя изречение (C) на (L (mathbf {HA})), така че (mathbf {PA}) не доказва нито (C), нито (neg C), така че със свойството на разединяване (mathbf {HA}) не може да се докаже ((C / vee / neg C)). Но семантичното доказателство на де Йонг също установи, че всяка интуиционистично недоказуема формула на предикат от ограничен вид има аритметична инстанция за заместване, която е недоказуема в (mathbf {HA}). Използвайки синтактичен метод, Даниел Лийвант [1979] разширява теоремата на де Йонг до всички интуиционистично недоказуеми предикатични формули, доказвайки, че (mathbf {IQC}) е аритметично пълен за (bf {HA}). Вижте van Oosten [1991] за историческо изложение и по-просто доказателство за пълната теорема, използвайки абстрактна осъществимост с моделите на Бет вместо моделите на Крипке.

Без да твърди, че реализируемостта на числата съвпада с интуиционистичната аритметична истина, Нелсън забеляза, че за всяка формула (A) на (L (mathbf {HA})) предикатът "(y) реализира (A)”Може да бъде изразено в (mathbf {HA}) с друга формула (съкратено„ (y / realizerel A)”), а схемата (A / leftrightarrow / съществува y (y / realizerel A)) е в съответствие с (mathbf {HA}). Troelstra [1973] показа, че (mathbf {HA}) (+) ((A / leftrightarrow / съществува y (y / realizerel A))) е еквивалентно на (mathbf {HA}) (+) ECT, където ECT е засилена форма на КТ. В (mathbf {HA}) (+) MP (+) ECT, който Troelstra счита за формализация на руската рекурсивна математика (вж. Раздел 3.2 от записа на конструктивната математика), всяка формула на формата ((y / реализира A)) има еквивалентна „класическа“предварителна форма (A “(y)), състояща се от безформална количествена подформула, предшествана от редуващи се „класически“количествени характеристики на формите (neg / neg / съществува x) и (forall z / neg / neg), и така (съществува y A '(y)) е вид пренекс форма на (A).

6. Допълнителни теми и допълнително четене

6.1 Субинтуиционистична и междинна логика

Понастоящем има няколко други записа в тази енциклопедия, лекуващи интуиционистичната логика в различни контексти, но като цяло липсва общо третиране на по-слаби и по-силни логически предложения и предикативни логики. Много такива логики са идентифицирани и проучени. Ето няколко примера.

Субинтуиционистичната логика на предложенията може да бъде получена от (mathbf {IPC}) чрез ограничаване на езика или отслабване на логиката или и двете. Краен пример за първото е (mathbf {RN}), интуиционистка логика с една единствена променлива променлива (P), която е кръстена на своите откриватели Ригер и Нишимура [1960]. (mathbf {RN}) се характеризира с решетката на Rieger-Nishimura на безкрайно много нееквивалентни формули (F_n), така че всяка формула, чиято единствена предложна променлива е (P), е еквивалентна по интуиционистична логика на някои (F_n). Версията на Нишимура е

) начало {подравняване *} F _ { infty} & = P / rightarrow P. \\ F_0 & = P / oldand / neg P. \\ F_1 & = P. \\ F_2 & = / neg P. \\ F_ {2 n + 3} & = F_ {2 n + 1} vee F_ {2n + 2}. \\ F_ {2 n + 4} & = F_ {2 n + 3} rightarrow F_ {2 n + 1}. / Край {подравняване *})

В (mathbf {RN}) нито (F_ {2 n + 1}), нито (F_ {2 n + 2}) предполага другото; но (F_ {2 n}) означава (F_ {2 n + 1}), а (F_ {2 n + 1}) означава всяко от (F_ {2 n + 3}) и (F_ {2 n + 4}).

Фрагменти от (mathbf {IPC}) липсващи един или повече логически съединители ограничават езика и случайно логиката, тъй като интуиционистичните съединители (oldand), (vee), (rightarrow), (neg) са логически независими над (mathbf {IPC}). Роуз [1953] доказа, че безмисленият фрагмент (без (rightarrow)) е пълен по отношение на реализируемостта, в смисъл, че ако всеки аритметичен заместващ екземпляр на формула на предложение (E) без (rightarrow) е (число) -реализуемо тогава (E) е теорема на (mathbf {IPC}). Този резултат контрастира с

Теоремата на Роуз [1953]

(mathbf {IPC}) е непълна по отношение на реализируемостта.

Нека (F) е формулата на предложения [((neg / neg D / rightarrow D) rightarrow (neg / neg D / vee / neg D)) rightarrow (neg / neg D / vee / neg D)) където (D) е ((neg P / vee / neg Q)) и (P), (Q) са първи. Всеки екземпляр на аритметично заместване на (F) е реализируем (използвайки класическата логика), но (F) не е доказуем в (mathbf {IPC}).

От това следва, че (mathbf {IPC}) е аритметично непълна за (mathbf {HA}) (+) ECT (вж. Раздел 5.2).

Минимална логика (mathbf {ML}) идва от интуиционистичната логика чрез изтриване на ex falso. Колмогоров [1925] показа, че този фрагмент вече съдържа отрицателна интерпретация на класическата логика, запазваща и двете количествени характеристики, вж. Leivant [1985]. Минималната логика доказва специалния случай (neg A / rightarrow (A / rightarrow / neg B)) на ex falso за отрицания. Колакито, де Йонг и Вардас [2017] изучават различни подсъзнателни логики, всяка по-слаба от (mathbf {ML}).

Griss оспорва използването на отрицанието на Brouwer, като се противопоставя както на закона за противоречие, така и на ex falso. Заслужава да се отбележи, че отрицанието всъщност не е необходимо за интуиционистичната математика, тъй като (0 = 1) е известно противоречие, така че (neg A) може да бъде определено чрез (A / rightarrow 0 = 1). Тогава ex falso може да бъде посочен като (0 = 1 / прав прах A), а законът за противоречие е доказуем от останалите аксиоми на (mathbf {H}).

Междинна логика на предложенията е всяка последователна колекция от формули за предложения, съдържаща всички аксиоми на (mathbf {IPC}) и затворена под modus ponens и заместване на произволни формули за букви с предложение. Всяка междинна логика на предложенията се съдържа в (mathbf {CPC}). Някои конкретни междинни предложения, характеризиращи се с добавяне на една или повече класически правилни, но интуиционистично недоказуеми схеми на аксиома към (mathbf {IPC}), бяха проучени подробно.

Една от най-простите междинни предложения за логика е логиката на Гьодел-Дамет (mathbf {LC}), получена чрез добавяне към (mathbf {IPC}) схемата ((A / rightarrow B) vee (B / rightarrow A)), което е валидно за всички и само онези крипке рамки, в които частичният ред на възлите е линеен. Гьодел [1932] използва безкрайна последователност от последователно по-силни междинни логики, за да покаже, че (mathbf {IPC}) няма ограничена интерпретация на таблицата за истинност. За всяко положително цяло число (n), нека (mathbf {G_n}) бъде (mathbf {LC}) плюс схемата ((A_1 / rightarrow A_2) vee / ldots / vee (A_1 / oldand / ldots / oldand A_n / rightarrow A_ {n + 1})). Тогава (mathbf {G_n}) е валиден за всички и само тези линейно подредени крипке рамки с не повече от (n) възли.

Логиката на Янков (mathbf {KC}), която добавя към (mathbf {IPC}) принципа на удостоверяемостта (neg A / vee / neg / neg A), очевидно няма разединението Имот. Логиката на Kreisel-Putnam (mathbf {KP}), получена чрез добавяне към (mathbf {IPC}) схемата ((neg A / rightarrow B / vee C) rightarrow ((neg A / rightarrow B) vee (neg A / rightarrow C))), има свойството на разединяване, но не отговаря на всички правила на Visser. Междинната логика, получена чрез добавяне на схемата (((neg / neg D / rightarrow D) rightarrow (D / vee / neg D)) rightarrow (neg / neg D / vee / neg D)), съответстваща към контрапримера на Роуз, към (mathbf {IPC}) също има свойството на разединяване. Iemhoff [2005] доказа, че (mathbf {IPC}) е единствената междинна логика на предложенията със свойството на разединението, което е затворено по всички правила на Visser. Iemhoff и Metcalfe [2009] разработиха официално смятане за обобщена допустимост за (mathbf {IPC}) и някои междинни логики. Goudsmit [2015] е задълбочено проучване на допустимите правила на междинната логика, с изчерпателна библиография.

Каза се, че междинната логика на предложение (mathbf {L}) има свойството на крайния кадър, ако има клас от крайни рамки, в които формулите, валидни за Крипке, са точно теоремите на (mathbf {L}), Много междинни логики, включително (mathbf {LC}) и (mathbf {KP}), имат това свойство. Янков [1968] използва безкрайна последователност от крайно вкоренени крипкески рамки, за да докаже, че има непрекъснато много междинни логики. De Jongh, Verbrugge и Visser [2009] доказаха, че всяка междинна логика (mathbf {L}) със свойството на ограничения кадър е логиката на предложението (mathbf {HA (L)}), т.е. клас на всички формули на езика на (mathbf {IPC}) всички чиито случаи на аритметично заместване са доказуеми в логическото разширение на (mathbf {HA}) от (mathbf {L}).

Една междинна логика на предложение (mathbf {L}) е структурно завършена, ако всяко правило, допустимо за (mathbf {L}), може да бъде извлечено в (mathbf {L}) и е наследствено структурно завършено, ако всяка междинна логика, която се простира (mathbf {L}) също е структурно завършена. Всяка междинна логика (mathbf {L}) има структурно завършване (mathbf { overline {L}}), получена чрез присъединяване на всички нейни допустими правила. (mathbf {LC}) и (mathbf {G_n}) са наследствено структурно завършени. Докато (mathbf {IPC}), (mathbf {RN}) и (mathbf {KC}) не са структурно завършени, структурните им завършения са наследствено структурно завършени. За тези резултати и повече вижте Citkin [2016, Други интернет ресурси].

Някои междинни предикатични логики, разширяващи се (mathbf {IQC}) и затворени при заместване, са (mathbf {IQC}) (+) DNS (раздел 4.1), (mathbf {IQC}) (+) MP (вж. Раздел 5.2), (mathbf {IQC}) (+) MP (+) IP (вж. Раздел 4.2) и интуиционистичната логика на постоянните домейни (mathbf {CD}) получена чрез добавяне към (mathbf {IQC}) схемата (forall x (A / vee B (x)) rightarrow (A / vee / forall x B (x))) за всички формули (A), (B (x)) с (x), които не се срещат в (A). Mints, Olkhovikov и Urquhart [2012, Other Internet Resources] показаха, че (mathbf {CD}) няма свойството за интерполация, опровергавайки по-рано публикувани доказателства от други автори.

6.2 Разширени теми

Влиянието на Брауър върху Гьодел е значително, въпреки че Гьодел никога не е станал интуиционист. Преводът на Гьодел [1933f] на интуиционистичната логика на предложение в модалната логика (mathbf {S4}) е описан в раздел 2.5 на записа на Гьодел и във встъпителната бележка на Troelstra към превода на [1933f] в том I от Събрания на Gödel Върши работа. Вижте също Mints [2012]. Крипке моделите за модална логика предхождаха тези за интуиционистичната логика.

Алтернативите на семантиката на Крипке и Бет за интуиционистичната логика на предсказанието и предиката включват топологичното тълкуване на Стоун [1937], Тарски [1938] и Мостовски [1948] (вж. Rasiowa и Sikorski [1963], Rasiowa [1974]), което беше разширено към интуиционистичния анализ от Скот [1968] и Крол [1978]. М. Hyland [1982] определи ефективния топос Eff и доказа, че неговата логика е интуиционистка. За много информативно обсъждане на семантиката за интуиционистичната логика и математика от У. Руйтенберг и интересна нова перспектива на Г. Бежанишвили и У. Холидей, вижте Други интернет ресурси (по-долу).

Една алтернатива на семантиката на реализируемост за интуиционистичната аритметика е интерпретацията на "Геодел" [1958] на "Диалектика", която свързва с всяка формула (B) на (L (mathbf {HA})) формула без количествено определяне (B_D) на езика на интуиционистичната аритметика от всички крайни типове. Интерпретацията на "Dialectica" на (B), наречете го (B ^ D), е (съществува Y / forall x B_D (Y, x)). Ако (B) е затворена теорема на (mathbf {HA}), тогава (B_D (F, x)) е доказуем за някакъв термин (F) в теорията на Гьодел (mathbf { T}) на „примитивни рекурсивни“функционалности от по-висок тип. Преводът от (B) в (B ^ D) изисква аксиома на избор (при всички крайни типове), MP и IP, така че не е строго конструктивен; въпреки това,числово-теоретичните функции, изразими чрез термини (F) на (mathbf {T}), са точно проривно рекурсивните функции на (mathbf {HA}) (и на (mathbf {PA})). Интерпретацията беше разширена до анализ от Spector [1962]; cf. Хауърд [1973]. Ясни експозиции и допълнителни справки се намират във въвеждането на Троелстра към превода на английски в Gödel [1990] на оригиналната статия на Dialectica, в Avigad и Feferman [1998] и във Ferreira [2008].

Докато (mathbf {HA}) е правилна част от класическата аритметика, интуитивното отношение към математическите обекти води до теория за реалните числа (вж. Раздели 3.4–3.7 от записа на интуиционизма във философията на математиката), разминавайки се от класическото. Интерпретацията на Kleene за реализиране на функции, разработена, за да докаже последователността на неговата формализация (mathbf {FIM}) на интуиционистичната теория на последователностите („интуиционистичен анализ“), променя интерпретацията на аритметичните формули; например, (neg / neg / forall x (A (x) vee / neg A (x))) е реализируема по функция за всяка аритметична формула (A (x)). На езика на анализа,Принципът на Марков и отрицателният превод на изброената аксиома на избор са сред многото неинтуиционистични принципи, които могат да се реализират във функция (чрез класически аргументи) и следователно съответстват на (mathbf {FIM}); cf. Kleene [1965], Vesley [1972] и Moschovakis [2003].

Конкретна и абстрактна семантика на реализирането на голямо разнообразие от формални системи са разработени и изучени от логици и компютърни учени; cf. Troelstra [1998] и van Oosten [2002] и [2008]. Вариациите на основните понятия са особено полезни за установяване на относителна последователност и относителна независимост на нелогичните аксиоми в теориите, основани на интуиционистичната логика; някои примери са Moschovakis [1971], Lifschitz [1979] и понятията за осъществимост за конструктивни и интуиционистични теории за множествата, разработени от Rathjen [2006, 2012] и Chen [2012]. Ранните абстрактни понятия за реализация включват наклона на Kleene [1962, 1963] и Aczel [1968] и Läuchli [1970]. Коленбах, Авигад и други са разработили интерпретации за реализация за части от класическата математика.

Логиката на оправданието на Артемов е алтернативно тълкуване на обяснението на БНК за интуиционистичните съединители и количествени характеристики, с (идеализирани) доказателства, играещи ролята на реализиращи обекти. Вижте също Артемов и Иемхоф [2007].

Друга линия на изследване в интуиционистичната логика се отнася до много противоречивото „създаване на предметни контрапримери“на Броууър на принципи на класическия анализ (като принципа на Марков), които не могат да бъдат опровергани въз основа на теорията на (Клайх и ФИМ) Весли [1965]. Чрез отслабване на формата на Kleene от принципа на непрекъснатия избор на Brouwer и добавяне на аксиома, която той нарече Схема на Крипке (KP), Myhill успя да формализира създаването на аргументи за предмет. KP е в противоречие с (mathbf {FIM}), но Vesley [1970] намери алтернативен принцип (схема на VESLE) на Vesley, който постоянно може да бъде добавен към (mathbf {FIM}) и предполага всички контрапримери, за които Brouwer изискваше създаване на тема. Krol [1978] и Scowcroft дават доказателства за топологична последователност за интуиционистичен анализ със схемата на Крипке и слабата приемственост.

6.3 Препоръчително четене

Записът на LEJ Brouwer обсъжда философията и математиката на Brouwer, с хронология на живота му и избран списък с публикации, включително преводи и вторични източници. Най-добрият начин да научите повече е да прочетете някои от оригиналните документи. Английски преводи на докторска дисертация на Брууър и други доклади, които първоначално са се появили на холандски, заедно с редица статии на немски език, могат да бъдат намерени в LEJ Brouwer: Collected Works [1975], редактиран от Heyting. Основната книга на Benacerraf и Putnam съдържа Brouwer [1912] (на английски превод), Brouwer [1949] и Dummett [1975]. Mancosu's [1998] предоставя преводи на английски на много основни статии на Брауър, Хейтинг, Гливенко и Колмогоров, с илюминация на уводен материал от У. ван Стигт, чийто [1990] е друг ценен ресурс.

Третото издание [1971] на класиката на Хейтинг [1956] е атрактивно въведение в интуиционистичната философия, логика и математическа практика. Като част от страхотния проект за редактиране и публикуване на Nachlass на Brouwer, van Dalen [1981] предоставя цялостен поглед върху собствената интуиционистка философия на Brouwer. Преводът на английски, в Van Heijenoort [1969], на Brouwer's [1927] (с фино въведение от Парсънс) все още е неизменна справка за теорията на Brouwer за континуума. Veldman [1990] и [2005] са автентични съвременни примери на традиционната интуиционистична математическа практика. Troelstra [1991] поставя интуиционистичната логика в своя исторически контекст като обща основа на конструктивната математика през ХХ век. Бежанишвили и де Йонг [2005,Други интернет ресурси] включва последните разработки в интуиционистичната логика.

[1965] на Kleene and Vesley дава внимателно аксиоматично третиране на интуиционистичния анализ, доказателство за неговата последователност по отношение на класически правилната подтеория и разширено приложение към теорията на Brouwer за генераторите на реални числа. [1969] на Kleene формализира теорията за частичните рекурсивни функционалности, позволявайки прецизни формализации на интерпретацията на функционалност, използвана през 1965 г., и на свързана интерпретация на q-реализацията, която дава правилото на Църквата-Клейн за интуиционистичен анализ.

Троелстра [1973], Бейсън [1985] и Троелстра и ван Дален [1988] (с корекции) се открояват като най-изчерпателните изследвания на интуиционистичните и полуинтуиционистичните формални теории, използвайки както конструктивни, така и класически методи, с полезни библиографии. Troelstra and Schwichtenberg [2000] представя теорията на доказателството за класическа, интуиционистична и минимална логика паралелно, като се фокусира върху последователни системи. [1998] на Troelstra представя формули като типове и (Kleene и Aczel) наклонени интерпретации за предложения и логика на предикати, както и абстрактни и конкретни реализуемости за множество приложения. Конструктивната теория на типовете на Мартин-Льоф [1984] (вж. Раздел 3.4 от записа на конструктивната математика) предоставя друга обща рамка, в която интуиционистичното разсъждение продължава да се развива.

библиография

• Aczel, P., 1968, "Наситени интуиционистични теории", в HA Schmidt, K. Schütte и H.-J. Thiele (ред.), Приноси към математическата логика, Амстердам: Северна Холандия: 1–11.
• Артемов, С. и Иемхоф, Р., 2007, „Основната интуиционистка логика на доказателствата“, сп. „Символна логика“, 72: 439–451.
• Avigad, J. и Feferman, S., 1998, функционална интерпретация на „Гьодел“(„Диалектика“), Глава V на Buss (съст.) 1998: 337–405.
• Bar-Hillel, Y. (съст.), 1965, Логика, методология и философия на науката, Амстердам: Северна Холандия.
• Бийсън, MJ, 1985, Основи на конструктивната математика, Берлин: Спрингер.
• Benacerraf, P. and Hilary Putnam (ред.), 1983, Философия на математиката: Избрани четения, 2-ро издание, Cambridge: Cambridge University Press.
• Beth, EW, 1956, „Семантична конструкция на интуиционистична логика“, Koninklijke Nederlandse Akad. von Wettenscappen, 19 (11): 357–388.
• Brouwer, LEJ, 1907 г., “За основите на математиката”, Теза, Амстердам; Превод на английски на Хейтинг (съст.) 1975: 11–101.
• –––, 1908, „Ненадеждността на логическите принципи“, английски превод в Heyting (съст.) 1975: 107–111.
• –––, 1912, „Интуиционизъм и формализъм“, английски превод от А. Дрезден, Бюлетин на Американското математическо дружество, 20 (1913): 81–96, препечатано в Benacerraf and Putnam (ред.) 1983: 77–89; също преиздаден в Heyting (ed.) 1975: 123–138.
• –––, 1923 г. [1954], „За значението на принципа на изключената средна в математиката, особено във теорията на функциите“, „Добавка и коригинда“и „По-нататък добавка и корекция“, превод на английски език от van Heijenoort (изд.) 1967: 334–345.
• –––, 1923 г., „Intuitionistische Zerlegung mathematischer Grundbegriffe“, Jahresbericht der Deutschen Mathematiker-Vereinigung, 33 (1925): 251-256; препечатано в Heyting (ed.) 1975, 275–280.
• –––, 1927 г., „Интуиционистични размисли за формализма“, първоначално публикуван през 1927 г., превод на английски език в Van Heijenoort (ed.) 1967: 490–492.
• –––, 1948, „Съзнание, философия и математика“, първоначално публикувана (1948), препечатана в Benacerraf and Putnam (ред.) 1983: 90–96.
• Burr, W., 2004, „Интуиционистичната аритметична йерархия“, в J. van Eijck, V. van Oostrom и A. Visser (ред.), Logic Colloquium '99 (Бележки за лекции в Logic 17), Wellesley, MA: ASL и AK Peters, 51–59.
• Buss, S. (ed.), 1998, Наръчник по теория на доказателствата, Амстердам и Ню Йорк: Elsevier.
• Чен, РМ. и Rathjen, M., 2012, „Lifschitz осъзнаваемост за интуиционистичната теория на множествата Zermelo-Fraenkel“, Архив за математическа логика, 51: 789–818.
• Colacito, A., de Jongh, D. and Vargas, A., 2017, „Subminimal отрицание“, Soft Computing, 21: 165–164.
• Crossley, J. и MAE Dummett (ред.), 1965 г., Формални системи и рекурсивни функции, Амстердам: Издателство Северна Холандия.
• van Dalen, D. (ed.), 1981, Cambridge Lectures on the Intuitionism, Brouwer's Cambridge: Cambridge University Press.
• Дамет, М., 1975, „Философската основа на интуиционистичната логика“, първоначално публикувана (1975), препечатана в Benacerraf and Putnam (ред.) 1983: 97–129.
• Dyson, V. and Kreisel, G., 1961,, Анализ на семантичната конструкция на Бет на интуиционистичната логика, Технически доклад № 3, Stanford: Лаборатория по приложна математика и статистика, Станфордския университет.
• Ферейра, Ф., 2008, „Най-артистичният пакет от смесица от идеи“, Диалектика, 62: 205–222.
• Фридман, Х., 1975, „Свойството на дисюнкция предполага свойството на числовото съществуване“, Трудове на Националната академия на науките, 72: 2877–2878.
• Gentzen, G., 1934–5, „Untersuchungen Über das logische Schliessen“, Mathematische Zeitschrift, 39: 176–210, 405–431.
• Ghilardi, S., 1999, "Обединение в интуиционистичната логика", Journal of Symbolic Logic, 64: 859–880.
• Гливенко, В., 1929, „Sur quelques point of la logique de M. Brouwer“, Académie Royale de Belgique, Billetins de la classe des Sciences, 5 (15): 183–188.
• Gödel, K., 1932, „Zum intuitionistischen Aussagenkalkül“, Anzeiger der Akademie der Wissenschaften във Виена, 69: 65–66. Възпроизведено и преведено с уводна бележка от AS Troelstra в Gödel 1986: 222–225.
• –––, 1933e, „Zur intuitionistischen Arithmetik und Zahlentheorie“, Ergebnisse eines mateischen Kolloquiums, 4: 34–38.
• –––, 1933f, „Eine Interpretation des intuitionistischen Aussagenkalküls“, възпроизведено и преведено с уводна бележка от AS Troelstra в Gödel 1986: 296–304.
• –––, 1958 г., „Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes“, Диалектика, 12: 280–287. Възпроизведено с английски превод в Gödel 1990: 241–251.
• –––, 1986, Събрани съчинения, кн. I, S. Feferman et al. (изд.), Оксфорд: University of Oxford.
• –––, 1990, Събрани съчинения, кн. II, S. Feferman et al. (изд.), Оксфорд: University of Oxford.
• Goudsmit, JP, 2015, Интуиционистични правила: Допустими правила за междинна логика, доктор на науките. дисертация, Университет в Утрехт.
• Harrop R., 1960, „Относно формулите на типовете (A / rightarrow B / vee C, A / rightarrow (Ex) B (x)) в интуиционистичните формални системи“, Journal of Symbolic Logic, 25: 27–32,
• van Heijenoort, J. (ed.), 1967, От Frege до Gödel: Книга-източник в математическата логика 1879-1931, Cambridge, MA: Harvard University Press.
• Heyting, A., 1930, „Die formalen Regeln der intuitionistischen Logik“, в три части, Sitzungsberichte der preussischen Akademie der Wissenschaften: 42–71, 158–169. Английски превод на част I в Манкосу 1998: 311–327.
• –––, 1956 г., Интуиционизъм: Въведение, Амстердам: издателство „Северна Холандия“, 3-то преработено издание, 1971 г.
• Heyting, A. (ed.), 1975, LEJ Brouwer: Collected Works (том 1: Философия и основи на математиката), Амстердам и Ню Йорк: Elsevier.
• Хауърд, Вашингтон, 1973 г., „Наследствено мажоризируеми функционалности от краен тип“, в Troelstra (ed.) 1973: 454–461.
• Hyland, JME, 1982, „Ефективните топоси“, в Troelstra and van Dalen (ed.) 1982: 165–216.
• Iemhoff, R., 2001, „За допустимите правила на интуиционистичната логика на предложенията“, Journal of Symbolic Logic, 66: 281–294.
• –––, 2005 г., „Междинна логика и правила на Визър“, сп. Notre Dame of Formal Logic, 46: 65–81.
• Iemhoff, R. and Metcalfe, G., 2009, “Теория на доказателството за допустими правила”, Annals of Pure and Applied Logic, 159: 171–186.
• Янков, В. А., 1968, „Изграждането на последователност от силно независими суперинтуиционистични предложения за калкули,” Съветска математика. Доклади, 9: 801–807.
• Jerabek, E., 2008, „Независими основи на допустимите правила“, Logic Journal of IGPL, 16: 249-267.
• de Jongh, DHJ, 1970 г., „Максималността на интуиционисткото предложение за изчисление по отношение на аритметиката на Хейтинг“, Journal of Symbolic Logic, 6: 606.
• de Jongh, DHJ, и Smorynski, C., 1976, „Крипке модели и интуиционистката теория на видовете“, Анали на математическата логика, 9: 157–186.
• de Jongh, D., Verbrugge, R. and Visser, A., 2011, „Междинна логика и свойството de Jongh“, Архив за математическа логика, 50: 197–213.
• Kino, A., Myhill, J. and Vesley, RE (ред.), 1970, Интуиционизъм и теория на доказателствата: Протоколи от лятната конференция в Buffalo, NY, 1968, Amsterdam: North-Holland.
• Kleene, SC, 1945, „За интерпретацията на интуиционистичната теория на числата“, Journal of Symbolic Logic, 10: 109–124.
• –––, 1952 г., Въведение в метаматематиката, Принстън: Ван Ностранд.
• –––, 1962, „Съединение и съществуване под влияние на елементарни интуиционистични формализми“, сп. „Символична логика“, 27: 11–18.
• –––, 1963 г., „Допълнение“, сп. „Символична логика“, 28: 154–156.
• –––, 1965, „Класически разширения на интуиционистичната математика“, в Бар-Хилел (съст.) 1965: 31–44.
• –––, 1969 г., Формализирани рекурсивни функции и формализирана реализация, мемоари на Американското математическо общество 89.
• Kleene, SC и Vesley, RE, 1965, Основите на интуиционистичната математика, особено във връзка с рекурсивните функции, Амстердам: Северна Холандия.
• Kreisel, G., 1958, „Елементарни свойства на завършеност на интуиционистичната логика с бележка за отрицанията на формулите на предварителен приклад“, Journal of Symbolic Logic, 23: 317–330.
• –––, 1962, „За слабата пълнота на интуиционистичната предикатна логика“, сп. „Символична логика“, 27: 139–158.
• Kripke, SA, 1965, „Семантичен анализ на интуиционистичната логика“, в J. Crossley и MAE Dummett (ред.) 1965: 92–130.
• Крол, М., 1978, „Топологичен модел на интуиционистичен анализ със схемата на Крипке“, Zeitschrift für Math. Logik und Grundlagen der Math., 24: 427–436.
• Leivant, D., 1979, „Максималност на интуиционистичната логика“, Математически център Tracts 73, Mathematisch Centrum, Amsterdam.
• –––, 1985 г., „Синтактични преводи и доказано рекурсивни функции“, Journal of Symbolic Logic, 50: 682–688.
• Läuchli, H., 1970, „Абстрактно понятие за осъществимост, за което е завършено интуитивното предикатно смятане“, в A. Kino et al. (ред.) 1965: 227–234.
• Lifschitz, V., 1979, „CT (_ 0) е по-силен от CT (_ 0)!“, Proceedings of the American Mathematical Society, 73 (1): 101–106.
• Mancosu, P., 1998, От Brouwer to Hilbert: Дебатът за основите на математиката през 1920-те, Ню Йорк и Оксфорд: University of Oxford.
• Martin-Löf, P., 1984, Интуиционистична теория на типа, Бележки на Джовани Самбин от поредица от лекции, изнесени в Падуа, юни 1980 г., Наполи: Библиополис.
• Mints, G., 2012, „Преводите на Гьодел – Тарски на интуиционистични формулировки на предложение“, в „Правилно разсъждение“(Лекции Бележки в компютърните науки 7265), Е. Ердем и др. (изд.), Dordrecht: Springer-Verlag: 487–491.
• Moschovakis, JR, 1971, „Може ли да няма нерекурсивни функции?“, Сп. „Символична логика“, 36: 309–315.
• –––, 2003, „Класически и конструктивни йерархии в разширения интуиционистичен анализ“, сп. „Символична логика“, 68: 1015–1043.
• –––, 2009 г., „Логиката на Брауър и Хейтинг“, в „Логика от Ръсел до Чърч“(Наръчник за историята на логиката, том 5), Дж. Уудс и Д. Габай (ред.), Амстердам: Elsevier: 77 -125.
• –––, 2017, „Интуиционистичен анализ и краят на времето“, Бюлетин на символичната логика, 23: 279–295.
• Nelson, D., 1947, "Рекурсивни функции и теория на интуиционистичните числа", сделки на Американското математическо общество, 61: 307-368.
• Нишимура, И., 1960, „За формулите на една променлива в интуиционистичното предложение за смятане“, сп. „Символична логика“, 25: 327–331.
• van Oosten, J., 1991, „Семантично доказателство за теоремата на де Йонг“, Архив за математическа логика, 31: 105–114.
• –––, 2002, „Реализируемост: историческо есе“, Математически структури в компютърните науки, 12: 239–263.
• –––, 2008 г., Реализируемост: Въведение в категоричната му страна, Амстердам: Elsevier.
• Плиско, В. Е., 1992, “За аритметичната сложност на някои конструктивни логики”, Математически бележки, (1993): 701–709. Преведено от Matematicheskie Zametki, 52 (1992): 94–104.
• Rasiowa, H., 1974, Алгебраичен подход към некласическата логика, Амстердам: Северна Холандия.
• Rasiowa, H. and Sikorski, R., 1963, The Mathematics of Metamathematics, Warsaw: Panstwowe Wydawnictwo Naukowe.
• Rathjen, M., 2006, „Реализируемост на конструктивната теория на множествата Zermelo-Fraenkel“, в Logic Colloquium 2003 (Бележки за лекции в Logic 24), J. Väänänen et al. (ред.), AK Peters 2006: 282–314.
• –––, 2012, „От слабото към силното съществуване”, Анали на чистата и приложна логика, 163: 1400–1418.
• Роуз, GF, 1953 г., "Предлагане на смятане и реализация", сделки на Американското математическо дружество, 75: 1–19.
• Рибаков, В., 1997, Допустимост на правилата за логически изводи, Амстердам: Elsevier.
• Скот, Д., 1968, "Разширяване на топологичната интерпретация до интуиционистичен анализ", Compositio Mathematica, 20: 194-210.
• Smorynski, CA, 1973, „Приложения на крипке модели“, в Troelstra (ed.) 1973: 324–391.
• Spector, C., 1962, „Доказано рекурсивни функционални функции на анализа: доказателство за последователност на анализа чрез разширение на принципите, формулирани в настоящата интуиционистка математика,“Теория на рекурсивните функции: Proceedings of Symposia in Pure Mathematics, том 5, JCE Dekker (изд.), Providence, RI: Американско математическо дружество, 1–27.
• van Stigt, WP, 1990, Интуиционизмът на Брауер, Амстердам: Северна Холандия.
• Стоун, MH, 1937 г., „Топологично представяне на разпределителни решетки и броуверска логика“, Casopis Pest. Мат. Fys., 67: 1–25.
• Тарски, А., 1938, „Der Aussagenkalkül und die Topologie“, Fundamenta Mathematicae, 31: 103–104.
• Troelstra, AS, 1991, „История на конструктивизма през ХХ век“, ITLI Prepublication Series ML – 1991–05, Амстердам. Окончателна версия в теорията на множествата, аритметика и основи на математиката (бележки от лекции в логиката 36), J. Kenney и R. Kossak (ред.), Асоциация за символична логика, Ithaca, NY, 2011: 150–179.
• –––, 1998, „Реализируемост“, глава VI от Buss (ed.), 1998: 407–473.
• –––, уводна бележка към 1958 г. и 1972 г. в Gödel, 1990: 217–241.
• Troelstra, AS (съст.), 1973 г., Метаматематическо изследване на интуиционистичната аритметика и анализ (Бележки от лекции по математика 344), Берлин: Springer-Verlag. Поправки и допълнения, достъпни от редактора.
• Troelstra, AS и Schwichtenberg, H., 2000, Основна доказателствена теория (Cambridge Tracts in Theoretical Computer Science: том 43), 2-ро издание, Cambridge: Cambridge University Press.
• Troelstra, AS и van Dalen, D., 1988, Конструктивизъм в математиката: Въведение, 2 тома, Амстердам: Издателство Северна Холандия. [Вижте също и поправките в други интернет ресурси.]
• Troelstra, AS и van Dalen, D. (ред.), 1982 г., Столичният симпозиум на Брайър LEJ, Амстердам: издателство North-Holland.
• Veldman, W., 1976, „Интуиционистична теорема за пълнота на интуиционистичната логика на предиката“, Journal of Symbolic Logic, 41: 159–166.
• –––, 1990 г., „Изследване на интуиционистичната теория на описателните множества“, в П. П. Петков (съст.), „Математическа логика“, сборник с Хейтинг конференцията, Ню Йорк и Лондон: Пленум Прес, 155–174.
• –––, 2005 г., „Два прости множества, които не са положително Борел“, Анали на чистата и приложна логика, 135: 151–209.
• Vesley, RE, 1972, „Избор на последователности и принцип на Марков“, Compositio Mathematica, 24: 33–53.
• –––, 1970 г., „приятна алтернатива на схемата на Крипке“, от A. Kino et al. (изд.) 1970: 197ff.
• Visser, A., 1999, „Правила и аритметика“, списание Notre Dame of Formal Logic, 40: 116–140.
• –––, 2002, „Заместване на изречения (Sigma ^ {0} _1): проучвания между интуиционистичната логика на предложенията и интуиционистичната аритметика,„ Анали на чистата и приложна логика, 114: 227–271.
• –––, 2006, „Предсказваща логика на конструктивните аритметични теории“, сп. „Символична логика“, 72: 1311–1326.

Академични инструменти

	Как да цитирам този запис.
	Вижте PDF версията на този запис в Дружеството на приятелите на SEP.
	Разгледайте тази тема за вписване в интернет философския онтологичен проект (InPhO).
	Подобрена библиография за този запис в PhilPapers, с връзки към неговата база данни.

Други интернет ресурси

• Бежанишвили, Г. и Холидей, W., 2018, „Семантична йерархия за интуиционистична логика“, ръкопис, публикации на UC Berkeley.
• Бежанишвили, Н. и де Йонг, DHJ, 2005 г., Интуиционистична логика, Бележки от лекции, представени в ESSLLI, Единбург.
• Brouwer, Откъси от лекциите на Brouwer's Cambridge.
• Циткин, А., 2016, „Наследствено структурно завършени суперинтуиционистични дедуктивни системи“, ръкопис на arXiv.org.
• Mints, G., Olkhovikov, G. and Urquhart, A., 2012, „Провал на интерполация в интуиционистичната логика на постоянните домейни“, ръкопис, arXiv.org.
• Troelstra, AS и JR Moschovakis, 2018, Corrections to AS Troelstra and D. van Dalen, 1988, Конструктивизъм в математиката.
• Проблеми в логиката на доказване, поддържана от Лев Беклемишев.
• Библиография на осъществимост, поддържана от Ларс Биркедал.
• van Oosten 2000 и други предпечатки, свързани с реализируемостта, поддържани от Jaap van Oosten.