In responding to your question, I hope that I can convince you of the following two claims:
- Gödel held that the formal system of the actual Principia was that of ramified type thoery (simple type theory with orders built into the syntax).
- Gödel held that the formal system of Principia without orders built into the syntax would have been motivated by a kind of realist position.
But first, I want to address your leading question about the formal system of Principia.
Is there serious doubt of whether the first edition of Russell and Whitehead's Principia Mathematica used the ramified theory of types?
Yes. The appearance that Principia has a ramified theory of types (in which orders are part of the syntax) is not accepted by all Russell scholars, and there have been serious challenges to that reading. The most detailed source for the interpretation on which Principia embraces a simple theory of types (in which orders are only part of the nominalistic intended interpretation) is
Landini is the leading proponent of the view that Principia embraces a simple type theory. There is a nice centenary anthology in which the controversy over the formal system of Principia is treated:
- Nicholas Griffin and Bernard Linsky (2013) The Palgrave Centenary Companion to Principia Mathematica: Palgrave Macmillan.
Yet Gödel says the simple theory of types "is the system of the first Principia in an appropriate interpretation" (in his 1944 essay "Russell's mathematical logic"). I wonder if Gödel was referring loosely to Russell's 1903 Principles of Mathematics as "the first Principia." Or did Gödel have some way to read the first edition of Russell and Whitehead's Principia Mathematica as using simple type theory?
I think that the answer to this is decidedly no. Gödel is fairly consistent about calling the formal system of Principia one on which there is a simple type theory with orders. For there is no textual evidence to suggest that Gödel was referring obliquely to the 1903 Principles or to the formal system of the actual Principia as Gödel understood it. In the remark that you cite, Gödel really is suggesting that on a "realist" interpretation of Principia, the syntax would be just that of a simple type theory. In Gödel's telling, the "constructive" standpoint motivated by a Vicious Circle Principle is wholly unmotivated on a "realist" picture. This reading seems to be supported by Gödel's holding that (1) the theory of simple types and the theory of ramified types are logically independent and (2) the theory of simple types is (a) inconsistent with the "constructive" position and (b) is well-motivated by a "realist" stance with an additional assumption. I quote from the Schilpp volume printing of Gödel's 1944:
(1) I now come in somewhat more detail to the theory of simple types which appears in Principia as combined with the theory of orders; the former is, however, (as remarked above) quite independent of the latter... (p. 147; see also pp. 134-135, especially note 17)
(2)(a) But, it should be noted that the theory of simple types (in contradistinction to the vicious circle principle) cannot in a strict sense follow from the constructive standpoint... (p. 148)
(2)(b) The theory of simple types (in its realistic interpretation) can be considered as a carrying through of this scheme, based, however, on the following additional assumption concerning meaningfulness: ... (p. 149)
So when Gödel calls simple type theory "the system of the first edition of Principia in an appropriate interpretation" (p. 152), he is referring to Principia "in its realistic interpretation" - which is not one Gödel himself endorses, nor the one that Gödel identifies with the actual formal system of Principia but one on which the theory of simple types would be motivated by a kind of "realist" position.
It bears mentioning that, Landini and company are right about the formal system of Principia being just simple type theory (with orders built into the intended interpretation and not built into the syntax) if and only if Gödel is wrong about the formal system of Principia being ramified type theory (simple type theory with orders built into the syntax). It is a fun debate in Russell scholarship!