Из приведённых выше определений существует уже по построению глубокое различие между концепциями доказательства и истинности. Эти понятия относятся к двум различным областям. Априорно ничто не гарантирует, что всякое утверждение, истинное в обычном смысле слова, соответствует какой-то доказуемой формуле. Ведь не только то истинно, для чего у нас есть доказательство!
На самом деле имеются четыре варианта взаимоотношений между доказательством и значением истинности, поскольку формула, с одной стороны, может быть теоремой либо не-теоремой, а с другой стороны, её интерпретация может быть истинной либо ложной.
Первый вариант, когда интерпретация истинна, не представляет проблемы. Если формула доказуема и соответствует определённой интерпретации, значение которой ложно, то такая интерпретация просто не представляет интереса. Вариант теорема «ложь» исключается из рассмотрения и может использоваться для определённой корректировки рассматриваемой формальной системы таким образом, чтобы с ней остались связанными только те интерпретации, которые истинны для всех теорем системы. Теперь рассмотрим варианты: не-теорема «истина», не-теорема «ложь». Что касается последнего, то весьма желательно, чтобы значение «ложь» было бы присвоено всем не-теоремам; однако это не всегда возможно. Тем не менее наиболее часто используемые формальные системы относятся именно к этому случаю, как, например, логика высказываний (которую называют также пропозициональной логикой или исчислением высказываний).
Наиболее сложным является вариант не-теорема «истина», когда не всегда можно избежать трудностей, заключающихся в том, что могут существовать не-теоремы данной формальной системы, которые в определённых интерпретациях являются истинными, причём такие интерпретации часто оставляются для рассмотрения. В качестве примера назовём знаменитое утверждение Ферма: «Для всякого целого n > 2, уравнение в целых числах xn+yn=zn не имеет решения ». Вполне возможно, что оно является истинным в обычной интерпретации, где используемые имеют обычный арифметический характер. Это утверждение проверено с помощью ЭВМ, на которой оно просчитано до значений n=10000. Однако остаётся возможность того, что оно не доказуемо в существующей арифметической аксиоматике. Ещё более неприятным является тот факт, что существуют формальные системы, в которых класс формул не-теорема «истина» не является пустым ни при какой интерпретации!
Сюда относится и проблема наличия ограничений формализмов. Одни из них связаны с формой представления (записи) интерпретации, в то время как другие ограничения от этого не зависят. Однако во всех случаях существует одна и та же проблема: исходя из аксиом и правил вывода, во-первых, как сделать хороший выбор исходных из них для быстрого получения доказательств конкретной формулы в качестве теоремы и, во-вторых, как доказать, что некая формула недоказуема в данной формальной системе? В общем случае проблема, поставленная таким образом, является неразрешимой.
Зная, что комбинаторные методы в нашем случае не эффективны, мы будем подходить к проблеме исследования формальных систем со строго формальной точки зрения, что позволит получить результаты, выявляющие формальные свойства формальных систем. В свою очередь это позволит значительно усовершенствовать и сами комбинаторные методы. Например, если в данной формальной системе не употребляется какая-то константа (например, A) ни в аксиомах, ни в правилах вывода, то она не может появиться и ни в одной теореме.
Другим подробным примером является следующий: если никакое правило вывода данной системы не порождает формулы, более длинной (т.е. содержащей большее число символов), чем теорема, к которой оно применяется, то всякая теорема большего размера, чем аксиома, может быть удалена из рассмотрения. В этом случае всегда можно получить результат за конечное число шагов, так как дерево поиска уменьшено в этом случае до конечной величины ≤Ln , где L – число символов в алфавите, а n – длина доказываемой формулы.
Именно такой подход позволил трём великим математикам Черчу, Геделю и Тарскому получить к 1930 г. весьма общие результаты, относящиеся к формальным системам и называемые теоремами ограничения.