[Agda] Why no impredicative prop?

[Bas Spitters]

Hi Jon,

Thanks.

Do you have a reference to the meaning explanations for CTT, and
specifically, a discussion on why it is intuitionistic?

Some formal systems for intuitionism restrict exponentation. It can be
claimed that e.g. N^(N^(N^N)) is not well understood.

van Atten follows one particular interpretation of intuitionism. E.g. in some of
his work he accepts the Kripke scheme (he is a student of van Dalen).
Not all intuitionists would accept that.

Best wishes,

Bas

On Wed, Dec 30, 2015 at 8:20 PM, Jon Sterling <jon at jonmsterling.com> wrote:
> Bas,
>
> I'm not making this identification at all, but perhaps my comment was
> less than clear.
>
> The type-theoretic meaning explanations are indeed constructive and not
> necessarily intuitionistic—but they come out of a tradition that goes
> back at least to Heyting's 1956 meaning explanation for intuitionistic
> logic, and I view Martin-Löf's meaning theory in this light; meaning
> explanations for Computational Type Theory, for instance, are strictly
> intuitionistic rather than merely constructive, as an example. Dybjer's
> recent meaning explanation for CoC is an example of a
> constructive-but-not-intuitionistic meaning theory, I suppose.
>
> Sundholm & van Atten like to make a very nice point that intuitionism
> (in the sense of Brouwer) is not just constructivism (as in BISH)
> plus/minus various principles—it relies on a very different notion of
> data and time.
>
> Coming back to the topic at hand, we were discussing the lack of an
> *intuitionistic* meaning explanation that justifies impredicativity; the
> fact that Martin-Löf's meaning explanations are compatible with an
> impredicative & constructivist (as opposed to specifically
> intuitionistic) ambient mathematics is not really the point here, I
> think.
>
> best,
> jon
>
>
> [Sorry if anyone has received a duplicate message from me.]
>
> On Wed, Dec 30, 2015, at 10:52 AM, Bas Spitters wrote:
>> 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