[Agda] Re: Classical Mathematics for a Constructive World

[Ramana Kumar]

The * is not just conjunction, it is separating conjunction.
Maybe you know that already, but just to make sure, the semantics of P * R
is
(P * R)(x,h) = exists h1. exists h2. h = h1 + h2 & P(x,h1) & R(x,h2)
where + is disjoint union.
The choice issue is that the h2 for R on the Q * R side doesn't have to be
the same.


On Sun, Dec 2, 2012 at 10:41 AM, Jan Burse <janburse at fastmail.fm> wrote:

> 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
>
>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121202/9ab99486/attachment.html