Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthortomr
    • CommentTimeJun 18th 2018
    I know only logics whose predicates and functions accept terms as arguments and all the modal operators are defined at the logical level and only modla operators and connectives can accept sentences (propositions, formulas) as arguments, usual functions and prediactes can not do this.

    But are there efforts to create 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?

    Such feature would be essential for formal semantics of natural language. Of course, the verb BELIEVE(subject, sentence) can be modelled as usual model operator in doxastic logic, but there can be many more shades of belief modality - subject, web tense, degrees of belief strength and so on, so on. Clearly to capture all those possibilties one should move the definition of modal operators from the logical language to the non logical language (where the usual functions reside).

    So - are there efforts to define and research such logics?

    I am aware of the book "Toward Predicate Approaches to Modality" whose opening chapter states, that modality could be modelled as the predicate on the sentence name (sic! - sentence name)! I am still studying this book, maybe it will provide solution for me.
    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 18th 2018

    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.

    • CommentRowNumber3.
    • CommentAuthortomr
    • CommentTimeJun 18th 2018
    I will have a look on type theory, in fact, type theory would be welcome shift, because I am planning to use Coq (and Calculus of Inductive Constructions) for implementation of the logic if I will not found relevant custom theorem prover. I am suspicious about HoTT because (I don't remember reference) it is in quite low position in the lambda cube (not the most general lambda-P-omega). But many thanks for directions, I will certainly investigate this idea!
    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJun 18th 2018

    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.

    • CommentRowNumber5.
    • CommentAuthortomr
    • CommentTimeJun 18th 2018
    I have negative experience with Isabelle/HOL and automation of logics. The already existing implementations are quitė promising, but they are old (including non-Isar syntax) and even L. C. Paulson, FRS, himself acknowledged in one forum communication, that the meaning of variables in and other files are forgotten. That is why I have switched to Coq, e.g. Of course, Isabelle/HOL has Archive of Formalized Proofs - incredible resource, Coq has less defined completed works. Though, this all is offtopic.

    Every automation of the logics of which I am aware of, defines the modal operators in the logic itself. But it would be nice to define modal operators at the level of functions and predicates (well, one can be even more greedy and would like to define connectives at this level too, but at present there is no need for this, connectives are quite stable constructions) and e.g. maybe even allow quantifiers to run over functions, predicates and modal operators (though this isn't requirement also). So - if we pursure the traditional path of logical frameworks, then we have to build new logic for each new set of modal operators and we are required to build new logic even in the case when we just tune the axioms of the modal operators. Such rebuild would not be required if modal operators and their axioms existed in non-logical level, e.g. if one allows to have functions and predicates with sentence arguments.

    HoTT ir promising approach and I am investigating it. Of course, one is eager to seek what is Curry-Howard partner to the HoTT...
    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeJun 18th 2018

    the meaning of variables in 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).

    • CommentRowNumber7.
    • CommentAuthortomr
    • CommentTimeJun 24th 2018
    • (edited Jun 24th 2018)
    About sequent calculus in Isabelle - here is the question about some meaning of variables:
    And here is some discouraging reply by Lawrence Paulson:

    Of course, I am aware of (there is chapter about sequents module) but still I can not grasp whats going on. If someone better understand sequents in Isabelle/HOL (and the general process of object logics in Isabelle) then it could be greated idea to write some contribution or clarification to this document. Of course, it would be great to share notes here as well. Maybe Isabelle is good.

    So, I had no other chance than to switch to Coq.

    Regarding implementations of logics in Coq, I am aware of two directions:
    - older one: - purely syntactic approach
    - pretty modern one: - using higher order parametrized synatx by Chipala and also providing metatheorems - more extended work, but not in English
    It is also quite hard, but presentation is good (article contains link to complete GitHub repository of Coq code). But there is something misterious about this paper - it is not officially published, at least DBPL does not contain entry for it, although it seems to be that is very good paper.

    Regarding my initial question - Dynamic Logic - seems to have something similar what I sought: action operators can server as modal operators and dynamic logic allows the user of logic to creat arbitrary action operators like functions or predicates. I am reading about it further.
    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeJun 25th 2018

    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](

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJun 25th 2018

    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.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJun 25th 2018

    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.

    • CommentRowNumber11.
    • CommentAuthortomr
    • CommentTimeJun 26th 2018
    • (edited Jun 26th 2018)

    Just for reference - another message from L.P. suggesting directions for automation of sequent calculus and logics: message