46 found
Order:
  1. M. W. Bunder (1976). The Inconsistency of F*21. Journal of Symbolic Logic 41 (2):467 - 468.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  2. M. W. Bunder & W. J. M. Dekkers (2005). Equivalences Between Pure Type Systems and Systems of Illative Combinatory Logic. Notre Dame Journal of Formal Logic 46 (2):181-205.
    Pure Type Systems, PTSs, were introduced as a generalization of the type systems of Barendregt's lambda cube and were designed to provide a foundation for actual proof assistants which will verify proofs. Systems of illative combinatory logic or lambda calculus, ICLs, were introduced by Curry and Church as a foundation for logic and mathematics. In an earlier paper we considered two changes to the rules of the PTSs which made these rules more like ICL rules. This led to four (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography  
  3. M. W. Bunder (2000). Expedited Broda-Damas Bracket Abstraction. Journal of Symbolic Logic 65 (4):1850-1857.
    A bracket abstraction algorithm is a means of translating λ-terms into combinators. Broda and Damas, in [1], introduce a new, rather natural set of combinators and a new form of bracket abstraction which introduces at most one combinator for each λ-abstraction. This leads to particularly compact combinatory terms. A disadvantage of their abstraction process is that it includes the whole Schonfinkel [4] algorithm plus two mappings which convert the Schonfinkel abstract into the new abstract. This paper shows how the new (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  4.  4
    M. W. Bunder (1978). Equality in 21* with Restricted Subjects. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 24 (8):125-127.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  5.  4
    M. W. Bunder (1974). Some Inconsistencies in Illative Combinatory Logic. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 20 (13-18):199-201.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  6.  12
    M. W. Bunder (1980). A Note on Quantified Significance Logics. Bulletin of the Section of Logic 9 (4):159-161.
    Direct download  
     
    Export citation  
     
    My bibliography  
  7.  3
    M. W. Bunder (1982). Some Results in Aczel-Feferman Logic and Set Theory. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 28 (19):269-276.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  8.  6
    M. W. Bunder (1979). Paraconsistent Combinatory Logic,„. Bulletin of the Section of Logic 8 (4):177-180.
    Direct download  
     
    Export citation  
     
    My bibliography  
  9.  21
    M. W. Bunder (1987). Some Consistency Proofs and a Characterization of Inconsistency Proofs in Illative Combinatory Logic. Journal of Symbolic Logic 52 (1):89-110.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  10.  13
    M. W. Bunder (1983). A Weak Absolute Consistency Proof for Some Systems of Illative Combinatory Logic. Journal of Symbolic Logic 48 (3):771-776.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  11.  4
    M. W. Bunder (1974). Propositional and Predicate Calculuses Based on Combinatory Logic. Notre Dame Journal of Formal Logic 15 (1):25-34.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  12.  5
    M. W. Bunder (1984). Category Theory Based on Combinatory Logic. Archive for Mathematical Logic 24 (1):1-16.
    Direct download  
     
    Export citation  
     
    My bibliography  
  13.  5
    M. W. Bunder (1987). Some Generalizations to Two Systems of Set Theory Based on Combinatory Logic. Archive for Mathematical Logic 26 (1):5-12.
    Direct download  
     
    Export citation  
     
    My bibliography  
  14.  31
    M. W. Bunder (1982). Deduction Theorems for Weak Implicational Logics. Studia Logica 41 (2-3):95 - 108.
    The standard deduction theorem or introduction rule for implication, for classical logic is also valid for intuitionistic logic, but just as with predicate logic, other rules of inference have to be restricted if the theorem is to hold for weaker implicational logics.In this paper we look in detail at special cases of the Gentzen rule for and show that various subsets of these in effect constitute deduction theorems determining all the theorems of many well known as well as not well (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  15.  25
    M. W. Bunder (1988). Arithmetic Based on the Church Numerals in Illative Combinatory Logic. Studia Logica 47 (2):129 - 143.
    In the early thirties, Church developed predicate calculus within a system based on lambda calculus. Rosser and Kleene developed Arithmetic within this system, but using a Godelization technique showed the system to be inconsistent.Alternative systems to that of Church have been developed, but so far more complex definitions of the natural numbers have had to be used. The present paper based on a system of illative combinatory logic developed previously by the author, does allow the use of the Church numerals. (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  16.  3
    M. W. Bunder (1973). A Deduction Theorem for Restricted Generality. Notre Dame Journal of Formal Logic 14 (3):341-346.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  17.  3
    M. W. Bunder (1970). A Paradox in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 11 (4):467-470.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  18.  22
    M. W. Bunder (1984). Some Definitions of Negation Leading to Paraconsistent Logics. Studia Logica 43 (1-2):75 - 78.
    In positive logic the negation of a propositionA is defined byA X whereX is some fixed proposition. A number of standard properties of negation, includingreductio ad absurdum, can then be proved, but not the law of noncontradiction so that this forms a paraconsistent logic. Various stronger paraconsistent logics are then generated by putting in particular propositions forX. These propositions range from true through contingent to false.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  19.  5
    M. W. Bunder & Jonathan P. Seldin (1978). Some Anomalies in Fitch's System QD. Journal of Symbolic Logic 43 (2):247-249.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  20.  11
    M. W. Bunder (1979). A More Relevant Relevance Logic. Notre Dame Journal of Formal Logic 20 (3):701-704.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  21.  3
    M. W. Bunder (1979). Variable Binding Term Operators in $\Lambda $-Calculus. Notre Dame Journal of Formal Logic 20 (4):876-878.
  22.  9
    M. W. Bunder & R. M. Rizkalla (2009). Proof-Finding Algorithms for Classical and Subclassical Propositional Logics. Notre Dame Journal of Formal Logic 50 (3):261-273.
    The formulas-as-types isomorphism tells us that every proof and theorem, in the intuitionistic implicational logic $H_\rightarrow$, corresponds to a lambda term or combinator and its type. The algorithms of Bunder very efficiently find a lambda term inhabitant, if any, of any given type of $H_\rightarrow$ and of many of its subsystems. In most cases the search procedure has a simple bound based roughly on the length of the formula involved. Computer implementations of some of these procedures were done in Dekker. (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  23.  1
    M. W. Bunder & R. K. Meyer (1978). On the Inconsistency of Systems Similar to $Mathscr{F}^Ast_{21}$. Journal of Symbolic Logic 43 (1):1-2.
  24.  14
    M. W. Bunder (1990). Some Improvements to Turner's Algorithm for Bracket Abstraction. Journal of Symbolic Logic 55 (2):656-669.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  25. M. W. Bunder (1985). A result for combinators, BCK logics and BCK algebras. Logique Et Analyse 28 (9):33.
    Translate
     
     
    Export citation  
     
    My bibliography   1 citation  
  26.  9
    M. W. Bunder (1995). A Simplified Form of Condensed Detachment. Journal of Logic, Language and Information 4 (2):169-173.
    This paper gives a simple, elegant statement of the condensed detachment rule that is independent of most general unifiers and proves that this is equivalent to the longer, more usual, formulation.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  27.  3
    M. W. Bunder (1982). Some Results in Aczel‐Feferman Logic and Set Theory. Mathematical Logic Quarterly 28 (19):269-276.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  28. M. W. Bunder (1973). A Generalised Kleene-Rosser Paradox for a System Containing the Combinator ${\Bf K}$. Notre Dame Journal of Formal Logic 14 (1):53-54.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  29.  8
    M. W. Bunder (1974). Various Systems of Set Theory Based on Combinatory Logic. Notre Dame Journal of Formal Logic 15 (2):192-206.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  30.  6
    M. W. Bunder (1977). Consistency Notions in Illative Combinatory Logic. Journal of Symbolic Logic 42 (4):527-529.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  31.  2
    M. W. Bunder (1978). Equality In. Mathematical Logic Quarterly 24 (8):125-127.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  32.  5
    M. W. Bunder (1982). Illative Combinatory Logic Without Equality as a Primitive Predicate. Notre Dame Journal of Formal Logic 23 (1):62-70.
  33.  4
    M. W. Bunder (2002). A Classification of Intersection Type Systems. Journal of Symbolic Logic 67 (1):353-368.
    The first system of intersection types, Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules (( $\wedge$ I) and ( $\wedge$ E)) to the type assignment system. The major advantage of these new types was that they were invariant under β-equality, later work by Barendregt, Coppo and Dezani [1], extended this to include an (η) rule which gave types invariant under βη-reduction. Urzyczyn proved in [6] that for both these systems it is (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  34.  4
    M. W. Bunder (1980). Significance and Illative Combinatory Logics. Notre Dame Journal of Formal Logic 21 (2):380-384.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  35.  3
    M. W. Bunder (1979). $\Lambda$-Elimination in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):628-630.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  36.  4
    M. W. Bunder & R. K. Meyer (1978). On the Inconsistency of Systems Similar to F*21. Journal of Symbolic Logic 43 (1):1 - 2.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  37.  3
    M. W. Bunder (1979). Alternative Forms of Propositional Calculus for a Given Deduction Theorem. Notre Dame Journal of Formal Logic 20 (3):613-619.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  38.  1
    M. W. Bunder (1979). Scott's Models and Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):609-612.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  39. M. W. Bunder (1988). Corrections to some results for BCK logics and algebras. Logique Et Analyse 31 (21):115.
    Translate
     
     
    Export citation  
     
    My bibliography  
  40. M. W. Bunder (1980). Quantified relevance logic and generalised restricted generality. Logique Et Analyse 23 (90):319.
    Translate
     
     
    Export citation  
     
    My bibliography  
  41. M. W. Bunder (1974). Some Inconsistencies in Illative Combinatory Logic. Mathematical Logic Quarterly 20 (13‐18):199-201.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  42. M. W. Bunder (1976). The Inconsistency of $Mathscr{F}^Ast_{21}$. Journal of Symbolic Logic 41 (2):467-468.
  43. M. W. Bunder (1979). Deduction Theorems in Significance Logics. Notre Dame Journal of Formal Logic 20 (3):695-700.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  44. M. W. Bunder (1979). Generalized Restricted Generality. Notre Dame Journal of Formal Logic 20 (3):620-624.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  45. M. W. Bunder (1979). On the Equivalence of Systems of Rules and Systems of Axioms in Illative Combinatory Logic. Notre Dame Journal of Formal Logic 20 (3):603-608.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  46. M. W. Bunder (1976). Some Notes On: ``A Deduction Theorem for Restricted Generality''. Notre Dame Journal of Formal Logic 17 (1):153-154.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography