21 found
Sort by:
  1. Katalin Bimbó & J. Michael Dunn (2014). Extracting BB′IW Inhabitants of Simple Types From Proofs in the Sequent Calculus {LT_to^{T}} for Implicational Ticket Entailment. Logica Universalis 8 (2):141-164.
    The decidability of the logic of pure ticket entailment means that the problem of inhabitation of simple types by combinators over the base { B, B′, I, W } is decidable too. Type-assignment systems are often formulated as natural deduction systems. However, our decision procedure for this logic, which we presented in earlier papers, relies on two sequent calculi and it does not yield directly a combinator for a theorem of ${T_\to}$ . Here we describe an algorithm to extract an (...)
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  2. Katalin Bimbó & J. Michael Dunn (2013). On the Decidability of Implicational Ticket Entailment. Journal of Symbolic Logic 78 (1):214-236.
    The implicational fragment of the logic of relevant implication, $R_\to$ is known to be decidable. We show that the implicational fragment of the logic of ticket entailment, $T_\to$ is decidable. Our proof is based on the consecution calculus that we introduced specifically to solve this 50-year old open problem. We reduce the decidability problem of $T_\to$ to the decidability problem of $R_\to$. The decidability of $T_\to$ is equivalent to the decidability of the inhabitation problem of implicational types by combinators over (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  3. Katalin Bimbó (2012). Combinatory Logic: Pure, Applied, and Typed. Taylor & Francis.
    Reader-friendly without compromising the precision of exposition, the book includes many new research results not found in the available literature.
    Direct download  
     
    My bibliography  
     
    Export citation  
  4. Katalin Bimbó & J. Michael Dunn (2012). New Consecution Calculi for $R^{T}_{\To}$. Notre Dame Journal of Formal Logic 53 (4):491-509.
    The implicational fragment of the logic of relevant implication, $R_{\to}$ is one of the oldest relevance logics and in 1959 was shown by Kripke to be decidable. The proof is based on $LR_{\to}$ , a Gentzen-style calculus. In this paper, we add the truth constant $\mathbf{t}$ to $LR_{\to}$ , but more importantly we show how to reshape the sequent calculus as a consecution calculus containing a binary structural connective, in which permutation is replaced by two structural rules that involve $\mathbf{t}$ (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  5. Katalin Bimbó & J. Michael Dunn (2012). New Consecution Calculi for $R^{T}_{To}$. Notre Dame Journal of Formal Logic 53 (4):491-509.
    The implicational fragment of the logic of relevant implication, $R_{\to}$ is one of the oldest relevance logics and in 1959 was shown by Kripke to be decidable. The proof is based on $LR_{\to}$, a Gentzen-style calculus. In this paper, we add the truth constant $\mathbf{t}$ to $LR_{\to}$, but more importantly we show how to reshape the sequent calculus as a consecution calculus containing a binary structural connective, in which permutation is replaced by two structural rules that involve $\mathbf{t}$. This calculus, (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  6. Katalin Bimbó (2010). Schönfinkel-Type Operators for Classical Logic. Studia Logica 95 (3):355-378.
    We briefly overview some of the historical landmarks on the path leading to the reduction of the number of logical connectives in classical logic. Relying on the duality inherent in Boolean algebras, we introduce a new operator ( Nallor ) that is the dual of Schönfinkel’s operator. We outline the proof that this operator by itself is sufficient to define all the connectives and operators of classical first-order logic ( Fol ). Having scrutinized the proof, we pinpoint the theorems of (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  7. Katalin Bimbó, Combinatory Logic. Stanford Encyclopedia of Philosophy.
    Direct download  
     
    My bibliography  
     
    Export citation  
  8. Katalin Bimbó (2009). Dual Gaggle Semantics for Entailment. Notre Dame Journal of Formal Logic 50 (1):23-41.
    A sequent calculus for the positive fragment of entailment together with the Church constants is introduced here. The single cut rule is admissible in this consecution calculus. A topological dual gaggle semantics is developed for the logic. The category of the topological structures for the logic with frame morphisms is proven to be the dual category of the variety, that is defined by the equations of the algebra of the logic, with homomorphisms. The duality results are extended to the logic (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  9. Katalin Bimbó & J. Michael Dunn (2009). Symmetric Generalized Galois Logics. Logica Universalis 3 (1):125-152.
    Symmetric generalized Galois logics (i.e., symmetric gGl s) are distributive gGl s that include weak distributivity laws between some operations such as fusion and fission. Motivations for considering distribution between such operations include the provability of cut for binary consequence relations, abstract algebraic considerations and modeling linguistic phenomena in categorial grammars. We represent symmetric gGl s by models on topological relational structures. On the other hand, topological relational structures are realized by structures of symmetric gGl s. We generalize the weak (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  10. Katalin Bimbó, J. Michael Dunn & Roger D. Maddux (2009). Relevance Logics and Relation Algebras. Review of Symbolic Logic 2 (1):102-131.
    Relevance logics are known to be sound and complete for relational semantics with a ternary accessibility relation. This paper investigates the problem of adequacy with respect to special kinds of dynamic semantics (i.e., proper relation algebras and relevant families of relations). We prove several soundness results here. We also prove the completeness of a certain positive fragment of R as well as of the first-degree fragment of relevance logics. These results show that some core ideas are shared between relevance logics (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  11. Katalin Bimbó (2007). Functorial Duality for Ortholattices and de Morgan Lattices. Logica Universalis 1 (2):311-333.
    . Relational semantics for nonclassical logics lead straightforwardly to topological representation theorems of their algebras. Ortholattices and De Morgan lattices are reducts of the algebras of various nonclassical logics. We define three new classes of topological spaces so that the lattice categories and the corresponding categories of topological spaces turn out to be dually isomorphic. A key feature of all these topological spaces is that they are ordered relational or ordered product topologies.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  12. Katalin Bimbó (2007). LEt ® , LR °[^( ~ )], LK and Cutfree Proofs. Journal of Philosophical Logic 36 (5):557-570.
    Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  13. Katalin Bimbó (2007). LEt ® LE^{T}{ \to } , LR °[^( ~ )]LR^{ \Circ }{{\Widehat{ \Sim }}}, LK and Cutfree Proofs. Journal of Philosophical Logic 36 (5):557-570.
    Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  14. Katalin Bimbó (2007). $LE^{T}{Rightarrow}$ , $LR^{Circ}{Wedgesim}$ , LK and Cutfree Proofs. Journal of Philosophical Logic 36 (5):557 - 570.
    Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique-attributable to Gentzen-that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional (...)
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  15. Katalin Bimbó (2005). Admissibility of Cut in LC with Fixed Point Combinator. Studia Logica 81 (3):399 - 423.
    The fixed point combinator (Y) is an important non-proper combinator, which is defhable from a combinatorially complete base. This combinator guarantees that recursive equations have a solution. Structurally free logics (LC) turn combinators into formulas and replace structural rules by combinatory ones. This paper introduces the fixed point and the dual fixed point combinator into structurally free logics. The admissibility of (multiple) cut in the resulting calculus is not provable by a simple adaptation of the similar proof for LC with (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  16. Katalin Bimbó (2005). Types of I -Free Hereditary Right Maximal Terms. Journal of Philosophical Logic 34 (5/6):607 - 620.
    The implicational fragment of the relevance logic "ticket entailment" is closely related to the so-called hereditary right maximal terms. I prove that the terms that need to be considered as inhabitants of the types which are theorems of $T_\rightarrow$ are in normal form and built in all but one casefrom B, B' and W only. As a tool in the proof ordered term rewriting systems are introduced. Based on the main theorem I define $FIT_\rightarrow$ - a Fitch-style calculus (related to (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  17. Katalin Bimbó (2005). The Church-Rosser Property in Symmetric Combinatory Logic. Journal of Symbolic Logic 70 (2):536 - 556.
    Symmetic combinatory logic with the symmetric analogue of a combinatorially complete base (in the form of symmetric λ-calculus) is known to lack the Church-Rosser property. We prove a much stronger theorem that no symmetric combinatory logic that contains at least two proper symmetric combinators has the Church-Rosser property. Although the statement of the result looks similar to an earlier one concerning dual combinatory logic, the proof is different because symmetric combinators may form redexes in both left and right associated terms. (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  18. Katalin Bimbó & J. ~Michael Dunn (2005). Relational Semantics for Kleene Logic and Action Logic. Notre Dame Journal of Formal Logic 46 (4):461-490.
    Kleene algebras and action logic were proposed to be solutions to the finite axiomatization problem of the algebra of regular sets (of strings). They are treated here as nonclassical logics—with Hilbert-style axiomatizations and semantics. We also provide intuitive accounts in terms of information states of the semantics which provide further insights into the formalisms. The three types of "Kripke-style'' semantics which we define develop insights from gaggle theory, and from our four-valued and generalized Kripke semantics for the minimal substructural logic. (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  19. Katalin Bimbó (2004). Semantics for Dual and Symmetric Combinatory Calculi. Journal of Philosophical Logic 33 (2):125-153.
    We define dual and symmetric combinatory calculi (inequational and equational ones), and prove their consistency. Then, we introduce algebraic and set theoretical relational and operational - semantics, and prove soundness and completeness. We analyze the relationship between these logics, and argue that inequational dual logics are the best suited to model computation.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  20. Katalin Bimbó (2003). The Church-Rosser Property in Dual Combinatory Logic. Journal of Symbolic Logic 68 (1):132-152.
    Dual combinators emerge from the aim of assigning formulas containing ← as types to combinators. This paper investigates formally some of the properties of combinatory systems that include both combinators and dual combinators. Although the addition of dual combinators to a combinatory system does not affect the unique decomposition of terms, it turns out that some terms might be redexes in two ways (with a combinator as its head, and with a dual combinator as its head). We prove a general (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  21. Katalin Bimbó (2000). Investigation Into Combinatory Systems with Dual Combinators. Studia Logica 66 (2):285-296.
    Combinatory logic is known to be related to substructural logics. Algebraic considerations of the latter, in particular, algebraic considerations of two distinct implications (, ), led to the introduction of dual combinators in Dunn & Meyer 1997. Dual combinators are "mirror images" of the usual combinators and as such do not constitute an interesting subject of investigation by themselves. However, when combined with the usual combinators (e.g., in order to recover associativity in a sequent calculus), the whole system exhibits (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation