14/04/14 20:21:27.10
このパズルみたいな簡単な不変量じゃないし
厳密にいえば不変量でもないけど、
subformula propertyとかcut除去とかは式の複雑さが
単調に増加していくということだから、似た空気ではあるよね。
逆に順序数の単調減少な量を定義するというのもよくあるテクニック。
ただ証明論についてあまり詳しくないから
「同じような議論」とまで言えるかどうかは分からんけど。
14/04/14 20:21:27.10
このパズルみたいな簡単な不変量じゃないし
厳密にいえば不変量でもないけど、
subformula propertyとかcut除去とかは式の複雑さが
単調に増加していくということだから、似た空気ではあるよね。
逆に順序数の単調減少な量を定義するというのもよくあるテクニック。
ただ証明論についてあまり詳しくないから
「同じような議論」とまで言えるかどうかは分からんけど。