"in ZF the fundamental source of impredicativity is the seperation axiom which asserts that for each well formed function p(x)of the language ZFthe existence of the set x : x } a ^ p(x) for any set a Since the formular p may contain quantifiers ranging over the supposed "totality" of all the sets this is impredicativity according to the VCP this impredicativity is given teeth by the axiom of infinity "

3. Axiom schema of specification (also called the axiom schema of separation or of restricted comprehension): If z is a set, and is any property which may characterize the elements x of z, then there is a subset y of z containing those x in z which satisfy the property. The "restriction" to z is necessary to avoid Russell's paradox and its variants.

simple colin leslie dean has not presented it to the academic world
no journals
no nothing
he is a no body who preferes to step out side the grove
he believes that the academic world has and should not have a monopoly on truth

Say pam69ur, do you mean meaninglesness as in falso?

Absurdities or meaninglessness or irrationality is no hindrance [sic] to something being 'true' rationality, or, Freedom from contradiction or paradox is not a necessary an/or sufficient condition for 'truth': mathematics and science examples

EXAMPLES FROM MATHEMATICS AND SCIENCE SHOW THE
DEAN THEOREM


CONTRADICTION, OR INCONSISTENCY WITHIN A VIEW AS WELL AS MUTUAL CONTRADICTION, OR INCOMMENSURABLITY BETWEEN VIEWS DOES NOT PRECLUDE THE VIEW OR BOTH VIEWS FROM BEING 'TRUE'

How does that advance your career or recognition?

Godel does not actually use the axiom of reducibility as you like to point out.

Proposition VI: To every ω-consistent recursive class c of formulae there correspond recursive class-signs r, such that neither v Gen r nor Neg (v Gen r) belongs to Flg(c) (where v is the free variable of r).

In the proof of Proposition VI the only properties of the system P employed were the following:
1. The class of axioms and the rules of inference (i.e. the relation "immediate consequence of") are recursively definable (as soon as the basic signs are replaced in any fashion by natural numbers).
2. Every recursive relation is definable in the system P (in the sense of Proposition V).

P is essentially the system obtained by superimposing on the Peano axioms the logic of PM

IV. Every formula derived from the schema
1. (∃u)(v ∀ (u(v) ≡ a))
on substituting for v or u any variables of types n or n + 1 respectively, and for a a formula which does not contain u free. This axiom represents the axiom of reducibility (the axiom of comprehension of set theory).
V. Every formula derived from the following by type-lift (and this formula itself):
1. x1 ∀ (x2(x1) ≡ y2(x1)) ∨ x2 = y2.
This axiom states that a class is completely determined by its elements.

A formula c is called an immediate consequence of a and b, if a is the formula (~(b)) ∨ (c), and an immediate consequenee of a, if c is the formula v ∀ (a), where v denotes any given variable. The class of provable formulae is defined as the smallest class of formulae which contains the axioms and is closed with respect to the relation "immediate consequence of".24
The basic signs of the system P are now ordered in one-to-one correspondence with natural numbers,

40. R-Ax(x) ≡ (∃u,v,y,n)[u, v, y, n <= x & n Var v & (n+1) Var u & u Fr y & Form(y) & x = u ∃x {v Gen [[R(u)*E(R(v))] Aeq y]}]:>
x is a formula derived from the axiom-schema IV [ie axiom of reducibility], 1 by substitution

