I develop a basic theory of content within the framework of truthmaker semantics and, in the second part, consider some of the applications to subject matter, common content, logical subtraction and ground.

In the Böhm theorem workshop on Crete, Zoran Petric called Statman’s “Typical Ambiguity theorem” the typed Böhm theorem. Moreover, he gave a new proof of the theorem based on set-theoretical models of the simply typed lambda calculus. In this paper, we study the linear version of the typed Böhm theorem on a fragment of Intuitionistic Linear Logic. We show that in the multiplicative fragment of intuitionistic linear logic without the multiplicative unit the weak typed Böhm theorem holds. The system IMLL (...) exactly corresponds to the linear lambda calculus with multiplicative pairing. The system IMLL also exactly corresponds to the free symmetric monoidal closed category without the unit object. As far as we know, our separation result is the first one with regard to these systems in a purely syntactical manner. (shrink)

Sufficient conditions for first-order-based sequent calculi to admit cut elimination by a Schütte–Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related to the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic modal (...) logic S4, and classical and intuitionistic linear logic and some of its fragments. Moreover the conditions are such that there is an algorithm for checking if they are satisfied by a sequent calculus. (shrink)

The description of resources in game semantics has never achieved the simplicity and precision of linear logic, because of the misleading conception that linear logic is more primitive than game semantics. Here, we defend the opposite view, and thus advocate that game semantics is conceptually more primitive than linear logic. This revised point of view leads us to introduce tensor logic, a primitive variant of linear logic where negation is not involutive. After formulating its categorical semantics, we interpret tensor logic (...) in a model based on Conway games equipped with a notion of payoff, in order to reflect the various resource policies of the logic: linear, affine, relevant or exponential. (shrink)

The paper is concerned with a logical difficulty which Lionel Shapiro’s deflationist theory of logical consequence (as well as the author’s favoured, non-deflationist theory) gives rise to. It is argued that Shapiro’s non-contractive approach to solving the difficulty, although correct in its broad outlines, is nevertheless extremely problematic in some of its specifics, in particular in its failure to validate certain intuitive rules and laws associated with the principle of modus ponens. An alternative non-contractive theory is offered which does not (...) suffer from the same problem. (shrink)

Grammar can be formulated as a kind of substructural propositional logic. In support of this claim, we survey bare Gentzen style deductive systems and two kinds of non-commutative linear logic: intuitionistic and compact bilinear logic. We also glance at their categorical refinements.

In this paper, I discuss the analysis of logic in the pragmatic approach recently proposed by Brandom. I consider different consequence relations, formalized by classical, intuitionistic and linear logic, and I will argue that the formal theory developed by Brandom, even if provides powerful foundational insights on the relationship between logic and discursive practices, cannot account for important reasoning patterns represented by non-monotonic or resource-sensitive inferences. Then, I will present an incompatibility semantics in the framework of linear logic which allow (...) to refine Brandom’s concept of defeasible inference and to account for those non-monotonic and relevant inferences that are expressible in linear logic. Moreover, I will suggest an interpretation of discursive practices based on an abstract notion of agreement on what counts as a reason which is deeply connected with linear logic semantics. (shrink)

We take a fresh look at the logics of informational dependence and independence of Hintikka and Sandu and Väänänen, and their compositional semantics due to Hodges. We show how Hodges’ semantics can be seen as a special case of a general construction, which provides a context for a useful completeness theorem with respect to a wider class of models. We shed some new light on each aspect of the logic. We show that the natural propositional logic carried by the semantics (...) is the logic of Bunched Implications due to Pym and O’Hearn, which combines intuitionistic and multiplicative connectives. This introduces several new connectives not previously considered in logics of informational dependence, but which we show play a very natural rôle, most notably intuitionistic implication. As regards the quantifiers, we show that their interpretation in the Hodges semantics is forced, in that they are the image under the general construction of the usual Tarski semantics; this implies that they are adjoints to substitution, and hence uniquely determined. As for the dependence predicate, we show that this is definable from a simpler predicate, of constancy or dependence on nothing. This makes essential use of the intuitionistic implication. The Armstrong axioms for functional dependence are then recovered as a standard set of axioms for intuitionistic implication. We also prove a full abstraction result in the style of Hodges, in which the intuitionistic implication plays a very natural rôle. (shrink)

