Метасимволика и.В. И и.П.

Г- множество посылок (гипотез). Обычно Г записывают в виде Г=А₁, А₂,…, А_n (Г читается как “гамма”)

Ф – теорема; А_i – метаформула; R(J) – множество правил вывода в исчислении;

| - символ отношения дедуктивного вывода.

Пример. Запись Г|Ф ( из гипотез Г дедуктивно выводима формула Ф) означает А₁, А₂,…, А_n |Ф, или А₁, А₂,…, А_n

Ф

Пример. Запись |А означает, что А доказуема.

Пример. Запись А₁, А₂,…, А_n | означает, что множество посылок противоречива.

Пример. |=, ₁ |= ₂, ₁ | ₂ – метавысказывания.

Замечание. Специфика отношений |= и | в том, что в отличие от логических связок (отношений отрицания, конъюнкции, дизъюнкции) они реализуются не на денотатах высказываний, а на пропозициональных формулах.