In this article, a qualitative notion of subjective plausibility and its revision based on a preorder relation are implemented in higher-order logic. This notion of plausibility is used for modeling pragmatic aspects of communication on top of traditional two-dimensional semantic representations.

Higher-Order Logic (HOL) is a proof development system intended for applications to both hardware and software. It is principally used in two ways: for directly proving theorems, and as theorem-proving support for application-specific verification systems. HOL is currently being applied to a wide variety of problems, including the specification and verification of critical systems. Introduction to HOL provides a coherent and self-contained description of HOL containing both a tutorial introduction and most of the material (...) that is needed for day-to-day work with the system. After a quick overview that gives a "hands-on feel" for the way HOL is used, there follows a detailed description of the ML language. The logic that HOL supports and how this logic is embedded in ML, are then described in detail. This is followed by an explanation of the theorem-proving infrastructure provided by HOL. Finally two appendices contain a subset of the reference manual, and an overview of the HOL library, including an example of an actual library documentation. (shrink)

The history of building automated theorem provers for higher-order logic is almost as old as the field of deduction systems itself. The first successful attempts to mechanize and implement higher-order logic were those of Huet [13] and Jensen and Pietrzykowski [17]. They combine the resolution principle for higher-order logic (first studied in [1]) with higher-order unification. The unification problem in typed λ-calculi is much more complex than that for first- (...) class='Hi'>order terms, since it has to take the theory of αβη-equality into account. As a consequence, the higher-order unification problem is undecidable and sets of solutions need not even always have most general elements that represent them. Thus the mentioned calculi for higher-order logic have take special measures to circumvent the problems posed by the theoretical complexity of higher-order unification. In this paper, we will exemplify the methods and proof- and model-theoretic tools needed for extending first-order automated theorem proving to higherorder logic. For the sake of simplicity take the tableau method as a basis (for a general introduction to first-order tableaux see part I.1) and discuss the higherorder tableau calculi HT and HTE first presented in [19]. The methods in this paper also apply to higher-order resolution calculi [1, 13, 6] or the higher-order matings method of Peter [3], which extend their first-order counterparts in much the same way. Since higher-order calculi cannot be complete for the standard semantics by Gödel’s incompleteness theorem [11], only the weaker notion of Henkin models [12] leads to a meaningful notion of completeness in higher-order logic. It turns out that the calculi in [1, 13, 3, 19] are not Henkin-complete, since they fail to capture the extensionality principles of higher-order logic. We will characterize the deductive power of our calculus HT (which is roughly equivalent to these calculi) by the semantics of functional Σ-models. To arrive at a calculus that is complete with respect to Henkin models, we build on ideas from [6] and augment HT with tableau construction rules that use the extensionality principles in a goal-oriented way.. (shrink)

This book constitutes the strictly refereed post-workshop proceedings of the 11th International Workshop on Computer Science Logic, CSL '97, held as the 1997 Annual Conference of the European Association on Computer Science Logic, EACSL, in Aarhus, Denmark, in August 1997. The volume presents 26 revised full papers selected after two rounds of refereeing from initially 92 submissions; also included are four invited papers. The book addresses all current aspects of computer science logics and its (...) class='Hi'>applications and thus presents the state of the art in the area. (shrink)

This chapter offers an opinionated introduction to higher-order formal languages with an eye towards their applications in metaphysics. A simply relationally typed higher-order language is introduced in four stages: starting with first-order logic, adding first-order predicate abstraction, generalizing to higher-order predicate abstraction, and finally adding higher-order quantification. It is argued that both β-conversion and Universal Instantiation are valid on the intended interpretation of this language. Given these two principles, (...) it is then shown how we can use pure higher-order logic to ask, and begin to answer, metaphysical questions with non-trivial implications. In particular, while we must reject the popular idea that structural differences between sentences correspond to parallel distinctions in the logical structure of extra-linguistic reality, it may still be possible to give a purely logical characterization of objectual aboutness and related notions. (shrink)

This volume contains finalized versions of papers presented at an international workshop on extensions of logic programming, held at the Seminar for Natural Language Systems at the University of Tübingen in December 1989. Several recent extensions of definite Horn clause programming, especially those with a proof-theoretic background, have much in common. One common thread is a new emphasis on hypothetical reasoning, which is typically inspired by Gentzen-style sequent or natural deduction systems. This is not only of theoretical (...) significance, but also bears upon computational issues. It was one purpose of the workshop to bring some of these recent developments together. The volume covers topics such as the languages Lambda-Prolog, N-Prolog, and GCLA, the relationship between logic programming and functional programming, and the relationship between extensions of logic programming and automated theorem proving. It contains the results of the first conference concentrating on proof-theoretic approaches to logic programming. (shrink)

Kleene's realizability interpretation for first-order arithmetic was shown by Hyland to fit into the internal logic of an elementary topos, the “Effective topos” . In this paper it is shown, that there is an internal realizability definition in , i.e. a syntactical translation of the internal language of into itself of form “n realizes ” , which extends Kleene's definition, and such that for sentences , the equivalence [harr]n is true in . The internal realizability definition depends on (...) finding separated covers for non-separated objects of . However, for the objects arising in higher-order arithmetic, canonical covers are available, which are definable in higher-order arithmetic. These canonical covers yield “covering axioms”. It is shown that these covering axioms, together with uniformity principles and Extended Church's Thesis, axiomatize a formalized extension of Kleene realizability to a constructive system of higher-order arithmetic. The details are worked out for second and third-order arithmetic, but the method can be extended to any order. As an application, it is shown in the final section that a certain completeness property of the category of “modest sets” can be derived in third-order arithmetic from the realizability axioms. (shrink)

This is the first comprehensive textbook on higher order logic that is written specifically to introduce the subject matter to graduate students in philosophy. The book covers both the formal aspects of higher-order languages -- their model theory and proof theory, the theory of λ-abstraction and its generalizations -- and their philosophical applications, especially to the topics of modality and propositional granularity. The book has a strong focus on non-extensional higher-order logics, making (...) it more appropriate for foundational metaphysics than other introductions to the subject from computer science, mathematics, and linguistics. A Philosophical Introduction to Higher Order Logics assumes only that readers have a basic knowledge of first-order logic. With an emphasis on exercises, it can be used as a textbook though is also ideal for self-study. Author Andrew Bacon organizes the book's 18 chapters around four main parts: I. Typed Language II. Higher Order Languages III. General Higher-Order Languages IV. Higher-Order Model Theory In addition, two appendices cover the Curry-Howard isomorphism and its applications for modeling propositional structure. Each chapter includes exercises that move from easier to more difficult, strategically placed throughout the chapter, and concludes with an annotated suggested reading list providing graduate students with most valuable additional resources. Key Features Is the first comprehensive introduction to higher-order logic as a grounding for addressing problems in metaphysics Introduces the basic formal tools that are needed to theorize in, and model, higher order languages Offers an abundance of: - Simple exercises throughout the book, serving as comprehension checks on basic concepts and definitions - More difficult exercises designed to facilitate long-term learning Contains annotated sections on further reading, pointing the reader to related literature, learning resources, and historical context. (shrink)

This volume contains papers presented at the second international workshop on extensions of logic programming, which was held at the Swedish Institute of Computer Science, Stockhom, January 27-29, 1991. The 12 papers describe and discuss several approaches to extensions of logic programming languages such as PROLOG, as well as connections between logic programming and functional programming, theoretical foundations of extensions, applications, and programming methodologies. The first workshop in this series was held in T}bingen (...) in 1989 and its proceedings areavailable as LNCS 475. The third workshop will be held in Bologna in 1992. (shrink)

A major strategy to reduce transport congestion and other social costs of transport is to ensure that travellers make the best decisions, based on real time information. A wide range of technological systems have been developed to provide this information, but little is known about how travellers actually respond to it. This book offers an overview of various transport telematics options and provides an appropriate methodological framework, followed by a presentation of results from actual applications of these telematics systems (...) from a range of European countries in various transport sectors. The empirical results are supplemented by analytical models and geographic information systems representations with a view on generalizing these findings and identifying the key parameters which determine user response. (shrink)

On at least one of its uses, ‘higher-order evidence’ refers to evidence about what opinions are rationalized by your evidence. This chapter surveys the foundational epistemological questions raised by such evidence, the methods that have proven useful for answering them, and the potential consequences and applications of such answers.

This paper deals with higher-order vagueness in Williamson's 'logic of clarity'. Its aim is to prove that for 'fixed margin models' (W,d,α ,[ ]) the notion of higher-order vagueness collapses to second-order vagueness. First, it is shown that fixed margin models can be reformulated in terms of similarity structures (W,~). The relation ~ is assumed to be reflexive and symmetric, but not necessarily transitive. Then, it is shown that the structures (W,~) come along with (...) naturally defined maps h and s that define a Galois connection on the power set PW of W. These maps can be used to define two distinct boundary operators bd and BD on W. The main theorem of the paper states that higher-order vagueness with respect to bd collapses to second-order vagueness. This does not hold for BD, the iterations of which behave in quite an erratic way. In contrast, the operator bd defines a variety of tolerance principles that do not fall prey to the sorites paradox and, moreover, do not always satisfy the principles of positive and negative introspection. (shrink)

There is an intrinsic connection between genocide and colonialism where both concepts are in close proximity and are based on the logic of elimination. The fact that an active genocide of the Palestinian people continues in 2024 is extremely disturbing. A plethora of human rights laws and principles complement and reinforce the protections afforded under international humanitarian law. These laws were developed in order to prevent historical atrocities from repeating themselves. As history is re-written, it is submitted (...) that these laws, while good on paper, are not being put into practice in the case of Palestine. This article reflects on the application of specific international humanitarian laws, namely protecting healthcare, preserving nutrition and safeguarding children during times of conflict, and analyses how these protections are being flouted in the case of Gaza. (shrink)

This article defends the teaching of Mortimer J. Adler that human education must aim at the betterment of human beings by forming good habits in us; and that, if intellectual and moral virtues, or good habits, are the same for all human beings because our natural capacities are the same and tend naturally to the same developments, then what logically follows is that the intellectual and moral virtues, or good habits, as the ends of education, are the absolute and universal (...) principles on which education should always and everywhere be founded. This being the case, it concludes that, because of its essential foundation in the essentially flawed Enlightenment understanding of human nature, the New World Order can never be a cause of higher education, can, at best, cause a caricature of it. (shrink)

