Крейг-Линдон теоремасы және логикалық интерполяция
Craig interpolation
Крейг теоремасы – математикалық логикадағы формулалар арасындағы байланыс. Φ→Ψ болса, ортақ белгілері бар формула ρ табылады: Φ→ρ және ρ→Ψ. SEO үшін маңызды!
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Математикалық логикада Крейгтің интерполяция теоремасы – әр түрлі логикалық теориялар арасындағы байланыс туралы мәлімдеме. Қарапайым түсіндіргенде, егер φ формуласы ψ формуласын логикалық түрде тудырса, және екеуінің де кем дегенде бір атомдық айнымалы белгісі ортақ болса, онда ρ формуласы болады, ол интерполянт деп аталады. Онда ρ формуласындағы барлық логикалық емес символдар φ және ψ формулаларында кездеседі, φ формуласы ρ формуласын тудырады, ал ρ формуласы ψ формуласын тудырады. Бұл теореманы алғаш рет 1957 жылы Уильям Крейг бірінші реттік логика үшін дәлелдеген. Теореманың түрлері басқа логикалар үшін де қолданылады, мысалы, есептік логика үшін. 1959 жылы Роджер Линдон бірінші реттік логика үшін Крейгтің интерполяция теоремасының күшті түрін дәлелдеді; осы жалпы нәтиже кейде Крейг–Линдон теоремасы деп аталады.
In mathematical logic, Craig's interpolation theorem is a result about the relationship between different logical theories. Roughly stated, the theorem says that if a formula φ implies a formula ψ, and the two have at least one atomic variable symbol in common, then there is a formula ρ, called an interpolant, such that every non logical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ. The theorem was first proved for first order logic by William Craig in 1957. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's interpolation theorem for first order logic was proved by Roger Lyndon in 1959; the overall result is sometimes called the Craig–Lyndon theorem.
Линдонның интерполяция теоремасы
S және T екі бірінші реттік теория болсын деп есептейік. Белгі ретінде S ∪ T, S және T екеуін де қамтитын ең кіші теорияны білдірсін; S ∪ T теориясының сигнатурасы, S және T сигнатураларын қамтитын ең кіші сигналтура болады. Сондай-ақ, S ∩ T екі теорияның тілдерінің қиылысы болсын; S ∩ T теориясының сигнатурасы, екі тілдің сигнатураларының қиылысы болады. Линдон теоремасы бойынша, егер S ∪ T қанағаттандырылмаса, онда S ∩ T тілінде ρ интерполяциялық сөйлем болады, ол S-тің барлық модельдерінде дұрыс, ал T-тің барлық модельдерінде жалған. Одан әрі, ρ мықты қасиетке ие, яғни ρ-да оң мәнде қолданылған әрбір қатынас символы S-тің кейбір формуласында оң мәнде, ал T-тің кейбір формуласында теріс мәнде қолданылады, ал ρ-да теріс мәнде қолданылған әрбір қатынас символы S-тің кейбір формуласында теріс мәнде, ал T-тің кейбір формуласында оң мәнде қолданылады.
Suppose that S and T are two first order theories. As notation, let S ∪ T denote the smallest theory including both S and T; the signature of S ∪ T is the smallest one containing the signatures of S and T. Also let S ∩ T be the intersection of the languages of the two theories; the signature of S ∩ T is the intersection of the signatures of the two languages. Lyndon's theorem says that if S ∪ T is unsatisfiable, then there is an interpolating sentence ρ in the language of S ∩ T that is true in all models of S and false in all models of T. Moreover, ρ has the stronger property that every relation symbol that has a positive occurrence in ρ has a positive occurrence in some formula of S and a negative occurrence in some formula of T, and every relation symbol with a negative occurrence in ρ has a negative occurrence in some formula of S and a positive occurrence in some formula of T.
Қолданбалар
Крейг интерполяциясының көптеген қолданыстары бар, олардың ішінде дәйектілік дәлелдеу, модельді тексеру, модулдік спецификацияларда дәлелдеу, модулдік онтологиялар.
Craig interpolation has many applications, among them consistency proofs, model checking, proofs in modular specifications, modular ontologies.