Kleene’s well-known strong three-valued logic is shown to be one of a family of logics with similar mathematical properties. These logics are produced by an intuitively natural construction. The resulting logics have direct relationships with bilattices. In addition they possess mathematical features that lend themselves well to semantical constructions based on fixpoint procedures, as in logic programming.

In the tech report Artemov and Yavorskaya [4] an elegant formulation of the first-order logic of proofs was given, FOLP. This logic plays a fundamental role in providing an arithmetic semantics for first-order intuitionistic logic, as was shown. In particular, the tech report proved an arithmetic completeness theorem, and a realization theorem for FOLP. In this paper we provide a possible-world semantics for FOLP, based on the propositional semantics of Fitting [5]. We also give an Mkrtychev semantics. Motivation and intuition (...) for FOLP can be found in Artemov and Yavorskaya [4], and are not fully discussed here.This paper is dedicated to Sergei Artemov, an honored colleague and friend, who has made wonderful things for the rest of us to play with. (shrink)

Strict/tolerant logic, ST, evaluates the premises and the consequences of its consequence relation differently, with the premises held to stricter standards while consequences are treated more tolerantly. More specifically, ST is a three-valued logic with left sides of sequents understood as if in Kleene’s Strong Three Valued Logic, and right sides as if in Priest’s Logic of Paradox. Surprisingly, this hybrid validates the same sequents that classical logic does. A version of this result has been extended to meta, metameta, … (...) consequence levels in Barrio et al.. In my earlier paper Fitting I showed that the original ideas behind ST are, in fact, much more general than first appeared, and an infinite family of many valued logics have Strict/Tolerant counterparts. This family includes both Kleene’s and Priest’s logic individually, as well as first degree entailment. For instance, for both the Kleene and the Priest logic, the corresponding strict/tolerant logic is six-valued, but with differing sets of strictly and tolerantly designated truth values. The present paper extends that generalization in two directions. We examine a reverse notion, of Tolerant/Strict logics, which exist for the same structures that were investigated in Fitting. And we show that the generalization extends through the meta, metameta, … consequence levels for the same infinite family of many valued logics. Finally we close with remarks on the status of cut and related rules, which can actually be rather nuanced. Throughout, the aim is not the philosophical applications of the Strict/Tolerant idea, but the determination of how general a phenomenon it is. (shrink)

This book describes computability theory and provides an extensive treatment of data structures and program correctness. It makes accessible some of the author's work on generalized recursion theory, particularly the material on the logic programming language PROLOG, which is currently of great interest. Fitting considers the relation of PROLOG logic programming to the LISP type of language.

We continue a series of papers on a family of many-valued modal logics, a family whose Kripke semantics involves many-valued accessibility relations. Earlier papers in the series presented a motivation in terms of a multiple-expert semantics. They also proved completeness of sequent calculus formulations for the logics, formulations using a cut rule in an essential way. In this paper a novel cut-free tableau formulation is presented, and its completeness is proved.

Strict/tolerant logic is a formally defined logic that has the same consequence relation as classical logic, though it differs from classical logic at the metaconsequence level. Specifically, it does not satisfy a cut rule. It has been proposed for use in work on theories of truth because it avoids some objectionable features arising from the use of classical logic. Here we are not interested in applications, but in the formal details themselves. We show that a wide range of logics have (...) strict/tolerant counterparts, with the same consequence relations but differing at the metaconsequence level. Among these logics are Kleene’s K3\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {K_3}$$\end{document}, Priest’s LP\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathsf {LP}}$$\end{document}, and first-degree entailment, FDE. The primary tool we use is the bilattice. But it is more than a tool, it seems to be the natural home for this kind of investigation. (shrink)

