Impredicative theory?

[taeto]

A definition of an object \(x\) is called impredicative if the expression used to explain the value of \(x\) contains mention of \(x\) itself.

The example that I want to ask about is perhaps illustrative enough: In Group Theory, \(e\) is a neutral element for \(G\) if \(ex = xe = x\) holds for every element \(x\) of \(G\). Since \(e\) is itself an element of \(G\), this is a typical example of an impredicative definition. This statement is the axiom that a group has a neutral element. Therefore I began wondering if perhaps Group Theory is an impredicative theory. 

My original motivation comes from a nice booklet written by Edward Nelson titled Predicative Arithmetic:

web.math.princeton.edu/~nelson/books/pa.pdf

The title of Chapter 1, which has a length of about one printed page, is "The impredicativity of induction". Superficially a single axiom of the axiom schema of induction appears to have a similar structure to the example from Group Theory. If \(P\) is a predicate for which both \(P(0)\) and \(P(n) \rightarrow P(n+1)\) hold, then \(P(n)\) is true for all \(n.\) This axiom does again contain a universal quantifier. But if you look for an element which is defined and which is also similarly quantified by the quantifier, you are harder pressed than in the group example above, at least in my limited understanding. Nelson must have meant something by this. Unfortunately he passed on some years ago. Maybe someone can provide an insight? I honestly believe that my understanding is not up to par with this.

The point of it all is that a theory that contains impredicative definitions is somehow reasonably deemed deficient. A little similar to having circular definitions.

I did ask around for an explanation for why Group Theory is not equally considered deficient. Now I am not mentioning names, but I got the explanation from a very knowledgeable mathematician that the point is that you may substitute the above definition of the neutral element \(e\) by the equivalent definition "there exists a unique element \(e\) in \(G\) with the property \(ee = e.\)" This is indeed the case. The problem now is that to say the \(e\) is `unique' means to say \(\forall x : xx = x \rightarrow x = e,\) and now you have a universal quantifier which has \(e\) in its scope, and it makes the definition impredicative. If you do not include the `unique' part, I leave it as an exercise to show that \((\{ 0,1 \},\cdot)\) becomes a group, where \(\cdot\) is usual multiplication. My question here is whether there is some clear argument to say that the definition of a group is not necessarily impredicative?

Edited January 2, 2020 by taeto

[studiot]

1 hour ago, taeto said:

A definition of an object x  is called impredicative if the expression used to explain the value of x  contains mention of x  itself.

The example that I want to ask about is perhaps illustrative enough: In Group Theory, e  is a neutral element for G  if ex=xe=x  holds for every element x  of G . Since e  is itself an element of G , this is a typical example of an impredicative definition. This statement is the axiom that a group has a neutral element. Therefore I began wondering if perhaps Group Theory is an impredicative theory. 

My original motivation comes from a nice booklet written by Edward Nelson titled Predicative Arithmetic:

web.math.princeton.edu/~nelson/books/pa.pdf

The title of Chapter 1, which has a length of about one printed page, is "The impredicativity of induction". Superficially a single axiom of the axiom schema of induction appears to have a similar structure to the example from Group Theory. If P  is a predicate for which both P(0)  and P(n)→P(n+1)  hold, then P(n)  is true for all n.  This axiom does again contain a universal quantifier. But if you look for an element which is defined and which is also similarly quantified by the quantifier, you are harder pressed than in the group example above, at least in my limited understanding. Nelson must have meant something by this. Unfortunately he passed on some years ago. Maybe someone can provide an insight? I honestly believe that my understanding is not up to par with this.

The point of it all is that a theory that contains impredicative definitions is somehow reasonably deemed deficient. A little similar to having circular definitions.

I did ask around for an explanation for why Group Theory is not equally considered deficient. Now I am not mentioning names, but I got the explanation from a very knowledgeable mathematician that the point is that you may substitute the above definition of the neutral element e  by the equivalent definition "there exists a unique element e  in G  with the property ee=e. " This is indeed the case. The problem now is that to say the e  is `unique' means to say ∀x:xx=x→x=e,  and now you have a universal quantifier which has e  in its scope, and it makes the definition impredicative. If you do not include the `unique' part, I leave it as an exercise to show that ({0,1},⋅)  becomes a group, where ⋅  is usual multiplication. My question here is whether there is some clear argument to say that the definition of a group is not necessarily impredicative?

 

