Мы будем говорить, что некоторая формула ДС "доказуема" или "выводима", если мы ее доказали или
знаем, как построить ее доказательство (знаем набор строгих правил, по котороым строится такое
доказательство). Символически факт доказуемости некоторой формулы X
будем обозначать так:
X (1)
Так же будем обозначать само доказательство формулы X, то есть,
формула (1) обозначает текст, состоящий из последовательности дедуктивных шагов.
Экспериментируя с доказательствами, можно обнаружить разные полезные приемы, которые действуют
более-менее одинаково для самых разных формул. Допустим, мы обнаружили, что, имея на руках
какую-нибудь доказанную формулу X и любую, даже недоказанную формулу
Y, можно доказать в несколько шагов формулу Y 
X.
Этот факт будет полезен сам по себе для поиска доказательств, даже если мы сейчас
не рассматриваем никаких конкретных X и Y.
Запись:
G1, G2,... GN X (2)
- будет означать, что, имея доказанные (в любом порядке)
формулы G1, G2,... GN,
можно доказать формулу X. Запись читается:
"X доказуема на основании G1, G2,... GN" или
"X выводима из G1, G2,... GN".
Так же будем обозначать само доказательство формулы X, на
основании гипотез. То есть, формула (2) обозначает текст, состоящий из
последовательности дедуктивных шагов. Если выписать доказательства гипотез,
и к ним добавить этот текст, то в сумме получится доказательство формулы X.
Формулы G1, G2,... GN называются "гипотезами" в том смысле,
что они могут быть не доказаны, но если вдруг мы сможем их доказать, то мы знаем,
какие еще шаги дедукции надо сделать, чтобы доказать X.
X будем называть "выводом" (доказательства). Вывод не
обязательно будет теоремой или аксиомой, ведь возможно, что гипотезы никогда
не удастся доказать.
Предполагается, что гипотезы перечисляются через запятую в произвольном порядке и могут
быть в любой момент переставлены местами. Поэтому доказательство любого утверждения,
вида (2) не должно строить каких-либо предположений о порядке доказательства гипотез.
В частном случае, когда формула X доказывается без привлечения
каких-либо гипотез, N = 0 и из формулы (2) получается формула (1).
Заметим: обе формулы (1) и (2) принадлежат к метаязыку.