These are the proceedings of the First International Conference on Compu- tional Logic (CL 2000) which was held at Imperial College in London from 24th to 28th July, 2000. The theme of the conference covered all aspects of the theory, implementation, and application of computational logic, where computational logic is to be understood broadly as the use of logic in computer science. The conference was collocated with the following events: { 6th International Conference on (...) Rules and Objects in Databases (DOOD 2000) { 10th International Workshop on Logic-based Program Synthesis and Tra- formation (LOPSTR 2000) { 10th International Conference on Inductive Logic Programming (ILP 2000). CL 2000 consisted of seven streams: { Program Development (LOPSTR 2000) { Logic Programming: Theory and Extensions { Constraints { Automated Deduction: Putting Theory into Practice { Knowledge Representation and Non-monotonic Reasoning { Database Systems (DOOD 2000) { Logic Programming: Implementations and Applications. The LOPSTR 2000 workshop constituted the program development stream and the DOOD 2000 conference constituted the database systems stream. Each stream had its own chair and program committee, which autonomously selected the papers in the area of the stream. Overall, 176 papers were submitted, of which 86 were selected to be presented at the conference and appear in these proceedings. The acceptance rate was uniform across the streams. In addition, LOPSTR 2000 accepted about 15 extended abstracts to be presented at the conference in the program development stream. (shrink)

This edited book focuses on non-classical logics and their applications, highlighting the rapid advances and the new perspectives that are emerging in this area. Non-classical logics are logical formalisms that violate or go beyond classical logic laws, and their specific features make them particularly suited to describing and reason about aspects of social interaction. The richness and diversity of non-classical logics mean that this area is a natural catalyst for ideas and insights from many different fields, from information (...) theory to game theory and business science. This volume is the post-proceedings of the 8th International Conference on Logic and Cognition, held at Sun Yat-Sen University Institute of Logic and Cognition in Guangzhou, China in December 2016. The conference series started in 2001, and is organized by the ILC, often in collaboration with various international research groups. This eighth installment was jointly organized by ILC and Alessandra Palmigiano's Applied Logic research group. The conference series aims to foster the development of effective logical tools to study social behavior from a philosophical, cognitive and formal perspective in order to challenge the field of logic in ways that open up new and exciting research directions. Chapter "The Category of Node-and-Choice Forms, with Subcategories for Choice-Sequence Forms and Choice-Set Forms" of this book is available open access under a CC BY 4.0 license at link.springer.com. (shrink)

A number of authors have objected to the application of non-classical logic to problems in philosophy on the basis that these non-classical logics are usually characterised by a classical metatheory. In many cases the problem amounts to more than just a discrepancy; the very phenomena responsible for non-classicality occur in the field of semantics as much as they do elsewhere. The phenomena of higher order vagueness and the revenge liar are just two such examples. The aim of (...) this paper is to show that a large class of non-classical logics are strong enough to formulate their own model theory in a corresponding non-classical set theory. Specifically I show that adequate definitions of validity can be given for the propositional calculus in such a way that the metatheory proves, in the specified logic, that every theorem of the propositional fragment of that logic is validated. It is shown that in some cases it may fail to be a classical matter whether a given sentence is valid or not. One surprising conclusion for non-classical accounts of vagueness is drawn: there can be no axiomatic, and therefore precise, system which is determinately sound and complete. (shrink)

This volume contains several invited papers as well as a selection of the other contributions. The conference was the first meeting of the Soviet logicians interested in com- puter science with their Western counterparts. The papers report new results and techniques in applications of deductive systems, deductive program synthesis and analysis, computer experiments in logic related fields, theorem proving and logic programming. It provides access to intensive work on computer logic both in the USSR and (...) in Western countries. (shrink)

The systems Kα of transfinite cumulative types up to α are extended to systems K∞α that include a natural infinitary inference rule, the so-called limit rule. For countable α a semantic completeness theorem for K∞α is proved by the method of reduction trees, and it is shown that every model of K∞α is equivalent to a cumulative hierarchy of sets. This is used to show that several axiomatic first-order set theories can be interpreted in K∞α, for suitable α.

The question motivating my investigation is: Are the basic philosophical principles underlying the "core" system of contemporary logic exhausted by the standard version? In particular, is the accepted narrow construal of the notion "logical term" justified? ;As a point of comparison I refer to systems of 1st-order logic with generalized quantifiers developed by mathematicians and linguists . Based on an analysis of the Tarskian conception of the role of logic I show that the standard division of (...) terms into logical and extra-logical is partly arbitrary. I argue that the semantic principles of Tarskian logic allow any higher order mathematical predicate or relation to function as a logical term in a 1st-order system, provided it is introduced in the right way into the syntactic-semantic apparatus. ;Formally, I propose a new, "constructive", semantic characterization of logical terms. A logical term is defined by a function which, given a model, "shows" how to construct relations, sets, or n-tuples of individuals which satisfy it. I discuss the linguistic applicability of the extended logic and bring numerous examples. ;One chapter is devoted to branching quantification--a non-standard logico-linguistic construction obtained by affixing a non-linear, partially-ordered quantifier-prefix to a well-formed formula. Although standard branching quantifiers were given a complete account by Henkin and Walkoe, it is not altogether clear what the meaning of branching generalized quantifiers is. I propose a new analysis of the generalized branching prefix which extends the existent, partial, definitions due to Barwise, and I develop a generalization leading to a "family" of branching structures. ;In conclusion I discuss the philosophical impact of the generalized conception of logic on such issues as the logicist thesis, the interaction between mathematics and logic, ontological commitment via logic, metaphysics and logical semantics. (shrink)

This chapter provides an introduction to higher-order metaphysics as well as to the contributions to this volume. We discuss five topics, corresponding to the five parts of this volume, and summarize the contributions to each part. First, we motivate the usefulness of higher-order quantification in metaphysics using a number of examples, and discuss the question of how such quantifiers should be interpreted. We provide a brief introduction to the most common forms of higher-order logics (...) used in metaphysics, and indicate a number of questions which can be raised in such systems using logical vocabulary alone. Using a further example, we return to applications of higher-order logics in metaphysics. We also mention key developments in the history of higher-order logic as it pertains to metaphysics. Finally, we mention certain arguments which have been raised against the use of higher-order logic, and some ways of responding to them. (shrink)

The Annual Conference of the European Association for Computer Science Logic, CSL 2002, was held in the Old College of the University of Edinburgh on 22–25 September 2002. The conference series started as a programme of Int- national Workshops on Computer Science Logic, and then in its sixth meeting became the Annual Conference of the EACSL. This conference was the sixteenth meeting and eleventh EACSL conference; it was organized by the Laboratory for Foundations of Computer Science at the (...) University of Edinburgh. The CSL 2002 Programme Committee considered 111 submissions from 28 countries during a two week electronic discussion; each paper was refereed by at least three reviewers. The Committee selected 37 papers for presentation at the conference and publication in these proceedings. The Programme Committee invited lectures from Susumu Hayashi, Frank Neven, and Damian Niwinski; ́ the papers provided by the invited speakers appear at the front of this volume. In addition to the main conference, two tutorials – ‘Introduction to Mu- Calculi’ and ‘Parametrized Complexity’ – were given on the previous day. (shrink)

We extend epistemic stit theory with a modality \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$I_\alpha \varphi $$\end{document}, meant to express that at some moment agent \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\alpha $$\end{document} had a present-directed intention toward the realization of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\varphi $$\end{document}. The semantics is based on the extension of stit frames with special topologies associated to agents. The open sets of the associated topology (...) are interpreted as present-directed intentions, that support whether an agent had an intention of realizing a specific state of affairs when it chose one of its available actions and executed it. As an important application, we use \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$I_\alpha \varphi $$\end{document} to formalize intentional action and intentional responsibility. We present an axiom system for our logic of intentionality, and prove that it is sound and complete. (shrink)

Second-order quantifier elimination in the context of classical logic emerged as a powerful technique in many applications, including the correspondence theory, relational databases, deductive and knowledge databases, knowledge representation, commonsense reasoning and approximate reasoning. In the current paper we first generalize the result of Nonnengart and Szałas [17] by allowing second-order variables to appear within higher-order contexts. Then we focus on a semantical analysis of conditionals, using the introduced technique and Gabbay’s semantics provided in (...) [10] and substantially using a third-order accessibility relation. The analysis is done via finding correspondences between axioms involving conditionals and properties of the underlying third-order relation. (shrink)

The usage of sorts in first-order automated deduction has brought greater conciseness of representation and a considerable gain in efficiency by reducing the search spaces involved. This suggests that sort information can be employed in higher-order theorem proving with similar results.

Semantical arguments, based on the completeness theorem for first-order logic, give elegant proofs of purely syntactical results. For instance, for proving a conservativity theorem between two theories, one shows instead that any model of one theory can be extended to a model of the other theory. This method of proof, because of its use of the completeness theorem, is a priori not valid constructively. We show here how to give similar arguments, valid constructively, by using Boolean models. (...) These models are a slight variation of ordinary first-order models, where truth values are now regular ideals of a given Boolean algebra. Two examples are presented: a simple conservativity result and Herbrand's theorem. (shrink)

A growing number of applications of automated reasoning exhibitsthe necessity of flexible deduction systems. A deduction system should beable to execute inference rules which are appropriate to the given problem.One way to achieve this behavior is the integration of different calculi. Thisled to so called hybrid reasoning [22, 1, 10, 20] which means the integrationof a general purpose foreground reasoner with a specialized background reasoner. A typical task of a background reasoner is to perform special purposeinference rules according to (...) a built-in theory. The aim of this paper is togo a step further, i.e. to treat the background reasoner as a hybrid systemitself. The paper formulates sufficient criteria for the construction of complete calculi which enable reasoning under hybrid theories combined fromsub-theories. For this purpose we use a generic approach described in [20].This more detailed view on built-in theories is not covered by the knowngeneral approaches [1, 3, 6, 20] for building in theories into theorem provers.The approach is demonstrated by its application to the target calculi of thealgebraic translation [9] of multi-modal and extended multi-modal [7] logicto first-order logic. (shrink)

An embedding of many-valued logics based on SIXTEEN in classical higher-order logic is presented. SIXTEEN generalizes the four-valued set of truth degrees of Dunn/Belnap’s system to a lattice of sixteen truth degrees with multiple distinct ordering relations between them. The theoretical motivation is to demonstrate that many-valued logics, like other non-classical logics, can be elegantly modeled (and even combined) as fragments of classical higher-order logic. Equally relevant are the pragmatic aspects of the presented approach: (...) interactive and automated reasoning in many-valued logics, which have broad applications in computer science, artificial intelligence, linguistics, philosophy and mathematics, become readily enabled with state of the art reasoning tools for classical higher-order logic. (shrink)

THINKER is an automated natural deduction first-order theorem proving program. This paper reports on how it was adapted so as to prove theorems in modal logic. The method employed is an indirect semantic method, obtained by considering the semantic conditions involved in being a valid argument in these modal logics. The method is extended from propositional modal logic to predicate modal logic, and issues concerning the domain of quantification and existence in a world's domain are (...) discussed. Finally, we look at the very interesting issues involved with adding identity to the theorem prover in the realm of modal predicate logic. Various alternatives are discussed. (shrink)

The naive theory of vagueness holds that the vagueness of an expression consists in its failure to draw a sharp boundary between positive and negative cases. The naive theory is contrasted with the nowadays dominant approach to vagueness, holding that the vagueness of an expression consists in its presenting borderline cases of application. The two approaches are briefly compared in their respective explanations of a paramount phenomenon of vagueness: our ignorance of any sharp boundary between positive and negative cases. These (...) explanations clearly do not provide any ground for choosing the dominant approach against the naive theory. The decisive advantage of the former over the latter is rather supposed to consist in its immunity to any form of sorites paradox. But another paramount phenomenon of vagueness is higher-order vagueness: the expressions introduced in order to express in the object language the vagueness of the object language are themselves vague. Two highly plausible claims about higher-order vagueness are articulated and defended: the existence of “definitely ω ” positive and negative cases and the “radical” character of higher-order vagueness itself. Using very weak logical principles concerning vague expressions and the ‘definitely’-operator, it is then shown that, in the presence of higher-order vagueness as just described, the dominant approach is subject to higher-order sorites paradoxes analogous to the original ones besetting the naive theory, and therefore that, against the communis opinio, it does not fare substantially better with respect to immunity to any form of sorites paradox. (shrink)

First-order modal logic, in the usual formulations, is not suf- ficiently expressive, and as a consequence problems like Frege’s morning star/evening star puzzle arise. The introduction of predicate abstraction machinery provides a natural extension in which such difficulties can be addressed. But this machinery can also be thought of as part of a move to a full higher-order modal logic. In this paper we present a sketch of just such a higher-order modal (...) class='Hi'>logic: its formal semantics, and a proof procedure using tableaus. Naturally the tableau rules are not complete, but they are with respect to a Henkinization of the “true” semantics. We demonstrate the use of the tableau rules by proving one of the theorems involved in G¨ odel’s ontological argument, one of the rare instances in the literature where higher-order modal constructs have appeared. A fuller treatment of the material presented here is in preparation. (shrink)

In this book the authors reconcile two different viewpoints of the foundations of mathematics, namely mathematical logic and category theory. In Part I, they show that typed lambda-calculi, a formulation of higher order logic, and cartesian closed categories are essentially the same. In Part II, it is demonstrated that another formulation of higher order logic is closely related to topos theory. Part III is devoted to recursive functions. Numerous applications of the close (...) relationship between traditional logic and the algebraic language of category theory are given. The authors have included an introduction to category theory and develop the necessary logic as required, making the book essentially self-contained. Detailed historical references are provided throughout, and each section concludes with a set of exercises. Thus it is well-suited for graduate courses and research in mathematics and logic. Researchers in theoretical computer science, artificial intelligence and mathematical linguistics will also find this an accessible introduction to a subject of increasing application to these disciplines. (shrink)

Reverse mathematics is a program in the foundations of mathematics. It provides an elegant classification in which the majority of theorems of ordinary mathematics fall into only five categories, based on the “big five” logical systems. Recently, a lot of effort has been directed toward finding exceptional theorems, that is, those which fall outside the big five. The so-called reverse mathematics zoo is a collection of such exceptional theorems. It was previously shown that a number of uniform versions of the (...) zoo theorems, that is, where a functional computes the objects stated to exist, fall in the third big five category, arithmetical comprehension, inside Kohlenbach’s higher-order reverse mathematics. In this paper, we extend and refine these previous results. In particular, we establish analogous results for recent additions to the reverse mathematics zoo, thus establishing that the latter disappear at the uniform level. Furthermore, we show that the aforementioned equivalences can be proved using only intuitionistic logic. Perhaps most surprisingly, these explicit equivalences are extracted from nonstandard equivalences in Nelson’s internal set theory, and we show that the nonstandard equivalence can be recovered from the explicit ones. Finally, the following zoo theorems are studied in this paper: Π10G, FIP, 1-GEN, OPT, AMT, SADS, AST, NCS, and KPT. (shrink)

We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typedλ-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews' higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratethe parallels and differences of the extensionality treatment of these approachesand demonstrate that extensional (...) higher-order resolution is the sole approach thatcan completely avoid additional extensionality axioms. (shrink)

INTRODUCTION BY NANCY FUMERO What is a translation that stalls comprehension? That, when read, parsed, obfuscates comprehension through any language – English, Portuguese. It is inevitable that readers expect fidelity from translations. That language mirror with a sort of precision that enables the reader to become of another location, condition, to grasp in English in a similar vein as readers of Portuguese might from João Guimarães Rosa’s GRANDE SERTÃO: VEREDAS. There is the expectation that translations enable mobility. That what was (...) written in one language be accessible in another. And that a translator is to serve as a mediator, acting ultimately in service to ideas within the source text. To disperse them. However, this notion of translation is partly antithetical to the ideas in Rosa’s work. Or, alternately, to convey the despair of terrain slipping beneath one’s feet, and to encounter the heightened suspense of magic, the translation, as part of its strategy, cannot devotedly rely on its original language, not as its source text. The work undertaken by Felipe W.Martinez is a new form of translation that risks everything in order to encounter the same treacherous knowing Rosa had traversed. And it takes its risks by not taking risks: by being, almost word for word, a literal translation. This is an approach that reductively converts, as opposed to translates. The idiomatic differences between English and Portuguese are not accented. The syntax is not finessed. Liberties are not assumed on account of improving readability. What stands, resoundingly amid such absences, is the awakened challenge of reading. The genuine peril of not knowing. That is, this translation, one that purports to know nothing, creates access into the guileful world Rosa had created in Portuguese. But not by translating. If anything, GRANDE SERTÃO: VEREDAS is speaking a cosmic language through a linguistic one. And W.Martinez does us the service of recognizing this, as what configures the shapes of words and sentences is not as simple as neologisms, portmanteaus, and digressions, but as terrifying as the path the fool traverses: all paths. As such, this translation doesn’t speak English, just as the original does not speak Portuguese. It is the assemblage of paradox as a new logic that can be navigated, if only one could suspend the comfort of readability, of expectation. If one could descend a mountain in the pitch dark of night, each step shocking the body, unable to acclimate to the unleveled heights. Without a doubt, the translation is incongruous to the Portuguese. Taking a small excerpt to compare: Eh, well, thereafter, the rest the Sir provide: comes the bread, comes the hand, comes the god, comes the dog. What is striking is the interplay between “god” and “dog”. To most English speakers, this anagram is a familiar one. But in Portuguese the words god (“deus”) and dog (“cão”) are not so closely linked. In fact, there is no direct mention of “deus” in Rosa’s text: Eh, pois, empós, o resto o senhor prove: vem o pão, vem a mão, vem o são, vem o cão. Both are fascinating. In Rosa’s excerpt, the rhythm is unmistakable and precise, despite, of course, the indices of hesitation: the commas, the Eh, the uncomfortable way of searching through prolongation and wait. This is the sort of paradox Rosa can engage within a sentence. W.Martinez’s does this as well, at a scale that reverberates beyond the sentence, and with one noticeable addition: deus. What may appear to be an overstep, to add such a weighted word that draws out wordplay but is, nevertheless, not in the source text, is exemplary of risk. The translation buzzes because of it. This is because throughout the text we encounter dogs frequently, as some primal beast on par with humans. The dog is one that masters and can be mastered. A creature that is at times its face, and at others a mask. It is a powerful presence. For the translator to be attuned to the reverent undercurrent attributed to this animal, and create within the translation such charged play in English from what was only an implication in Portuguese, is in tribute to the grand beauty within dissonance. What aberrant modes of writing and translation can teach us most assuredly, is that things, words, are not in states of rightness or wrongness, but of oscillation. This isn’t so different from what Rosa says himself: The Sir look…see: the most important and beautiful, of the world, is this: that the people are not always same, still were not completed — but that they go always shifting. They tune or detune. We find this so readily in W.Martinez’s translation, this tuning and detuning. Nancy Fumero Los Angeles GRAND SERTÃO: VEREDAS BY JOÃO GUIMARÃES ROSA TRANSLATED FROM THE PORTUGUESE BY FELIPE W.MARTINEZ Nonothing. Shots that the Sir heard were man brawling not, God be. Bleach white sights on the tree in the backyard, down in the river. By my right. I do this every day, I like; from the bad of boyhood. Thereof they came to call on me. Case of a calf: a white calf, errorful, eyes of to not be—saw selves—; and with a mask of a dog! They told me; I didn’t want to catch a sight. Same that, by the defects of birth, upturned lips, looked to be a laughing man. Folkface, dogface: they determined—it was the devil. Bananas. Killed it. Do not know who owned it. They came to borrow my guns. I caved. I’ve no power to impose. Oh, sir, you laugh certain laughs…Look: when it’s a true shot, first the dogs begin to bark, instantly—after, then, you see who’s handed death. Sir, endure, this is the Sertão. Some want that it is not: that situated Sertão is in and out of those general fields, they say, end of the road, highlands, the other Urucuia. Toleima. For those of Cortino and of Curvelo, then, isn’t here said Sertão? Ah! That there’s more! To place the Sertão it’s told: it’s where the pastures lack latches; where one can tear off ten, fifteen leagues without running into a houseinhabitant; where criminalousness lives out its christ jesus. Sifted out from the tightening grip of the law. The Urcuia comes from the western mountains. But today, its banks, give all—farmlands of farms, pastures of meadows of good yield, low tides, cultures that go kill for kill, until these virgins there are. The general fields run round. These general fields are without size. Ultimately, whichever one one approves, the Sir knows: bread or breads, it’s a question of heads…the Sertão is everywhere. Of the devi? No comment. Sir ask the dwellers. Falsely I fear they unspeak that name of his—only say: whatsitcalled. Volt! no… Whosoever over avoids it, lives with it. In the sentence of one Aristides—who exists in the first palm grove on the right hand side, called Vereda-of-Cow-Calm-of-Saint-Rita—everyone believes: he can't pass in three designated places: then can be heard the tiny cry, behind, a little voice warning:— "Here I come! Here I come!... "— that is the Capirote, the whatsitcalled... And one Jise Simplicio—who anyone from here will swear he keeps an imp in house, a little satanite, imprisoned and obliged to help in all greedful deeds; reason that Simplicio emprises en route to complete riches. As such, for this they say too that his beast bristles and refuses, denying his banner, unyielding, when he wishes to mount... Superstition. Jise Simplicio and Aristides, continue getting fatter, thence unheard or heard. Still the Sir study: right now, in these days of time, you have people purporting that the devil proper stopped, mid-passage, in Andrequice. A boy out of there, to whom'd appeared, and there lauded that, to get here—normally, by horse, a day-n-half—he was capable of such with only some twenty minutes enough... by coasting the River of Chico by the headwaters! Or, too, who knows—sans offense—will not have been, for example, even yourself the Sir who announced such, when you passed by there, for fun run funny? Thereof, not my given crime, I know that wasn't. And evil I wanted not. Only that one question, in hours, at times, brightens peaceful reason. But, the Sir understand: if such a boy, there was, he wanted to dupe. Because, hey, that, to cut the river off by the springs, would be the same thing as one redoubling in the internals of this our state of ours, costant of a journey of some three months... Then? Whatsitcalled? Dodo. The fantastication. And, the respect of giving him such these names of delicacy, is what it is for one to want to invoke that he form of form, with his presence! Not that is. I, personally, almost that have lost in him the creed, deserving to Deus; is the that to the Sir I say, to pure-secret. I know that it is well established, that it greases our Saintly-Gospels. On occasion, I conversed with a young seminarian, super suitable, conferring in the book of prayers and coated in vestments, with a stick of black-sage in hand—prosed that he went auxilitator to the father, to extract the Cujo, from the body living of an oldwoman, in Waterfalls-of-Bulls, he went with the vicar of Field-Round... I conceive. The Sir not is as I? I didn't believe a single thing. Compadre mine Quelemem describes that that which reveals effect are the low spirits meager, of third, adoing in the worst darkness and with anxieties of connecting selves with the livers—they give support. Compadre mine Quelemem is who much me consoles—Quelemem of Goias. But he has to live far from here, in Jijuja, Vereda of Buriti Dark... Ahrr, I leave myself there, that in enevildemonment or with support—the Sir too must have had known diverse, men, women. As not yes? For me, umpteen I've seen, that I've learned. Ma-Neigh, Blood-o'Other, or Legion-Lips, or Tear-em-Down, Cold-Cutter, or Sissy-Goat, one Treciziano, or Verdigris... or Hermogenes... o'them, pileload. If I could forget so many names... I'm not a man for calming horses! And, same, whom of yes of to be jagunço self enters, yea is for some competence entrant of demonion. Will it not? Will it? From first, I made and mixed, and to think not I thought. I didn't have the deadlines. I lived pulling difficult from difficult, fish alive on griddle: who lives asp'rously, no fantasies. But, now, fete of fate to me comes, and sans little disquietudes, I'm from creaky net. And myself invented in this like, of to speculate ideas. The devil exists and nonexists? I say the saying. Opennouncement. These melancholies. The Sir sees: exists waterfall; and since? But waterfall is gulch of ground, and water so pouring from it, retumbling; the Sir consume that water, or undo that bankment, remainder waterfall any? To live is negotiation much perilous. I explain to the Sir: the devil vigors inside of human, the wrinkles of human— or is the human ruin, or the human of adversess. I free, per se, citizen, is that not has devil notone. Notone!— is the that I say. The Sir approve? Me declares total, frank— is high merit that me make: and to beg might, increased. This case— by rashtravagance that me they see— is of mine certain importance. God grant not was... But, not say that the Sir, awised and instructed, that agrees in people of them?! Not? You I appreciate! Your high opinion composes my value. Yea I knew, waited for it— yea the field! Ah, a we, in oldness, we lack of to have plowing of rest. You I appreciate. Is devil notone. Nor esprit. Never I've seen. Someone ought to see, then was I myself, this your servant. Was I you to tell... Well, the devil regulate his state black, ins creatures, ins womens, ins humans. E'en: ins childrens— I declaim. Since not is said: "boy—trainee of the devil"? And ins thes uses, ins plants, ins waters, in terra, in wind... Manures. …The devil in the street, in the middle of the vortex... Hey? Hey? Ah. Figuration mine, of worse by back, the certain memories. Mal-make me! I suffer pain of to tell not…Meliorate, if chillingly: well, in a ground and with equal format of branches and leaves, not give to cassava-calm, that is eaten common, and the cassava-mad that kills? Now, the Sir yea saw a strangeness? A cassava-sweet can rapidly to turn agonizing— motives not I know, at times is said that is for replanted in the terrain always, with mutations then, of caules—go embittering, of s’much in s’much, of its self takes poisons. And, well look: the other, the cassava-mad, too is that at times can fix calm, the estimate, of is to eat sans notone mal. And what this is? Eh, the Sir yea saw, for to see, the ugliness of hate pleated, facetorqued, on the faces of one cobrarattlesnake? Observed the porker fat, capita day more felicity brute, capable of, could, snort and engulf for its own dirty coziness the world total? And sparrowhawk, blackbird, some, the features of they yea represent the need of cleave for before, rend and shred by beak, appears a knife much fine for ruin I desire. Total. Has even twisted races of stone, horrorous, venomous— that spoil mortal the aquas, if they are buried beneath of well; the devil inside of them sleeps: they are the devil. Is known? And the demon— that is only thus the significance of one mercury malign— have order of to follow the path of him, have license to brag?! Arr, he is variegated in all! What the what wastes, goes spending the devil of inside of the people, by itttybits, is the reasonable to suffer. And the delight of love—compadre mine Quelemem says. Family. Really? Is, and not is. The Sir think and not think. Total is and not is… Almost all more grave criminous ferocity, always is much good husband, good son, good father, and is good-friend-of-your-friends! I know of those. Solo that have the afters— and Deus, joined. I spy many nimbi. But, in veracity, son, too, softens. Look: one called Aleixo, resident a league from Step-of-Sour, in Of-Sand, was the man of major badness calm that yea you saw. Me agreed that near the house of his had a weir, amidst the palms, with traíras, for souls of enormous, desenormous, to the real, that received fame; the Aleixo gave of to eat to them, in hours just, they self accustomed to if assuch of lunacies, in order to gobble, seemed to be fishes instructed. One day, solo for grace rustic, he killed an oldman who by there passed, destitute begging alms. The Sir not doubt—have people, in this bored world, that kill solo in order to see someone make grimace… Eh, well, thereafter, the rest the Sir provide: comes the bread, comes the hand, comes the god, comes the dog. This Aleixo was man afamilied, had children small; they were the love of his, total, absurdity. Gave good, that not even a year there passed, of to killed the oldman poor, and the children of Aleixo there they asickened. Smallepidemic of measles, they said, but complex; they never heal. When, then, they healed. But the eyes of theirs vermillionized high in an inflame of spraining to rebellion; and nexthing— the that not I know is if they went of at once, or one later and later other and other— they remained blind. Blind, sans remission of one sweet of light of this Ours! The Sir imagine: stairset— three boys and one girl— all blind. Sans remediable. The Aleixo not lost the judgment, but he changed; ah, mutated complete— now lives of band of Deus, sweating to be good and charitous in all his hours of night and of day. Appears even that he fixed the felicity, that before not was. He himself says he was a man of luck, because Deus wanted to have pity of him, to transform for there the route of his soul. That I heard, and me it gave rage. Reason of the children. If being castigated, what culpa of the let-there-bes of Aleixo those little children had?! Compadre mine Quelemem reproved my uncertainties. That, for certain, inother life returnaound, the children too had been the most wicked, of the mass and part of the father, demons of the same kettle of place. Sir the what thinks? And the oldman, assassinated? — I know the Sir goes to discuss. Well, too. In order that he had a sin of crime, in the body, by to pay. If the people— conforming compadre mine Quelemem is who says— if the people turn to to incarnate renovated, I contemplate even that enemy of death can come as son of the enemy. Look see: if to myself I say, has a subject Pedro Pindo, neighbor of here more six leagues, man of good for all in all, he and the woman of his, always been good, of goodness. They have a son of some ten years called Valtei—name modern, is the that the population of here now appreciates, the Sir knows. Well this-little-thing, thislet, since that some understanding illuminated in him, deed demonstrated the that is: petition stepfather, acid burner, likeful of ruin of inside of the profundity of the species of its nature. In which that torments, to the slowly, of all beasts or raisinglings little that quarrel; one time he found a creole woman hooched foolish sleeping, he arranged a shard of bottle, lashed at three points on the stern of the legs of hers. The what this boy drooled seeing, is bleeding hen or to knife pig.— “I enjoy of to kill…”— one occasion he teeny me told. He opened in me a fright; because: birdy that self leans over— the flight yea is ready! Well the Sir oversee: the pa, Pedro Pindo, mode of to correct this, and the ma, they give in him, misery and mast—they cast the boy sans to eat, they tied to trees in the yard, he nude, unplumed, even in June cold, they tilled the bittybody of his with the trammel and with the goblet, after they cleansed the skin of the sanguine, with bottle gourd brine. The people know, spy, fix wasted. The boy yea relowered of thinness, the eyes entering, caress of bones, enskulled, and tuberculated, the time total hacking, coughness of the that draw parched pectorals. Arr, that now, visible, the Pindo and the woman self habituated of on him hit, of little bit in little they were creating in this a pleasure ugly of diversion— as they regulate the canings in hours certain comfortable, until they call people to see the example good. I think that boy not endure, yea there is in the ta-da, not arrive for the lent to come… Ooee-ooee, then?! Not being as compadre mine Quelemem to want, that explication is that the Sir bestowed? That boy had to be a man. He should, in swing, terrible perversities. Soul of his was in the pitch. Demonstrated. And, now, paid. Ah, but, happens, when he’s crying and paining, he suffers equal that as was as a boy good… Bird, I saw all, in this world! Yea I saw even horse with hiccups… —the that the thing most costous that is. Good, but the Sir may say, should of: and in the start— for offenses and arts, the people— as for that was that s’much amended was started? Ey, ey, ey all collided. Compadre mine Quelemem, too. Am solo a sertanite, in these high ideas I navigate mal. Am much poor poor-thing. Envy my pedigree and of ones conform the Sir, with total reading and doctoration. Not is that I be illiterate. I spelt, years and middle, midly speller, memory and palmer. I had master, Master Lucas, in the Curralinho, he memorized grammar, the operations, rule-of-three, even geography and study patria. On leaves great of paper, with caprice I traced handsome maps. Ah, not is for to speak: but, since of the start, me they thought sophisticated of side. And that I merited of to go to course latin, in Lesson Waterlily—that too they said. Time nostalgic! Going today, I appreciate a good book, despaced. On the farm The Lilittlelemon, of one mine friend Vito Soziano, so sign of this almanac thick, of logoglyphs and conundrums and other divided matters, all year come. In s’much, I place primacy is in the reading advantageous, life of saints, virtues and examples— missionary astute engambling the Indians, or Saint Francis of Assis, Saint Anthony, Saint Gerald… I like much of moral. To ratiocinate, exhort the others for the good way, to acounsel to just. Mine woman, that the Sir knows, vigils for me: much prayer. She is a blessable. Compadre mine Quelemem always says that I may to aquiet my fears on conscience, that being well-attended, terrible good-esprits me protect. Eep! With like… As is of saint effect, I help with mine to want to accredit. But not even always can I. The Sir knew: I total the mine life I thought for me, lining, I am born different. I am and I same. I divert of total the world… I almost that nothing not I know. But I disconfide of many things. The Sir, conceding, I say: in order to think long, I am dog master— the Sir loose in mine front an idea ease and I research that by profundity of total the backwoods, amen! Look: the should of to have, was of so reunited-selves the wise, politicos, constitutions graded, closed the definitive the notion— to proclaim for one time, art assemblies, that not have devil notone, not exists, not possible. Valor of law! Solo assuch, they gave tranquility good to the people. Because the government not cares?! Ah, I know that not is possible. Not me settled the Sir for philistine. One this is to place ideas arranged, other is to deal with country of people, of flesh and sanguine, of thousand-and-many miseries… S’many people—gives scare of to know—and notone so calms: All nascenting, crescendoing, so wedding, wanting collocation of employment, consumables, health, abundance, to be important, wanting rain and affairs good… Of luck that lacks of so to choose: or we t’weave of to live in the salacious common, or care solo of religion solo. I could to be: father clergyman, if not chief of jagunços; for other things not was I birthed. But mine oldness yea principaled I erred of total account. And the rheumatism… There as whom says: in the primers. Ahem. Hey? Hey? The that more I think, I testify and explain: all-the-world is mad. The Sir, I, we, the people all. For this is that so lacks principally of religion: in order to desendodorize, to disdodoate. Pray is that heals of lunacy. In the general. This is that is the salvation-of-the-soul…Much religion your servant! I here, not I lose occasion of religion. I profit of all. I drink water of all rivers… One solo, for me is little, maybe not me arrives. I pray christian, catholic, I burrow the certain; and I accept the prayers of compadre mine Quelemem, doctrine of he, of Kardec. But, when I can, I go in the Mindubim, where one Matias is believer, methodist: the people so accuse of sinner, reads high the bible, and why, singing hymns beautiful of his. Total me quiets, me suspends. Whatever small shade me refreshes. But is solo much provisory. I wanted to pray— the time total. Many people not me approve, they think that law of Deus is privileges, invariable. And I! Doof! I Detest! The what I am? — the what I do, that want, much curia. And in face of total I face, executed. I? —not I trammel. Look: I have a black girl, Maria Leoncia, long from here not she lives, the prayers of her afame much virtue of power. Well to her I pay, every month— ordering of to pray for me one third, every saint day, and, on the Sundays, a rosary. Value, so values. Mine woman not sees mal in this. And I am, yea mandated word for an other, of the voyage-voyage, a Izina Calanga, in order to come here, I heard of that prayer too with grand mermermerits, I go to effect with she treatment equal. I want handful of those, me defending in Deus, reunited of me in volta… Cuts of Christ! To live is much perilous… To want the good with too much force, of incertain way, can yea to be being so wanting the mal, per to initiate. These humans! All they pull the world for itself, for the to concert amended. But capita one solo sees and understands the things of one his world. Amountain, the most supro, most serious was Mediero Vaz. That one man ancient… his Joaozy Ben-Ben, the most brave of all, no-one never can decipher how he by inside consisted. Joca Ramiro— grand man prince!— was politico. Zé Bebelo wanted to be politico, but had and not had luck: fox that lingered. So Candelario so demonized, by to think that was with illness mal. Titao Passos was the by the appreciation of friends: solo per via of them, of his same amities, were that such high so ajagunçoed. Antonio Do— severe bandit. But by half, grand majority half that be. Andalecio, in the profound, a good man-of-good, being raving in his total justice. Ricardao, same, wanted was to be rich in peace: for this he warred. Solo the Hermogenes was that born formed tiger, and assassinite. And the “Ofidios White”? Ah, not me speak. Ah this… joyless mischeivious, that was— that was a poor boy of the destiny… So good, congruous. The Sir heard, I you told: the ruin with the ruin, they terminate by the spine-bushes so to crack— Deus awaits that spendance. Boy!: Deus is patience. The contrary, is the devil. So consumes. The Sir file knife on knife— and file— that so they scrape. Even the rocks of the profound, one of in the other, they go-so aroundabounding even, that the rivulet rolls. Per enquantity, that I think, total as hath, in this world, is because so merits and lacks. Afterly precise. Deus not so reports with rifle, not garrotes the regulation. For what? Quit: goof with goof—one day, some illumination and learn: smart. Solo that, at times, for most auxiliar, Deus begets, in the middle, a pinch of pepper… Therebe? Well, for example: some time, I went of train, there in Seven-Lagoons, for parts of to consult a medical, of name me indicated. He went vested well, and in car of first, by via of the doubts, not me they shadowed for jagunço ancient. It goes and happens, that, close same of me, enfront, he took aseat, returning from the wild North, a mac Jazevedao, delegate professionale. Came with a capanga of his, an undercover, and I well knew the two, of that s’much a was ruin, as the other ruin was. The veracity to say, first I had the strict of me to surpasss for one lonng, to mutate of my place. Judgement me told, meliorate stay. Well, looking, I looked. And— you I tell: never I saw face of man furnished of brutez or malady more, of the them in that. As that was ogre, trussed of thickset, relustered of crude in the eyes small, and armed a chin of stone, toweringbrow; not of mid nor forehead. Not laughed, not so laughed not even one time; but, speaking or silent, the people appeared always to him some teeth, prey pointed of canids. Arr, and blustered, an ittybit. Solo growled curt, low, the mid-words grizzled. He came relooking, historicizing the documents— one by one the leaves with portraits and with the blacks of the digits of jagunços, lifters of horses and criminouses of death. That application of work, in one thing of those, generated the ire in the people. The undercover, busybodyguard, total close, seated joined, attending, excelling of to be dog. Me made a dread, but solo in the goof of the corpus, not in the intern of the courages. One hour, one of those reports fell— and I bent quickly, I knew there precisely by why, not I wanted, not I thought— even today I raise shame of this— I picked the paper of the ground, and delivered to him. Thereof, I say: I had more rage, because I did that; but there yea it was done. The man not even me looked, not even said notone thankfulment. Event he soles of the shoes of his— solo looking— that soles rough thick, bent of enormous, appearing iron bronzed. Because I knew: This Jazevedao, when he apprehended someone, the primary quiet thing that proceeded was that he came entering, sans to have to to say, feigning some hurry, and go stepping on the top of the feet of the poorthings. And that on these occasions he gave laughters, gave… Well, geck! I delivered to him the leaf of paper, and went leaving of there, by to have hand on me of not to destroy by shots that subject. Meat that much they weigh… And umbilicated beginning of belly pot bellied, that me created will… With my lightness, joyful that I’d kill. But, the barbarities that this delegate made and happened, the Sir not even has callus in heart to be able me to hear. He achieved of many men and women to cry blood, for the simple universolo ours here. Sertão. The Sir knows: sertão is where mandates who is strong, with the guile. And bullet is a tidbit of metal… S’much, I say: Jazevedao— one assuch, should of to have, needed? Ah, need. Leather ruined is that calls goad of point. That there be that, after— business particular of he— in the life or in the other, each Jazevedao, accomplished the that he has, desclimbs in his time of pain, too, until to pay the that he gave— compadre mine Quelemem is there, in order to fiscalize. The Sir knows: the peril that is to live… But solo of the mode, of these, by ugly instrument, was that the jagunsaga so finished. Sir thinks that Antonio Do or Olivino Oliviano were going to fix goodies by pure spelling of itself, or by begging of the infelicitous, or by always to hear sermon of father? You I think! In the aims… Of jagunço comported active in order so to repent in the middle of his jagunsagas, solo I lay of one: called Joe Cazuzo— was in smashing of one shotshow, for on the summit of the place Sierra New, district of river rusted, on the stream Traçadal. We made mal minority small, and they closed in order summit of us the personnel of one Coronel Adalvino, forted politico, with many soldiers uniformed in the center, commanding of the Lieutenant Epiphany Helm, that after fixed captain. We lasted hour more hour, and yea gave almost of encircled. There, of misslip, that Joe Cazuzo— man much valiant— so kneeled turned on the ground of the thick, lifted the arms that not even shoots of Jatoba dry, and solo yell, howl clear and howl deaf:— “I saw the Virgin Ours, in the resplendor of the Heavens, with her children of angels!... ” He screamed not touched. — “I saw the Virgin!... ” He ensouled? We desequaled. Bolt for my horse—that I thought— I leaped in mal seat, noteven I knew in which rupture-time I unfastened the halter, of tied up it foot of timber. I flew, arrived. Bullet come. The pasture roared. In the brush, the fear of the people so goes to the whole, one fear intentional. I could to lash out, fated burro brute, giv-that, giv-that. Some two or three bullets so drovein the pad of the mine saddle, they perforated of to tear away almost much the kapok of the filling. Horse trembled in pro, in middle of gallop, I know: thinks in the owner. I not fit of to be more well shrunken. Bulleted came to the sack that I had on the back, with few mine things. And other, of fusil, in ricochet decreed, heated my thigh, sans me wound, the Sir see: bullet does the what to want—so pierced impressed, between in me and the harness! Times crazy… Burumbum!: the horse so kneeled in the fall, dead perhaps, and I yea falling for front, embraced in foliage full, branched and linias, that me swayed and skewered, done I was pendulating in web of spider… Whither? I traversed that life total… Of fear of anxiety, I ruptured to read with mine corpus that forest, I know there — and me fell world below, rolled for the hollow of a grotto closed of shrubs, always me grasped— rolled same assuch: after: after, when I saw mine hands, total on they that not was withdrawn sanguine, was smeared green, on the digits, of leaves living that I pulled and mashed… I landed on the sedge of the profound— and a beast dark gave a releap, with a sneeze, too mad of fright: that was a papa-mel, that I descried; in order to flee, this is solely. Bigger being I, me doused mine overcoat; I spigotted total. And of one bit of thought: if that beast irara lying there then there not had cobra. I took the place of his. Existed cobra notone. I could me to lose. I was solo spineless, softness, but that not deadened, inside, the collisions of the heart. I gasped. I conceived that they came, me kill. Not even did mal, me mattered not. Assuch, some moments, at least I guarded the license of term in order me to rest. Conforming I thought in Diadorim. Solo I thought was in he. One joão-congo sang. I wanted to die thinking in my friend Diadorim, hand-o-bro, who was on the Sierra of WoodO’Bow, almost on the border baiana, with our other half of the so-candelarios… With my friend Diadorim me embraced, sentiment my went-flew right for he… Ay, arr, but: that this mine mouth not has order notone. I am accounting outside, things divagated. In the Sir me confide? Til-that, til-that. Say the angel-of-the-guard… But, conforming I came: after so knew, that same the soldiers of the Lieutenant and the goats of Coronel Adalvino remitted of to respect the blast of that Joe Cazuzo. And that this ended being the man most pacificious of the world, fabricator of oil and sacristan, in the Saint Sundays White. Times! For total, cleaned revelation, I fix thinking. I like. Meliorate, for the idea if well to open, is travelling in train-of-iron. Could, lived to top and to bottom, inside of it. Information that I ask: same in the Heavens, end of end, how is that the soul wins so to forget s’much sufferments and maladies, in the received and in the given? The how? The Sir knows: are things of hideous ofmuch, have. Pain of corpus and pain of idea mark forted, that forted as the total love and rage of hate. Goes, sea… Of luck that, then, the Firmiano, by appellationed Louse-of-Snake, so leoprosized with the leg disconformed, thickening, of that disease that not so cures; and not discern almost more, constant the branchials in the eyes, of the cataracts. Of before, years, had to of so disarray of the jagunsaga. Well, one occasion, some was on the ranch of his, on the High Jeuitai, after accounted—that, turns time, comes subject, he would say: “Me give yearning is of to seize a soldier, and such, for one good flay, with knife blind… But, first, to castrate…” The Sir conceive? Who has more dose of demon in self is Indian, any race of brusque. Folk see nation ofthese, for there profound of the generals of Goias, theofwhere has vagarous grand rivers, of aquas always so clear pleasantly, running of down crystal rosed… Louse-of-Snake gave of sanguine of heathen. Sir me will say: but that he pronounced that out of mouth, manner of to represent that yet not was old decadent. Opus of to oppose, for fear of to be tame, and cause in order so to see respected. Total listened for such rule: palavered of ruins, for more so valued, because we to the environs is hard durability. The worst, but, is that they finish, through the same ford, given of one day to execute the declared, in the real. I saw s’much crudity! Pain not pays to account; if I go, I collide. And me dedrip, three that me sicken, this total. Me convokes that the personnel, today in day, is good of heart. This is, good in the trivial. Malices wildwants, and perversities, always have some, but scarcities. Generation mine, true, was not assuch. Ah, goes to turn a time, in which not is used more to kill people… I yea am old. Good, I was saying: question, this that me excavates… Ah, I formed that question, for compadre mine Quelemem. That me responded: that, for close to heaven, we so amplified so, that total the uglies past so exhaled of not to be—fated sans-modus from time of youngster, mal-arts. As we not lack of to have remorse of the which divulged in the pulsation of his nightmares of one night. Assuch that: fleeced-so, flourished-so! Ahem. For this said, is that the journey to the Heavens is delayed. I confide with compadre mine Quelemem, the Sir knows: reason of creed same that has—that, for total the mal, that so does, one day so repays, the exact. Subject assuch rises three times, in ante of to want to facilitate in any minutia reprehensible… Compadre mine Quelemem never speaks vacant, not subtreats. Solo that this to he not I go to expose. We never should have to declare that accept entire the alien—that is what is the rule of the king! The Sir look…see: the most important and beautiful, of the world, is this: that the people are not always same, still were not completed — but that they go always shifting. They tune or detune. Truth major. Is the that the life me taught. This that me animates, mound. And, other thing: the devil and the brutes; but Deus is treacherous! Ah, a beauty of treacherous— gives like! The force of his, when he wants— boy!— me gives the fear dread! Deus comes coming: no one not sees. He does in the law of gentle— assuch is the miracle. And Deus attacks beautiful, so amusing, so economizes. The well: one day in a tannery, the little knife mine I had dropped inside of a tank, solo soup of bark of tan, stryphnodendron adstringens, angico, there I know. —“Tomorrow I try…”— I said, withmyself. Because it was of night, light notone I not disputed. Ah, then, I found: on the other day, early, the knife, the iron of it, had been gnawed, almost by half, by that aqua dark, total quiet. I left, for more to see. Crack, fuse! Know the what was? Well, in that same of afternoon, there: of the little knife solo so found the handle… The handle, for not to be of cold metal, but of horn of deer. There is: Deus… Good, the Sir heard knows, the that knows me understands… We sum, not think that religion fractures. Sir think the contrary. Visible that, those other times, I painted—belief that the neoglaziovia variegata lifts the flower. Ah, good my joy… Boyhood. But boyhood is task for more later so to deny. Too, I of that of to think in vague in s’much, lost mine hand-of-man for the management hot, in the middle of all. But, today, that I ratiocinated, and think the endeavor, not nor for this not I give for low my competence, in a fire-and-iron. The to see. Would approach would come here with war on me, with bad parts, with other laws, or with excessive looks, and I even draw to ignite this zone, ay, if, if! Is in the mouth of the blunderbuss: is in the rete-te-tem… And lonelyonly not I am, there-of-the. For not this, I was I placed encircle my mine people. Look the Sir: here, close, vereda below, the Paspe — cropper my — is mine. More league, if that, have the Herpetotheres, and have the compadre Ciril, him and three children, I know that they serve. Band of that hand, the Alaripe: knew the Sir the that is that so boasts, in rifleation and by the knife, one cearense did this! After more: the João Innatal, the Quipes, Lophiosilurus-of-claws. And the Fafafa— this gave fights high, all side with me, in the combat old of the Anteater-such: we cleaned the wind of whom not had order of to respirate, and ante these we desencompassed… The Fafafa has a mass of mares. He raises horses good. Even a little more distant, on the ped-of-sierra, of band mine was the Sesfred, Jesualdo, the Nelson, and João Concliz. Some others. The Triol… And not I go valuing? I leave terra with them, of theirs the what is mine is, we close that we not even brothers. For what I want to gather richness? They are there, of arms aireated. Enemy to come, we cross called, gathering: is hour of one good shotshowerment in peace, they exp’riment to see. I say this to the Sir, of confidence. Too, not go to think in double. We want is to work, propose tranquility. Of me, person, I live for mine woman, that total mode-meliorate merits, and for the devotion. Well-to want of mine woman was that me assisted, prayers of hers, graces. Love comes of love. I say. In Diadorim, I think too— but Diadorim is the mine nebulina… Now, well: not I wanted to touch on this more— of the Tineaous; arrive. But has a nevertheless: I ask: the Sir believe, think trust of truth in that parlance, of with the demon so to able to deal with pact? No, no is no? I knew that not there. I spoke of favas. But I like of total good confirmation. To vend you proper soul… Inventionate false! And, soul, the what is? Soul of has to be thing internal supremed, much more of the of inside, and is solo, of the that one if thought: ah, soul sheer! Decision of to vend soul is fearless moll, fantasied of moment, has not the obedience legal. Can I to vend those good terras, thereof of between the Veredas-Four— that are of one Mr. Admiral, who resides in the capital federal? Can I some? Then, if one boy boy is, and for this not so authorizes of to negotiate… And we, this I know, at times is solo fated boy. Mal that in mine life I prepared, I was in a certain infancy in dreams — total runs and arrives so swift —; will be that if hath flame of responsibilities? If dream; yea so did… I gave rapadura to the chump! Ahem. Well. If his soul, and has, it is of Deus established, not even that the person want or not want. Not is vendible. The Sir not thinks? Me declare, frank, I beg. Ah, you I appreciate. You so see that the Sir knows much, in idea firm, beyond of to have letter of doctor. You I appreciate, for much. Your company me gives high pleasures. In terms, I liked that I would live here, or close, was a help. Here not so has conviviation that to instruct. Sertão. Knows the Sir: sertão is where the thought of the people so forms more forted of the than power of the place. To live is much perilous… Eh, that you so go? Yeayea? Is that not. Today, no. Tomorrow, no. Not I consense. The Sir me forgive, but in endeavor of mine friendship accept: the Sir stay. After fifth of-morning-early, the Sir wanting to go, then goes, same me leaves feeling your absence. But, today or tomorrow, no. Visit, here in house, with me, is for three days! But, the Sir really intends to trespass the field this sea of territotires, for sortment of to confer the what exists? You have your motives. Now— I say for me — the Sir comes, came late, Times were, the customs mutate. Almost that, of legitimate loyal, little surplus, not even no excess more nothing. The bands good of valientoughs they reparted their end; many who were jagunço, by ouch pain, beg alms. Same as the herdsmen they doubt of to come in the commerce vested of clothes entire of leather, they think that garb of jerkin is ugly and boor. And even the herd in the shrubbed pasture goes waning less mad, more educated: casted of zebu, dissee with the rest of corralers and captiveborns. Always, in the generals is to the poverty, to the sadness. A sadness that even gladdens. But, then, for a crop reasonable of bizzarancies, I recounsel of the Sir to entest journey more dilated. Not were my desmight, by acids and rheumatism, there I went. I guided the Sir till total. March 2013 San Diego, CA ORIGINAL TEXT NONADA. TIROS QUE O SENHOR ouviu foram de briga de homem não, Deus esteja. Alvejei mira em árvores no quintal, no baixo do córrego. Por meu acerto. Todo dia isso faço, gosto; desde mal em minha mocidade. Daí, vieram me chamar. Causa dumbezerro: um bezerro branco, erroso, os olhos de nem ser – se viu –; e com máscara de cachorro. Me disseram; eu não quis avistar. Mesmo que, por defeito como nasceu, arrebitado de beiços, esse figurava rindo feito pessoa. Cara de gente, cara de cão: determinaram – era o demo. Povo prascóvio. Mataram. Dono dele nem sei quem for. Vieram emprestar minhas armas, cedi. Não tenho abusões. O senhor ri certas risadas... Olhe: quando é tiro de verdade, primeiro a cachorrada pega a latir, instantaneamente – depois, então, se vai ver se deu mortos. O senhor tolere, isto é o sertão. Uns querem que não seja: que situado sertão é por os campos-gerais a fora a dentro, eles dizem, fim de rumo, terras altas, demais do Urucuia. Toleima. Para os de Corinto e do Curvelo, então, o aqui não é dito sertão? Ah, que tem maior! Lugar sertão se divulga: é onde os pastos carecem de fechos; onde um pode torar dez, quinze léguas, sem topar com casa de morador; e onde criminoso vive seu cristo-jesus, arredado do arrocho de autoridade. O Urucuia vem dos montões oestes. Mas, hoje, que na beira dele, tudo dá – fazendões de fazendas, almargem de vargens de bom render, as vazantes; culturas que vão de mata em mata, madeiras de grossura, até ainda virgens dessas lá há. O gerais corre em volta. Esses gerais são sem tamanho. Enfim, cada um o que quer aprova, o senhor sabe: pão ou pães, é questão de opiniães... O sertão está em toda a parte. Do demo? Não gloso. Senhor pergunte aos moradores. Em falso receio, desfalam no nome dele – dizem só: o Que-Diga. Vote! não... Quem muito se evita, se convive. Sentença num Aristides – o que existe no buritizal primeiro desta minha mão direita, chamado a Vereda-da-Vaca-Mansa-deSanta-Rita – todo o mundo crê: ele não pode passar em três lugares, designados: porque então a gente escuta um chorinho, atrás, e uma vozinha que avisando: – “Eu já vou! Eu já vou!...” – que é o capiroto, o que-diga... E um José Simpilício – quem qualquer daqui jura ele tem um capeta em casa, miúdo satanazim, preso obrigado a ajudar em toda ganância que executa; razão que o Simpilício se empresa em vias de completar de rico. Apre, por isso dizem também que a besta pra ele rupeia, nega de banda, não deixando, quando ele quer amontar... Superstição. José Simpilício e Aristides, mesmo estão se engordando, de assim nãoouvir ou ouvir. Ainda o senhor estude: agora mesmo, nestes dias de época, tem gente porfalando que o Diabo próprio parou, de passagem, no Andrequicé. Um Moço de fora, teria aparecido, e lá se louvou que, para aqui vir – normal, a cavalo, dum dia-e-meio – ele era capaz que só com uns vinte minutos bastava... porque costeava o Rio do Chico pelas cabeceiras! Ou, também, quem sabe – sem ofensas – não terá sido, por um exemplo, até mesmo o senhor quem se anunciou assim, quando passou por lá, por prazido divertimento engraçado? Há-de, não me dê crime, sei que não foi. E mal eu não quis. Só que uma pergunta, em hora, às vezes, clareia razão de paz. Mas, o senhor entenda: o tal moço, se há, quis mangar. Pois, hem, que, despontar o Rio pelas nascentes, será a mesma coisa que um se redobrar nos internos deste nosso Estado nosso, custante viagem de uns três meses... Então? Que-Diga? Doideira. A fantasiação. E, o respeito de dar a ele assim esses nomes de rebuço, é que é mesmo um querer invocar que ele forme forma, com as presenças! Não seja. Eu, pessoalmente, quase que já perdi nele a crença, mercês a Deus; é o que ao senhor lhe digo, à puridade. Sei que é bem estabelecido, que grassa nos Santos- Evangelhos. Em ocasião, conversei com um rapaz seminarista, muito condizente, conferindo no livro de rezas e revestido de paramenta, com uma vara de maria-preta na mão – proseou que ia adjutorar o padre, para extraírem o Cujo, do corpo vivo de uma velha, na Cachoeira-dos-Bois, ele ia com o vigário do Campo-Redondo... Me concebo. O senhor não é como eu? Não acreditei patavim. Compadre meu Quelemém descreve que o que revela efeito são os baixos espíritos descarnados, de terceira, fuzuando nas piores trevas e com ânsias de se travarem com os viventes – dão encosto. Compadre meu Quelemém é quem muito me consola – Quelemém de Góis. Mas ele tem de morar longe daqui, na Jijujã, Vereda do Buriti Pardo... Arres, me deixe lá, que – em endemoninhamento ou com encosto – o senhor mesmo deverá de ter conhecido diversos, homens, mulheres. Pois não sim? Por mim, tantos vi, que aprendi. Rincha- Mãe, Sangued’Outro, o Muitos-Beiços, o Rasgaem-Baixo, Faca-Fria, o Fancho-Bode, um Treciziano, o Azinhavre... o Hermógenes... Deles, punhadão. Se eu pudesse esquecer tantos nomes... Não sou amansador de cavalos! E, mesmo, quem de si de ser jagunço se entrete, já é por alguma competência entrante do demônio. Será não? Será? De primeiro, eu fazia e mexia, e pensar não pensava. Não possuía os prazos. Vivi puxando difícil de dificel, peixe vivo no moquém: quem mói no asp’ro, não fantaseia. Mas, agora, feita a folga que me vem, e sem pequenos dessossegos, estou de range rede. E me inventei neste gosto, de especular idéia. O diabo existe e não existe? Dou o dito. Abrenúncio. Essas melancolias. O senhor vê: existe cachoeira; e pois? Mas cachoeira é barranco de chão, e água se caindo por ele, retombando; o senhor consome essa água, ou desfaz o barranco, sobra cachoeira alguma? Viver é negócio muito perigoso... Explico ao senhor: o diabo vige dentro do homem, os crespos do homem – ou é o homem arruinado, ou o homem dos avessos. Solto, por si, cidadão, é que não tem diabo nenhum. Nenhum! – é o que digo. O senhor aprova? Me declare tudo, franco – é alta mercê que me faz: e pedir posso, encarecido. Este caso – por estúrdio que me vejam – é de minha certa importância. Tomara não fosse... Mas, não diga que o senhor, assisado e instruído, que acredita na pessoa dele?! Não? Lhe agradeço! Sua alta opinião compõe minha valia. Já sabia, esperava por ela-já o campo! Ah, a gente, na velhice, carece de ter sua aragem de descanso. Lhe agradeço. Tem diabo nenhum. Nem espírito. Nunca vi. Alguém devia de ver, então era eu mesmo, este vosso servidor. Fosse lhe contar... Bem, o diabo regula seu estado preto, nas criaturas, nas mulheres, nos homens. Até: nas crianças – eu digo. Pois não é ditado: “menino – trem do diabo”? E nos usos, nas plantas, nas águas, na terra, no vento... Estrumes. ... O diabo na rua, no meio do redemunho... Hem? Hem? Ah. Figuração minha, de pior pra trás, as certas lembranças. Mal hajame! Sofro pena de contar não... Melhor, se arrepare: pois, num chão, e com igual formato de ramos e folhas, não dá a mandioca mansa, que se come comum, e a mandioca-brava, que mata? Agora, o senhor já viu uma estranhez? A mandioca-doce pode de repente virar azangada – motivos não sei; às vezes se diz que é por replantada no terreno sempre, com mudas seguidas, de manaíbas – vai em amargando, de tanto em tanto, de si mesma toma peçonhas. E, ora veja: a outra, a mandiocabrava, também é que às vezes pode ficar mansa, a esmo, de se comer sem nenhum mal. E que isso é? Eh, o senhor já viu, por ver, a feiúra de ódio franzido, carantonho, nas faces duma cobra cascavel? Observou o porco gordo, cada dia mais feliz bruto, capaz de, pudesse, roncar e engolir por sua suja comodidade o mundo todo? E gavião, corvo, alguns, as feições deles já representam a precisão de talhar para adiante, rasgar e estraçalhar a bico, parece uma quicé muito afiada por ruim desejo. Tudo. Tem até tortas raças de pedras, horrorosas, venenosas – que estragam mortal a água, se estão jazendo em fundo de poço; o diabo dentro delas dorme: são o demo. Se sabe? E o demo – que é só assim o significado dum azougue maligno – tem ordem de seguir o caminho dele, tem licença para campear?! Arre, ele está misturado em tudo. Que o que gasta, vai gastando o diabo de dentro da gente, aos pouquinhos, é o razoável sofrer. E a alegria de amor – compadre meu Quelemém, diz. Família. Deveras? É, e não é. O senhor ache e não ache. Tudo é e não é... Quase todo mais grave criminoso feroz, sempre é muito bom marido, bom filho, bom pai, e é bom amigo-de-seus-amigos! Sei desses. Só que tem os depois – e Deus, junto. Vi muitas nuvens. Mas, em verdade, filho, também, abranda. Olhe: um chamado Aleixo, residente a légua do Passo do Pubo, no da-Areia, era o homem de maiores ruindades calmas que já se viu. Me agradou que perto da casa dele tinha um açudinho, entre as palmeiras, com traíras, pra-almas de enormes, desenormes, ao real, que receberam fama; o Aleixo dava de comer a elas, em horas justas, elas se acostumaram a se assim das locas, para papar, semelhavam ser peixes ensinados. Um dia, só por graça rústica, ele matou um velhinho que por lá passou, desvalido rogando esmola. O senhor não duvide – tem gente, neste aborrecido mundo, que matam só para ver alguém fazer careta... Eh, pois, empós, o resto o senhor prove: vem o pão, vem a mão, vem o são, vem o cão. Esse Aleixo era homem afamilhado, tinha filhos pequenos; aqueles eram o amor dele, todo, despropósito. Dê bem, que não nem um ano estava passado, de se matar o velhinho pobre, e os meninos do Aleixo aí adoeceram. Andaço de sarampão, se disse, mas complicado; eles nunca saravam. Quando, então, sararam. Mas os olhos deles vermelhavam altos, numa inflama de sapiranga à rebelde; e susseguinte – o que não sei é se foram todos duma vez, ou um logo e logo outro e outro – eles restaram cegos. Cegos, sem remissão dum favinho de luz dessa nossa! O senhor imagine: uma escadinha – três meninos e uma menina – todos cegados. Sem remediável. O Aleixo não perdeu o juizo; mas mudou: ah, demudou completo – agora vive da banda de Deus, suando para ser bom e caridoso em todas suas horas da noite e do dia. Parece até que ficou o feliz, que antes não era. Ele mesmo diz que foi um homem de sorte, porque Deus quis ter pena dele, transformar para lá o rumo de sua alma. Isso eu ouvi, e me deu raiva. Razão das crianças. Se sendo castigo, que culpa das hajas do Aleixo aqueles meninozinhos tinham?! Compadre meu Quelemém reprovou minhas incertezas. Que, por certo, noutra vida revirada, os meninos também tinham sido os mais malvados, da massa e peça do pai, demônios do mesmo caldeirão de lugar. Senhor o que acha? E o velhinho assassinado? – eu sei que o senhor vai discutir. Pois, também. Em ordem que ele tinha um pecado de crime, no corpo, por pagar. Se a gente – conforme compadre meu Quelemém é quem diz – se a gente torna a encarnar renovado, eu cismo até que inimigo de morte pode vir como filho do inimigo. Mire veja: se me digo, tem um sujeito Pedro Pindó, vizinho daqui mais seis léguas, homem de bem por tudo em tudo, ele e a mulher dele, sempre sidos bons, de bem. Eles têm um filho duns dez anos, chamado Valtei – nome moderno, é o que o povo daqui agora apreceia, o senhor sabe. Pois essezinho, essezim, desde que algum entendimento alumiou nele, feito mostrou o que é: pedido madrasto, azedo queimador, gostoso de ruim de dentro do fundo das espécies de sua natureza. Em qual que judia, ao devagar, de todo bicho ou criaçãozinha pequena que pega; uma vez, encontrou uma crioula bentabêbada dormindo, arranjou um caco de garrafa, lanhou em três pontos a popa da perna dela. O que esse menino babeja vendo, é sangrarem galinha ou esfaquear porco. – “Eu gosto de matar...” – uma ocasião ele pequenino me disse. Abriu em mim um susto; porque: passarinho que se debruça – o vôo já está pronto! Pois, o senhor vigie: o pai, Pedro Pindó, modo de corrigir isso, e a mãe, dão nele, de miséria e mastro – botam o menino sem comer, amarram em árvores no terreiro, ele nu nuelo, mesmo em junho frio, lavram o corpinho dele na peia e na taca, depois limpam a pele do sangue, com cuia de salmoura. A gente sabe, espia, fica gasturado. O menino já rebaixou de magreza, os olhos entrando, carinha de ossos, encaveirada, e entisicou, o tempo todo tosse, tossura da que puxa secos peitos. Arre, que agora, visível, o Pindó e a mulher se habituaram de nele bater, de pouquinho em pouquim foram criando nisso um prazer feio de diversão – como regulam as sovas em horas certas confortáveis, até chamam gente para ver o exemplo bom. Acho que esse menino não dura, já está no blimbilim, não chega para a quaresma que vem... Uê-uê, então?!Não sendo como compadre meu Quelemém quer, que explicação é que o senhor dava? Aquele menino tinha sido homem. Devia, em balanço, terríveis perversidades. Alma dele estava no breu. Mostrava. E, agora, pagava. Ah, mas, acontece, quando está chorando e penando, ele sofre igual que se fosse um menino bonzinho... Ave, vi de tudo, neste mundo! lá vi até cavalo com soluço... – o que é a coisa mais custosa que há. Bem, mas o senhor dirá, deve de: e no começo – para pecados e artes, as pessoas – como por que foi que tanto emendado se começou? Ei, ei, aí todos esbarram. Compadre meu Quelemém, também. Sou só um sertanejo, nessas altas idéias navego mal. Sou muito pobre coitado. Inveja minha pura é de uns conforme o senhor, com toda leitura e suma doutoração. Não é que eu esteja analfabeto. Soletrei, anos e meio, meante cartilha, memória e palmatória. Tive mestre, Mestre Lucas, no Curralinho, decorei gramática, as operações, regra-de-três, até geografia e estudo pátrio. Em folhas grandes de papel, com capricho tracei bonitos mapas. Ah, não é por falar: mas, desde o começo, me achavam sofismado de ladino. E que eu merecia de ir para cursar latim, em Aula Régia – que também diziam. Tempo saudoso! Inda hoje, apreceio um bom livro, despaçado. Na fazenda O Limãozinho, de um meu amigo Vito Soziano, se assina desse almanaque grosso, de logogrifos e charadas e outras divididas matérias, todo ano vem. Em tanto, ponho primazia é na leitura proveitosa, vida de santo, virtudes e exemplos – missionário esperto engambelando os índios, ou São Francisco de Assis, Santo Antônio, São Geraldo... Eu gosto muito de moral. Raciocinar, exortar os outros para o bom caminho, aconselhar a justo. Minha mulher, que o senhor sabe, zela por mim: muito reza. Ela é uma abençoável. Compadre meu Quelemém sempre diz que eu posso aquietar meu temer de consciência, que sendo bem-assistido, terríveis bons-espíritos me protegem. Ipe! Com gosto... Como é de são efeito, ajudo com meu querer acreditar. Mas nem sempre posso. O senhor saiba: eu toda a minha vida pensei por mim, forro, sou nascido diferente. Eu sou é eu mesmo. Diverjo de todo o mundo... Eu quase que nada não sei. Mas desconfio de muita coisa. O senhor concedendo, eu digo: para pensar longe, sou cão mestre – o senhor solte em minha frente uma idéia ligeira, e eu rastreio essa por fundo de todos os matos, amém! Olhe: o que devia de haver, era de se reunirem-se os sábios, políticos, constituições gradas, fecharem o definitivo a noção – proclamar por uma vez, artes assembléias, que não tem diabo nenhum, não existe, não pode. Valor de lei! Só assim, davam tranqüilidade boa à gente. Por que o Governo não cuida?! Ah, eu sei que não é possível. Não me assente o senhor por beócio. Uma coisa é pôr idéias arranjadas, outra é lidar com país de pessoas, de carne e sangue, de mil-e-tantas misérias... Tanta gente – dá susto de saber – e nenhum se sossega: todos nascendo, crescendo, se casando, querendo colocação de emprego, comida, saúde, riqueza, ser importante, querendo chuva e negócios bons... De sorte que carece de se escolher: ou a gente se tece de viver no safado comum, ou cuida só de religião só. Eu podia ser: padre sacerdote, se não chefe de jagunços; para outras coisas não fui parido. Mas minha velhice já principiou, errei de toda conta. E o reumatismo... Lá como quem diz: nas escorvas. Ahã. Hem? Hem? O que mais penso, testo e explico: todo-omundo é louco. O senhor, eu, nós, as pessoas todas. Por isso é que se carece principalmente de religião: para se desendoidecer, desdoidar. Reza é que sara da loucura. No geral. Isso é que é a salvaçãoda- alma... Muita religião, seu moço! Eu cá, não perco ocasião de religião. Aproveito de todas. Bebo água de todo rio... Uma só, para mim é pouca, talvez não me chegue. Rezo cristão, católico, embrenho a certo; e aceito as preces de compadre meu Quelemém, doutrina dele, de Cardéque. Mas, quando posso, vou no Mindubim, onde um Matias é crente, metodista: a gente se acusa de pecador, lê alto a Bíblia, e ora, cantando hinos belos deles. Tudo me quieta, me suspende. Qualquer sombrinha me refresca. Mas é só muito provisório. Eu queria rezar – o tempo todo. Muita gente não me aprova, acham que lei de Deus é privilégios, invariável. E eu! Bofe! Detesto! O que sou? – o que faço, que quero, muito curial. E em cara de todos faço, executado. Eu não tresmalho! Olhe: tem uma preta, Maria Leôncia, longe daqui não mora, as rezas dela afamam muita virtude de poder. Pois a ela pago, todo mês – encomenda de rezar por mim um terço, todo santo dia, e, nos domingos, um rosário. Vale, se vale. Minha mulher não vê mal nisso. E estou, já mandei recado para uma outra, do Vau-Vau, uma Izina Calanga, para vir aqui, ouvi de que reza também com grandes meremerências, vou efetuar com ela trato igual. Quero punhado dessas, me defendendo em Deus, reunidas de mim em volta... Chagas de Cristo! Viver é muito perigoso... Querer o bem com demais força, de incerto jeito, pode já estar sendo se querendo o mal, por principiar. Esses homens! Todos puxavam o mundo para si, para o concertar consertado. Mas cada um só vê e entende as coisas dum seu modo. Montante, o mais supro, mais sério – foi Medeiro Vaz. Que um homem antigo... Seu Joãozinho Bem-Bem, o mais bravo de todos, ninguém nunca pôde decifrar como ele por dentro consistia. Joca Ramiro – grande homem príncipe! – era político. Zé- Bebelo quis ser político. (shrink)

The concept of burden of proof is used in a wide range of discourses, from philosophy to law, science, skepticism, and even in everyday reasoning. This paper provides an analysis of the proper deployment of burden of proof, focusing in particular on skeptical discussions of pseudoscience and the paranormal, where burden of proof assignments are most poignant and relatively clear-cut. We argue that burden of proof is often misapplied or used as a mere rhetorical gambit, with little appreciation of the (...) underlying principles. The paper elaborates on an important distinction between evidential and prudential varieties of burdens of proof, which is cashed out in terms of Bayesian probabilities and error management theory. Finally, we explore the relationship between burden of proof and several (alleged) informal logical fallacies. This allows us to get a firmer grip on the concept and its applications in different domains, and also to clear up some confusions with regard to when exactly some fallacies (ad hominem, ad ignorantiam, and petitio principii) may or may not occur. (shrink)

This book constitutes the refereed proceedings of the 4th International Conference on Frontiers of Combining Systems, FroCoS 2002, held in Santa Margherita Ligure, Italy, in April 2002.The 14 revised full papers presented together with 3 invited papers were carefully reviewed and selected from 35 submissions. Among the topics covered are combination of logics, combination of constraint solving techniques, combination of decision procedures, combination problems in verification, modular problems of theorem proving, and the integration of decision procedures and other (...) solving processes into constraint programming and deduction systems. (shrink)

As its title is meant to suggest, this paper is a reply to Sir Tim Lankester’s article “International Aid: Experience, Prospects and the Moral Case”, published in the World Economics last year 1 . Therefore, I would like to begin by expressing my gratitude for the author’s responsiveness to my interest and queries in the area of development economics. The main point of Sir Lankester’s article was, I believe, to strengthen the case for international aid by showing first, (...) that it was not just a theoretical matter 2 and second, that its efficiency was not a self-evident fait accompli, but a still-to-achieve objective, entirely contingent upon human and institutional factors such as the will, interests, and past experience of donors, as well as the system of governance and existing policies from the recipient countries. Moreover, the human factor is actually two-fold, in the sense that one can focus either on the external part engaged in the aid mission – the donor –, or on the internal one – the recipient. Sir Tim Lankester looks into what motivates the former, whereas I intend to unpack the life-experience of the latter, for I strongly believe that what ultimately decides the success or failure of development projects has more to do with understanding their life situation, than with the actual quantum of aid. Although the two cases grounded on the above-mentioned claims may seem completely separated in Tim Lankester’s article for he allocates distinct sections to them, I have reasons to believe that they are not only inter-connected, but also deeply inter-dependent, which is crucial for the kind of existentialist scenario that I intend to outline here. In order to prove this, I am going to combine two sets of argumentative tools: one will be logical, the other – empirical. The former will help us address the issues at stake in Tim Lankester’s moral case, and find ways of strengthening it; the latter will help reminding the real goal of this attempt – which is to improve the prospects of aid missions in real-life scenarios, rather than in theory. The first, rather theoretical section will consist of an extended analysis of the moral case that Sir Lankester started to build. The focus will be not only on the supposedly fruitful aspects of social justice theories, but also on their potential risks; both heroes and villains will emerge from the analysis, and new leads will be discovered. The main criterion for testing whatever findings will remain the pragmatic one: questioning their implications on the life-experiences of the poor. The other approach that I have mentioned will consist of providing a description of life in a particular community, which I have known and learnt from. In this case, the ‘empirical’ obviously means more than just the use of examples – which can be invented, or refined: it actually involves relying on a set of personal experiences and convictions, thereby testifying in – rather than just advocating – the case for aid and development projects, under discussion here. Again, the purpose will be not so much to prove that my claim has the sort of objective validity that a theoretician would normally seek to achieve, as to enforce it by whatever relevant testimonies – be them contextual, perhaps even biased; in this case, the ‘biased’ aspect consists of using an example derived from lifeexperiences in a particular developing country: my own. And it is exactly what I regard as the strength of it; indeed, I would not be writing this, had I not learnt that lesson. (shrink)

This is a collection of invited papers from the 1975 International Sym posium on Multiple-valued Logic. Also included is an extensive bib liography of works in the field of multiple-valued logic prior to 1975 - this supplements and extends an earlier bibliography of works prior to 1965, by Nicholas Rescher in his book Many-Valued Logic, McGraw-Hill, 1969. There are a number of possible reasons for interest in the present volume. First, the range of various uses covered (...) in this collection of papers may be taken as indicative of a breadth which occurs in the field of multiple-valued logic as a whole - the papers here can do no more than cover a small sample: question-answering systems, analysis of computer hazards, algebraic structures relating to multiple-valued logic, algebra of computer programs, fuzzy sets. Second, a large part of the interest in such uses and applications has occurred in the last twenty, even ten years. It would be too much to expect this to be reflected in Rescher's 1969 book. Third, in the 1970's a series of annual symposia have been held on multiple-valued logic, which have brought much of this into a sharp focus. * The 1971 and 1972 symposia were held at the SUNY at Buffalo, the 1973 symposium at the Uni versity of Toronto, and the 1974 symposium at West Virginia Uni versity. Papers from these symposia are included in the bibliography which may be found in an appendix of this book. (shrink)

This book constitutes the refereed proceedings of the Third International Workshop on Frontiers of Combining Systems, FroCoS 2000, held in Nancy, France, in March 2000.The 14 revised full papers presented together with four invited papers were carefully reviewed and selected from a total of 31 submissions. Among the topics covered are constraint processing, interval narrowing, rewriting systems, proof planning, sequent calculus, type systems, model checking, theorem proving, declarative programming, logic programming, and equational theories.

A theory of higher-order vagueness for partially-defined, context-sensitive predicates like is blue is offered. According to the theory, the predicate is determinately blue means roughly is an object o such that the claim that o is blue is a necessary consequence of the rules of the language plus the underlying non-linguistic facts in the world. Because the question of which rules count as rules of the language is itself vague, the predicate is determinately blue is both vague and (...) partial in a sense analogous (though not completely identical) to the sense in which is blue is vague and partial. However, higher-order vagueness stops there. Although the anti-extension of is determinately blue differs from that of is blue, further iterations of determinately have no semantic effect. The paper closes with a discussion of the need to posit sharp and precise lines dividing the range of potential application of a vague predicate into semantically distinct categories. It is argued that this is less of a problem for the present theory than for many others, because the categories into which the range is divided by the present theory -- like the category of counting as blue because the rules of the language offer speakers no discretion, as opposed to the category of counting as blue because speakers have invoked an absolute minimum of discretion in adjusting the contextually sensitive boundaries of the predicate -- are not those that the linguistic competence of ordinary speakers equips them to make highly accurate and reliable judgments about. (shrink)

Higher-order vagueness is widely thought to be a feature of vague predicates that any adequate theory of vagueness must accommodate. It takes a variety of forms. Perhaps the most familiar is the supposed existence, or at least possibility, of higher-order borderline cases—borderline borderline cases, borderline borderline borderline cases, and so forth. A second form of higherorder vagueness, what I will call ‘prescriptive’ higher-order vagueness, is thought to characterize complex predicates constructed from vague predicates by (...) attaching operators having to do with the predicates’ proper application. For example, the predicates ‘mandates application of “old”’ and ‘can competently be called “old”’ are prescriptively higher-order vague. Higher-order vagueness appears in other guises as well,1 but these two have been of particular interest to philosophers and will be my target here. I want to expose some misconceptions about them. If I am right, higher-order vagueness is less prevalent, and less important theoretically, than is usually supposed.2 In what follows I am going to assume that vagueness is a semantic feature of natural language. For the most part I won’t discuss epistemic or pragmatic views, and I will say nothing about so-called metaphysical vagueness. (shrink)

In this paper we present a general theory of normal forms, based on a categorial result for the free monoid construction. We shall use the theory mainly for proposictional modal logic, although it seems to have a wider range of applications. We shall formally represent normal forms as combinatorial objects, basically labelled trees and forests. This geometric conceptualization is implicit in and our approach will extend it to other cases and make it more direct: operations of a purely (...) geometric and combinatorial nature will be introduced in order to give a mathematical description of the basic logical/algebraic constructions .We begin by recalling the above-mentioned categorial construction: we need a careful inspection of it because in the various examples considered later we plan to deduce from it in a uniform way the normal forms and the description of finitely generated free algebras. This method always works whenever we can describe the category of algebras corresponding to the logic under consideration as a T-objects category. When this simple description seems not to be available, still the general theory might be of some interest, because a description of the category of algebras as a T-objects category plus equation is possible .The central part of the paper is more advanced and specific: we show how the general approach presented here can provide some insights even in the basic case of the modal system K. Section 4 contains a contribution to the theory of normal forms, namely the description of the uniform substitution. This result will enable us to give a duality theorem for the category of finitely generated free modal algebras and in Section 5 to provide a characterization of the collections of normal forms which happen to be normal forms for a logic, thus giving a description of the lattice of modal logics.Section 6 deals with some applications: we shall show how to use normal forms in order to prove for the modal system K the definability of higher-order propositional quantifiers and of the tense operator F .As to the prerequisites, the paper is almost self-contained. The reader is only assumed to have familiarity with standard techniques in algebraic logic ). Knowledge of the basic facts about adjoint functors is required too, see e.g. McLane or the appendix. (shrink)

The paper contains a review and a discussion of Robert Trueman's book Properties and Propositions: The Metaphysics of Higher-Order Logic, Cambridge University Press, 2021, pp. xii + 227. ISBN 978-1-108-81410-2. The discussion is focused on the consistency of Truema's language-based ontology and on its value in defending higher-order logic.

It is usually taken as given that consciousness involves superior or more elaborate forms of information processing. Contemporary models equate consciousness with global processing, system complexity, or depth or stability of computation. This is in stark contrast with the powerful philosophical intuition that being conscious is more than just having the ability to compute. I argue that it is also incompatible with current empirical findings. I present a model that is free from the strong assumption that consciousness predicts superior performance. (...) The model is based on Bayesian decision theory, of which signal detection theory is a special case. It reflects the fact that the capacity for perceptual decisions is fundamentally limited by the presence and amount of noise in the system. To optimize performance, one therefore needs to set decision criteria that are based on the behaviour, i.e. the probability distributions, of the internal signals. One important realization is that the knowledge of how our internal signals behave statistically has to be learned over time. Essentially, we are doing statistics on our own brain. This ‘higherorder’ learning, however, may err, and this impairs our ability to set and maintain optimal criteria for perceptual decisions, which I argue is central to perception consciousness. I outline three possibilities of how conscious perception might be affected by failures of ‘higher-order’ representation. These all imply that one can have a dissociation between consciousness and performance. This model readily explains blindsight and hallucinations in formal terms, and is beginning to receive direct empirical support. I end by discussing some philosophical implications of the model. (shrink)

Two expressive limitations of an infinitary higher-order modal language interpreted on models for higher-order contingentism – the thesis that it is contingent what propositions, properties and relations there are – are established: First, the inexpressibility of certain relations, which leads to the fact that certain model-theoretic existence conditions for relations cannot equivalently be reformulated in terms of being expressible in such a language. Second, the inexpressibility of certain modalized cardinality claims, which shows that in such a (...) language, higher-order contingentists cannot express what is communicated using various instances of talk of ‘possible things’, such as ‘there are uncountably many possible stars’. (shrink)

This discussion treats a set of familiar social derelictions as consequences of the perversion of a universalistic moral theory in the service of an ill-considered or insufficiently examined personal agenda.The set includes racism, sexism, anti-Semitism, homophobia, and class elitism, among other similar pathologies, under the general heading of discrimination. The perversion of moral theory from which these derelictions arise, I argue, involves restricting its scope of application to some preferred subgroup of the moral community of human beings. -/- The following (...) analysis of higher-order discrimination suggests that we often select the individuals who constitute such subgroups for reasons that we ourselves would reject on moral grounds were we to examine them carefully, but that we choose instead to put our rational resources in the service of avoiding any such examination at all costs. The implication is that arguments that truncate the scope of moral theory in fact justify bestowing the gift of moral treatment on a select few who deserve it no more than the many from whom we withhold it. Therefore, it would be precipitous to conclude that universalistic moral theory can be legitimately restricted in its practical scope of application in any way at all. (shrink)

We shall introduce in this paper a language whose formulas will be interpreted by games of imperfect information. Such games will be defined in the same way as the games for first-order formulas except that the players do not have complete information of the earlier course of the game. Some simple logical properties of these games will be stated together with the relation of such games of imperfect information to higher-order logic. Finally, a set of (...) class='Hi'>applications will be outlined. (shrink)

ABSTRACT This paper introduces a multi-valued variant of higher-order resolution and proves it correct and complete with respect to a variant of Henkin's general model semantics. This resolution method is parametric in the number of truth values as well as in the particular choice of the set of connectives (given by arbitrary truth tables) and even substitutional quantifiers. In the course of the completeness proof we establish a model existence theorem for this logical system. The work reported in (...) this paper provides a basis for developing higher-order mechanizations for many non-classical logics. (shrink)