[Agda] Re: Classical Mathematics for a Constructive World
Jan Burse
janburse at fastmail.fm
Sun Dec 2 11:41:44 CET 2012
Jan Burse schrieb:
>
> Or what would be the mild condition on R
> to make the inference rule meaningful?
Ramana Kumar just wrote me:
> The condition is that R does not mention any
> variables assigned in C.
Then I also wonder how this is related to choice
principles. I see that it is related to variable
occurence rules. So if I desugar the following:
{ P } C { Q }
I get:
P(x,z) -> forall y (C(x,y) -> Q(y,z))
Question is now whether this implies:
P(x,z)&R(z) -> forall y(C(x,y) -> Q(y,z)&R(z))
I guess the answer is affirmative already in
minimal logic. But I might be also wrong here.
Bye
More information about the Agda
mailing list