We compare fork arrow logic, an extension of arrow logic, and its natural first-order counterpart (the correspondence language) and show that both have the same expressive power. Arrow logic is a modal logic for reasoning about arrow structures, its expressive power is limited to a bounded fragment of first-order logic. Fork arrow logic is obtained by adding to arrow logic the fork modality (related to parallelism and synchronization). As a result, fork arrow logic attains the expressive power of its first-order (...) correspondence language, so both can express the same input-output behavior of processes. (shrink)

Vague notions, such as ‘generally’, ‘rarely’, ‘often’, ‘almost always’, ‘a meaningful subset of a whole’, ‘most’, etc., occur often in ordinary language and in some branches of science. We introduce modal logical systems, with generalized operators, for the precise treatment of assertions involving some versions of such vague notions. We examine modal logics, constructed in a modular fashion, with generalized operators corresponding to some versions of ‘generally’ and ‘rarely’.

Logics for ‘generally’ are intended to express some vague notions, such as ‘generally’, ‘several’, ‘many’, ‘most’, etc., by means of the new generalized quantifier ∇ and to reason about assertions with ‘generally’ . We introduce the idea of functional interpretation for ‘generally’ and show that representative functions enable elimination of ∇ and reduce consequence to classical theories. Thus, one can use proof procedures and theorem provers for classical first-order logic to reason about assertions involving ‘generally’.

Logics for generally were introduced for handling assertions with vague notions,such as generally, most, several, etc., by generalized quantifiers, ultrafilter logic being an interesting case. Here, we show that ultrafilter logic can be faithfully embedded into a first-order theory of certain functions, called coherent. We also use generic functions (akin to Skolem functions) to enable elimination of the generalized quantifier. These devices permit using methods for classical first-order logic to reason about consequence in ultrafilter logic.

We compare fork arrow logic, an extension of arrow logic, and its natural first-order counterpart (the correspondence language) and show that both have the same expressive power. Arrow logic is a modal logic for reasoning about arrow structures, its expressive power is limited to a bounded fragment of first-order logic. Fork arrow logic is obtained by adding to arrow logic the fork modality (related to parallelism and synchronization). As a result, fork arrow logic attains the expressive power of its first-order (...) correspondence language, so both can express the same input–output behavior of processes. (shrink)

Some arguments use ‘generic’, or ‘typical’, objects. An explanation for this idea in terms of ‘almost all’ is suggested. The intuition of ‘almost all’ as ‘but for a few exceptions’ is rendered precise by means of ultrafilters. A logical system, with generalized quantifiers for ‘almost all’, is proposed as a basis for generic reasoning. This logic is monotonic, has a simple sound and complete deductive calculus, and is a conservative extension of classical first-order logic, with which it shares several properties. (...) For generic reasoning, generic individuals are introduced and internalized as generic constants, thereby producing conservative extensions where one can reason about generic objects as intended. A many-sorted version of this logic is introduced to handle distinct notions of ‘large’ subsets. Other possible applications for this logic are indicated. (shrink)

A lógica não contém teoremas puramente existenciais: as únicas sentenças existenciaisválidas são aquelas com análogas universais válidas. Aqui, mostramos que istorealmente é assim quando corretamente interpretado: toda validade ex- istencial possuiuma análoga universal simples, que também é válida. Também caracterizamos validadesuniversais e existenciais em termos de tautologias.

We consider a paradigm of applications of Logic Engineering to illustrate the information interchange among different areas of knowledge, through the formal approach to some aspects of computing. We apply the paradigm to the area of distributed systems, taking the demand for specification formalisms, treated in three areas of knowledge: modal logics, first-order logic and algebra. In doing so, we obtain transfer of intuitions and results, establishing that, as far as input/output representation is concerned, these three formalisms are equivalent.

This paper analyzes the theory of area developed by Euclid in the Elements and its modern reinterpretation in Hilbert’s influential monograph Foundations of Geometry. Particular attention is bestowed upon the role that two specific principles play in these theories, namely the famous common notion 5 and the geometrical proposition known as De Zolt’s postulate. On the one hand, we argue that an adequate elucidation of how these two principles are conceptually related in the theories of Euclid and Hilbert is highly (...) relevant for a better understanding of the respective geometrical practices. On the other hand, we claim that these conceptual relations unveil interesting issues between the two main contemporary approaches to the study of area of plane rectilinear figures, i.e., the geometrical approach consisting in the geometrical theory of equivalence and the metrical approach based on the notion of measure of area. Finally, in an appendix logical relations among equivalence, comparison and addition of magnitudes are examined schematically in an abstract setting. (shrink)

