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; просмотров: 958;