In an earlier paper, [5], I gave semantics and tableau rules for a simple firstorder intensional logic called FOIL, in which both objects and intensions are explicitly present and can be quantified over. Intensions, being non-rigid, are represented in FOIL as (partial) functions from states to objects. Scoping machinery, predicate abstraction, is present to disambiguate sentences like that asserting the necessary identity of the morning and the evening star, which is true in one sense and not true in another.In this (...) paper I address the problem of axiomatizing FOIL. I begin with an interesting sublogic with predicate abstraction and equality but no quantifiers. In [2] this sublogic was shown to be undecidable if the underlying modal logic was at least K4, though it is decidable in other cases. The axiomatization given is shown to be complete for standard logics without a symmetry condition. The general situation is not known. After this an axiomatization for the full FOIL is given, which is straightforward after one makes a change in the point of view. (shrink)

Kripke’s work on modal logic has been immensely influential. It hardly needs remarking that this is not his only work. Here we address his pioneering applications of fixpoint constructions to the theory of truth, and related work by others. In his fundamental paper on this he explicitly described a modal version, applying a fixpoint construction world by world within a modal frame. This can certainly be carried out, and doubtless has been somewhere. Others have suggested a variety of other extensions (...) such as using the unit interval as the underlying space of truth values, or using a four valued logic instead of three, or various combinations of these. When many similar formal constructions have been proposed, one naturally asks what is the common core. Is there some setting in which things can be proved once and for all, with the various specific proposals seen as applications of this common core. In fact this is the case, with bilattices providing the desired structure. Much of such a development has already appeared in some form or other. It is the purpose of this article to bring everything together, and also add a few things. We present general results that, more or less, have everything currently in the fixpoint literature as special cases. Fortunately this does not make things more complicated, since the underlying proofs are essentially the same as they have always been. It is just that they are being carried out in generality rather than in specificity. (shrink)

An interpolation theorem holds for many standard modal logics, but first order $S5$ is a prominent example of a logic for which it fails. In this paper it is shown that a first order $S5$ interpolation theorem can be proved provided the logic is extended to contain propositional quantifiers. A proper statement of the result involves some subtleties, but this is the essence of it.

A refutation mechanism is introduced into logic programming, dual to the usual proof mechanism; then negation is treated via refutation. A four-valued logic is appropriate for the semantics: true, false, neither, both. Inconsistent programs are allowed, but inconsistencies remain localized. The four-valued logic is a well-known one, due to Belnap, and is the simplest example of Ginsberg’s bilattice notion. An efficient implementation based on semantic tableaux is sketched; it reduces to SLD resolution when negations are not involved. The resulting system (...) can give reasonable answers to queries that involve both negation and free variables. Also it gives the same results as Prolog when there are no negations. Finally, an implementation in Prolog is given. (shrink)

Among non-monotonic systems of reasoning, non-monotonic modal logics, and autoepistemic logic in particular, have had considerable success. The presence of explicit modal operators allows flexibility in the embedding of other approaches. Also several theoretical results of interest have been established concerning these logics. In this paper we introduce non-monotonic modal logics based on many-valued logics, rather than on classical logic. This extends earlier work of ours on many-valued modal logics. Intended applications are to situations involving several reasoners, not just one (...) as in the standard development. (shrink)

Justification logics are logics of knowledge in which explicit reasons are formally represented. Standard logics of knowledge have justification logic analogs. Connecting justification logics and logics of knowledge are Realization Theorems. In this paper we give a new, constructive proof of the Realization Theorem connecting S5 and its justification analog, JS5. This proof is, I believe, the simplest in the literature.

Consider those many-valued logic models in which the truth values are a lattice that supplies interpretations for the logical connectives of conjunction and disjunction, and which has a De Morgan involution supplying an interpretation for negation. Assume that the set of designated truth values is a prime filter in the lattice. Each of these structures determines a simple many-valued logic. We show that there is a single Smullyan-style signed tableau system appropriate for all of the logics these structures determine. Differences (...) between the logics are confined entirely to tableau branch closure rules. Completeness, soundness, and interpolation can be proved in a uniform way for all cases. Since branch closure rules have a limited number of variations, in fact all the semantic structures determine just four different logics, all well-known ones. Asymmetric logics such as strict/tolerant, ST, also share all the same tableau rules, but differ in what constitutes an initial tableau. It is also possible to capture the notion of antivalidity using the same set of tableau rules. Thus a simple set of tableau rules serves as a unifying and classifying device for a natural and simple family of many-valued logics. (shrink)

