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) является теоремой (осуществить доказательство), мы получим следующую, уже имеющую исключённые формулы последовательность: