PRISM :: Browsing by Author "Zach, Richard"

Browsing by Author "Zach, Richard"

Now showing 1 - 20 of 30

Open Access
A study in the logic of institutions
(2012-07-13) Payette, Gillman; Zach, Richard
In my dissertation A Study in the Logic of Institutions I develop a logical system for reasoning about institutions and their consistency. Since my dissertation is a work in logic rather than one in socio-political philosophy, I don’t defend a particular theory of institutions. Instead, I did as Yogi Bera suggested and simply took the fork in the road. A well-developed account of institutions is given by John Searle in (1995); and (2010). His account bases all social reality on language, and I use his account to provide a logic for institutional norms. Briefly, social reality is constructed via language by making our intentions clear to one another. And we do this via speech acts. There is one particular type of speech act that is important to institutions: declarations. Declarations bring about new social objects and create social states of affairs. It is via declarations that social institutions are created. In so far as groups recognize an institution sustaining/making authority, that authority has the ability to generate new institutional rules via declarations. According to Vanderveken (1990, 1991); see also Searle and Vanderveken (1985), speech acts have a logic. That is, performing one speech act can satisfy the conditions of having performed another speech act. A priest declaring a baby baptized will also make it so that the priest has asserted that the baby is baptized, for instance. More importantly, certain declarations will result in the declarations of some of the logical consequences of the initial declarations. I characterize the set of speech acts that stand in that relationship and develop a logical system around that characterization. The formal framework incorporates action and permits representations of complex institution-dependent relations, e.g., rights and duties. I further develop this formalism to investigate the notion of normative consistency. I show how to represent at least a minimal conception of normative inconsistency within the formal framework, and characterize its properties. I conclude by comparing my work to that of others.
Open Access
Art/ificial intelligence: a short bibliography on AI and the arts
(1990-01) Zach, Richard; Widmer, Gerhard; Trappl, Robert
Open Access
A Categorical Extension of the Curry-Howard Isomorphism
(2019-09) McDonald, Joseph; Zach, Richard; Wyatt, Nicole; Cockett, J. Robin B.
Within this work, we investigate some aspects of the interaction that occurs between category theory and the typed λ-calculus. In particular, we examine the equivalence of categories that can be demonstrated between the category of Cartesian closed categories and the category of typed λ-theories. As will be seen, a convenient technique that can be employed so as to make this interaction explicit is the application of algebraic theories (often known as “Lawvere theories”), which allow us to characterize various model-theoretical aspects of typed λ-theories in the abstract algebraic setting of a Cartesian closed category. What follows from this interaction between Cartesian closed categories and typed λ-theories is that of a categorical extension of the Curry-Howard isomorphism, which attributes a similar correspondence between the typed λ-calculus and the positive fragment of the intuitionistic propositional calculus.
Open Access
The Continuum: History, Mathematics, and Philosophy
(2017-12-21) Hayashi, Teppei; Zach, Richard; Bauer, Kristine; Linsky, Bernard; MacIntosh, Jack; Migotti, Mark
The main aim of this dissertation is to depict a wide variety of the conceptions of the continuum by tracing the history of the continuum from the ancient Greece to the modern times, and in so doing, to find a new way to look at the continuum. In the first part, I trace the history of the continuum with a special emphasis on unorthodox views at each period. Basically, the history of the continuum is the history of the rivalry between two views, namely, between the punctiform and the non-punctiform views of the continuum. According to the punctiform view, the continuum is composed of indivisibles; on the other hand, according to the non-punctiform view, the continuum cannot be composed of indivisibles. In the second part, I present Richard Dedekind’s and Georg Cantor’s standard mathematical theories of the continuum as the modern representative of the punctiform view of the continuum, and then examine Charles Saunders Peirce’s non-punctiform view of the continuum. In the last chapter, I give some mathematical interpretations to Aristotle’s and Peirce’s theories of the continuum according to both of which the continuum cannot be composed of points. In interpreting Aristotle’s view, I use modern topology and show that Aristotle’s view can be nicely captured by topology. On the other hand, in interpreting Peirce’s view, I appeal to the theory of category and show that in the category-theoretic framework the continuum appears quite differently from the standard one conceived in the Dedekindian and Cantorian ways. In conclusion, I try to defend a sort of pluralistic view concerning the conceptions of the continuum.
Open Access
Counterfactual Logic: A Modern Overview
(2024-01-26) Rios Flores, Mohamar; Bauer, Kristine; Zach, Richard; Cunningham, Clifton; Payette, Gillman
Lewis (1973) described a family of logics for reasoning about counterfactual statements. These logics also contained additional connectives for reasoning about comparative possibility statements and modalities. Moreover, Lewis described a possible world semantics involving a ``sphere system'' that effectively lets you talk about some worlds being more ``similar'' to a given world than others. The resulting theory is very powerful and flexible in many ways similar to the theory of normal modal logics. Unfortunately, Lewis provided an extremely terse formal description of the theory with many important theorems, definitions, and details omitted or described vaguely. There are no other resources that present a complete formal description of this theory. Without this formal description one is unable to propose new logics in this family and prove soundness and completeness theorems for them. To remedy this, we present a reformulation of Lewis' theory using modern methods and notation. All definitions are described formally and all core results are proven in explicit detail. We include an informal overview of the different kinds of statements associated with each connective. The semantics is reformulated in terms of frames. The syntax includes additional rules and theorems to make it easier to use. Both the soundness and the strong soundness theorems are proven. The completeness theorem uses canonical models and the entire construction is shown explicitly. The first edition of Counterfactuals (Lewis, 1973) had an error exposed by Krabbe (1978) that led to the second edition (Lewis, 2001) having a more complex definition. So we present a reformulation of Krabbe's construction within our modernized setting.
Open Access
The Curry-Howard Correspondence
(2021-08-13) Farooqui, Husna; Zach, Richard; Wyatt, Nicole; Fantl, Jeremy
Outside of logic, computer science, and mathematics, the Curry-Howard correspondence is ordinarily described as a deep connection between proofs and programs. However, without sufficient requisite background knowledge, such a description can be mystifying and contribute to the correspondence’s general obscurity. In this thesis, we attempt to introduce the Curry-Howard correspondence by presenting an elementary correspondence between the extended simply-typed lambda calculus and intuitionistic natural deduction. Our introduction aims to provide the necessary theoretical background to understand the basic correspondence, which can help bridge the gap between non-specialists and the more advanced literature on the topic. Such an introduction also serves to better demonstrate and clarify the correspondence’s significance, which is a topic we explore towards the end. To introduce the correspondence, we introduce the lambda calculus and the simply-typed lambda calculus. Moreover, we introduce natural deduction and subsequently develop a novel sequent-style natural deduction for reasons philosophical as well as logically advantageous. As a result, we methodically prove a full isomorphism between our system of natural deduction and the extended simply-typed lambda calculus.
Open Access
Dual systems of sequents and tableaux for many-valued logics
(European Association for Theoretical Computer Science, 1993-01) Baaz, Matthias; Fermüller, Christian G.; Zach, Richard
The aim of this paper is to emphasize the fact that for all finitely-many-valued logics there is a completely systematic relation between sequent calculi and tableau systems. More importantly, we show that for both of these systems there are always two dual proof systems (not just only two ways to interpret the calculi). This phenomenon may easily escape one's attention since in the classical (two-valued) case the two systems coincide. (In two-valued logic the assignment of a truth value and the exclusion of the opposite truth value describe the same situation.
Open Access
Elimination of cuts in first-order finite-valued logics
(Institut für Informatik, 1994-01) Baaz, Matthias; Fermüller, Christian G.; Zach, Richard
A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand’s theorem for the four-valued knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information.
Open Access
Formal Models of Fallible Knowledge
(2017) Ahmadianhosseini, Zahra; Zach, Richard; Fantl, Jeremy; Wyatt, Nicole
In this thesis I review and analyze Holliday’s \citeyearpar{KWF} work on the relation between fallibilism and closure. The main concern in Holliday’s work is to show that most major fallibilistic theories of knowledge inherently suffer from at least one problem among a set of problems and that there are essential assumptions that must be added to the models representing this family of theories to solve the problem. I first review the epistemologic theories which are the basis of the study, and later discuss their formalizations and how Holliday’s theory identifies and solves the problem. At the end I evaluate Holliday’s formalization of one of these theories of knowledge, namely Lewis’s theory, and argues that the model presented by Holliday is not entirely faithful to Lewis’s theory and needs to undergo certain changes.
Open Access
Fuzzy Logic & Vagueness
(2005) Serchuk, Phil; Zach, Richard
Open Access
Gödel vs. Mechanism
(2013) Darnell, Eamon; Zach, Richard
Open Access
Hilbert’s Finitism: Historical, Philosophical, and Metamathematical Perspectives
(2001-05) Zach, Richard
In the 1920s, David Hilbert proposed a research program with the aim of providing mathematics with a secure foundation. This was to be accomplished by first formalizing logic and mathematics in their entirety, and then showing—using only so-called finitistic principles—that these formalizations are free of contradictions. In the area of logic, the Hilbert school accomplished major advances both in introducing new systems of logic, and in developing central metalogical notions, such as completeness and decidability. The analysis of unpublished material presented in Chapter 2 shows that a completeness proof for propositional logic was found by Hilbert and his assistant Paul Bernays already in 1917-18, and that Bernays’s contribution was much greater than is commonly acknowledged. Aside from logic, the main technical contribution of Hilbert’s Program are the development of formal mathematical theories and proof-theoretical investigations thereof, in particular, consistency proofs. In this respect Wilhelm Ackermann’s 1924 dissertation is a milestone both in the development of the Program and in proof theory in general. Ackermann gives a consistency proof for a second-order version of primitive recursive arithmetic which, surprisingly, explicitly uses a finitistic version of transfinite induction up to ω^ω^ω. He also gave a faulty consistency proof for a system of second-order arithmetic based on Hilbert’s epsilon-substitution method. Detailed analyses of both proofs in Chapter 3 shed light on the development of finitism and proof theory in the 1920s as practiced in Hilbert’s school. In a series of papers, Charles Parsons has attempted to map out a notion of mathematical intuition which he also brings to bear on Hilbert’s finitism. According to him, mathematical intuition fails to be able to underwrite the kind of intuitive knowledge Hilbert thought was attainable by the finitist. It is argued in Chapter 4 that the extent of finitistic knowledge which intuition can provide is broader than Parsons supposes. According to another influential analysis of finitism due to W. W. Tait, finitist reasoning coincides with primitive recursive reasoning. The acceptance of non-primitive recursive methods in Ackermann’s dissertation presented in Chapter 3, together with additional textual evidence presented in Chapter 4, shows that this identification is untenable as far as Hilbert’s conception of finitism is concerned. Tait’s conception, however, differs from Hilbert’s in important respects, yet it is also open to criticisms leading to the conclusion that finitism encompasses more than just primitive recursive reasoning.
Open Access
Hypersequent Calculi for Modal Logics
(2018-04-23) Burns, Samara Elizabeth; Zach, Richard; Wyatt, Nicole; Kazmi, Ali Akhtar
This thesis surveys and examines hypersequent approaches to the proof theory of modal logics. Traditional sequent calculi for modal logics often fail to have many of the desirable properties that we expect of a sequent calculus. Cut cannot be eliminated from the system for S5, the axioms of each logic are not straightforwardly related to the sequent rules, and variation between modal sequent calculi occurs in the presence and absence of logical rules, rather than structural rules, which violates Došen’s principle. The hypersequent framework is beneficial as we can provide Cut-free complete treatments of many modal logics. However, hypersequent approaches often lack generality, or do not conform to Došen’s principle. A recent development in the proof theory of modal logics, called relational hypersequents, appears to overcome many of these issues. Relational hypersequents provide a unified proof theory for many modal logics, where the logical rules are held constant between modal systems. This thesis provides some preliminary results for relational hypersequents by providing a Cut-free completeness proof for the modal logic K.
Open Access
Implementation of Message Passing Language
(2018-02) Kumar, Prashant; Cockett, Robin; Zach, Richard; Wang, Mea
Message Passage Language (MPL) is a programming language based on the work of Cockett and Pastro. MPL is a statically typed concurrent programming language with message passing as the concurrency primitive. It brings communication safety to interacting processes using a type system. MPL consists of two languages, concurrent MPL and sequential MPL, which can interact with each other. Concurrent MPL programs are written using concurrency constructs built into the language and protocols, which are concurrent data types. These concurrency constructs allow intuitive modelling of real world concurrency scenarios. Sequential MPL is a functional programming language. In addition to data definitions, sequential MPL allows codata definitions, which can model infinite structures. Sequential MPL allows for disciplined recursion using folds and unfolds in addition to normal recursion. In this thesis, we develop the first prototype of a compiler for MPL. We reformulate MPL's design to allow normal recursion in addition to primitive recursion, the only form of recursion allowed in previous designs. In light of the changes made to MPL, we describe MPL's type system. Then we develop an algorithm for type inferencing MPL programs, and implement it. In addition, we develop and implement an abstract machine to run MPL programs. We also develop the intermediate languages through which MPL programs compile to the abstract machine. We describe and implement the algorithms used in the compilation of MPL programs to the abstract machines, namely lambda lifting and compilation of pattern-matching.
Open Access
Indiscernibility and Mathematical Structuralism
(2010) Kouri, Teresa; Zach, Richard
Open Access
Lesniewski's systems of logic and mereology: history and re-evaluation
(2008) Urbaniak, Rafal; Zach, Richard
Open Access
Leśniewski’s Systems of Logic and Mereology; History and Re-evaluation.
(2008) Urbaniak, Rafal; Zach, Richard
Open Access
New Directions for Neo-logicism
(2018-07-10) Thomas-Bolduc, Aaron Robert; Zach, Richard; Wyatt, Nicole; Liebesman, David
In this dissertation I focus on a program in the philosophy of mathematics known as neo-logicism that is a direct descendant of Frege’s logicist project. That program seeks to reduce mathematical theories to logic and definitions in order to put those theories on stable epistemic and logical footing. The definitions that are of greatest importance are abstraction principles, biconditionals associating identity statements for abstract objects on one side, with equivalence classes on the other. Abstraction principles are important because they provide connections between logic on the one hand, and mathematics and its ontology on the other. Throughout this work, I advocate that the epistemic goals of neo-logicism be taken into account when we’re looking to solve problems that are of central importance to its success. Additionally, each chapter either discusses or advocates for a methodological shift, or sets up and implements a novel methodological position I believe to be broadly beneficial to the neo-logicist project. Chapter 2 traces thinking about the status of higher-order logic through the mid-twentieth century, setting the stage for issues dealt with in later chapters. Chapter 3 asks neo-logicists to look beyond set theory and consider other foundational theories, or something entirely new when looking for reductions of foundational mathematical theories. Chapter 4 is an extended argument involving non-standard analysis showing that Hume’s Principle ought not be considered analytic in Frege’s sense of the termChapters 5 and 6 move away form the (somewhat) historical work in the first three chapters, and set up new strategies for solving central neo-logicist problems by integrating formal and epistemic considerations. Chapter 5 introduces the notion of a canonical equivalence relation via a discussion of content carving. That notion is a particular way of understanding the relationship between equivalence relations and abstracts. Finally, chapter 6 makes use of canonical equivalence relations to introduce a new direction in the search for solutions to the Bad Company objection. As whole, the project can be seen as providing, as the title suggests, new directions that ought to be considered by those wishing to vindicate neo-logicism
Open Access
Note on calculi for a three-valued logic for logic programming
(1992) Baaz, Matthias; Zach, Richard
Open Access
The Paradox of Knowability and Semantic Anti-Realism
(2007) Chung, Julianne; Zach, Richard