Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2



страница2/5
Дата02.01.2013
Размер0.5 Mb.
ТипДокументы
1   2   3   4   5

Как построить вывод уже заданной формулы в NJ- исчислении?
Прежде еще раз обратимся к определению NJ-вывода и выделим в нем два важных утверждения:

  1. вывод начинается с допущений;

  2. конечная формула не зависит ни от каких допущений.


Что это означает в случае уже заданной формулы? Здесь возникает несколько вопросов.

  1. Как найти допущения, с которых начинается вывод заданной формулы?

  2. Как из этих допущений построить заданную формулу?

  3. Как отбрасываются эти допущения?

  4. Все ли допущения, используемые в выводе заданной формулы, входят в нее в качестве подформул?

  5. Если выявленные допущения не позволяют построить заданную формулу, является ли это достаточным и необходимым условием для утверждения о не выводимости заданной формулы?

  6. Что будет критерием для прекращения поиска вывода в случае не выводимости заданной формулы и возможно ли точно указать такой критерий?


Для того чтобы ответить на эти вопросы мы должны изучить фигуры заключения NJ-исчисления. Первое, на что нам следует обратить внимание - это на формальное различие в способах записи допущений для NJ-фигур заключений.

Заметим, что фигурам заключения , , и сопоставлены допущения, взятые в квадратные скобки, а другим фигурам нет. Подобное различие является формальным признаком деления фигур заключения на два вида, а именно:

  1. фигуры заключения, применение которых приводит к отбрасыванию допущений ( , , , );

  2. фигуры заключения, применение которых не приводит к отбрасыванию допущений (все другие фигуры).


Это различие и определяет способ поиска вывода в NJ-исчислении. Для того чтобы продемонстрировать это, мы должны указать еще и на различие между фигурами заключения первого вида. Рассмотрим их структуру.

Фигура заключения содержит три допущения: Аgif" name="object58" align=absmiddle width=17 height=18>В, А и В, но только А и В взяты в квадратные скобки, т.е. допущения А и В, в результате применения этой фигуры, отбрасываются, а допущение АВ не отбрасывается. В выводе этот факт записывается следующим образом:

.

Здесь видно, что вводимые допущения мы нумеруем со знаком "+", а отбрасываемые со знаком " - ". Заметим, что при построении конкретного вывода квадратные скобки не пишут.

Далее. Фигура заключения содержит два допущения: xFx и Fa, но только Fa взято в квадратные скобки, т.е. только Fa отбрасывается в результате применения данной фигуры. Этот факт мы записываем следующим образом:



Фигуры заключения и содержат по одному отбрасываемому допущению, и эти факты записываются так:

и
Итак, первое различие между фигурами: , и , состоит в том, что с помощью итеративного применения фигур заключения и мы можем отбросить все допущения, а с помощью фигур и все допущения отбросить нельзя.

Второе различие состоит в том, что в фигурах и допущение входит в нижнюю формулу в качестве подформулы, для фигур и это не имеет места.

***
Подведем некоторые предварительные итоги.

Фигуры заключения NJ-исчисления делятся на фигуры введения логических знаков и фигуры удаления логических знаков. Хотя структура фигур заключения и определение вывода являются достаточными условиями для построения вывода в NJ-исчислении, в учебных целях мы вводим расширенную классификацию фигур заключения удобную для определения пути поиска вывода. Мы разделяем их на:

1.1) содержащие допущения в качестве подформул нижней формулы: , , , , , ;

1.2) не содержащие допущения в качестве подформул нижней формулы: , , , , , , ;

2.1) отбрасывающие допущения: , , , ;

    1. не отбрасывающие допущения: , , ,, , , , ,;

3.1) отбрасывающие, при итеративном применении, все допущения: , ;

3.2) отбрасывающие не все допущения: , .
Заметим, что в этой классификации мы разделили фигуры на те, которые обладают некоторым свойством и те, которые этим же свойством не обладают. Всеми тремя свойствами обладают только две фигуры: , : они содержат допущения в качестве подформул; отбрасывают допущения; отбрасывают, при итеративном применении, все допущения.
Очевидно, что всякий NJ-вывод формул, не зависящих от допущений, обязательно содержит применение (возможно и неоднократное) или фигуры , или фигуры , или той и другой вместе.

Этот факт наводит на мысль о способе анализа заданных формул, вывод которых необходимо найти. Для демонстрации этого мы рассмотрим несколько примеров.

***

Итак, вернемся к формуле (p q) ((q  r)(p  r)). Предположим, что эта формула выводима в NJ. Следовательно, она является конечной формулой некоторого вывода. Запишем это следующим образом:

.
Здесь черта означает, что данная формула является нижней формулой некоторой фигуры заключения, выражение означает часть вывода, расположенного над данной H-формулой, т.е. формулой вместе с ее местом в выводе. Наша формула имеет вид АВ, где в качестве А выступает подформула (pq), а в качестве В - подформула ((qr)(pr)).

