Cтраница 2
Новикова, можно сказать, что чистое доказательство алгоритмической разрешимости некоторого класса задач означает не более того, что невозможно доказать алгоритмическую неразрешимость для этого класса. [16]
Важным является § 3, в котором доказательство разрешимости задачи ( 1), ( 2), ( 3) сводится к доказательству двух энергетических оценок, названных основной и дуальной онснкнмн В § 4 собран вспомогательный материал о псевдодифферснциальпых операторнх и формулах Грина, используемый при выводе энергетических оценок. В § 5 проводится локализация и микролокалилшин основного результата и рассмотрена оценка в более простой зоне, названной ними параболической. В § 7 результаты § § 5, 6 переносятся на зпдпчи с тряпичными условиями более общего вида, что позволяет доказать дуальную оценку. [17]
Итак, доказательство теоремы ( ТВ) завершено. Теперь легко показать, что эта теорема влечет за собой доказательство разрешимости для С-ЛЛсистемы теории дедукции. Если - все элементарные выражения, к которым было сведено данное выражение а, истинны, то есть если они имеют среди своих антецедентов два выражения типа р и Np, то IB таком случае а является положением, которое должно быть принято. С другой стороны, если среди элементарных выражений, к которым было сведено а, существует ino крайней мере одно такое выражение, что никаких два его антецедента не есть типа р и Np, то тогда а должно быть отброшено. [18]
Вопрос о разрешимости теорий не принадлежит к числу рассматриваемых в этой книге, поскольку им обычно в теории моделей не занимаются. Однако это очень важный вопрос, и на самом деле наиболее замечательные приложения метода элиминации кванторов заключаются как раз в доказательстве разрешимости некоторых теорий. Этот метод оказывается важным и как источник до конца понятных теорий, полезных при проверке гипотез и для иллюстрации результатов. [19]
Настоящий параграф в каком-то смысле параллелен § 3 из предыдущей глапы. Там мы редуцировали вопрос о разрешимости задачи Коши с нулевыми начальными данными при t - О к доказательству двух энергетических оценок для исходного и формально сопряженного операторов. Доказательство разрешимости проводилось н лни тапа. [20]
Этапами ее построения были: введение Петровским в 30-с годы класса гиперболических уравнений высокого порядка ( систем), обобщающего волновое уравнение, исследование Петровским и Лере задачи Коши для гиперболических уравнений произвольного порядка с переменными коэффициентами, и, наконец, занявшее не одно десятилетие изучение смешанной задачи для гиперболических уравнений произвольного порядка ( систем первого порядка), которое было завершено Агмоном, Крайсом и Сакамото. По нашему мнению, наиболее адекватным подходом к доказательству разрешимости гиперболических задач является метод, использующий разделяющий оператор и связанную с ним дефинитную квадратичную форму. Указанный метод был предложен в начале 50 - х годов Лере, который, отталкиваясь от закона сохранения энергии для для мембраны ( ее движение описывается волновым уравнением), нвел энергетические квадратичные формы для гиперболических уравнений высокого порядка с переменными коэффициентами. [21]
Проблема достижимости является центральной в специальной теории сетей Петри, так как многие другие проблемы эквивалентны ей в том смысле, что их разрешимость или неразрешимость непосредственно следует из разрешимости или неразрешимости проблемы достижимости. Неоднократные попытки доказать общепринятую гипотезу о разрешимости последней, в том числе опубликованные, страдали одним общим недостатком - в доказательствах были обнаружены ошибки. Последней работой в этом ряду является статья Майра [63], в которой приведено очередное доказательство разрешимости проблемы достижимости. [22]
При установлении такой оценки ( 8) мы разбиваем те методы. Справедливость указанной щенки вида ( 8) позволяет доказать существование решений задач Дирихле-для регуляризованных уравнений ( см. (6.2.21)) и осуществить предельный переход в интегральных тождествах, соответствующих таким задачам. Следует заметить, что на одном из этапов доказательства последних теорем полезную роль играет одна специальная срезающая функция, аналогичная той, которая была использована в работе [117], посвященной доказательству разрешимости первой краевой задачи для линейного вырождающегося эллиптического уравнения. [23]
Известно [25, 57, 197], что для среды с поглощением ( Im е 0) условия 1 - 5 обеспечивают единственность решения исходной электродинамической задачи. Оно заключается в требовании конечности энергии электромагнитного поля, запасенной в любом конечном объеме. Если искомое поле представлено в виде Фурье, то это условие определяет пространство числовых последовательностей, которому должны принадлежать неизвестные амплитудные коэффициенты. В таком виде это условие удобно использовать при доказательстве разрешимости полученных тем или иным путем бесконечных систем уравнений относительно этих коэффициентов. Последнее обычно применяют при рассмотрении различных математических особенностей полученного решения и анализа рассеянного поля вблизи ребер структуры. [24]
В систематической части я пытался объяснить некоторые теории современной формальной логики, которые необходимы для понимания силлогистики Аристотеля, и пытался пополнить эту силлогистику в пределах, установленных самим Аристотелем. Я стремился быть ясным, насколько это возможно, так чтобы мое изложение могло быть понято учащимися, не тренированными в области символического или математического мышления. Поэтому я надеюсь, что эта часть моей работы сможет быть использована как введение в современную формальную логику. Наиболее важными новыми результатами, содержащимися в этой части, я считаю доказательство разрешимости, данное моим учеником Я. [25]
Все известные положения силлогистики являются либо элементарными выражениями, либо выражениями, которые легко могут быть преобразованы в элементарные. Законы обращения, то есть Clablba или САаЫЬа, - это элементарные выражения. Все силлогизмы имеют форму С / Софт, а выражения этого вида дедуктивно эквивалентны элементарным выражениям формы СосОД относительно законов экспортации и импортации. Однако имеются другие осмысленные выражения силлогистики - некоторые из них истинные, не которые ложные, - которые не являются элементарными. Существует, разумеется, бесконечное множество таких выражений, и все они должны быть приняты во внимание при доказательстве разрешимости. [26]
Этот метод применим только к теориям очень специального вида. Более того, всякий раз, когда этот метод применяется к новой теории, приходится проводить доказательства с самого начала, так как для использования общих теорем о моделях здесь представляется мало возможностей. С другой стороны, этот метод оказывается чрезвычайно ценным, если мы хотим как следует разобраться в некоторой конкретной теории. В тех случаях, когда его удается применить, метод элиминации кванторов дает огромное количество информации о рассматриваемой теории. Так, он дает сведения о поведении всех формул, равно как и всех предложений соответствующего языка, по отношению к этой теории. Обычно он приводит также к регулярному способу, позволяющему решать, принадлежит ли некоторое высказывание нашей теории - иными словами, он дает доказательство разрешимости теории. [27]