This article presents an analysis of Gödel's dialectica interpretation via a refinement of intuitionistic logic known as linear logic. Linear logic comes naturally into the picture once one observes that the structural rule of contraction is the main cause of the lack of symmetry in Gödel's interpretation. We use the fact that the dialectica interpretation of intuitionistic logic can be viewed as a composition of Girard's embedding of intuitionistic logic into linear logic followed by de Paiva's dialectica interpretation of linear (...) logic. We then investigate the various properties of the dialectica interpretation, such as the characterisation theorem, and variants of Gödel's interpretation within the linear logic context. The role of contraction in extensions to classical logic, arithmetic and analysis is also discussed. (shrink)

This paper contributes to the theory of hybrid substructural logics, i.e. weak logics given by a Gentzen-style proof theory in which there is only alimited possibility to use structural rules. Following the literture, we use an operator to mark formulas to which the extra structural rules may be applied. New in our approach is that we do not see this as a modality, but rather as themeet of the marked formula with a special typeQ. In this way we can make (...) the specific structural behaviour of marked formulas more explicit.The main motivation for our approach is that we can provide a nice, intuitive semantics for hybrid substructural logics. Soundness and completeness for this semantics are proved; besides this we consider some proof-theoretical aspects like cut-elimination and embeddings of the strong system in the hybrid one. (shrink)

In this paper, we consider multiplicative-additive fragments of affine propositional classical linear logic extended with n-contraction. To be specific, n-contraction (n 2) is a version of the contraction rule where (n+ 1) occurrences of a formula may be contracted to n occurrences. We show that expansions of the linear models for (n + 1)- valued ukasiewicz logic are models for the multiplicative-additive classical linear logic, its affine version and their extensions with n-contraction. We prove the finite axiomatizability for the classes (...) of finite models, as well as for the class of infinite linear models based on the set of rational numbers in the interval [0, 1]. The axiomatizations obtained in a Gentzen-style formulation are equivalent to finite and infinite-valued ukasiewicz logics. (shrink)

In this paper, we introduce connectification operators for intuitionistic and classical linear algebras corresponding to linear logic and to some of its extensions withn-contraction. In particular,n-contraction (n2) is a version of the contraction rule, wheren+1 occurrences of a formula may be contracted ton occurrences. Since cut cannot be eliminated from the systems withn-contraction considered most of the standard proof-theoretic techniques to investigate meta-properties of those systems are useless. However, by means of connectification we establish the disjunction property for both intuitionistic (...) and classical affine linear logics withn-contraction. (shrink)

Each Girard quantale (i.e., commutative quantale with a selected dualizing element) provides a support for a semantics for linear propositional formulas (but not for linear derivations). Several constructions of Girard quantales are known. We give two more constructions, one using an arbitrary partially ordered monoid and one using a partially ordered group (both commutative). In both cases the semantics can be controlled be a relation between pairs of elements of the support and formulas. This gives us a neat way of (...) handling duality. (shrink)

Wansing’s extended intuitionistic linear logic with strong negation, called WILL, is regarded as a resource-conscious refinment of Nelson’s constructive logics with strong negation. In this paper, (1) the completeness theorem with respect to phase semantics is proved for WILL using a method that simultaneously derives the cut-elimination theorem, (2) a simple correspondence between the class of Petri nets with inhibitor arcs and a fragment of WILL is obtained using a Kripke semantics, (3) a cut-free sequent calculus for WILL, called twist (...) calculus, is presented, (4) a strongly normalizable typed λ-calculus is obtained for a fragment of WILL, and (5) new applications of WILL in medical diagnosis and electric circuit theory are proposed. Strong negation in WILL is found to be expressible as a resource-conscious refutability, and is shown to correspond to inhibitor arcs in Petri net theory. (shrink)