Generalized databases will be examined, in which attributes can be sets of attributes, or sets of sets of attributes, and other higher type constructs. A precise semantics will be developed for such databases, based on a higher type modal/intensional logic.

We present a logic programming language, which we call Proflog, with an operational semantics based on tableaus, and a denotational semantics based on supervaluations. We show the two agree. Negation is well-behaved, and semantic non-computability issues do not arise. This is accomplished essentially by dropping a domain closure requirement. The cost is that intuitions developed through the use of classical logic may need modification, though the system is still classical at a level once removed. Implementation problems are discussed very briefly (...) — the thrust of the paper is primarily theoretical. (shrink)

Propositional modal logic is a standard tool in many disciplines, but first-order modal logic is not. There are several reasons for this, including multiplicity of versions and inadequate syntax. In this paper we sketch a syntax and semantics for a natural, well-behaved version of first-order modal logic, and show it copes easily with several familiar difficulties. And we provide tableau proof rules to go with the semantics, rules that are, at least in principle, automatable.

Hybrid logics internalize their own semantics. Members of the newer family of justification logics internalize their own proof methodology. It is an appealing goal to combine these two ideas into a single system, and in this paper we make a start. We present a hybrid/justification version of the modal logic T. We give a semantics, a proof theory, and prove a completeness theorem. In addition, we prove a Realization Theorem, something that plays a central role for justification logics generally. Since (...) justification logics are newer and less well-known than hybrid logics, we sketch their background, and give pointers to their range of applicability. We conclude with suggestions for future research. Indeed, the main goal of this paper is to encourage others to continue the investigation begun here. (shrink)

We give a basic introduction to modal logic. This includes possible world semantics, axiom systems, and quantification. Ideas and formal machinery are discussed, but all proofs are omitted. Recommendations are given for those who want more.

This chapter contains sections titled: Introduction Intensions Models About Quantification Truth in Models Equality Rigidity De Re/De Dicto Partial Designation Designation and Existence Definite Descriptions What Next?

A generalization of conventional Horn clause logic programming is proposed in which the space of truth values is a pseudo-Boolean or Heyting algebra, whose members may be thought of as evidences for propositions. A minimal model and an operational semantics is presented, and their equivalence is proved, thus generalizing the classic work of Van Emden and Kowalski.

We present non-clausal resolution systems for propositional modal logics whose Kripke models do not involve symmetry, and for first order versions whose Kripke models do not involve constant domains. We give systems for K, T , K4 and S4; other logics are also possible. Our systems do not require preliminary reduction to a normal form and, in the first order case, intermingle resolution steps with Skolemization steps.

odel-L¨ ob computability logic. In order to make things relatively self-contained, I sketch the essential ideas of GL, and discuss the significance of its fixpoint theorem. Then I give the algorithm embodied in the program in a little more detail. It should be emphasized that nothing new is presented here — all the theory and methodology are due to others. The main interest is, in a sense, psychological. The approach taken here has been declared in the literature, more than once, (...) to be of theoretical interest only, being too unwieldly in practice. Experimentation shows this is not so provided formulas are not too complicated. A copy of the program can be obtained by ftp from venus.gc.cuny.edu. It is in the subdirectory “/pub/fitting,” under the name “glfixpt.pro.” Log on as “anonymous” and use your full e-mail address as password. If there are difficulties with ftp, send e-mail to the author at mlfl[email protected]. The Prolog code is standard, and should run under any implementation, though minor modifications may be necessary for some systems. These modifications are described in the last section, and also in the program itself. (shrink)