In this paper we show that the class of fork squares has a complete orthodox axiomatization in fork arrow logic (FAL). This result may be seen as an orthodox counterpart of Venema's non-orthodox axiomatization for the class of squares in arrow logic. FAL is the modal logic of fork algebras (FAs) just as arrow logic is the modal logic of relation algebras (RAs). FAs extend RAs by a binary fork operator and are axiomatized by adding three equations to RAs equational (...) axiomatization. A proper FA is an algebra of relations where the fork is induced by an injective operation coding pair formation. In contrast to RAs, FAs are representable by proper ones and their equational theory has the expressive power of full first-order logic. A square semantics (the set of arrows is ᵎ x ᵎ for some set ᵎ) for arrow logic was defined by Y. Venema. Due to the negative results about the finite axiomatizability of representable RAs, Venema provided a non-orthodox finite axiomatization for arrow logic by adding a new rule governing the applications of a difference operator. We address here the question of extending the type of relational structures to define orthodox axiomatizations for the class of squares. Given the connections between this problem and the finitization problem addressed by I. Németi, we suspect that this cannot be done by using only logical operations. The modal version of the FA equations provides an orthodox axiomatization for FAL which is complete in view of the representability of FAs. Here we review this result and carry it further to prove that this orthodox axiomatization for FAL also axiomatizes the class of fork squares. (shrink)

One of the main problems in computer science is to ensure that programs are implemented in such a way that they satisfy a given specification. There are many studies about methods to prove correctness of programs. This work presents a method, belonging to the constructive synthesis or proofs-as-programs paradigm, that comes from the Curry-Howard isomorphism and extracts the computational contents of intuitionist proofs. The synthesis process proposed produces a program in an imperative language from a proof in many-sorted intuitionist logic, (...) where the axioms define the abstract data types, using Natural Deduction as deductive system. It is proved the correctness, as well as the completeness of the method regarding the Heyting arithmetic with ω-rule . A discussion about the use of the finitary induction instead of computational ω-rule concludes the work. (shrink)

In this paper we show that the class of fork squares has a complete orthodox axiomatization in fork arrow logic (FAL). This result may be seen as an orthodox counterpart of Venema's non-orthodox axiomatization for the class of squares in arrow logic. FAL is the modal logic of fork algebras (FAs) just as arrow logic is the modal logic of relation algebras (RAs). FAs extend RAs by a binary fork operator and are axiomatized by adding three equations to RAs equational (...) axiomatization. A proper FA is an algebra of relations where the fork is induced by an injective operation coding pair formation. In contrast to RAs, FAs are representable by proper ones and their equational theory has the expressive power of full first-order logic. A square semantics (the set of arrows is U×U for some set U) for arrow logic was defined by Y. Venema. Due to the negative results about the finite axiomatizability of representable RAs, Venema provided a non-orthodox finite axiomatization for arrow logic by adding a new rule governing the applications of a difference operator. We address here the question of extending the type of relational structures to define orthodox axiomatizations for the class of squares. Given the connections between this problem and the finitization problem addressed by I. Németi, we suspect that this cannot be done by using only logical operations. The modal version of the FA equations provides an orthodox axiomatization for FAL which is complete in view of the representability of FAs. Here we review this result and carry it further to prove that this orthodox axiomatization for FAL also axiomatizes the class of fork squares. (shrink)

Resumo: O objetivo deste artigo é problematizar algumas das principais práticas da filosofia universitária brasileira, de forma a denunciar seus pressupostos colonizadores e apontar seus limites na elaboração de um pensamento filosófico capaz de se relacionar, efetivamente, com os problemas do território brasileiro. Analisa-se como a estratégia de leitura e explicação dos textos europeus e estadunidenses, considerados predominantemente as referências clássicas à filosofia, faz funcionar as relações de saber e dominação existentes do Norte global sobre os povos do Sul por (...) eles colonizados. Utiliza-se a experiência constitutiva do curso de filosofia da Universidade de São Paulo como exemplo das práticas e dos pressupostos de colonialidade pelos quais nossa filosofia acadêmica é modelada. A partir das contribuições de Lélia Gonzalez, Ailton Krenak, Silvia Rivera Cusicanqui e Leanne Betasamosake Simpson, serão questionados essas práticas e pressupostos, demonstrando como tais autores desafiam não só a alterar o habitual referencial teórico naturalizado na filosofia brasileira, mas, principalmente, a operar uma mudança ética e política nas relações que se estabelecem, usualmente, com a filosofia.: The goal of this article is to problematize some of the main practices of Brazilian university philosophy, in order to denounce its colonizing assumptions and point out its limits to elaborate a philosophical thought capable of relating, effectively, with the problems that affect us in the Brazilian territory. We will analyze how the strategy of reading and explaining European and unitedstatian texts, predominantly considered the classic references to philosophy, operate the relations of knowledge and domination that exist between the global North under the peoples of the South that they colonized. We will use the constitutive experience of the degree in philosophy at the University of São Paulo as an example of the practices and assumptions of coloniality by which our academic philosophy is modeled. From the contributions of Lélia Gonzalez, Ailton Krenak, Silvia Rivera Cusicanqui and Leanne Betasamosake Simpson, we will question those practices and assumptions, demonstrating how these authors challenge us not only to change the usual theoretical framework naturalized in Brazilian philosophy, but, above all, to operate an ethical and political change in the relationships that we usually establish with philosophy. (shrink)