"A. Whitehead and B. Russell, Principia Mathematica, 2nd edition, Cambridge 1925. In particular, we also reckon among the axioms of PM the axiom of infinity (in the form: there exist denumerably many individuals), andthe axioms of reducibility and of choice (for all types)" ((K Godel , On formally undecidable propositions of principia mathematica and related systems in The undecidable , M, Davis, Raven Press, 1965, p.5). NOTE HE SAYS HE IS USING 2ND ED PM- WHICH RUSSELL ABANDONED REJECTED GAVE UP DROPPED THE AXIOM OF REDUCIBILITY.

he uese it
he even tells you he uses it

The most comprehensive formal systems yet set up are, on the one hand, the system of Principia Mathematica (PM)2 and, on the other, the axiom system for set theory of Zermelo-Fraenkel (later extended by J. v. Neumann).3 These two systems are so extensive that all methods of proof used in mathematics today have been formalized in them, i.e. reduced to a few axioms and rules of inference. It may therefore be surmised that these axioms and rules of inference are also sufficient to decide all mathematical questions which can in any way at all be expressed formally in the systems concerned. It is shown below that this is not the case...

He makes examples of it and other axioms. His proof doesn't rely on its soundness. He's making a point about axioms in general.

In the proof of Proposition VI the only properties of the system P employed were the following:
1. The class of axioms and the rules of inference (i.e. the relation "immediate consequence of") are recursively definable (as soon as the basic signs are replaced in any fashion by natural numbers).
2. Every recursive relation is definable in the system P (in the sense of Proposition V)

IV. Every formula derived from the schema
1. (∃u)(v ∀ (u(v) ≡ a))
on substituting for v or u any variables of types n or n + 1 respectively, and for a a formula which does not contain u free. This axiom represents the axiom of reducibility (the axiom of comprehension of set theory).
V. Every formula derived from the following by type-lift (and this formula itself):
1. x1 ∀ (x2(x1) ≡ y2(x1)) ∨ x2 = y2.
This axiom states that a class is completely determined by its elements.

Yes, I read what you wrote the first time you pasted it in. And you apparently didn't read Godel's own introduction in which he sets out to disprove the necessary internal coherence of the axioms that follow.

In the proof of Proposition VI the only properties of the system P employed were the following:
1. The class of axioms and the rules of inference (i.e. the relation "immediate consequence of") are recursively definable (as soon as the basic signs are replaced in any fashion by natural numbers).
2. Every recursive relation is definable in the system P (in the sense of Proposition V)

It may therefore be surmised that these axioms and rules of inference are also sufficient to decide all mathematical questions which can in any way at all be expressed formally in the systems concerned. It is shown below that this is not the case...

1 paradox
Godel makes the claim that there are undecidable propositions in a constructed system [PM and ZF] that dont depend upon the special nature of the constructed system [PM and ZF]
Quote

As he states
"It is reasonable therefore to make the conjecture that these axioms and rules of inference are also sufficent to decide all mathematical questions which can be formally expressed in the given systems. In what follows it will be shown that this is not the case but rather that in both systems cited [PM and ZF] there exist relatively simple problems of ordinary whole numbers [undecidability] which cannot be decided on the basis of the axioms. [NOTE IT IS CLEAR]This situation [ undecidability which cannot be decided on the basis of the axioms]. does not depend upon the special nature of the constructed systems [PM and ZF] but rather holds for a very wide class of formal systems among which are included in particular all those which arise from the given systems [PM and ZF] by addition of finitely many axioms" (K Godel , On formally undecidable propositions of principia mathematica and related systems in The undecidable , M, Davis, Raven Press, 1965, p.6).( K Godel , On formally undecidable propositions of principia mathematica and related systems in The undecidable , M, Davis, Raven Press, 1965, p.6)

Thus Godel says he is going to show that undecidability is not dependent on the
axioms of a system or the speacial nature of PM and ZF
Also
Godels refers to PM and ZF AS FORMAL SYSTEMS

"the most extensive formal systems constructed .. are PM ZF" ibid, p.5
so when he states that
"This situation does not depend upon the special nature of the constructed
systems but rather holds for a very wide class of formal systems"
he must be refering to PM and ZF as belonging to these class of formal systems- further down you will see this is true as well


thus he is saying
the undecidability claim is independent of the axioms of the formal system but PM is a formal system


Godel says he is going to show undecidabilitys by using the system of PM (ibid)
he then sets out to show that there are undecidable propositions in PM (ibid. p.8)

where Godel states
"the precise analysis of this remarkable circumstance leads to surprising results concerning consistence proofs of formal systems which will be treated in more detail in section 4 (theorem X1) ibid p. 9 note this theorem comes out of his system P
he then sets out to show that there are undecidable propositions in his system P -which uses the axioms of PM and Peano axioms.
at the end of this proof he states
"we have limited ourselves in this paper essentially to the system P and have only indicated the applications to other systems" (ibid p. 38)

now
it is based upon his proof of undecidable propositions in P that he draws out broader conclusions for a very wide class of formal systems
After outlining theorem V1 in his P proof - where he uses the axiom of choice- he states
"in the proof of theorem V1 no properties of the system P were used other than the following
1) the class of axioms and the riles of inference- note these axioms include reducibility
2) every recursive relation is definable with in the system of P
hence in every formal system which satisfies assumptions 1 and 2 [ which uses system PM] and is w - consistent there exist undecidable propositions ". (ibid, p.28)

CLEARLY GODEL IS MAKING SWEEPING CLAIMS JUST BASED UPON HIS P PROOF . Note from above the version of PM he is using AR was abandoned rejected given up DROPPED So system P is completely artificial and invalid as it uses the invalid axiom of reducibility. Thus his theorem has no value outside this invalid artificial system P


Godel has said that undecidability is not dependent on the
axioms of a system or the special nature of PM and ZF

There is a paradox here
He says every formal system which satisfies assumption 1 and 2 ie
based upon axioms - but he has said undecidablity is independent of axioms

dean attacks godel for many reasons
one being
his incompleteness theorem is invalid-regardless of what it says he uses in his proof of that theorem an invalid axiom ie AR

Interestingly, the basic idea underlying Russell's ramified hierarchy of types is a crucial ingredient for Godel's later consistency proof of the continuum hypothesis via its inner model L of constructible sets. Also, as already observed in Godel (1944), a form of AR becomes true in L in the sense that, roughly, an arbitrary propositional function of natural numbers is extensionally equivalent to some function of order alpha, for some countable ordinal alpha.

Except for the fact that it's not part of his proof in the way you describe.

Furthermore, parts of the AR are apparently valid as used by Godel (according to the entry in the Stanford Encyclopedia):

In the proof of Proposition VI the only properties of the system P EMPLOYED were the following:
1. The class of axioms and the rules of inference (i.e. the relation "immediate consequence of") are recursively definable (as soon as the basic signs are replaced in any fashion by natural numbers).
2. Every recursive relation is definable in the system P (in the sense of Proposition V)

http://www.math.ucla.edu/~asl/bsl/1302/1302-001.ps.



"The system P of footnote 48a is Godel's
streamlined version of Russell's theory of types built on the natural
numbers as individuals, the system used in [1931]. The last sentence ofthe footnote allstomindtheotherreferencetosettheoryinthatpaper;
KurtGodel[1931,p. 178] wrote of his comprehension axiom IV, foreshadowing
his approach to set theory, "This axiom plays the role of [Russell's]
axiom of reducibility (the comprehension axiom of set theory).

the standford encyclopdeia of philosophy says of AR

Principia Mathematica (Stanford Encyclopedia of Philosophy)

"many critics concluded that the axiom of reducibility was simply too ad hoc to be justified philosophically

My quote was from that very article you cited. It names a special example in which AR was valid as used by Godel.

"many critics concluded that the axiom of reducibility was simply too ad hoc to be justified philosophically

From Kurt Godels collected works vol 3 p.119

Collected Works - Google Book Search

"the axiom of reducibility is generally regarded as the grossest philosophical expediency