Herbrand’s theorem is a central fact about classical logic, [9, 10]. It provides a constructive method for associating, with each first-order formula X, a sequence of formulas X1, X2, X3, . . . , so that X has a first-order proof if and only if some Xi is a tautology. Herbrand’s theorem serves as a constructive alternative to..

Drawing on interviews with seasonal agricultural workers employed in Canada from Jamaica and Mexico, this paper focuses in on the experiences of a Jamaican farmworker who remits funds to pay a neighbour to farm his land (or the land he leases) while in Canada, and who participates in regular long-distance discussions with family members and neighbours back home about the upkeep of the farm. The concept of a “transnational agricultural care chain” is proposed here to capture a series of personal (...) links between people, located, at least temporarily, in different countries, who tend to the crops and farmland as a practice that entails asymmetrical relations of obligation to care for others. Agricultural care chains form part of a strategy to get by and possibly even advance the economic and social standing of one’s family under difficult economic conditions. Land access, as a co-constitutive sphere of production and reproduction, is another important factor in the livelihood strategies of rurally-rooted migrants, but the significance placed on land must be understood in connection to the uneven processes of global capitalism, histories of colonialism and, in the case of Jamaica, plantation slavery. The paper concludes with a reflection on how transnational agricultural care chains as paradigmatic of the contemporary food system are relevant to political and conceptual discussions around food sovereignty. (shrink)

This is a thorough treatment of first-order modal logic. The book covers such issues as quantification, equality (including a treatment of Frege's morning star/evening star puzzle), the notion of existence, non-rigid constants and function symbols, predicate abstraction, the distinction between nonexistence and nondesignation, and definite descriptions, borrowing from both Fregean and Russellian paradigms.

This paper continues my work of [9], which showed there was a broad family of many valued logics that have a strict/tolerant counterpart. Here we consider a generalization of weak Kleene three valued logic, instead of the strong version that was background for that earlier work. We explain the intuition behind that generalization, then determine a subclass of strict/tolerant structures in which a generalization of weak Kleene logic produces the same results that the strong Kleene generalization did. This paper provides (...) much background, but is not self-contained. Some results from [9] are called on, and are not reproved here. [9] Melvin C. Fitting. “A Family of Strict/Tolerant Logics”. In: Journal of Philosophical Logic. Online. Print publication forthcoming. (shrink)

This article explores the labour behind local food in the Canadian Atlantic province of Nova Scotia. Based on surveys and interviews with farmers, migrant farmworkers, and farmers’ market consumers in the province, we suggest that the celebration of local food by government and industry is a form of “local washing.” Local washing hides key aspects of the social relations of production: in this case, it hides insufficient financial and policy supports for Nova Scotian farms and the increased reliance on migrant (...) farmworkers via the Seasonal Agricultural Worker Program and the Temporary Foreign Worker Program. Our research found that a growing reliance on migrant farmworkers was not just the case for larger, industrial farms, but also for smaller farms participating in local and alternative food initiatives, like farmers’ markets and fresh produce subscription boxes. Additionally, our surveys show that while farmers’ market shoppers expressed an interest in supporting local foods, they reported knowing little about farm workers or working conditions. Our paper contributes to the literature on local and alternative food initiatives by connecting the relations of production to consumption. Rather than focusing solely on the nature of the relationships between farmers and consumers and the values embodied in direct agricultural markets, this research explores the central role of permanently temporary migrant workers in local agriculture. (shrink)

Suppose there are several experts, with some dominating others (expert A dominates expert B if B says something is true whenever A says it is). Suppose, further, that each of the experts has his or her own view of what is possible — in other words each of the experts has their own Kripke model in mind (subject, of course, to the dominance relation that may hold between experts). How will they assign truth values to sentences in a common modal (...) language, and on what sentences will they agree? This problem can be reformulated as one about many-valued Kripke models, allowing many-valued accessibility relations. This is a natural generalization of conventional Kripke models that has only recently been looked at. The equivalence between the many-valued version and the multiple expert one will be formally established. Finally we will axiomatize many-valued modal logics, and sketch a proof of completeness. (shrink)