前提という概念

前提（premise; プレミス）は次のもの達の総称する。

1. 公理（axiom）
2. 定理（theorem）
3. 仮説（hypothesis, 複数形 -ses）
4. 仮定（assumption）

公理と定理はどちらも論理式またはシーケントで、表現形式上の差はなくて（Mizarでは公理と定理の区別はない）、定理が証明により正当化されているだけ。公理は天下りに正当化される。

仮説は公理と扱いは同じなので、同義語と思ってもよい。違いは、仮説は同じスコープ内で後から証明されてもよい。公理は証明を受け付けない。

仮定は証明スコープ内で導入される。同じスコープ内で、含意導入によりドロップされなくてはならない。何度ドロップされてもよい（複数回利用可能）が、仮定が残るのは許されない。

公理、定理、仮説、、仮定のいずれも証明中に使ってよいので、まとめて前提と呼ぶ。