Броуэр-Хейтинг-Колмогоров интерпретациясы – интуиционистік логиканың стандартты түсіндірмесі. Дәлелдеудің негізгі принциптері, формулалар мен реализациясы туралы ақпарат.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Математикалық логикада интуиционистік логиканың Брауэр-Хейтинг-Колмогоров интерпретациясы, немесе БХК интерпретациясы, Л. Е. Ж. Брауэр және Аренд Хейтинг, сондай-ақ Андрей Колмогоров дербес ұсынған. Оны кейде Стивен Клиннің іске асыру теориясымен байланысты болғандықтан, іске асыру интерпретациясы деп те атайды. Бұл интуиционистік логиканың стандартты түсіндірмесі болып табылады.
In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer and Arend Heyting, and independently by Andrey Kolmogorov. It is also sometimes called the realizability interpretation, because of the connection with the realizability theory of Stephen Kleene. It is the standard explanation of intuitionistic logic.
Түсіндіру
Түсіндірілімде берілген формуланың дәлелі ретінде не көзделгені айтылады. Бұл формула құрылымы бойынша индукция арқылы анықталады:
The interpretation states what is intended to be a proof of a given formula. This is specified by induction on the structure of that formula:
-ның дәлелі – бұл жұп, мұнда -ның дәлелі және -ның дәлелі болады. -ның дәлелі – немесе, мұнда -ның дәлелі, немесе, мұнда -ның дәлелі. -ның дәлелі – бұл функция, ол -ның дәлелін -ның дәлеліне айналдырады. -ның дәлелі – бұл жұп, мұнда -ның элементі және -ның дәлелі болады. -ның дәлелі – бұл функция, ол -ның элементін -ның дәлеліне айналдырады. Формула мына түрде анықталады: , сондықтан оның дәлелі – бұл функция, ол -ның дәлелін -ның дәлеліне айналдырады. -ның дәлелі жоқ, бұл абсурд немесе төменгі тип (кейбір бағдарламалау тілдерінде тоқтамайды). Бастапқы өрнектің түсіндірілуі контекстен белгілі болады деп есептеледі. Арифметика контекстінде -ның дәлелі – екі терминиң мәнін бір санға келтіретін есептеу. Колмогоров осыған ұқсас жолмен жүрді, бірақ өзінің түсіндірілімін мәселелер мен шешімдер тұрғысынан баяндады. Формуланы растау – бұл сол формуламен бейнеленген мәселенің шешімін білуді мәлімдеу. Мысалы, - бұл -ны -ға келтіру мәселесі; оны шешу үшін -ның шешімі берілгенде - мәселесін шешу әдісі қажет.
A proof of is a pair where is a proof of and is a proof of A proof of is either where is a proof of or where is a proof of A proof of is a function that converts a proof of into a proof of A proof of is a pair where is an element of and is a proof of A proof of is a function that converts an element of into a proof of The formula is defined as , so a proof of it is a function that converts a proof of into a proof of There is no proof of , the absurdity or bottom type (nontermination in some programming languages). The interpretation of a primitive proposition is supposed to be known from context. In the context of arithmetic, a proof of the formula is a computation reducing the two terms to the same numeral. Kolmogorov followed the same lines but phrased his interpretation in terms of problems and solutions. To assert a formula is to claim to know a solution to the problem represented by that formula. For instance is the problem of reducing to ; to solve it requires a method to solve problem given a solution to problem .
Абсурдтың анықтамасы
Жалпы алғанда, логикалық жүйенің формальды жоққа шығару операторы болуы мүмкін емес, сондықтан «жоқ» дегеннің дәлелі болмағанда; Гёдельдің толық еместік теоремаларын қараңыз. BHK интерпретациясы «жоқ» дегенді абсурдқа алып келу деп түсіндіреді, яғни абсурдқа белгіленген , сондықтан дәлелі – бұл дәлелін абсурдқа түрлендіретін функция. Абсурдқа мысал арифметикада кездеседі. 0 = 1 деп есептейік және математикалық индукция арқылы жүрелік: 0 = 0 теңдік аксиомасы бойынша. Енді (индукция гипотезасы бойынша), егер 0 белгілі бір n табиғи санына тең болса, онда 1, n + 1-ге тең болар еді (Пеано аксиомасы: Sm = Sn егер және тек қана m = n болса), бірақ 0 = 1 болғандықтан, 0 сондай-ақ n + 1-ге тең болар еді. Индукция бойынша, 0 барлық сандарға тең, демек, кез келген екі табиғи сан тең болады. Сондықтан, 0 = 1 дәлелінен кез келген қарапайым арифметикалық теңдікті, осылайша кез келген күрделі арифметикалық тұжырымды дәлелдеуге болады. Бұған қоса, бұл нәтижеге қол жеткізу үшін 0 кез келген табиғи санның «мұрагері емес» дегенді айтатын Пеано аксиомасын пайдалану қажет емес. Бұл 0 = 1-ді Heyting арифметикасында қолдануға ыңғайлы жасайды (ал Пеано аксиомасы 0 = Sn → 0 = S0 түрінде қайта жазылады). 0 = 1-ді осылай қолдану жарылыс принципін растайды.
It is not, in general, possible for a logical system to have a formal negation operator such that there is a proof of "not" exactly when there isn't a proof of ; see Gödel's incompleteness theorems. The BHK interpretation instead takes "not" to mean that leads to absurdity, designated , so that a proof of is a function converting a proof of into a proof of absurdity. A standard example of absurdity is found in dealing with arithmetic. Assume that 0 = 1, and proceed by mathematical induction: 0 = 0 by the axiom of equality. Now (induction hypothesis), if 0 were equal to a certain natural number n, then 1 would be equal to n + 1, (Peano axiom: Sm = Sn if and only if m = n), but since 0 = 1, therefore 0 would also be equal to n + 1. By induction, 0 is equal to all numbers, and therefore any two natural numbers become equal. Therefore, there is a way to go from a proof of 0 = 1 to a proof of any basic arithmetic equality, and thus to a proof of any complex arithmetic proposition. Furthermore, to get this result it was not necessary to invoke the Peano axiom that states that 0 is "not" the successor of any natural number. This makes 0 = 1 suitable as in Heyting arithmetic (and the Peano axiom is rewritten 0 = Sn → 0 = S0). This use of 0 = 1 validates the principle of explosion.
Функцияның анықтамасы
BHK түсіндіруі бір дәлелді екіншісіне түрлендіретін немесе доменнің бір элеметін дәлелге түрлендіретін функцияның не екендігі туралы қабылданған көзқарасқа байланысты болады. Конструктивизмнің әртүрлі нұсқалары осы мәселеде келіспейді. Клиннің іске асырылатындық теориясы функцияларды есептеуге болатын функциялармен теңестіреді. Ол Heyting арифметикасымен айналысады, онда квантификация домені – табиғи сандар, ал бастапқы тұжырымдар x = y түрінде болады. x = y дәлелі – егер x пен y мәндері бірдей болса (бұл табиғи сандар үшін әрқашан шешіледі), әйтпесе дәлел жоқ. Содан кейін олар индукция арқылы күрделі алгоритмдерге құрастырылады. Егер лямбда-есептеу функция ұғымын анықтаса, онда BHK түсіндіруі табиғи дедукция мен функциялар арасындағы сәйкестікті сипаттайды.
The BHK interpretation will depend on the view taken about what constitutes a function that converts one proof to another, or that converts an element of a domain to a proof. Different versions of constructivism will diverge on this point. Kleene's realizability theory identifies the functions with the computable functions. It deals with Heyting arithmetic, where the domain of quantification is the natural numbers and the primitive propositions are of the form x = y. A proof of x = y is simply the trivial algorithm if x evaluates to the same number that y does (which is always decidable for natural numbers), otherwise there is no proof. These are then built up by induction into more complex algorithms. If one takes lambda calculus as defining the notion of a function, then the BHK interpretation describes the correspondence between natural deduction and functions.