[POPLmark] how to believe a twelf proof

[Karl Crary]

Randy,

Randy Pollack wrote:

>"sr" also checks in the following extended context
>
>  false : type.
>
>  %block fblock : block {d:false}.
>  %worlds (bind | fblock) (sr _ _ _).
>  %total D (sr D _ _).
>
>This seems to say that "sr" is total in any world (bind | fblock).
>This is a world extending "bind" with possible extra entries
>{d:false}.  This doesn't say how you could ever get an assumption
>{d:false} in the context, but if you could, you would be able to prove
>that every term has object type "o" (just for example).  That is,
>{d:false} cannot occur (directly) in any canonical form proof of
>judgements "red" or "of", but may occur indirectly, by theorems which
>may not have been stated.  How does Twelf check that some assumption
>in an extended context may not contribute indirectly, by yet unproved
>theorems, to some canonical form of interest?
>
>  
>

I'm pretty sure that was the full story.  You're missing here the 
distinction between theorem inputs and higher-order assumptions.  They 
are not at all the same thing.  If we had an input term of type false 
(where false had no assumptions, constant or variable), then we could 
use it to prove whatever we like.  (See raa_sub in our solution to 1a.)  
But that is not what is happening here.

Here, you are creating a type family called "false", but once you add 
assumptions of that type, it has nothing to do with falsity other than 
the spelling.  Actually the truth is quite the opposite from what you 
suggested.  It's easy to get an assumption of type "false"; simply 
introduce it with a quantifer.  But, having that assumption won't allow 
you to do anything, since the type "false" is irrelevant (ie, not 
subordinate) to the types involved in sr.

To say it another way, for "false" to have anything to do with falsity, 
there needs to be no way to build "false".  There's no difference 
between constants and variables other than scoping; there must be 
neither of them.  Try adding your fblock to the world for raa_sub:

raa_sub : false -> sub S T -> type.
%mode +{S:tp} +{T:tp} +{X1:false} -{X2:sub S T} (raa_sub X1 X2).
%worlds (bind | vblock | ablock) (raa_sub _ _).
%total {} (raa_sub _ _).

You'll find that the theorem no longer checks.  The error message will 
be similar to what you would have gotten if you added a constant of type 
false.

    -- Karl