Алгоритмическая разрешимость — свойство формальной теории обладать алгоритмом, определяющим по данной формуле, выводима она из множества аксиом данной теории или нет. Теория называется разрешимой, если такой алгоритм существует, и неразрешимой, в противном случае. Вопрос о выводимости в формальной теории является частным, но вместе с тем важнейшим случаем более общей проблемы разрешимости.
Понятия алгоритма и аксиоматической системы имеют давнюю историю. И то и другое известно ещё со времён античности. Достаточно вспомнить постулаты геометрии Евклида и алгоритм нахождения наибольшего общего делителя того же Евклида. Несмотря на это, чёткого математического определения исчисления и особенно алгоритма не существовало очень долгое время. Особенность проблемы, связанной с формальным определением неразрешимости состояла в том, что для того, чтобы показать, что некоторый алгоритм существует, достаточно его просто найти и продемонстрировать. Если же алгоритм не находится, возможно его не существует и это тогда требуется строго доказать. А для этого нужно точно знать, что такое алгоритм.
Большой прогресс в формализации этих понятий был достигнут в начале XX века Гильбертом и его школой. Тогда, сначала, сформировались понятия исчисления и формального вывода, а затем Гильбертом же, в его знаменитой программе обоснования математики была поставлена амбициозная цель формализации всей математики. Программа предусматривала, в том числе, возможность автоматической проверки любой математической формулы на предмет истинности. Отталкиваясь от работ Гильберта Гёдель впервые описал класс так называемых рекурсивных функций, с помощью которой доказал свои знаменитые теоремы о неполноте. Впоследствии был введён ряд других формализмов, таких как машина Тьюринга, λ-исчисление, оказавшихся эквивалентными рекурсивным функциям. В настоящее время каждый из них считается формальным эквивалентом интуитивного понятия вычислимой функции. Эта эквивалентность постулируется тезисом Чёрча.
Когда понятия исчисления и алгоритма были уточнены, последовал ряд результатов о неразрешимости различных теорий. Одним из первых таких результатов была теорема, доказанная Новиковым, о неразрешимости проблемы слов в группах. Разрешимые же теории были известны задолго до этого.
Интуитивно понятно, что чем сложнее и выразительнее теория, тем больше шансов, что она окажется неразрешимой. Поэтому, грубо говоря, «неразрешимая теория» — «сложная теория».