Nestes artigos da Nação Portuguesa é perceptível um pendor mais prático que surge com maior clareza no princípio da série seguinte, na qual o periódico é seccionado em duas partes distintas, já claramente perceptíveis nesta segunda leva: a primeira, onde se inserem os estudos de momentânea curiosidade, feitos de crónica, transcrições, referências à revista, etc.; a subsequente, onde se podem encontrar os ensaios de crítica, filosofia, história e ciência, “em que os altos problemas do espírito vão sendo discutidos”. Por esse (...) motivo, foi desta última secção que nos ocupámos, tentando traçar as linhas gerais dos textos de António Sardinha, Pequito Rebelo, Rolão Preto, Afonso Lucas, Francisco Veloso, Rodrigues Cavalheiro e Avelino Soares. (shrink)

Veloso-Pereira-Haeusler_On-what-there-must-be.

A theory of magnitudes involves criteria for their comparison, equivalence and addition. We examine these aspects from an abstract viewpoint, stressing independence and definability. These considerations are triggered by the so-called De Zolt’s principle in the theory of equivalence of plane polygons.

Logics for ‘generally’ were introduced for handling assertions with vague notions, by non-standard generalized quantifiers, and to reason qualitatively about them . Filter logic is intended to address ‘most’. Here, we show that filter logic can be faithfully embedded into a classical first-order theory of certain predicates, called compatible. We also use representative predicates to enable elimination of the generalized quantifier. These devices permit using classical first-order methods to reason about consequence in filter logic and help clarifying the role of (...) such extended logics for ‘generally’. (shrink)

We discuss some basic issues underlying the natural numbers: induction and recursion. We examine recursive formulations and their use in establishing universal and particular properties.

A new, simpler proof, based on internalisation of interpretations, of the Modularisation Theorem for logical specifications is presented. This result is a basic tool for composing implementations and specialisation by parameter instantiation.

Proper fork algebras are algebras of binary relations over a structured set. The underlying set has changed from a set of pairs to a set closed under an injective function. In this paper we present a representation theorem for their abstract counterpart, that entails that proper fork algebras — whose underlying set is closed under an injective function — constitute a finitely based variety.1.

We discuss the question of inclusions between positive relational terms and some of its aspects, using the form of a dialogue. Two possible approaches to the problem are emphasized: natural deduction and graph manipulations. Both provide sound and complete calculi for proving the valid inclusions, supporting nice strategies to obtain proofs in normal form, but the latter appears to present several advantages, which are discussed.

A theory of magnitudes involves criteria for their equivalence, comparison and addition. In this article we examine these aspects from an abstract viewpoint, by focusing on the so-called De Zolt’s postulate in the theory of equivalence of plane polygons (“If a polygon is divided into polygonal parts in any given way, then the union of all but one of these parts is not equivalent to the given polygon”). We formulate an abstract version of this postulate and derive it from some (...) selected principles for magnitudes. We also formulate and derive an abstract version of Euclid’s Common Notion 5 (“The whole is greater than the part”), and analyze its logical relation to the former proposition. These results prove to be relevant for the clarification of some key conceptual aspects of Hilbert’s proof of De Zolt’s postulate, in his classicalFoundations of Geometry(1899). Furthermore, our abstract treatment of this central proposition provides interesting insights for the development of a well-behaved theory ofcompatiblemagnitudes. (shrink)

Logics for ‘generally’ were introduced for handling assertions with vague notions , which occur often in ordinary language and in science. LG’s provide a framework for distinct notions of ‘generally’: one builds a specific logic for the notion one has in mind. We introduce deductive systems, in natural deduction style, for LG’s and show that these systems are normalizable.

This paper discusses John Hick’s response to the problem of religious diversity, based on the distinction between the Real itself and the way He is experienced and thought of by different religious communities. To this end, we divided this work into three sections in addition to the present introduction and the final considerations. In the first section we present the hickian concept of religious phenomenon and discuss the affirmation of him in favor of the ambiguity of the universe; the second (...) section is dedicated to the analysis of Hick’s defense of the rationality of religious belief and in the third section we present Hick’s pluralist hypothesis and some variations and criticisms of this hypothesis proposed by other authors. At the end we present some critical considerations about the success of Hick’s hypothesis to respond to the problem of religious diversity. (shrink)

