Cтраница 2
При построении формальной системы мы дали выводам простейшую возможную структуру-каждый вывод состоит из единичной последовательности формул. [16]
Сколем ( 1920) обобщил эту теорему для случая, когда вместо одной формулы речь идет о счетно-бесконечной последовательности формул, а сов. [17]
Для каждого случая мы покажем, как построить результирующий вывод, предоставляя читателю проверить, что предлагаемая в качестве такового последовательность формул имеет требуемый вид. [18]
В работе [31] дана предварительная оценка степени применимости и трудоемкости метода Брауна для расчета потоко-распределения в ГЦ с использованием систем контурных уравнений и упорядочена последовательность формул для преобразования коэффициентов в уравнениях. Разумеется, целесообразность практического использования метода Брауна еще должна быть подтверждена вычислительными экспериментами для расчета различных ГЦ, однако уже можно сделать вывод о перспективности метода. [19]
Над исходными формулами в фигуре разложения не стоят никакие другие формулы; над результирующей формулой любой схемы заключения стоят две формулы ( здесь имеет место ветвление вверх); над любой другой формулой стоит по одной формуле. Последовательность формул из данной фигуры разложения, начинающаяся какой-либо исходной формулой и такая, что за каждой формулой, не являющейся заключительной формулой вывода, следует формула, стоящая в этой фигуре непосредственно под ней, называется нитью доказательства. [20]
Для всех величин, используемых в программе, выбирают идентификаторы. Последовательность формул алгоритма записывают в виде соответствующей последовательности операторов. [21]
При формальном описании теории задается ее язык ( правила построения выражений разл. Доказательство есть последовательность формул, каждая из которых либо является аксиомой, либо получается из предыдущих по одному из правил вывода. А, либо А, либо отрицание А является теоремой. При построении формальных теорий вопрос о непротиворечивости является ключевым. Для установления непротиворечивости обычно используется метод интерпретаций. При семантической интерпретации строится модель теории: теоремы превращаются в истинные содержательные утверждения об объектах некоторого универсума. Если теория имеет модель, то она непротиворечива. Путем интерпретации доказательство непротиворечивости евклидовой геометрии сводится к доказательству непротиворечивости теории действительных чисел, а доказательство непротиворечивости геометрии Лобачевского - к доказательству непротиворечивости евклидовой геометрии. [22]
Результирующий вывод есть последовательность формул ( 1), приведенная в примере 2 § 19 в качестве доказательства А А. Так как В есть А, то формула А А есть А В. [23]
Таким образом, последовательность формул, в которую переходит данный вывод, является снова выводом с тем же самым анализом. [24]
Примеры комплексов приведены в гл. В частном случае последовательность формул в комплексе может сводиться к одной формуле или даже быть пустой. [25]
Последовательность формул (1.18) после замены в ней символов xitj конкретными названиями ячеек определяет некоторую последовательность локальных операций над словом W, в результате последовательного выполнения которых слово W оказывается преобразованным в новое слово W. Некоторые из символов xitj в последовательности формул (1.18) могут обозначать произвольные ячейки, другие - вполне определенные ячейки. [26]
Пусть Г - произвольное ( возможно, бесконечное) множество формул сигнатуры и. Выводом из Г называется такая последовательность формул BI... [27]
В такой формальной аксиоматической теории оказывается эффективным и понятие доказательства; иными словами, в такой теории имеется эффективная пррцедура, позволяющая для произвольной конечной последовательности формул решить, является ли она доказательством. Но если нам уже предъявлена некоторая последовательность формул, являющаяся по предположению доказательством, то эта эффективная процедура позволяет подтвердить ( или отклонить) это предположение. [28]
При выполнении схемы можно каждый раз, когда выполняется действующий оператор, выписывать нормальную последовательность его комплекса. При этом после выполнения схемы будет получена некоторая последовательность формул. Выберем все состояния g ( x) кортежа X, входящие в область задания схемы ( обозначим их совокупность через GJ), которые перерабатываются в состояния одного и того же кортежа Y и приводят к получению одной и той же последовательности формул. [29]
При выполнении схемы можно каждый раз, когда выполняется действующий оператор, выписывать нормальную последовательность его комплекса. При этом после выполнения схемы будет получена некоторая последовательность формул. Выберем все состояния g ( x) кортежа X, входящие в область задания схемы ( обозначим их совокупность через G), которые перерабатываются в состояния одного и того же кортежа Y и приводят к получению одной и той же последовательности формул. [30]