Трактенброт теоремасы: Бірінші реттік логикада шекті модельдер класында жарамдылық мәселесінің шешілмейтіні туралы
Trakhtenbrot's theorem
Трахтенброт теоремасы: Бірінші реттік логикада шекті модельдерде дұрыстық анықтау мүмкін емес. Бұл Гёдельдің толықтық теоремасының шектеуін көрсетеді. Логика, есептеу теориясы.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Логика, шекті модельдер теориясы және есептеу теориясында Трахтенброт теоремасы (Борис Трахтенброттың еңбегі) бірінші реттік логикадағы барлық шекті модельдер класындағы жарамдылық мәселесінің шешілмейтінін көрсетеді. Шындығында, шекті модельдерде жарамды болатын сөйлемдер класы рекурсивті тізімдемейді (бірақ ко-рекурсивті тізімдемелі). Трахтенброт теоремасы Гёдельдің толықтық теоремасының (бірінші реттік логиканың негізгі теоремасы) шекті жағдайда қолданылмайтынын білдіреді. Сондай-ақ, барлық құрылымдар үшін жарамды болу, тек шекті құрылымдар үшін жарамды болудан 'оңайырақ' екендігі интуицияға қарсы келеді. Теорема алғаш рет 1950 жылы жарияланды: "Шекті кластардағы шешілушілік мәселесі үшін алгоритмнің болу мүмкін еместігі".
In logic, finite model theory, and computability theory, Trakhtenbrot's theorem (due to Boris Trakhtenbrot) states that the problem of validity in first order logic on the class of all finite models is undecidable. In fact, the class of valid sentences over finite models is not recursively enumerable (though it is co recursively enumerable). Trakhtenbrot's theorem implies that Gödel's completeness theorem (that is fundamental to first order logic) does not hold in the finite case. Also it seems counter intuitive that being valid over all structures is 'easier' than over just the finite ones. The theorem was first published in 1950: "The Impossibility of an Algorithm for the Decidability Problem on Finite Classes".
Теорема
Шекті құрылымдар үшін қанағаттандырылатындығы бірінші реттік логикада шешілмейді. Яғни, барлық шекті құрылымдарда қанағаттандырылатын бірінші реттік логикалық формуланы құрайтын {φ | φ} жиыны шешілмейді.
Satisfiability for finite structures is not decidable in first order logic. That is, the set {φ | φ is a sentence of first order logic that is satisfied by all finite structures} is undecidable.
Интуитивті дәлелдеу
Бұл дәлел Х. Д. Эббингхаус жазған «Математикалық логика» кітабының 10-тарауы, 4- және 5-бөлімдерінен алынған. Гёделдің бірінші толық еместік теоремасын дәлелдеудің ең көп таралған тәсіліне тоқтату мәселесінің шешілмейтіндігін пайдалану арқылы, әрбір Тьюринг машинасы үшін сәйкес арифметикалық сөйлем бар , оны тиімді түрде алуға болады, және ол егер және тек бос лентада тоқтаса ғана дұрыс. Интуитивті түрде , «бос лентадағы есептеу жазбасының тоқтаумен аяқталатын Гёдель коды болатын натурал сан бар» дегенді білдіреді. Егер машина шекті қадамдарда тоқтаса, онда толық есептеу жазбасы да шекті болады, содан кейін натурал сандардың шекті бастапқы сегменті табылады, онда арифметикалық сөйлем осы бастапқы сегментте де дұрыс болады. Интуитивті түрде, бұл жағдайда оны дәлелдеу үшін тек шекті сандардың арифметикалық қасиеттерін пайдалану жеткілікті. Егер машина шекті қадамдарда тоқтамаса, онда ол кез келген шекті модельде жалған, себебі тоқтаумен аяқталатын шекті есептеу жазбасы жоқ. Осылайша, егер тоқтаса, ол кейбір шекті модельдерде дұрыс. Егер тоқтамаса, ол барлық шекті модельдерде жалған. Демек, машина тоқтамайды, егер және тек егер арифметикалық сөйлем барлық шекті модельдерде дұрыс болса. Тоқтамайтын машиналар жиыны рекурсивті түрде тізімделмейді, сондықтан шекті модельдердегі жарамды сөйлемдер жиыны да рекурсивті түрде тізімделмейді.
This proof is taken from Chapter 10, section 4, 5 of Mathematical Logic by H. D. Ebbinghaus. As in the most common proof of Gödel's First Incompleteness Theorem through using the undecidability of the halting problem, for each Turing machine there is a corresponding arithmetical sentence , effectively derivable from , such that it is true if and only if halts on the empty tape. Intuitively, asserts "there exists a natural number that is the Gödel code for the computation record of on the empty tape that ends with halting". If the machine does halt in finite steps, then the complete computation record is also finite, then there is a finite initial segment of the natural numbers such that the arithmetical sentence is also true on this initial segment. Intuitively, this is because in this case, proving requires the arithmetic properties of only finitely many numbers. If the machine does not halt in finite steps, then is false in any finite model, since there's no finite computation record of that ends with halting. Thus, if halts, is true in some finite models. If does not halt, is false in all finite models. So, does not halt if and only if is true over all finite models. The set of machines that does not halt is not recursively enumerable, so the set of valid sentences over finite models is not recursively enumerable.