Тогда на предыдущем шаге вывод имел вид:

.

Далее. Формула (qr)(pr) имеет вид АВ, где А- это (qr), а В - это (pr).


И наконец, формула pr также имеет вид АВ, где А - это p, а В - это r . Тогда на предыдущем шаге вывод имел вид:


Рассмотрим получившийся вывод. Формула r не содержит логических знаков. Формулы pq, qr и p - это допущения, которые, начиная с формулы r, мы использовали в процессе построения конечной формулы, если смотреть сверху вниз.

Заметим, что формула r является своеобразной "границей", разделяющей вывод на две части:

  1. от допущений до формулы r ;

2) от формулы r до конечной формулы.

Как действовать дальше? Для этого поставим вопрос: можно ли, используя только эти допущения, получить формулу r?

Далее рассуждаем следующим образом, причем оценку вывода проводим сверху вниз. Искомая формула r входит в качестве подформулы в формулу q r . Мы могли бы "добраться " до r, с помощью фигуры , если бы вывод содержал формулу q. Тогда эту часть вывода можно было бы представить в виде:
.
Однако формулы q у нас еще нет. Тем не менее, у нас есть допущения pq и p, а это значит, что, применяя фигуру - , мы можем получить формулу q, а следовательно и формулу r. Эта часть вывода будет иметь вид:


Искомая формула r получена.

Суммируя вышесказанное, получаем вывод формулы (pq)((qr)(pr)).


***
Воспроизведем ход данного доказательства по шагам:

  1. Определяем главный знак заданной формулы и фигуру заключения, с помощью которой был введен данный знак.

  2. Находим первое допущение и нумеруем его.

  3. Определяем главный знак формулы, являющейся верхней формулой фигуры заключения, найденной согласно пункту 1, фигуру заключения, с помощью которой введен главный знак рассматриваемой формулы и второе допущение.

  4. Этот пункт аналогичен пункту 3.

  5. Находим формулу, не содержащую логического знака.

  6. Составляем список выявленных допущений.

  7. Из допущений, посредством фигур заключения NJ-исчисления, выводим формулу найденную согласно пункту 5.

  8. Записываем вывод в целом.


Данное описание можно рассматривать как частный случай стандартной процедуры определения выводимости NJ-формул. Оно не является полным и требует дальнейшего уточнения. Характер уточнений будет ясен из последующих примеров, но прежде сделаем предварительное замечание, опираясь на пример 2. Доказанная нами формула содержала только один вид логических знаков - импликацию, а "пограничная" формула оказалась элементарной, т.е. она не содержала никаких логических знаков. Однако в общем случае это не имеет места.

***
Продолжим рассмотрение примеров.
1   2   3   4   5

Похожие:

Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconКлассическое определение вероятности. Комбинаторные методы решения задач
Цель: выработать умение решать задачи на определение классической вероятности с использованием основных формул комбинаторики
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconПриме Например, представим систему, которая состоит из трех подсистем. Соответственно, и требования могут быть разбиты на три части. Это можно представить в виде дерева следующим образом
Извлекаемые из документации требования представляются в виде дерева требований. Каждый узел-родитель в этом дереве является обобщением,...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 icon2001 Дифференциальное исчисление функции одной переменной. Производная функции, ее геометрический и физический смысл. Определение
Определение. Производной функции f(x) в точке х = х0 называется предел отношения приращения функции в этой точке к приращению аргумента,...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconПринципиальная схема сеточного метода решения детерминированного эквивалента стохастической задачи управления портфелем финансовых инструментов
Х переменных в динамике. Ключевая идея состоит в генерировании множества сценариев реализации случайных параметров в виде дерева...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconОпределение и свойства предела последовательности. Определение
Определение: задать числовую последовательность – это значит сопоставить каждому номеру действительное число
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconРешение задач на вывод формул органических веществ. Алгоритм решения задач на вывод формул органических веществ
Обозначить формулу вещества с помощью индексов Х,у,z и т д по числу элементов в молекуле. Если продуктами горения являются со2 и...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconУрок по теме «Функция квадратного корня»
В последствии появилось определение функции, данное Эйлером 1751 год, затем — у Лакруа в 1806 году — уже практически в современном...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 iconА. Определение: множество неограниченно. Определение: последовательность удовлетворяет критерию Коши. Определение: последовательность не удовлетворяет критерию Коши. Определение точной верхней грани. Определение точной нижней грани

Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 icon«Определение степени с целым показателем»
Образовательная: дать определение дроби с целым показателем, научить представлять степень с целым отрицательным показателем в виде...
Исчисление nj. Определение nj — вывод состоит из формул, расположенных в виде дерева. Определение 2 icon§ Определение доказуемой (выводимой) формулы
Следующим этапом в построении исчисления высказываний является выделение класса доказуемых (выводимых) формул
Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org