This article endeavours to prove that there were creation myths of human beings or certain things, but there were seldom creation myths of ontological cosmology in ancient China. This will be warranted through the distinction between the concepts of ‘to create’ and ‘to beget’, the distinction between ‘Cosmology I of creationism’ and ‘Cosmology II of begetting’, and the relationship between the One and Many. The only exception is the myth of Nüwa 女娲 as the creator of human beings, but not (...) the creator of the cosmos. Therefore, in ancient Chinese tradition, there were mainly myths of begetting rather than myths of complete creation in the sense similar to creatio ex nihilo.Contribution: Previous research frequently underscores the profound differences between ‘Cosmology I of creationism’ and ‘Cosmology II of begetting’. Based on the discussion of concepts of ‘to create’ [zao 造] and ‘to beget’ [sheng 生], this article argues that, there were mainly myths of begetting rather than myths of complete creation in the sense similar to creatio ex nihilo. (shrink)

Upon its recent publication in Portuguese, Paulo Freire’s newest book became an instant success. This English translation is sure to meet with similar acclaim. In Teachers as Cultural Workers, Freire speaks directly to teachers about the lessons learned from a lifetime of experience as an educator and social theorist. No other book so cogently explains the implications for classroom practice of Freire’s latest ideas and the pathbreaking theories found in Pedagogy of the Oppressed and other treatises.This book challenges all (...) who teach to reflect critically on the meaning of the act of teaching as well as the meaning of learning. Freire shows why a teacher’s success depends on a permanent commitment to learning and training, as part of an ongoing appraisal of classroom practice. By observing the curiosity of students and the manner through which students develop strategies for learning, the teacher is helped in discovering doubts, successes, and the teacher’s mistakes. When teachers open themselves to recognize the different roads students take in order to learn, they will become involved in a continual reconstruction of their own paths of curiosity, opening the doors to habits of learning that will benefit everyone in the classroom. (shrink)

One important issue in moral psychology concerns the proper characterisation of the folk understanding of the relationship between harmful transgressions and moral transgressions. Psychologist Elliot Turiel and associates have claimed with a broad range of supporting evidence that harmful transgressions are understood as transgressions that are authority independent and general in scope which, according to them, characterises these transgressions as moral transgressions. Recently many researchers questioned the position advocated by the Turiel tradition with some new evidence. We entered this debate (...) proposing an original, deflationary view in which perceptions of basic-rights violation and injustice are fundamental for the folk understanding of harmful transgressions as moral transgressions in Turiel's sense. In this article we elaborate and refine our deflationary view, while reviewing the debate, addressing various criticisms raised against our perspective, showing how our perspective explains the existent evidence, and suggesting new lines of inquiry. (shrink)

This article presents an analysis of Gödel's dialectica interpretation via a refinement of intuitionistic logic known as linear logic. Linear logic comes naturally into the picture once one observes that the structural rule of contraction is the main cause of the lack of symmetry in Gödel's interpretation. We use the fact that the dialectica interpretation of intuitionistic logic can be viewed as a composition of Girard's embedding of intuitionistic logic into linear logic followed by de Paiva's dialectica interpretation of linear (...) logic. We then investigate the various properties of the dialectica interpretation, such as the characterisation theorem, and variants of Gödel's interpretation within the linear logic context. The role of contraction in extensions to classical logic, arithmetic and analysis is also discussed. (shrink)

In this commentary I present five corollaries that follow the target article “How molecules became signs” by Terrence W. Deacon and also two outstanding questions the article rises. The corollaries revolve around the notion of interpretation as a form of thermodynamic work—specifically, non-expansion or “useful” work. This specific form of work, along with its path-dependent nature, may be critical for the fundamental understanding of semiotic processes, the subjective character of interpretation, and even the nature of viruses.

In this volume, we have chosen to highlight the importance of education to human rights by reprinting two articles written by Paulo Freire in 1970 for the _Harvard Educational Review_. These articles contain many of Freire's original ideas on human rights and education—issues that are central to his work. Freire was a pioneer in promoting the universal right to education and literacy as part of a commitment to people's struggle against oppression. As Jerome Bruner recognized after Freire's death in (...) May 1997, Freire left as a legacy his commitment to basic human rights: "He was a brave man as well as a far-sighted one. He made us aware of our mindless cruelties, and now the challenge to all of us is to do something about those cruelties.". (shrink)

Russell’s theory of memory as acquaintance with the past seems to square uneasily with his definition of acquaintance as the converse of the relation of presentation of an object to a subject. We show how the two views can be made to cohere under a suitable construal of ‘presentation’, which has the additional appeal of bringing Russell’s theory of memory closer to contemporary views on direct reference and object-dependent thinking than is usually acknowledged. The drawback is that memory as acquaintance (...) with the past falls short of fulfilling Russell’s requirement that knowledge by acquaintance be discriminating knowledge – a shortcoming shared by contemporary externalist accounts of knowledge from memory. (shrink)