Talk:ST type theory

Fork

I created this page by moving the description of ST out of the "type theory" page. Below are the comments about ST from the talk page on type theory.

mdnahas

Ontology

To me it is unclear what exactly is meant by "ontology" in regard to a (mathematical or logical) theory. I refer to the abstract:

"ST reveals how type theory can be made very similar to axiomatic set theory. Moreover, the more elaborate ontology of ST, grounded in what is now called the "iterative conception of set," makes for axiom (schemata) that are far simpler than those of conventional set theories, such as ZFC, with simpler ontologies. Set theories whose point of departure is type theory, but whose axioms, ontology, and terminology differ from the above, include New Foundations and Scott–Potter set theory."

In particular I think here it is not distinguished sufficiently between "theory", "axiomatization" and "ontology".Stephan Spahn (talk) 08:15, 14 May 2011 (UTC)[reply]

Axiom of Infinity

"Remark. Infinity is the only true axiom of ST and is entirely mathematical in nature. It asserts that R is a strict total order, with a domain identical to its codomain. If 0 is assigned to the lowest type, the type of R is 3."

OK, where did the 3 come from? Even if it's guaranteed to be true, tossing it out there without any explanation will just confuse any naïve readers.

I also don't think it is true, at least not with the definitions implied. I'm not entirely sure how you adapt the Kuratowski ordered pair to type theory, or how relations are intended to be defined here, or how ordered triplets and cartesian products (assuming the most obvious definition of relations) are adapted. But it seems to me that, if a and b are in type 0:

G = 0x0 (cartesian product) >= 1 (because however you define it, it doesn't contain elements of type 0)

R = <0, 0, G> (definition of relation)

R = <0, <0, G>> (definition of triple)

<0, G> = {{0}, {0, G}} (Kuratowski) >= 3 (it contains things that contain Gs, so it has to be 2 higher than G)

R >= <0, 3> = {{0}, {0, 3}} (Kuratowski) >= 5 (as above)

I could be wrong about wrong about all of this--but if so, it's only because the article is confusing and misleading to anyone who knows set theory but not type theory. --76.200.102.13 (talk) 08:37, 25 February 2009 (UTC)[reply]

With Kuratowski ordered pairs, but a type-level cartesian product, you do in fact get 3. It's because of this that, historically, people added another axiom specifying a type-level ordered pair, which gives you 1. But ST alone doesn't give you any particular answer unless you come up with either constructions or axioms for all of the relevant parts. (How could it?)

So, this needs to be fixed, but I'm not sure how. --75.36.134.30 (talk) 15:10, 26 February 2009 (UTC)[reply]

Theory ST

Unfortunately the reference to ST has neither link nor citation. I have a copy of Mendelson's 1964 textbook, which does not appear to have any information about ST, nor do I find it searching the Web or in other articles or books I know.

Can someone help with this reference? Also could someone describe the place of ST in the history of the subject? Crisperdue (talk) 18:36, 15 February 2011 (UTC)[reply]

I found something that may be of use. I make no pretensions at having read this chewy article, but I’ve skimmed it. In Kurt Goedel: Collected Works Volume II Publications 1938-1974, Oxford University Press, NY, ISBN-13 978-0-19-51472-6(v.2.pbk) there's a paper by Goedel titled "Russell's mathematical logic (1944)" (pages 119-141). This is prefaced with an "Introductory note to 1944" by Charles Parsons (pages 102-118). On page 126 we find this, together with footnote 17, and later expansion in pages 136-138:

"In the second edition of Principia, however, it is stated in the Introduction (pages xl and xli) that "in a limited sense" also functions of a higher order than the predicate itself (therefore also functions defined in terms of the predicate, as e.g., in p'k ∈ k) can appear as arguments of a predicate of functions, and in Appendix B such things occur constantly. This means that the vicious circle principle for propositional functions is virtually dropped. This change is connected with the new axiom that functions can occur in propositions only "through their values", i.e., extensionally, which has the consequence that any propositional function can take as an argument any function of appropriate type, whose extension is defined (no matter what order of quantifiers is used in the definition of this extension). There is no doubt that these things are quite unobjectionable even from the constructive standpoint (see page 136 [from pages 136-138 Goedel expands on the simple type theory, bringing up the notion from Frege "that a propositional function is something ambiguous (or, as Frege says, something unsaturated, wanting supplementation and therefore can occur in a meaningful proposition only in such a way that this ambiguity is eliminated (e.g. by substituting a constant for the variable or applying quantification to it). The consequences are that a function cannot replace an individual in a proposition . . ." [etc, etc] ]) provided that quantifiers are always restricted to definite orders. The paradoxes are avoided by the theory of simple types,¹⁷ which in Principia is combined with the theory of orders (giving as a result the "ramified hierarchy”) but is entirely independent of it and has nothing to do with the vicious circle principle (cf. page 147).

[Here Goedel launches into "the vicious circle principle proper". . ..]

" ¹⁷ By the theory of simple types I mean the doctrine which says that the objects of thought (or, in another interpretation, the symbolic expressions) are divided into types, namely: individuals, properties of individuals, relations between individuals, properties of such relations, etc. (with a similar hierarchy for extensions), and that sentences of the form: "a has property φ", "b bears the relation R top c", etc. are meaningless, if a, b, c, R, φ are not of types fitting together. Mixed types (such as classes containing individuals and classes as elements) and therefore also transfinite types (such as the class of all classes of finite types) are excluded. That the theory of simple types suffices for avoiding also the epistemological paradoxes is shown by a closer analysis of these. (Cf. Ramsey 1926 and Tarski 1935, p. 399)."(p. 126)

The Type theory article's history reflects this development, with the "matrix" business. But I haven't taken the topic beyond Wittgenstein, e.g. to the papers of Ramsey 1926 and Tarski 1935. In his paper Goedel also discusses more about the "no type theory", "the zig-zag theory" etc. which may be useful. In general this appears to be a very valuable article both for its own content and its history. Here are the Ramsey and Tarski references:

Ramsey, Frank P. 1926 "The foundations of mathematics," Proceedings of the London Mathematical Society (2) 25, 338-384, reprinted in Ramsey 1931, 1-61"

Ramsey, Frank P. 1931 The foundations of mathematics and other logical essays, edited by Richard B. Braithwaite (London: Kegan Paul).

Tarski, Alfred 1935 "Der Wahrheitsbegriff in den formalisierten Sprachen," Studia philosophica (Lemberg), 1, 261-405; German translation by L. Blaustein of Tarski 1933a)

1935a is from the Polish (The concept of truth in the languges of deductive sciences), English translation by Joseph H. Woodger in Tarski 1956, 152-278.

1956 Logic, semantics, metamathematics: Papers from 1923 to 1938, translated into English and edited by Joseph H. Woodger (Oxford: Clarendon Press).

The question I have as I type this, is, is any of this in the public domain so I don't have to tromp through the snow up the hill to the local college library. Bill Wvbailey (talk) 20:33, 16 February 2011 (UTC)[reply]

---

I just noticed that in two sections or so above this one, the "History section" cites these same references, plus a few more (coming from Reichenbach's text). So my take on it is this: these references are "solid" and probably as good as it gets unless someone has recently written a "survey text" about (the history of) type theory. In other words, there may not be much out there but these primary sources. Bill Wvbailey (talk) 20:44, 16 February 2011 (UTC)[reply]