More developments in the design of Sequent:
The modeling power of Sequent may be stunted by its limited ability to talk about objects. I keep invoking Skolem functions and the like in my models, which then need to leak into other propositions and I am then flooded by unnecessary equality assumptions just to say something that should be simple. This paragraph could be completely wrong, as I have no evidence for this, this is just the picture of the frustration in my mind.
But speaking of pictures, I had a new one of Sequent today. Instead of a Coq-like environment where you have hypotheses and a goal, I pictured an object environment (I have written about that phrase before); you always have a valid program, and you are merely manipulating it. (A valid program may need witnesses that you do not have, so in that sense you can't use it until more work is done).
When you look at objects in this environment, you always have a set of assumptions (it would not be Sequent without that!), and you have a set of constructed objects in terms of those assumptions. You can add new assumptions to the view, you can take assumptions out of the view (which adds them as hypotheses to each constructed object that needs them), if you construct one of your assumptions, then you may discharge it (here it plays the role of a goal). (There is a snag here in that we must be careful not to circularly construct anything, and the possible circularity is not immediately visible to the user.) You may discharge a construction and turn it into an assumption. Etc.
Of course we could offer some sort of interface where you can mouse-over a constructed object to highlight the assumptions it depends on -- and similarly mouse-over an assumption to see which constructions use it.
This is just a vision though, and it may not be the most essential interface for this way of thinking, whatever it is. For example, in the Coq world, identifiers can be in a special state where you know their definition; that strikes me as asymmetrical. Eg. the following two are different:
f : nat -> nat
f x := x + 1
f' : nat -> nat
def_f' : forall x, f' x = x + 1
Why must they be? Isn't a definition just a kind of knowledge about a thing? In Coq there is a difference in that f 4 evaluates to 5, whereas f' 4 is already in normal form (and you have to do some trickery with = to get 5 out of it). But it seems to me that evaluation is just a sort of tactic, and should not be any more essential than that. This implies that a construction is just a special form of assumption. So my vision:
ASSUMPTIONS
-----------
nat : *
(+) : nat -> nat -> nat
CONSTRUCTIONS
-------------
f : nat -> nat
f x := x + 1
Ought to be equivalent to
ASSUMPTIONS
-----------
nat : *
(+) : nat -> nat -> nat
f : nat -> nat
def_f : forall x, f x = x + 1
With the caveat that in the latter case we are not sure whether f actually exists.
Indeed, if we type the definition information
def_f : forall x : nat, f x = x + 1
then the type information f : nat -> nat is somewhat redundant (as in IXi)... we might say that f can be applied any argument whatsoever, but we only have information about the result when the argument is a nat. Since it is the information we crave, this is as good as saying it can only take nats.
f : nat -> nat is redundant if we have the following axioms for ->:
forall f, (forall x:A, f x : B) -> (f : A -> B)
forall f, (f : A -> B) -> (forall x:A, f x : B)
Which is um... a little circular. I suppose it is not circular since it is not a "definition", just a property. Here : is being used as an ordinary relation, meaning that things can have multiple types. In a land where things are not defined but only properties about them are mentioned, this makes sense.