[Agda] Re: Agda Digest, Vol 87, Issue 24

[Dan Licata]

Hi Thorsten and all,

(sorry for the delay, missed this message)

To my mind, the most compelling reasons not to identify "proposition"
with "hprop" (proof-irrelevant proposition) are:

1) We want "ordinary" mathematicians to start using homotopy type
   theory, and to start thinking in a proof-relevant way.  To accomplish
   this goal, the (somewhat devious) strategy is to rebind the words
   this mathematician is familiar with to the type-theoretic concepts, 
   so that they default to the type-theoretic logic.  
   
   To someone who already understands props-as-types, and thinks of
   types as logic, it makes some sense to use "proposition", in contrast
   with "type", to mean a more traditional proof-irrelevant logic.  
   But if our hypothetical ordinary mathematician doesn't already
   understand the props-as-types view of logic, and sees something
   called a "proposition", they will probably use that to state and
   prove a theorem.  So, it's the wrong default.   

2) I don't remember whether Mike talks about this in his post, but 
   there are lots of "modalities" that come up, of which hprop is just
   one example, and you get a notion of logic for each.  So it seems
   wrong to have "proposition" default to hprop-logic.  

-Dan

On Nov26, Altenkirch Thorsten wrote:
> Hi,
> 
> I agree with most of what Mike is saying but I don't see the problem with
> the word "proposition". Thinking propositionally as opposed to
> type-theoretically is less expressive because we can express any statement
> about the choice of proofs. In particular the strong statement 2. he makes
> (maybe with the added proviso that the conclusion is propositional too) I
> would call the "propositional axiom of choice" which opposed to the
> "type-theoretic axiom of choice" (1) is not provable (and indeed entails
> excluded middle). And we do have already the different terminologies: e.g.
> Pi-types vs forall and more importantly Sigma-types vs. exists and
> disjoint union vs. or.
> 
> Indeed, the use of adverbs may be a good idea as an alternative. So I
> could say "there exists, type-theoretically" (meaning Sigma) as opposed to
> "there exists, propositionally" (meaning "exists", I.e. the bracket of
> Sigma). 
> 
> Btw, there are other examples where the limitation on propositions is
> inapproriate. I.e. there are strictly positive propositional formulas
> where the existence of an inductive or coinductive closure is not
> acceptable intuitionistically.
> 
> Thorsten
> 
> 
> On 23/11/2012 13:54, "Dan Licata" <drl at cs.cmu.edu> wrote:
> 
> >On Nov21, Martin Escardo wrote:
> >> In HoTT, and even before HoTT, people define a "proposition" not to be
> >>a 
> >> type, but instead a type with at most one element (suitably
> >>formulated). 
> >> One also considers the "propositional reflection" of any type (similar
> >>to 
> >> so-called bracket types), which hides (some part of the) computational
> >> content. Denote the propositional reflection of a type X by X* or [X].
> >> Intuitively, X* is empty if X is empty, and X* has just one element if
> >>X* 
> >> is inhabited (the trick is how to say this without using excluded
> >>middle).
> >
> >Just a HoTT-related terminological note: There's been some pushback on
> >using the word "proposition" exclusively to mean "hprop" (where a type A
> >is an hprop iff there is a term of type (x y : A) -> Id x y), which is
> >what Martin is doing above.  Mike Shulman has a nice summary here:
> >http://golem.ph.utexas.edu/category/2012/11/freedom_from_logic.html
> >
> >The reason is that both the proof-relevant interpretation of logic
> >(forall=Pi/exists=Sigma) and the hprop interpretation of logic (using
> >bracket types for exists) are useful, and it's linguistically helpful to
> >use logical terminology for both.  And while it's very important to be
> >clear about which of the two you mean in a given context, I think it's a
> >bad idea to accomploish this by using logical terminology only for the
> >hprop interpretation.  I think Mike's suggestion of adverbs is much
> >better.
> >
> >-Dan
> >_______________________________________________
> >Agda mailing list
> >Agda at lists.chalmers.se
> >https://lists.chalmers.se/mailman/listinfo/agda
> 
> 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.