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 11 of 11
Does some version of modal type theory meet your wishes, see e.g., this tutorial? With homotopy type theory allowing propositions as kinds of type, and types themselves being taken as elements of a universe of types, the distinction you’re pointing out between functions applied to terms and modal operators applied to propositions is diminished.
logics with user-defined modal operators, effectively - logics which allow users to define functions (e.g. to act as polyadic modal operators) that can accept sentences (propositions, formulas) as arguments and that allow users to define (and fine tune) non-logical axioms on such user defined functions?
This sounds to me like you just want a logical framework. Right now I happen to be experimenting with Isabelle, which seems to be quite a reasonable logical framework for practical work with user-specified predicate logics (as opposed to, say, Twelf, which is adapted instead for metatheoretic reasoning about user-specified logics). I’m not sure how well it would do for dependent type theories though.
the meaning of variables in https://isabelle.in.tum.de/dist/library/Sequents/Sequents/Sequents.html and other files are forgotten
Could you give a link? I’m using Isabelle’s Sequents library myself right now and I haven’t experienced any problems that I would describe as “the meaning of variables are forgotten”.
I don’t think being old is a problem as long as it works. My own experience so far is that Isabelle/Sequents is much easier and more convenient than Coq for practical work in a sequent calculus; although perhaps I just never found the right way to code it up in Coq. The tactic language in Isabelle seems fairly good (including Eisbach, which is inspired by Ltac). You just have to put up with the Isabelle documentation unaccountably moaning about things like referring to variables by name (!) being “considered harmful”.
As for your original question, I think I can’t really tell what it is you are looking for, and why existing tools don’t satisfy you, without some examples (maybe it is a language barrier).
I’m not sure why you’re discouraged by that reply of Paulson. It seems to me he was just saying that he personally didn’t understand the details. But in any substantial software development, no one person will understand all the details. There are plenty of details of the Coq kernel that hardly anyone understands (maybe even no one understands completely), so I don’t know why switching to Coq would be any better in this respect.
I don’t understand the details of the Isabelle Sequents module, but it’s fairly short and I think if I took the time to learn the ML syntax I could probably understand it fairly easily. As far as I can see, the only real “magic” it’s doing is at the parsing stage (which is of course irrelevant to semantics), plus the cute trick of representing lists by the operation of concatenating with them so that concatenation becomes definitionally associative. (Floris van Doorn recently used a similar trick to formalize homomorphisms of graded groups of nonzero degree in Lean.)
I’ll take a look at your other links when I have a chance. (You can make hyperlinks with [markdown syntax](http://a.web.site).)
Parametrized HOAS is a neat trick; maybe not quite as convenient as true HOAS, but nice.
I’m kind of bothered by the need for “parametricity axioms” that are false in natural set-theoretic models. This is to me much more problematic, since it means one would have to go through some contortions in order to prove that the theory thus represented has in fact all the models one would want. With true HOAS in a logical framework without inductive types, like Isabelle or Twelf, I believe one can literally interpret the logical framework theory in a model and thereby obtain models of the object language as well.
On the other hand, it could be that those axioms are not necessary for “practical” work in the object language but only to prove metatheorems about it? It’s hard for me to tell because the article is largely focused on metatheory, and even in the github repo I had trouble finding any substantial examples of work in the object language. That also makes it hard for me to assess the practicality of such an encoding for such substantial work.
Also, does parametrized HOAS generalize to multi-sorted predicate logic? With the domains of binder arguments having to range over all types, it’s not obvious to me how to “tag” them with the information that the argument must belong to some particular object-language type.
Just for reference - another message from L.P. suggesting directions for automation of sequent calculus and logics: message
1 to 11 of 11