Разрешима теория е

Понятията алгоритъм и аксиоматична система имат дълга история. И двете са известни от древността. Достатъчно е да си припомним постулатите на геометрията на Евклид и алгоритъма за намиране на най-големия общ делител на същия Евклид. Въпреки това, ясна математическа дефиниция на смятането и особено на алгоритъма не съществуваше много дълго време. Особеността на проблема, свързан с формалната дефиниция на неразрешимостта, беше, че за да се покаже, че някакъв алгоритъм съществува, е достатъчно просто да се намери и демонстрира. Ако алгоритъмът не бъде намерен, възможно е той да не съществува и тогава това трябва да бъде строго доказано. А за това трябва да знаете точно какво е алгоритъм.

Голям напредък във формализирането на тези концепции беше постигнат в началото на 20 век от Хилберт и неговата школа. Тогава, първо, се формират концепциите за смятане и формално извеждане, а след това Хилберт, в своята известна програма за обосноваване на математиката, поставя амбициозната цел да формализира цялата математика. Това включва, наред с други неща, възможността за автоматична проверка на всяка математическа формула за истинност. Въз основа на работата на Хилберт, Гьодел за първи път описва клас от така наречените рекурсивни функции, с които доказва своите известни теореми за непълнотата. Впоследствие бяха въведени редица други формализми, като машината на Тюринг, λ-изчисление, което се оказа еквивалентно на рекурсивни функции. В момента всеки от тях се счита за формален еквивалент на интуитивното понятие за изчислима функция. Тази еквивалентност се постулира от тезата на Чърч.

Когато концепциите за смятане и алгоритъм бяха усъвършенствани, последваха поредица от резултати относно неразрешимостта на различни теории. Един от първите такива резултати беше теоремата, доказана от Новиков,относно неразрешимостта на проблема с думите в групи. Разрешимите теории са били известни много преди това.

Интуитивно, колкото по-сложна и изразителна е теорията, толкова по-голям е шансът тя да се окаже неразрешима. Следователно, грубо казано, "неразрешима теория" е синоним на "сложна теория".

Главна информация

Формалното смятане в общия случай трябва да дефинира езика, правилата за конструиране на термини и формули, аксиоми и правила за извод. По този начин за всяка теоремаTвинаги е възможно да се конструира веригаA1,A2, …,An=T, където всяка формулаAiе или аксиома, или изведена от предишните формули, съгласно едно от правилата за извод. Разрешимостта означава, че има алгоритъм, който за всяко добре оформено изречениеTдава недвусмислен отговор за крайно време: да, това изречение е изведено в рамките на изчислението или не, не е изведено.

Очевидно е, че противоречивата теория е разрешима, тъй като всяка формула ще бъде изведена. От друга страна, ако едно смятане няма рекурсивно изброим набор от аксиоми, като логика от втори ред, то очевидно не може да бъде решимо.

Примери за разрешими теории

Примери за неразрешими теории

Полурешимост и автоматично доказване

Разрешимостта е много силно свойство и повечето полезни и практически теории не го притежават. В това отношение беше въведена по-слаба концепция заполуразрешимост. Полуразрешим означава наличието на алгоритъм, който винаги ще потвърди за крайно време, че изречението е вярно, ако е вярно, но ако не е, то може да работи за неопределено време.

Изискването за полуразрешимост е еквивалентно на способността за ефективно изброяване на всички теореми на дадена теория. С други думи,наборът от теореми трябва да бъде рекурсивно изброим. Такава процедура за логика от първи ред е описана от Хилберт. Всъщност една теория ще бъде полуразрешима, ако множеството от нейните аксиоми и правила за извод са рекурсивни изброими множества. Повечето от теориите, използвани в практиката, отговарят на това изискване.

Ефективните полуразрешителни процедури за логика от първи ред са от голямо практическо значение, тъй като позволяват (полу)автоматично да се доказват формализирани твърдения от много широк клас. Пробив в тази област е откритието на Робинсън през 1965 г.на разделителния метод. Другият най-важен полуразрешителен алгоритъм днес етаблото с резултати.

Връзка между разрешимост и пълнота

В математическата логика традиционно се използват две концепции за пълнота: истинска пълнота и пълнота, свързана с някакъв клас интерпретации (или структури). В първия случай една теория е пълна, ако всяко изречение в нея е вярно или невярно. Във втория случай, ако всяко изречение, което е вярно при всички интерпретации от този клас, е изведено. Например естествената аритметика е непълна според теоремите за непълнота на Гьодел, но е пълна по отношение на нейната стандартна интерпретация - това следва от теоремата за пълнота на Гьодел.