We examine the notion of conditionals and the role of conditionals in inductive logics and arguments. We identify three mistakes commonly made in the study of, or motivation for, non-classical logics. A nonmonotonic consequence relation based on evidential probability is formulated. With respect to this acceptance relation some rules of inference of System P are unsound, and we propose refinements that hold in our framework.

In this paper we study the relations between the fragment L of classical logic having just conjunction and disjunction and the variety D of distributive lattices, within the context of Algebraic Logic. We prove that these relations cannot be fully expressed either with the tools of Blok and Pigozzi's theory of algebraizable logics or with the use of reduced matrices for L. However, these relations can be naturally formulated when we introduce a new notion of model of a sequent calculus. (...) When applied to a certain natural calculus for L, the resulting models are equivalent to a class of abstract logics (in the sense of Brown and Suszko) which we call distributive. Among other results, we prove that D is exactly the class of the algebraic reducts of the reduced models of L, that there is an embedding of the theories of L into the theories of the equational consequence (in the sense of Blok and Pigozzi) relative to D, and that for any algebra A of type (2,2) there is an isomorphism between the D-congruences of A and the models of L over A. In the second part of this paper (which will be published separately) we will also apply some results to give proofs with a logical flavour for several new or well-known lattice-theoretical properties. (shrink)

The author presents a deduction system for Quantum Logic. This system is a combination of a natural deduction system and rules based on the relation of compatibility. This relation is the logical correspondant of the commutativity of observables in Quantum Mechanics or perpendicularity in Hilbert spaces. Contrary to the system proposed by Gibbins and Cutland, the natural deduction part of the system is pure: no algebraic artefact is added. The rules of the system are the rules of Classical Natural Deduction (...) in which is added a control of contexts using the compatibility relation. The author uses his system to prove the following theorem: if propositions of a quantum logical propositional calculus system are mutually compatible, they form a classical subsystem. (shrink)

Pentus (1992) proves the equivalence of LCG's and CFG's, and CFG's are equivalent to BCG's by the Gaifman theorem (Bar-Hillel et al., 1960). This paper provides a procedure to extend any LCG to an equivalent BCG by affixing new types to the lexicon; a procedure of that kind was proposed as early, as Cohen (1967), but it was deficient (Buszkowski, 1985). We use a modification of Pentus' proof and a new proof of the Gaifman theorem on the basis of the (...) Lambek calculus. (shrink)

We present a semantic study of a family of modal intuitionistic linear systems, providing various logics with both an algebraic semantics and a relational semantics, to obtain completeness results. We call modality a unary operator on formulas which satisfies only one rale (regularity), and we consider any subsetW of a list of axioms which defines the exponential of course of linear logic. We define an algebraic semantics by interpreting the modality as a unary operation on an IL-algebra. Then we introduce (...) a relational semantics based on pretopologies with an additional binary relationr between information states. The interpretation of is defined in a suitable way, which differs from the traditional one in classical modal logic. We prove that such models provide a complete semantics for our minimal modal system, as well as, by requiring the suitable conditions onr (in the spirit of correspondence theory), for any of its extensions axiomatized by any subsetW as above. We also prove an embedding theorem for modal IL-algebras into complete ones and, after introducing the notion of general frame, we apply it to obtain a duality between general frames and modal IL-algebras. (shrink)

Logic has pride of place in mathematics and its 20th century offshoot, computer science. Modern symbolic logic was developed, in part, as a way to provide a formal framework for mathematics: Frege, Peano, Whitehead and Russell, as well as Hilbert developed systems of logic to formalize mathematics. These systems were meant to serve either as themselves foundational, or at least as formal analogs of mathematical reasoning amenable to mathematical study, e.g., in Hilbert’s consistency program. Similar efforts continue, but have been (...) expanded by the development of sophisticated methods to study the properties of such systems using proof and model theory. In parallel with this evolution of logical formalisms as tools for articulating mathematical theories (broadly speaking), much progress has been made in the quest for a mechanization of logical inference and the investigation of its theoretical limits, culminating recently in the development of new foundational frameworks for mathematics with sophisticated computer-assisted proof systems. In addition, logical formalisms developed by logicians in mathematical and philosophical contexts have proved immensely useful in describing theories and systems of interest to computer scientists, and to some degree, vice versa. Three examples of the influence of logic in computer science are automated reasoning, computer verification, and type systems for programming languages. (shrink)

