Wording question: predicative and impredicative

[Yannick Duchêne]

Hi happy people,

Am I right or wrong if I have a wording which says given this:

typedef t(i:int) = [i > 3] int(i)
typedef u = [i: int] t(i)

the first declaration is that of a predicative type and the second is that of an impredicative type?

[Hongwei Xi]

I think the word 'impredicativity' was coined by Poincare:

https://en.wikipedia.org/wiki/Henri_Poincar%C3%A9

My understanding is that 'impredicativity' usually involves some form of circularity.

For instance, we can define the smallest set satisfying a property P as the intersection

of all the sets satisfying P. This definition is often classified as being impredicative

(since all the sets satisfying P contains the one being defined).

In your example, both t and u are predicative. Here is an example of impredicative definition:

typedef u = [a:type] list(a)

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/7f31b1d0-9d5c-4fe9-9917-d2c5dcab4073%40googlegroups.com.

[Yannick Duchêne]

Le jeudi 10 décembre 2015 03:58:05 UTC+1, gmhwxi a écrit :

I think the word 'impredicativity' was coined by Poincare:

https://en.wikipedia.org/wiki/Henri_Poincar%C3%A9

My understanding is that 'impredicativity' usually involves some form of circularity.

For instance, we can define the smallest set satisfying a property P as the intersection

of all the sets satisfying P. This definition is often classified as being impredicative

(since all the sets satisfying P contains the one being defined).

In your example, both t and u are predicative. Here is an example of impredicative definition:

typedef u = [a:type] list(a)

I feel to see better: this one impredicative because (the reason is important) there is anyway, not `list` set and `[a:type] list(a)` defines a new whole set.

I've seen a definition at Wolfram, which is very terse:

http://mathworld.wolfram.com/Impredicative.html

“Definitions about a set which depend on the entire set.”

Do you agree with their definition?

Seems it depends on the proposition. Another site give this:

http://www.iep.utm.edu/predicat/

“Let n be the least natural number such that n cannot be written as the sum of at most four cubes.”

They says this is one impredicative because it generalize over all natural numbers, but it's ambiguous to me, due to “Let n be the least”. Or may be a sentence may have both predicative and impredicative parts and if is has an impredicative part, then the whole sentence is said impredicative.

I will have another question later, about propositions and predicates, something I need to clarify.

[gmhwxi]

Kreisel wrote in depth on impredicativity:

https://en.wikipedia.org/wiki/Georg_Kreisel

On Thursday, December 10, 2015 at 11:19:31 AM UTC-5, Yannick Duchêne wrote:

Le jeudi 10 décembre 2015 03:58:05 UTC+1, gmhwxi a écrit :

I think the word 'impredicativity' was coined by Poincare:

https://en.wikipedia.org/wiki/Henri_Poincar%C3%A9

My understanding is that 'impredicativity' usually involves some form of circularity.

For instance, we can define the smallest set satisfying a property P as the intersection

of all the sets satisfying P. This definition is often classified as being impredicative

(since all the sets satisfying P contains the one being defined).

In your example, both t and u are predicative. Here is an example of impredicative definition:

typedef u = [a:type] list(a)

I feel to see better: this one impredicative because (the reason is important) there is anyway, not `list` set and `[a:type] list(a)` defines a new whole set.

I've seen a definition at Wolfram, which is very terse:

http://mathworld.wolfram.com/Impredicative.html

“Definitions about a set which depend on the entire set.”

Do you agree with their definition?

 
Honestly, I do not know what this definition means. I could only guess.

Seems it depends on the proposition. Another site give this:

http://www.iep.utm.edu/predicat/

“Let n be the least natural number such that n cannot be written as the sum of at most four cubes.”

They says this is one impredicative because it generalize over all natural numbers, but it's ambiguous to me, due to “Let n be the least”. Or may be a sentence may have both predicative and impredicative parts and if is has an impredicative part, then the whole sentence is said impredicative.

Poincare was vehemently against anything infinite. He would simply reject the very EXISTENCE of the set of numbers that cannot be
written as the sum of at least for cubes.

The above definition can be given in a predicative form:

Let n be a number satisfying P(n) such that P(n2) implies n <= n2 for any natural number n2.

Girard, another French, who invented linear logic, actually showed that impredicativity is "okay".

[Yannick Duchêne]

Le jeudi 10 décembre 2015 17:58:55 UTC+1, gmhwxi a écrit :

Poincare was vehemently against anything infinite. He would simply reject the very EXISTENCE of the set of numbers that cannot be
written as the sum of at least for cubes.

He was not alone :-P 

I will stay with a rough understanding, as it seems a real understanding requires a lot of work, which I'm not sure is worth for the time.

The above definition can be given in a predicative form:

Let n be a number satisfying P(n) such that P(n2) implies n <= n2 for any natural number n2.

This, is important: so predicative vs impredicative, is a form, not a property of a fact.

Thanks for your answer.

(will go on later with another thread…)

 

[Yannick Duchêne]

An property worth to be noted, was mentioned here: https://groups.google.com/d/msg/ats-lang-users/5RdaKflpASs/A3_GN-3qBAAJ

  * A type index is of a predicative sort.

  * If a type constructor applies to an impredicative sort, it makes it polymorphic.

Additionally, looking at `pats_staexp2_sort.dats`, I got a reminder:

  * Only the predicative sorts have a covariant/contravariant aspect.

[Yannick Duchêne]

Le vendredi 29 juin 2018 16:33:13 UTC+2, Yannick Duchêne a écrit :

  * Only the predicative sorts have a covariant/contravariant aspect.

Oops, sorry, please read “only the *impredicative*”  sorts.