1 hour ago, taeto said:

I leave it as an exercise to show that ({0,1},⋅)  becomes a group, where ⋅  is usual multiplication

Can you clarify your notation here please ? Is the interval specified open or closed?

Further, if you are specifying that interval and the binary operation as multiplication then surely 0.5 is in the set but the inverse of multiplication by 0.5 is multiplication by 2 which is not in interval?

 

As regards (im)predicative definitions Russell specified that all definitions should be predicative in his type theory for this reason.

You might also like to look up Grelling's paradox of semantic self reference or heterological paradox.

[taeto]

3 minutes ago, studiot said:

 

Can you clarify your notation here please ? Is the interval specified open or closed?

Further, if you are specifying that interval and the binary operation as multiplication then surely 0.5 is in the set but the inverse of multiplication by 0.5 is multiplication by 2 which is not in interval?

 

As regards (im)predicative definitions Russell specified that all definitions should be predicative in his type theory for this reason.

You might also like to look up Grelling's paradox of semantic self reference or heterological paradox.

No, just the set of two elements \(0\) and \(1\). Yes, I know it is not a group. The point is that if you replace the group axiom which says that there is a neutral element by another axiom which says that there is an element \(e\) for which \(ee=e,\) then the set \(\{0,1\}\) satisfies this new axiom under usual multiplication, as well as the other axioms. Hence the suggested fix does not work.

At least Russell would then have a definition of a group that is predicative, so that is a nice pointer, thanks!

I still do not see how induction is not predicative. 

 

[studiot]

9 minutes ago, taeto said:

No, just the set of two elements 0 and 1 . Yes, I know it is not a group. The point is that if you replace the group axiom which says that there is a neutral element by another axiom which says that there is an element e for which ee=e, then the set {0,1} satisfies this new axiom under usual multiplication, as well as the other axioms. Hence the suggested fix does not work.

At least Russell would then have a definition of a group that is predicative, so that is a nice pointer, thanks!

I still do not see how induction is not predicative. 

 

Thanks I should have realised the set you meant.

The point is that the definition of a group requires that whatever you take as the single binary operation must have an inverse for every operation.
This disallows multiplication, since multiplication by zero does not have an inverse.
It does work if your binary operation is addition however.
(and yes it also requires one element is the identity element, which also works with zero as the identity element)

 

Edited January 2, 2020 by studiot

[taeto]

7 minutes ago, studiot said:

This disallows multiplication, since multiplication by zero does not have an inverse.

With the new axioms, each element does have an inverse under multiplication .

[studiot]

Not sure how {1, 0} forms a group under either addition or multiplication, since both have an element with no inverse.

 

Edited January 2, 2020 by studiot

[taeto]

32 minutes ago, studiot said:

Not sure how {1, 0} forms a group under either addition or multiplication, since both have an element with no inverse.

 

Indeed. So we should be more precise.

Let a pseudo-group be a structure that satisfies the group axioms, except the neutral element axiom is replaced by the axiom

[math] \exists e : ee = e [/math].

The purpose being to eliminate the impredicative axiom \(\exists e \forall x : xe=ex=x\), so that we obtain a predicative definition of a group.

Certainly any group is a pseudo-group; just take \(e\) to be the neutral element. So we are half-way there.

Unfortunately \( (\{0,1\},\cdot) \) is a pseudo-group, but not a group. Choose \(e = 0\), then \(e\) satisfies the new axiom, since \(0\cdot 0 = 0.\) The associativity axiom is trivial, since multiplication is associative on all \(\mathbb{R}\). The axiom of the existence of an inverse is satisfied, because \(1\cdot 0 = 0\cdot 1 = 0,\) hence \(0\) and \(1\) are mutual inverses.

I found 

math.stackexchange.com/questions/1744856/group-theory-vs-type-theory

with a definition of a group in type theory. But to me it just looks like the exact same definition as we are used to. In particular the neutral element axioms states that there exists an element \(e\) for which \(ae=ea=a\) for all \(a\). So I do not know why the usual definition is supposed to be impredicative, when it looks the exact same as the type theory definition .  

Edited January 2, 2020 by taeto

[studiot]

1 hour ago, taeto said:

Indeed. So we should be more precise.

Do you know there is a heirarchy of 'group' definitions?

