Линденбаум-Тарски алгебрасы: Логикалық теориялардың алгебралық негізі
Lindenbaum–Tarski algebra
Линденбаум-Тарски алгебрасы: логикалық теориялар, формулалардың эквиваленттілік кластары, дәлелдемелер, конгруенция қатынасы. Математикалық логикадағы маңызды құрылым.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Математикалық логикада логикалық теория T-ның Линденбаум-Тарски алгебрасы (немесе Линденбаум алгебрасы) теорияның сөйлемдерінің эквиваленттілік кластарынан тұрады (яғни, p ~ q эквиваленттілік қатынасы бойынша, дәлірек айтқанда, p және q теория T-да дәлелденген кезде эквивалентті болады). Яғни, егер теория T екі сөйлемнің бірін-бірі логикалық түрде қамтитынын дәлелдей алса, онда олар эквивалентті болып саналады. Линденбаум-Тарски алгебрасы – осы конгруенциялық қатынас арқылы формулалар алгебрасын бөлу нәтижесінде алынған факторлы алгебра. Алгебра логиктер Адольф Линденбаум және Альфред Тарскидің құрметіне аталған. Линденбаум 1926-1927 оқу жылынан бастап Ян Лукашевичтің математикалық логика семинарындағы әдісін дамытты, ал бұл әдіс Тарскидің жұмыстары арқылы келесі онжылдықтарда кеңінен танымал болды және жалпыланды. Линденбаум-Тарски алгебрасы қазіргі алгебралық логиканың бастауы деп есептеледі.
In mathematical logic, the Lindenbaum–Tarski algebra (or Lindenbaum algebra) of a logical theory T consists of the equivalence classes of sentences of the theory (i. e., the quotient, under the equivalence relation ~ defined such that p ~ q exactly when p and q are provably equivalent in T). That is, two sentences are equivalent if the theory T proves that each implies the other. The Lindenbaum–Tarski algebra is thus the quotient algebra obtained by factoring the algebra of formulas by this congruence relation. The algebra is named for logicians Adolf Lindenbaum and Alfred Tarski. Starting in the academic year 1926 1927, Lindenbaum pioneered his method in Jan Łukasiewicz's mathematical logic seminar, and the method was popularized and generalized in subsequent decades through work
by Tarski. The Lindenbaum–Tarski algebra is considered the origin of the modern algebraic logic.
Операциялар
Lindenbaum–Tarski алгебрасы А-ның операциялары негізгі теория Т-нің операцияларынан мұраға алынады. Оларға әдетте конъюнкция және дисъюнкция кіреді, олар эквиваленттік сыныптарда дұрыс анықталған. Егер T-де жоспарлау болса, онда A – Буль алгебрасы болады, егер логика классикалық болса. Егер Т теориясы пропозициялық таутологиялардан тұрса, онда Lindenbaum–Tarski алгебрасы пропозициялық айнымалылар арқылы құрылған еркін Буль алгебрасы болып табылады.
The operations in a Lindenbaum–Tarski algebra A are inherited from those in the underlying theory T. These typically include conjunction and disjunction, which are well defined on the equivalence classes. When negation is also present in T, then A is a Boolean algebra, provided the logic is classical. If the theory T consists of the propositional tautologies, the Lindenbaum–Tarski algebra is the free Boolean algebra generated by the propositional variables.
Байланысты алгебралар
Гейтинг алгебралары мен ішкі алгебралары интуиционистік логика және S4 модальдық логика үшін сәйкесінше Линденбаум-Тарски алгебралары болып табылады. Тарски әдісі қолданылатын логика алгебраланады деп аталады. Дегенмен, бұл әдіс қолданылмайтын бірнеше логикалар бар, мысалы, S1, S2 немесе S3 модальдық логикалары, оларда қажеттілік принципі жоқ (⊢φ болғанда ⊢□φ дегенді білдірмейді), сондықтан жоғарыда анықталған ~ конгруенция емес (өйткені ⊢φ→ψ болғанда ⊢□φ→□ψ дегенді білдірмейді). Тарски әдісі қолданылмайтын логиканың тағы бір түрі – релеванттылық логикасы, себебі екі теорема берілгенде, бірінен екіншісіне жасалған логикалық қорытынды релеванттылық логикасында теорема болып табылмайды. Алгебралау процесін (және осы ұғымды) зерттеу, Тарски әдісімен байланысты болмаса да, абстрактты алгебралық логиканың дамуына ықпал етті.
Heyting algebras and interior algebras are the Lindenbaum–Tarski algebras for intuitionistic logic and the modal logic S4, respectively. A logic for which Tarski's method is applicable, is called algebraizable. There are however a number of logics where this is not the case, for instance the modal logics S1, S2, or S3, which lack the rule of necessitation (⊢φ implying ⊢□φ), so ~ (defined above) is not a congruence (because ⊢φ→ψ does not imply ⊢□φ→□ψ). Another type of logic where Tarski's method is inapplicable is relevance logics, because given two theorems an implication from one to the other may not itself be a theorem in a relevance logic. The study of the algebraization process (and notion) as topic of interest by itself, not necessarily by Tarski's method, has led to the development of abstract algebraic logic.