Some think that logic concerns the “laws of truth”; others that logic concerns the “laws of thought.” This paper presents a way to reconcile both views by building a bridge between truth-maker theory, à la Fine, and normative bilateralism, à la Restall and Ripley. The paper suggests a novel way of understanding consequence in truth-maker theory and shows that this allows us to identify a common structure shared by truth-maker theory and normative bilateralism. We can thus transfer ideas from normative (...) bilateralism to truth-maker theory, such as non-transitive solutions to paradox, and vice versa, such as notions of factual equivalence and containment. (shrink)

To investigate the relationship between logical reasoning and majority voting, we introduce logic with groups Lg in the style of Gentzen’s sequent calculus, where every sequent is indexed by a group of individuals. We also introduce the set-theoretical semantics of Lg, where every formula is interpreted as a certain closed set of groups whose members accept that formula. We present the cut-elimination theorem, and the soundness and semantic completeness theorems of Lg. Then, introducing an inference rule representing majority voting to (...) Lg, we introduce logic with majority voting Lv. Formalizing the discursive paradox in judgment aggregation theory, we show that Lv is inconsistent. Based on the premise-based and conclusion-based approaches to avoid the paradox, we introduce logic with majority voting for axioms Lva, where majority voting is applied only to non-logical axioms as premises to construct a proof in Lg, and logic with majority voting for conclusions Lvc, where majority voting is applied only to the conclusion of a proof in Lg. We show that both Lva and Lvc are syntactically complete and consistent, and we construct collective judgments based on the provability in Lva and Lvc, respectively. Then, we discuss how these systems avoid the discursive paradox. (shrink)

The paper introduces a new type of rules into Natural Deduction, elimination rules by composition. Elimination rules by composition replace usual elimination rules in the style of disjunction elimination and give a more direct treatment of additive disjunction, multiplicative conjunction, existence quantifier and possibility modality. Elimination rules by composition have an enormous impact on proof-structures of deductions: they do not produce segments, deduction trees remain binary branching, there is no vacuous discharge, there is only few need of permutations. This new (...) type of rules fits especially to substructural issues, so it is shown for Lambek Calculus, i.e. intuitionistic non-commutative linear logic and to its extensions by structural rules like permutation, weakening and contraction. Natural deduction formulated with elimination rules by composition from a complexity perspective is superior to other calculi. (shrink)

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)

This research article revisits Hempel’s logic of confirmation in light of recent developments in categorical proof theory. While Hempel advocated several logical conditions in favor of a purely syntactical definition of a general non-quantitative concept of confirmation, we show how these criteria can be associated to specific logical properties of monoidal modal deductive systems. In addition, we show that many problems in confirmation logic, such as the tacked disjunction, the problem of weakening with background knowledge and the problem of irrelevant (...) conjunction, are also associated with specific logical properties and, incidentally, with some of Hempel’s logical conditions of adequacy. We discuss the raven paradox together with further objections against Hempel’s approach, showing how our analysis enables a clear understanding of the relationships between Hempel’s conditions, the problems in confirmation logic, and the properties of deductive systems. (shrink)

We group the existing variants of the familiar set-theoretical and truth-theoretical paradoxes into two classes: connective paradoxes, which can in principle be ascribed to the presence of a contracting connective of some sort, and structural paradoxes, where at most the faulty use of a structural inference rule can possibly be blamed. We impute the former to an equivocation over the meaning of logical constants, and the latter to an equivocation over the notion of consequence. Both equivocation sources are tightly related, (...) and can be cleared up by adopting a particular substructural logic in place of classical logic. We then argue that our perspective can be justified via an informational semantics of contraction-free substructural logics. (shrink)