They all start with a set and binary operation, but do not necessarily obey all 4 group axioms.

Groupoid is the most general and is just that a set with a closed binary operation, but not necessarily associative. (axiom 1)

For example the set of positive real numbers plus the binary operation a + b = √(a² + b) is a groupoid.

Semi-group or Hemi-group and is just that a set with a closed binary operation, but also associative. (axioms 1 & 2)

Monoid is a semigroup with an identity element. (axioms 1 & 2 & 3)

A Group is a monoid in which every element also has an inverse. (axioms 1 & 2 & 3 & 4)

 

And thank you for taking me down a path I don't usually frequent as an applied mathematician, although all these definitions have a place in numerical analysis. +1

Edited January 2, 2020 by studiot

[taeto]

14 hours ago, studiot said:

Do you know there is a heirarchy of 'group' definitions?

That is more or less how I learned it back in the day. Most recently I lectured "Abstract Algebra", and all that got skipped over by the textbook, basically because there are now so many applications of algebra to teach that there isn't enough time for the nitty-gritty 

[taeto]

As I began by saying, I got intrigued by a publication by Edward Nelson on "Predicative Arithmetic", in which the first few paragraphs state that usual induction is "impredicative".

Now induction is a basic defining property of natural numbers and their arithmetic. The more intricate behaviors of natural numbers are applied in everyday situations, especially when we want to transfer or extract amounts of money via electronic means, and also in ways of communicating messages confidentially, familiar by the difference between having an "http" or an "https" at the front of the name of an internet page like this. And for something to be "impredicative" is somehow indicative of it being in some way defective, almost circularly defined.

Wikipedia says: "Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more commonly) another set that contains the thing being defined. There is no generally accepted precise definition of what it means to be predicative or impredicative."

Clearly this clashes two-fold with the idea that induction is impredicative. First, induction is a collection of axioms, not a set. Second, none of the axioms of induction refers to induction or to any sets that are defined by induction.

I have tried to figure out if the axiom of the neutral element of a group is impredicative. The axiom says that if G is a group with addition +, then 0 is a neutral element of G if 0+x=x+0=x is true for every element x of G. All people whom I asked seem to agree that this is an impredicative definition, since by saying "every element x" you also include the element 0 itself, and therefore the definition already refers to the element which it defines. The best answer that I got so far says that you have to define not what a group (G,+) is, but you have to define what a group (G,+,e) with neutral element e is. Then the definition becomes predicative, which is to say, now it is alright, since you no longer get to choose e among the elements of G, but it is already fixed. 

Do you guys see what I am missing? I still do not know why arithmetic is supposed to be "impredicative", nor why group theory is somehow "wrong". 

 

[studiot]

My maths dictionary has

Quote

Predicative  adjective -  (Logic)

(Of a definition) given in terms that do not require quantification over entities of the same typeas that which it is thereby defined.

Part of Russell's solution to the paradoxes of self-reference as contained in hy type theory was to require all definitions to be predicative.

Compare with impredicative definition.

 

Quote

Impredicative Definition - noun (Logic)

A definition in terms that require quantification over a range that includes that which is to be defined.such as having all the properties of a ggreat general, where one of the properties so ascribed must be the property itself.

See type

 

These quantifier terms appear in Logic in the predicate calculus

[taeto]

1 hour ago, studiot said:

My maths dictionary has

Predicative  adjective -  (Logic)

(Of a definition) given in terms that do not require quantification over entities of the same type as that which it is thereby defined.

Part of Russell's solution to the paradoxes of self-reference as contained in hy type theory was to require all definitions to be predicative.

Thanks! 

If we define in the ordinary way a group \( (G,+) \) so that it satisfies the axiom (which I seem unable to typeset properly)

\( \exists 0 \forall x : x+0 = 0+x = x,\)

then we agree that the definition is impredicative, since the universal quantification is over all group elements.

It seems that in type theory you define a group \( (G,+,0) \) so that it satisfies the axiom

\( \forall x : x+0 = 0+ x = x,\)

and this definition is predicative, since 0 is not in the scope of the quantifier? A statement like \(0+0=0\) now becomes a theorem that does not follow immediately, since you cannot replace \(x\) by \(0\) in the definition of \(0\). So can you prove it?

 

Edited January 7, 2020 by taeto