И двете понятия са тясно свързани с решимостта. Например, ако наборът от аксиоми на пълна теория от първи ред е рекурсивно изброим, тогава той е разрешим. Това следва от добре известната теорема на Пост, която гласи, че ако едно множество и неговото допълнение са рекурсивно изброими, тогава те също са рекурсивни. Интуитивно, аргументът, показващ истинността на горното твърдение, е следният: ако теорията е пълна и наборът от нейните аксиоми е рекурсивно изброим, тогава има полуразрешаващи процедури запроверка на истинността на всяко твърдение, както и неговото отричане. Ако и двете от тези процедури се изпълняват паралелно, тогава, като се има предвид пълнотата на теорията, една от тях трябва някой ден да спре и да даде положителен отговор.

Ако теорията е пълна по отношение на някакъв клас интерпретации, това може да се използва за конструиране на процедура за вземане на решение. Например пропозиционалната логика е пълна по отношение на интерпретацията на таблиците на истината. Следователно, изграждането на таблица на истината съгласно тази формула ще бъде пример за разрешаващ алгоритъм за пропозиционална логика.

Литература

• Малцев А.И.,Алгоритми и рекурсивни функции, Наука, 1986.
• Акерман В.,Разрешими случаи на проблема с решението, North-Holland Publishing, Амстердам, 1954 г.
• Джон Алън Робинсън, Андрей Воронков (ред.):Наръчник за автоматизирано разсъждение(в 2 тома). Elsevier и MIT Press 2001, ISBN 0-444-50813-9, ISBN 0-262-18223-8

Фондация Уикимедия. 2010 г.

Вижте какво е "Разрешима теория" в други речници:

разрешима теория — теория, за която има ефективна процедура (алгоритъм), която позволява на всяко твърдение, формулирано по отношение на тази теория, да реши дали е изведено в теорията или не (вижте: Проблем с разрешението). R. t. са например елементарни ... ... Речник на термините на логиката

Теорията на Галоа е клон на алгебрата, който изучава симетриите на корените на полиноми. Симетриите се описват от гледна точка на пермутационната група от полиномни корени (група на уравнение), термин, използван за първи път от Еварист Галоа. Съдържание 1 Приложение към класически задачи ... Wikipedia

РАЗРЕШИМА ГРУПА е група, която има краен субнормален ред с абелеви фактори (вижте Серия от подгрупи). Тя също притежаванормални редове с абелеви фактори (такива редове се наричат ​​разрешими редове). Дължината на най-късата разрешима серия от група се нарича. дължината му и n ... ... Математическа енциклопедия

Разрешима група — В алгебрата една група се нарича разрешима, ако съдържа верига от вложени комутатори, последният от които се състои от неутрален елемент. Веригата от комутатори се дефинира по следния начин: това е самата група a, тоест това е комутаторът на предишния ... Wikipedia

ТЕОРИЯТА НА КОНСТРУКТИВНИТЕ МОДЕЛИ е един от клоновете на математиката, възникнал на границата на моделите на теорията, алгебрата и теорията на рекурсивните функции и е свързан с изучаването на проблемите на ефективността в моделите и алгебрите. Статията на A. I. Maltsev Constructive Algebras [1] беше първото проучване ... ... Математическа енциклопедия

LI РАЗРЕШИМА ГРУПА е група на Лъжа, разрешима като абстрактна група. По-нататък разглеждаме реални или комплексни Lie r. г. Нилпотентна, в частност абелева група на Лие е разрешима. Ако F = пълен флаг в крайномерно векторно пространство V (над или), ... ... Математическа енциклопедия

LI РАЗРЕШИМА АЛГЕБРА е алгебра на Лие над поле K, което удовлетворява едно от следните еквивалентни условия: 1) членовете на производната поредица за са равни за достатъчно голямо k; 2). има крайна намаляваща верига от алгебрични идеали, така че и (т.е. алгебрите на Ли са абелеви) ... Encyclopedia of Mathematics

ТЕОРИЯ НА ГАЛОА - в най-общ смисъл, теория, която изучава определена математика. обекти въз основа на техните автоморфни групи. Така например са възможни разнородни т. полета, пръстени и топологични структури. пространства и т. н. В по-тесен смисъл G. T. се разбира като G. T. полета. Имаше тази ... Енциклопедия по математика

ЛОКАЛНО РАЗРЕШИМА ГРУПА е група, в която всяка е крайно генериранаподгрупата е разрешима (виж Разрешима група). Клас L. r. d. е затворен при вземане на подгрупи и хомоморфни изображения, но не е затворен при разширения. Периодични L. r. g. е локално краен. Лит ... Енциклопедия по математика

ОБОБЩЕНА РАЗРЕШИМА ГРУПА е група от един от обобщените разрешими класове групи. Класът от групи, наречен. обобщено разрешима, ако съдържа всички разрешими групи и пресича класа на крайните групи в класа на всички крайни разрешими групи. Беше разгледано доста ... ... Математическа енциклопедия

---