[Agda] Why no impredicative prop?

[Bas Spitters]

You seem to be identifying "intuitionistic" (in the sense of Brouwer
and Heyting) with type theoretic meaning explanations (Martin-L"of,
Dybjer, ...).
They are not exactly the same.

Some constructive mathematicians (e.g. Richman, Bridges) are
comfortable with the power sets. There are some overview articles
here:
http://plato.stanford.edu/entries/set-theory-constructive/#PreConSetThe
http://plato.stanford.edu/entries/philosophy-mathematics/index.html#Pre

Best wishes,

Bas

On Wed, Dec 30, 2015 at 7:22 PM, Jon Sterling <jon at jonmsterling.com> wrote:
> Harley,
>
> System F is only "intuitionistic" in the formal sense (i.e. the sense of
> "intuitionistic logic" as lacking classical axioms). It is not
> intuitionistic in the sense of Brouwer or Heyting, i.e. there is not a
> convincing meaning explanation that would validate impredicative
> principles.
>
> Best,
> Jon
>
>
> On Wed, Dec 30, 2015, at 06:34 AM, Harley Eades III wrote:
>> Hi, Thorsten.
>>
>> > On Dec 29, 2015, at 5:11 PM, Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>> >
>> > More on the philosphical side: impredicativity is basically a classical idea which arises from the identification of Prop and Bool. I don’t know an intuitionistic justification of impredicativity.
>>
>> I am not sure I understand what this means.  Do you have a reference
>> regarding this?  System F is intuitionistic, but doesn’t this claim it
>> isn’t?
>>
>> Very best,
>> Harley
>>
>> >
>> > Thorsten
>> >
>> > From: <agda-bounces at lists.chalmers.se <mailto:agda-bounces at lists.chalmers.se>> on behalf of Timothy Carstens <intoverflow at gmail.com <mailto:intoverflow at gmail.com>>
>> > Date: Tuesday, 29 December 2015 17:19
>> > To: "agda at lists.chalmers.se <mailto:agda at lists.chalmers.se>" <agda at lists.chalmers.se <mailto:agda at lists.chalmers.se>>
>> > Subject: [Agda] Why no impredicative prop?
>> >
>> > Hello,
>> >
>> > I'm a relatively new Agda user, coming from a background using Coq for the past few years. As is well known, Coq has an impredicative Prop sort, while Agda does not.
>> >
>> > Why not? Is it simply a matter of project goals, or is there something about Agda's underlying theory which is incompatible with having an impredicative sort at the bottom of the universe hierarchy?
>> >
>> > Forgive me if this is an old topic or has an obvious answer; I'm not a logician, but I use proof assistants at work.
>> > -t
>> >
>> >
>> >
>> > This message and any attachment are intended solely for the addressee
>> > and may contain confidential information. If you have received this
>> > message in error, please send it back to me, and immediately delete it.
>> >
>> > Please do not use, copy or disclose the information contained in this
>> > message or in any attachment.  Any views or opinions expressed by the
>> > author of this email do not necessarily reflect the views of the
>> > University of Nottingham.
>> >
>> > This message has been checked for viruses but the contents of an
>> > attachment may still contain software viruses which could damage your
>> > computer system, you are advised to perform your own checks. Email
>> > communications with the University of Nottingham may be monitored as
>> > permitted by UK legislation.
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda