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

[Altenkirch Thorsten]

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.