9 Nov
2008
9 Nov
'08
6:04 p.m.
Thank you, everyone. You have addressed my concerns very accurately.
So in short, higer rank types subsume existentials. Good. And the burden
of emulating existentials can be lowered by a suitable macro system.
Very good.
2008/11/9 Derek Elkins
There are various rules for moving quantifiers around. Any text on intuitionistic predicate logic should list the rules.
Err, where can I find such texts? I don't even understand "intuitionistic predicate logic" :-( Cheers, Loup