We discuss the logic of pregroups, introduced by Lambek [34], and its connections with other type logics and formal grammars. The paper contains some new ideas and results: the cut-elimination theorem and a normalization theorem for an extended system of this logic, its P-TIME decidability, its interpretation in L1, and a general construction of (preordered) bilinear algebras and pregroups whose universe is an arbitrary monoid.

The aim of this paper is to argue that logic can play an important role in the “toolbox” of molecular biology. We show how biochemical pathways, i.e., transitions from a molecular aggregate to another molecular aggregate, can be viewed as deductive processes. In particular, our logical approach to molecular biology — developed in the form of a natural deduction system — is centered on the notion of Curry-Howard isomorphism, a cornerstone in nineteenth-century proof-theory.

This paper presents a coherence theorem for star-autonomous categories exactly analogous to Kelly and Mac Lane’s coherence theorem for symmetric monoidal closed categories. The proof of this theorem is based on a categorial cut-elimination result, which is presented in some detail.

In this document, we study a 3-polygraphic translation for the proofs of SKS, a formal system for classical propositional logic. We prove that the free 3-category generated by this 3-polygraph describes the proofs of classical propositional logic modulo structural bureaucracy. We give a 3-dimensional generalization of Penrose diagrams and use it to provide several pictures of a proof. We sketch how local transformations of proofs yield a non contrived example of 4-dimensional rewriting.

This work deals with the exponential fragment of Girard's linear logic without the contraction rule, a logical system which has a natural relation with the direct logic . A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a special treatment of the propositional constants, so that the process of cut-elimination can be performed using only “local” reductions. Hence a typed calculus, which admits only local rewriting rules, can be (...) introduced in a natural manner. Its main properties — normalizability and confluence — has been investigated; moreover this calculus has been proved to satisfy a Curry-Howard isomorphism with respect to the logical system in question. MSC: 03B40, 03F05. (shrink)

We show that every MALL proof-structure [9] satisfies the property of softness, originally a categorical notion introduced by Joyal. Furthermore, we show that the notion of hereditary softness precisely captures Girard’s algebraic restriction of the technical condition on proof-structures. Relying on this characterization, we prove a MALL+Mix sequentialization theorem by a proof-theoretical method, using Girard’s notion of jump. Our MALL+Mix correctness criterion subsumes the Danos/Fleury-Retoré criterion [6] for MLL+Mix.

If all dependent expressions were adjacent some variety of immediate constituent analysis would suffice for grammar, but syntactic and semantic mismatches are characteristic of natural language; indeed this is a, or the, central problem in grammar. Logical categorial grammar reduces grammar to logic: an expression is well-formed if and only if an associated sequent is a theorem of a categorial logic. The paradigmatic categorial logic is the Lambek calculus, but being a logic of concatenation the Lambek calculus can only capture (...) discontinuous dependencies when they are peripheral. In this paper we present the displacement calculus, which is a logic of intercalation as well as concatenation and which subsumes the Lambek calculus. On the empirical side, we apply the new calculus to discontinuous idioms, quantification, VP ellipsis, medial extraction, pied-piping, appositive relativisation, parentheticals, gapping, comparative subdeletion, cross-serial dependencies, reflexivization, anaphora, dative alternation, and particle shift. On the technical side, we prove that the calculus enjoys Cut-elimination. (shrink)

We present a reading of the traditional syllogistics in a fragment of the propositional intuitionistic multiplicative linear logic and prove that with respect to a diagrammatic logical calculus that we introduced in a previous paper, a syllogism is provable in such a fragment if and only if it is diagrammatically provable. We extend this result to syllogistics with complemented terms à la De Morgan, with respect to a suitable extension of the diagrammatic reasoning system for the traditional case and a (...) corresponding reading of such De Morgan style syllogistics in the previously referred to fragment of linear logic. (shrink)

