[Agda] Why no impredicative prop?

[Jon Sterling]

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