A number of general points behind the story of this paper may be worth setting out separately, now that we have come to the end.There is perhaps one obvious omission to be addressed right away. Although the word “information” has occurred throughout this paper, it must have struck the reader that we have had nothing to say on what information is. In this respect, our theories may be like those in physics: which do not explain what “energy” is (a notion (...) which seems quite similar to “information” in several ways), but only give some basic laws about its behaviour and transmission.The eventual recommendation made here has been to use a broad type-theoretic framework for studying various more classical and more dynamic notions of proposition in their interaction. This is not quite the viewpoint advocated by many current authors in the area, who argue for a whole-sale switch from a ‘static’ to a ‘dynamic’ perspective on propositions. This is not the place, however, to survey the conceptual arguments for and against such a more radical move.This still leaves many questions about possible reductions from one perspective to another. For instance, it would seem that classical systems ought to serve as a ‘limiting case’, which should still be valid after procedural details of some cognitive process have been forgotten. There are various ways of implementing the desired correspondence: e.g. by considering extreme cases with ⫅ equal to identity, or, in the pure relational algebra framework by considering only pairs (x, x). What we shall want then are reductions of dynamic logics, in those special cases, to classical logic. But perhaps also, more sophisticated views are possible. How do we take a piece of ‘dynamic’ prose, remove control instructions and the like, and obtain a piece of ‘classical’ text, suitable for inference ‘in the light of eternity’?There is also a more technical side to the matter of ‘reduction’. By now, Logic has reached such a state of ‘inter-translatability’ that almost all known variant logics can be embedded into each other, via suitable translations. In particular, once an adequate semantic has been given for a new system, this usually induces an embedding into standard logic: as we know, e.g., for the case of Modal Logic. Like-wise, all systems of dynamic interpretation or inference proposed so far admit of direct embedding into an ordinary ‘static’ predicate logic having explicit transition predicates (cf. van Benthem 1988b). Thus, our moral is this. The issue is not whether the new systems of information structure or processing are essentially beyond the expressive resources of traditional logical systems: for, they are not. The issue is rather which interesting phenomena and questions will be put into the right focus by them.The next broad issue concerns the specific use of the perspective proposed here, vis-à-vis concrete proposals for information-oriented or dynamic semantics. The general strategy advocated here is to locate some suitable base calculus and then consider which ‘extras’ are peculiar to the proposal. For instance, this is the spirit in which modal S4 would be a base logic of information models, and intuitionistic logicthe special theory devoting itself to upward persistent propositions. Or, with the examples in Section 4.1, the underlying base logic is our relational algebra, whereas, say, ordinary updates then impose special properties, such as ‘idempotence’: $$xRy \Rightarrow yRy$$ Does this kind of application presuppose the existence of one distinguished base logic, of which all others are extensions? This would be attractive-and some form of relational algebra or linear logic might be a reasonable candidate. Nevertheless, the enterprise does not rest on this outcome. What matters is an increased sensitivity to the ‘landscape’ of dynamic logics, just as with the ‘Categorial Hierarchy’ in Categorial Grammar (cf. van Benthem 1989a, 1991) where the family of logics with their interconnections seems more important than any specific patriarch.Finally, perhaps the most important issue in the new framework is the possibility of new kinds of questions arising precisely because of its differences from standard logic. Notably, given the option of regarding propositions as programs, it will be of interest to consider systematically which major questions about programming languages now make sense inside logic too.EXAMPLE. Correctness. When do we have $$\left[\kern-0.15em\left[ \pi \right]\kern-0.15em\right](\left[\kern-0.15em\left[ A \right]\kern-0.15em\right]) \subseteq \left[\kern-0.15em\left[ B \right]\kern-0.15em\right]$$ for (s, t) propositions A, B and a dynamic (s, (s, t)) proposition π?Program Synthesis. Which dynamic proposition will take us from an information state satisfying A to one satisfying B? (This question needs refinement, lest there be trivial answers.)Determinism. Which propositions as programs are deterministic, in the sense of defining single-valued functions from states to states?Querying. What does it mean to ask for information in the present setting? (Again, individual types referring to e will be crucial here.)This is not merely an agenda for wishful thinking. Within Logic, there are various ways of introducing such concerns into semantics, especially, using tools from Automata Theory. (See van Benthem 1989c for further discussion of such computational perspectives in ‘cognitive programming’.)At least if one believes that ‘dynamics’ is of the essence in cognition (rather than a mere interfacing problem between the halls of eternal truth and the noisy streets of reality), the true test for the present enterprise is the development of a significant new research program not merely copying the questions of old. (shrink)

This work contributes to the theory of judgement aggregation by discussing a number of significant non-classical logics. After adapting the standard framework of judgement aggregation to cope with non-classical logics, we discuss in particular results for the case of Intuitionistic Logic, the Lambek calculus, Linear Logic and Relevant Logics. The motivation for studying judgement aggregation in non-classical logics is that they offer a number of modelling choices to represent agents’ reasoning in aggregation problems. By studying judgement aggregation in logics that (...) are weaker than classical logic, we investigate whether some well-known impossibility results, that were tailored for classical logic, still apply to those weak systems. (shrink)

In this paper we will discuss the first order multiplicative intuitionistic fragment of linear logic, MILL1, and its applications to linguistics. We give an embedding translation from formulas in the Lambek Calculus to formulas in MILL1 and show this translation is sound and complete. We then exploit the extra power of the first order fragment to give an account of a number of linguistic phenomena which have no satisfactory treatment in the Lambek Calculus.

The paper continues a series of results on cut-rule axiomatizability of the Lambek calculus. It provides a complete solution of a problem which was solved partially in one of the author''s earlier papers. It is proved that the product-free Lambek Calculus with the empty string (L 0) is not finitely axiomatizable if the only rule of inference admitted is Lambek''s cut rule. The proof makes use of the (infinitely) cut-rule axiomatized calculus C designed by the author exactly for this purpose.

We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill’s calculi, and focus on their fragments including multiplicative (Lambek) connectives, additive conjunction and disjunction, brackets and bracket modalities, and the! subexponential modality. For both systems, we resolve issues connected with the cut rule and provide necessary modifications, after which we prove admissibility of cut (cut elimination theorem). We also prove (...) algorithmic undecidability for both calculi, and show that categorial grammars based on them can generate arbitrary recursively enumerable languages. (shrink)

ABSTRACTMonoidal logics were introduced as a foundational framework to analyze the proof theory of logical systems. Inspired by Lambek's seminal work in categorical logic, the objective is to defin...