V Пример. Если требуется вывести формулу Øp из посылок pÉØpи p(записывается: pÉØp,p |- Øp

Если требуется вывести формулу Øp из посылок pÉØpи p(записывается: pÉØp,p |- Øp, читается: «из посылок pÉØp и p выводимо Øp», где « |-» — знак выводимости), то следует найти и записать такую последовательность формул, в которой множество используемых посылок равно множеству формул pÉØpиp, а последней оказывается именно выводимая формула Øp:

1. pÉØp — пос.

2. p — пос.

3. Øp — Éи, 1, 2.

 

Как видно из предложенной записи данной последовательности, напротив каждой формулы указывается основание, по которому она используется в выводе. Первым из двух возможных оснований вывода является то, что данная конкретная формула служит посылкой (соответствующее обозначение — «пос.»). Второе основание заключается в том, что данная конкретная формула получена из предыдущих формул по некоторому правилу вывода (что фиксируется символом применённого правила вывода и номерами формул, к которым оно было применено). Исключённые формулы вывода на каждом его шаге принято обозначать вертикальной чертой, расположенной слева от колонки пронумерованных формул. В приведённом выше примере вывода нет исключённых формул, но если потребуется обосновать утверждение о выводимости |- (p É Øp) É Øp, т. е. обосновать утверждение о том, что формула ((p É Øp) É Øp) является теоремой (осуществить доказательство), мы получим следующую, уже имеющую исключённые формулы последовательность:

_______ ______________ 1. p É Øp — пос. 2. p — пос. 3. Øp — Éи, 1, 2. 4. Øp — Øв, 2, 3. 5. (p É Øp) É Øp — Éи, 1.

 








Дата добавления: 2015-09-07; просмотров: 950;


Поиск по сайту:

При помощи поиска вы сможете найти нужную вам информацию.

Поделитесь с друзьями:

Если вам перенёс пользу информационный материал, или помог в учебе – поделитесь этим сайтом с друзьями и знакомыми.
helpiks.org - Хелпикс.Орг - 2014-2024 год. Материал сайта представляется для ознакомительного и учебного использования. | Поддержка
Генерация страницы за: 0.003 сек.