15 Oct
2010
15 Oct
'10
5:16 p.m.
On Oct 15, 2010, at 1:36 PM, Andrew Coppin wrote:
Does anybody have any idea which particular dialect of pure math this paper is speaking? (And where I can go read about it...)
It's some kind of typed logic with lambda abstraction and some notion of witnessing, using Gertzen (I think!) style derivation notation. Those A |- B things mean A "derives" B. The "|-" is also called a Tee. If your mail client can see underlining, formulas like A, B | A mean: A, B |- A That's where the Tee gets its name. It's a T under A, B. The former notation is better for some uses, since it "meshes" with the method of "truth trees".