# Talk:Totality assertion

## Why I somewhat rudely deleted the whole page and redirected to something I wrote previously

I found the previous version of this troubling, mainly just because it was confusing, but also because I'm not sure what a page on "totality assertion" is supposed to contain. I redirected to my summary at %total; that summary is brief and should be expanded (especially with examples). But when a sentence needs to be bullet-pointed, I think it's either saying way too much for one sentence or way too little for us to understand! I propose that we have a page about metatheorem that discusses why you'd like to make a %total declaration and what it means for metatheory, and a page about %total (still needs work obviously) that explains how you do it and specifically what it means in terms of logic programming.

In case you disagree and recreate this, specifically:

• there are no infinite-sized terms; if we have a LF term then it is of finite size.
• Though a %total does prove it's "always possible to derive an object.." it is stronger than that: Twelf's logic program search procedure will always succeed.
• It's critical for correctness that the inputs are ground, and the outputs are also guaranteed to be ground.
• There may be no inputs or no outputs (or neither), so using the word "some" might be misleading (it can be read as "exists")
• I'd say (defined by %worlds consisting of zero or more %blocks), since that's all that worlds are.
— Tom 7 10:20, 9 March 2007 (EST)

### Original

A totality assertion states the following:

• Given one or more LF type families indexed by some number of objects
• If some of those indices are treated as inputs and some are treated as outputs (as defined by a %mode for each family)
• If the relevant part of the LF context is formed in a certain way (defined by %worlds and zero or more blocks)
• Then given terms for each of the indices treated as inputs, it is always possible to derive an object of any one of the type families, which means that it is possible to construct an object for each of the output types. Furthermore, based on an induction metric (defined by %total), this term has finite size.

If a type family is indexed by judgments, then a totality assertion proves the metatheorem that for all proof terms witnessing the truth of inputs, there exist proof terms witnessing the truth of each of the outputs; therefore, the totality assertion can be seen as the statement of a theorem that has the form AB for some sets of propositions A and B.