Математикалық логикадағы дедукция теоремасы: гипотезасыз шартты дәлелдеуді, A→B түріндегі қорытындыны A гипотезасынан B-ға шығаруды қамтиды. Ыңғайлы құрал!
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Кіріспе
Математикалық логикадағы метатеорема. Математикалық логикада дедукция теоремасы – гипотезадан шартты дәлелдемелерді, егер жүйе сол гипотезаны тікелей аксиоматизацияламайтын болса, жасауды негіздейтін метатеорема. Яғни, A → B импликациясын дәлелдеу үшін A-ны гипотеза ретінде қабылдап, содан кейін B-ны шығару жеткілікті. Дедукция теоремалары мәлімдемелік логика және бірінші реттік логика үшін де бар. Дедукция теоремасы – Гильберт стиліндегі дедукция жүйелерінде маңызды құрал, себебі ол одан да түсінікті және көбінесе әлдеқайда қысқа дәлелдемелерді жасауға мүмкіндік береді. Кейбір басқа формальды дәлелдеу жүйелерінде осыған ұқсас ыңғайлылық нақты қорытынды шығару ережесі арқылы қамтамасыз етіледі; мысалы, табиғи дедукция оны импликацияны енгізу деп атайды. Толығырақ айтқанда, мәлімдемелік логиканың дедукция теоремасы, егер формула болжамдар жиынынан дедукцияланса, онда оның импликациясы да дедукцияланады; символдармен көрсеткенде, болады. Егер болжамдар жиыны бос болса, дедукция теоремасы талабын былай жазуға болады: болады. Предикаттық логиканың дедукция теоремасы ұқсас, бірақ қосымша шектеулермен келеді (мысалы, егер жабық формула болса, олар орындалады). Жалпы алғанда, дедукция теоремасы қарастырылып отырған теорияның барлық логикалық егжей-тегжейін ескеруі керек, сондықтан әр логикалық жүйе техникалық тұрғыдан өзінің дедукция теоремасын қажет етеді, бірақ айырмашылықтар көбінесе шағын болады. Дедукция теоремасы бірінші реттік логиканың стандартты дедукциялық жүйелері бар барлық бірінші реттік теориялар үшін жарамды. Дегенмен, жаңа қорытынды шығару ережелері қосылған бірінші реттік жүйелер бар, онда дедукция теоремасы орындалмайды. Атап айтқанда, дедукция теоремасы Бёркхофф–фон Нейманның кванттық логикасында қолданылмайды, себебі Гильберт кеңістігінің сызықтық кіші кеңістіктері үлестірімді емес торды құрайды.
Metatheorem in mathematical logicIn mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs from a hypothesis in systems that do not explicitly axiomatize that hypothesis, i. e. to prove an implication A → B, it is sufficient to assume A as a hypothesis and then proceed to derive B. Deduction theorems exist for both propositional logic and first order logic. The deduction theorem is an important tool in Hilbert style deduction systems because it permits one to write more comprehensible and usually much shorter proofs than would be possible without it. In certain other formal proof systems the same conveniency is provided by an explicit inference rule; for example natural deduction calls it implication introduction. In more detail, the propositional logic deduction theorem states that if a formula is deducible from a set of assumptions then the implication is deducible from ; in symbols, implies In the special case where is the empty set, the deduction theorem claim can be more compactly written as: implies The deduction theorem for predicate logic is similar, but comes with some extra constraints (that would for example be satisfied if is a closed formula). In general a deduction theorem needs to take into account all logical details of the theory under consideration, so each logical system technically needs its own deduction theorem, although the differences are usually minor. The deduction theorem holds for all first order theories with the usual deductive systems for first order logic. However, there are first order systems in which new inference rules are added for which the deduction theorem fails. Most notably, the deduction theorem fails to hold in Birkhoff–von Neumann quantum logic, because the linear subspaces of a Hilbert space form a non distributive lattice.