Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 14 of 14
Trivia, just a question on terminology:
is there an established technical term for – given any type theory, maybe with some axioms added – the concept of: “the collection of all terms that may be constructed in the theory”?
I imagine in first-order logic one may speak of the collection of all “(constructibly) true propositions”. Here I am looking analogously for a word for the collection of “true types” understood in the evident constructive sense as the collection of all terms that may be constructed.
I’d just like some word that would serve to make the distinction between what a type might ideally “consist of” and what of its content one may actually get hold of.
So for instance in HoTT without HITs every type looks like it contains plenty of elements of homotopy groups (i.e., it’s higher identity types look like they ought to contain lots of terms), but without HITs almost no actual non-trivial such terms may be constructed. What would therefore be a good word for the collection of terms that do have a construction, given suitable axioms?
The closest would probably be the term model, aka the initial model. But perhaps you are looking for something else?
In usual first order logic one speaks of the theory generated by some axioms and rules by closing under standard (classical or constructive) axioms and inference rules. In type theory we can either say the provable propositions of some fragment (if for instance we are interested in the provable arithmetical statements, say) or just the inhabited types of the initial model (if we’re not considering a particular fragment but rather the whole collection of types).
Thanks for “term model”. Two questions:
is there more than a terminological difference with syntactic category?
is it right that one says “term model” also if some extra axioms/constructions have been added? For instance for plain DTT with some monad/modality added, would one still speak of its “term model” (I suppose so, but just to make sure).
Barely. By saying “term model” we are being agnostic about what notion of model is the right one. Cf. the myriad proposed notions of model of MLTT. But that caveat is already present at syntactic category, I see.
Yes. You can emphasize it by saying “the term model relative to the signature ”, where specifies the extra types/constants/equations.
Thanks!
One more question: what I am really after here would ideally not be a model/category (yet). Does it make sense to distinguish the introduction rules etc. of a type theory from the collection of syntactic objects that is being generated by these rules? I’d like a terminology for the latter, in contrast to the former. Does this exist?
So “provable propositions” would be what I am after, if only we’d have a version of this where “proposition” is replaced by “type”.
Hence “inhabited types” would go in the right direction, but I’d like a terminology that refers also to the collection of inhabitants, not just the information that there is one.
I’m a little bit confused – how does what you’re looking for differ from the word “term”, or maybe “closed term”?
I just re-read Bob Harpers “Constructive mathematics is not metamathematics” where he highlights the difference betwen the “computably enumerable set of formal provable propositions” and that of the provable propositions.
I was hoping for a word for the first of these, the “computably enumerable set of formal provable propositions”, but for the case that propositions are generalized to types.
Maybe “definable term”?
I see “definable term” used for instance in Paul Taylor’s “Practical Foundations” and in texts that refer to Gandy On the axiom of extensionality (1956).
In my experience, all terms are definable, but sure, that will do for emphasis. For instance, we might talk about the definable functions from to , but that is after all just the terms of type .
In parallel to Bob’s distinction between the propositions provable in a particular formal system and those provable simpliciter (i.e., the true propositions) we have the distinction between functions definable in a particular formal system (or provably total, depending on the formalism) and all functions.
Personally, I don’t think there is much meaning in talking about a proposition that is “true” or “provable” without reference to some formal system.
On the terminology, I agree with Ulrik and Mike, that “term” should basically be enough, though you probably mean “term of type X” for a given X, and you should clarify whether you are restricting to closed terms or also considering open terms.
I think the distinction that Harper was getting at becomes clearer when you consider open terms. Typically, whenever you have a derivation of in a given type system TS, that will determine a function from [terms of type ] to [terms of type ] in whatever ambient mathematics you are working in. Here, again it is important to clarify whether “terms of type X” is referring only to closed terms or to arbitrary open terms, but in either case one would still ask that such terms are equipped with an appropriate typing derivation in TS, and the function would map typing derivations to typing derivations. In the former case (where “terms of type X” = set of closed terms of type X), then generally the converse will not be true, that any such function between sets of closed terms is representable as a well-typed open term. On the other hand, if “terms of type X” is interpreted in a sufficiently liberal sense, and “function” is interpreted in a sufficiently restricted sense, then one can imagine situations where the converse is true, for Yoneda-like reasons.
Thanks for all this! I think I got what I needed, thanks.
But I’ll comment on one point just for it’s own sake: the issue re #7 #10 is that of levels of metatheories, isn’t it. When in contexts of Goedel incompleteness one distinguishes between “formally provable propositons” and “true propositions”, then one means by the second a formal derivation in a metatheory for the object theory to which the first refers, do. Doesn’t one?
Applied to the example that I mentioned in #1 this is just the distinction that I am after: Given HoTT without HITs then the typical model (built in a metatheory) consists of types that have plenty of terms in their higher identity types, but in the theory of HoTT without HIT, almost none of these terms are, well, definable.
Not really. “True proposition” is defined inductively à la Tarski. Of course, the only true propositions we can know about are the provable ones, but that doesn’t mean they are the only ones.
Unclear which statement you like to be disagreeing with. Tarski’s “correspondence principle” of truth is precisely by recourse to a metatheory.
1 to 14 of 14