Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Логикада қатаң шартты (символ: , немесе ⥽) – модальдық оператормен басқарылатын шартты, яғни модальдық логиканың логикалық байланысы. Ол логикалық тұрғыдан классикалық логиканың материалдық шарттысына, модальдық логиканың қажеттілік операторымен үйлесімді. Кез келген екі пікір p және q үшін, p → q формуласы p пікірінің q пікірін материалдық тұрғыдан білдіретінін, ал ⥽ p q пікірінің q пікірін қатаң түрде білдіретінін көрсетеді. Қатаң шарттылар – Кларенс Ирвинг Льюистің логика үшін, табиғи тілдегі индикативті шарттыларды жеткілікті түрде білдіре алатын шарттыны табуға жасаған әрекетінің нәтижесі. Олар Молинист дінтануын зерттеуде де қолданылған.
In logic, a strict conditional (symbol: , or ⥽) is a conditional governed by a modal operator, that is, a logical connective of modal logic. It is logically equivalent to the material conditional of classical logic, combined with the necessity operator from modal logic. For any two propositions p and q, the formula p → q says that p materially implies q while says that p strictly implies q. Strict conditionals are the result of Clarence Irving Lewis's attempt to find a conditional for logic that can adequately express indicative conditionals in natural language. They have also been used in studying Molinist theology.
Парадокстерден аулақ болу
Қатаң шарттылықтар материалдық импликацияның парадокстарын болдырмауға көмектеседі. Мысалы, келесі мәлімдеме материалдық импликация арқылы дұрыс формалдастырылмайды:
The strict conditionals may avoid paradoxes of material implication. The following statement, for example, is not correctly formalized by material implication:
Егер Билл Гейтс медицина мамандығын бітірген болса, онда Элвис ешқашан өлмеген. Бұл шарттың қате екені анық: Билл Гейтстің білімі Элвис әлі тірі ме, жоқ па, деген мәселеге ешқандай қатысы жоқ. Дегенмен, бұл формуланың классикалық логикаға материалдық импликация арқылы тікелей енгізілуі мынаған алып келеді:
If Bill Gates graduated in medicine, then Elvis never died. This condition should clearly be false: the degree of Bill Gates has nothing to do with whether Elvis is still alive. However, the direct encoding of this formula in classical logic using material implication leads to:
Билл Гейтс медицинаны бітірді → Элвис ешқашан өлмеді. Бұл формула дұрыс, себебі алғы шарты A жалған болғанда A → B формуласы дұрыс болады. Сондықтан бұл формула түпнұсқа сөйлемді толыққанды аудармайды. Қатаң шарттылықты қолдану арқылы кодтау:
Bill Gates graduated in medicine → Elvis never died. This formula is true because whenever the antecedent A is false, a formula A → B is true. Hence, this formula is not an adequate translation of the original sentence. An encoding using the strict conditional is:
(Билл Гейтс медицинаны бітірді → Элвис ешқашан өлмеді). Модальдық логикада бұл формула (шамамен) Билл Гейтс медицинаны бітірген барлық мүмкін әлемдерде Элвис ешқашан өлмегенін білдіреді. Бірақ Билл Гейтстің медицинаны бітірген және Элвистің қайтыс болған әлемін елестету оңай болғандықтан, бұл формула жалған. Демек, бұл формула түпнұсқа сөйлемнің дұрыс аудармасы болып көрінеді.
(Bill Gates graduated in medicine → Elvis never died). In modal logic, this formula means (roughly) that, in every possible world in which Bill Gates graduated in medicine, Elvis never died. Since one can easily imagine a world where Bill Gates is a medicine graduate and Elvis is dead, this formula is false. Hence, this formula seems to be a correct translation of the original sentence.
Конструктивті логика
Конструктивті ортада, ⥽ және арасындағы симметрия бұзылады, және екі оператор тәуелсіз зерттелуі мүмкін. Конструктивті қатаң импликация Хейтинг арифметикасының интерпретациялануын зерттеуге және компьютер ғылымында жебелерді және қорғалған рекурсияны модельдеуге қолданылуы мүмкін.
In a constructive setting, the symmetry between ⥽ and is broken, and the two connectives can be studied independently. Constructive strict implication can be used to investigate interpretability of Heyting arithmetic and to model arrows and guarded recursion in computer science.