式〈項〉をギリシャ文字で書くとして
- α providing x:X, y:Y
のような形がproviding式。これは、
- within {x:X, y:Y} α
- assuming x:X, y:Y α
と同じだが、providing, justificatin は定義義務／証明義務が発生する。
providingで導入された宣言は、バックログ（未処理案件）と呼ぶことにする。バックログとコンテキスト／前提／環境は扱いが違う。コンテキスト／前提／環境は与えられるものだが、バックログは自分で解決する必要がある。
前提とバックログの違いはコミュニケーション的な違い。だが重要。