Logics that do not have a deduction-detachment theorem (briefly, a DDT) may still possess a contextual DDT —a syntactic notion introduced here for arbitrary deductive systems, along with a local variant. Substructural logics without sentential constants are natural witnesses to these phenomena. In the presence of a contextual DDT, we can still upgrade many weak completeness results to strong ones, e.g., the finite model property implies the strong finite model property. It turns out that a finitary system has a contextual (...) DDT iff it is protoalgebraic and gives rise to a dually Brouwerian semilattice of compact deductive filters in every finitely generated algebra of the corresponding type. Any such system is filter distributive, although it may lack the filter extension property. More generally, filter distributivity and modularity are characterized for all finitary systems with a local contextual DDT, and several examples are discussed. For algebraizable logics, the well-known correspondence between the DDT and the equational definability of principal congruences is adapted to the contextual case. (shrink)

Many logics in the relevant family can be given a proof theory in the style of Belnap's display logic. However, as originally given, the proof theory is essentially more expressive than the logics they seek to model. In this paper, we consider a modified proof theory which more closely models relevant logics. In addition, we use this proof theory to show decidability for a large range of substructural logics.

We study a multiple-succedent sequent calculus with both of the structural rules Left Weakening and Left Contraction but neither of their counterparts on the right, for possible application to the treatment of multiplicative disjunction against the background of intuitionistic logic. We find that, as Hirokawa dramatically showed in a 1996 paper with respect to the rules for implication, the rules for this connective render derivable some new structural rules, even though, unlike the rules for implication, these rules are what we (...) call ipsilateral: applying such a rule does not make any formula change sides—from the left to the right of the sequent separator or vice versa. Some possibilities for a semantic characterization of the resulting logic are also explored. The paper concludes with three open questions. (shrink)

In this paper we study families of resource aware logics that explore resource restriction on rules; in particular, we study the use of controlled cut-rule and introduce three families of parameterised logics that arise from different ways of controlling the use of cut. We start with a formulation of classical logic in which cut is non-eliminable and then impose restrictions on the use of cut. Three Cut-and-Pay families of logics are presented, and it is shown that each family provides an (...) approximation process for full propositional classical logic when the control over the use of cut is progressively weakened. A sound and complete semantics is given for each component of each of the three families of approximated logics. One of these families is shown to possess the uniform substitution property, a new result for approximated reasoning. A tableau based decision procedure is presented for each element of the approximation families and the complexity of each decision procedure is studied. We show that there are families in which every component logic can be decided polynomially. (shrink)

This paper gives a simple method for providing categorial brands of feature-based unification grammars with a model-theoretic semantics. The key idea is to apply the paradigm of fibred semantics (or layered logics, see Gabbay (1990)) in order to combine the two components of a feature-based grammar logic. We demonstrate the method for the augmentation of Lambek categorial grammar with Kasper/Rounds-style feature logic. These are combined by replacing (or annotating) atomic formulas of the first logic, i.e. the basic syntactic types, by (...) formulas of the second. Modelling such a combined logic is less trivial than one might expect. The direct application of the fibred semantics method where a combined atomic formula like np (num: sg & pers: 3rd) denotes those strings which have the indicated property and the categorial operators denote the usual left- and right-residuals of these string sets, does not match the intuitive, unification-based proof theory. Unification implements a global bookkeeping with respect to a proof whereas the direct fibring method restricts its view to the atoms of the grammar logic. The solution is to interpret the (embedded) feature terms as global feature constraints while maintaining the same kind of fibred structures. For this adjusted semantics, the anticipated proof system is sound and complete. (shrink)

This paper critically examines logical instrumentalism as it has been put forth recently in the anti-exceptionalism about logic debate. I will argue that if one wishes to uphold the claim that logic is significantly similar to science, as the anti-exceptionalists have it, then logical instrumentalism cannot be what previous authors have taken it to be. The reason for this, I will argue, is that as the position currently stands, first, it reduces to a trivial claim about the instrumental value of (...) logical systems, and second, by its denial that logic aims to account for extra-systemic phenomena it significantly differs from science, in contrast with the AEL agenda. I will conclude by proposing a different kind of logical instrumentalism that I take to have a broad appeal, but especially for anti-exceptionalists, for it is developed as analogous to—and thus much closer aligned with—scientific instrumentalism. (shrink)

We show that numerous distinctive concepts of constructive mathematics arise automatically from an “antithesis” translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically “constructivize” classical definitions, handling the resulting bookkeeping automatically.

The notion of affordance remains elusive, notwithstanding its importance for the representation of agency, cognition, and behaviors. This paper lays down a foundation for an ontology of affordances by elaborating the idea of “core affordance” which would serve as a common ground for explaining existing diverse conceptions of affordances and their interrelationships. For this purpose, it analyzes M. T. Turvey’s dispositional theory of affordances in light of a formal ontology of dispositions. Consequently, two kinds of so-called “core affordances” are proposed: (...) specific and general ones. Inspired directly by Turvey’s original account, a specific core affordance is intimately connected to a specific agent, as it is reciprocal with a counterpart effectivity (which is a disposition) of this agent within the agent-environment system. On the opposite, a general core affordance does not depend on individual agents; rather, its realization involves an action by an instance of a determinate class of agents. The utility of such core affordances is illustrated by examining how they can be leveraged to formalize other major accounts of affordances. Additionally, it is briefly outlined how core affordances can be employed to analyze three notions that are closely allied with affordances: the environment, image schemas, and intentions. (shrink)

The method of morphisms is a well-known application of Dialectica categories to set theory. In a previous work, Valeria de Paiva and the author have asked how much of the Axiom of Choice is needed in order to carry out the referred applications of such method. In this paper, we show that, when considered in their full generality, those applications of Dialectica categories give rise to equivalents of either the Axiom of Choice or Partition Principle —which is a consequence of (...) $\textbf{AC}$ whose precise status of its relationship with$\textbf{AC}$ itself is an open problem for more than a hundred years. (shrink)

Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that (...) sequent calculi are more amenable to extensive investigation using the tools of proof theory, such as cut-elimination and rule invertibility, hence allowing a full analysis of the notion of Ecumenical entailment. We then present some extensions of the Ecumenical sequent system and show that interesting systems arise when restricting such calculi to specific fragments. This approach of a unified system enabling both classical and intuitionistic features sheds some light not only on the logics themselves, but also on their semantical interpretations as well as on the proof theoretical properties that can arise from combining logical systems. (shrink)

The category of coherent phase spaces introduced by the author is a refinement of the symplectic “category” of A. Weinstein. This category is *-autonomous and thus provides a denotational model for Multiplicative Linear Logic. Coherent phase spaces are symplectic manifolds equipped with a certain extra structure of “coherence”. They may be thought of as “infinitesimal” analogues of familiar coherent spaces of Linear Logic. The role of cliques is played by Lagrangian submanifolds of ambient spaces. Physically, a symplectic manifold is the (...) phase space of a classical dynamical system, and a Lagrangian submanifold is a phase of a short-wave oscillation. Typically, Lagrangian submanifolds represent such objects as short-wave approximations of wave functions in asymptotic quantization and wave fronts in geometrical optics. The coherent phase space semantics was motivated to a large extent by methods of geometric and asymptotic quantization and suggests some interesting intuitions on Linear Logic. In particular Lagrangian submanifold-cliques of types A and A can be interpreted as semiclassical limits of eigenstates of respectively position and momentum observables. These observables being canonically conjugate cannot be measured simultaneously, which corresponds to the idea that a formula A and its negation A cannot both simultaneously have proofs . We show that the coherent phase space semantics of Linear Logic enjoys several completeness properties in general much stronger than the usual full completeness with respect to the class of dinatural transformations. These properties of completeness in conjunction with a quite natural -physical meaning make the coherent phase space semantics an interesting object of investigation. (shrink)