We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the two systems (...) are dual to each other. The duality is expressed in a formal way which enables us to define a transformation of proofs in one of the systems into the proofs of the other. (shrink)

The aim of this paper is to emphasize the fact that for all finitely-many-valued logics there is a completely systematic relation between sequent calculi and tableau systems. More importantly, we show that for both of these systems there are al- ways two dual proof sytems (not just only two ways to interpret the calculi). This phenomenon may easily escape one’s attention since in the classical (two-valued) case the two systems coincide. (In two-valued logic the assignment of a truth value (...) and the exclusion of the opposite truth value describe the same situation.). (shrink)

An erotetic calculus for a given logic constitutes a sequent-style proof-theoretical formalization of the logic grounded in Inferential Erotetic Logic ). In this paper, a new erotetic calculus for Classical Propositional Logic ), dual with respect to the existing ones, is given. We modify the calculus to obtain complete proof systems for the propositional part of paraconsistent logic CLuN and its extensions CLuNs and mbC. The method is based on dual resolution. Moreover, the resolution rule is non-clausal. According (...) to the authors knowledge, this is the first account of resolution for mbC. Last but not least, as the method is grounded in IEL, it constitutes an important tool for the so-called question-processing. (shrink)

We present a dual tableau system, RLK, which is itself a deterministic decision procedure verifying validity of K-formulas. The system is constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. Furthermore, we describe an implementation of the system in Prolog, and we show some of its advantages.

A sequent calculus for the positive fragment of entailment together with the Church constants is introduced here. The single cut rule is admissible in this consecution calculus. A topological dual gaggle semantics is developed for the logic. The category of the topological structures for the logic with frame morphisms is proven to be the dual category of the variety, that is defined by the equations of the algebra of the logic, with homomorphisms. The duality results are extended to (...) the logic of entailment that includes a De Morgan negation. (shrink)

We offer a proof of the duality theorem for finitely presented MV-algebras and rational polyhedra, a folklore and yet fundamental result. Our approach develops first a general dual adjunction between MV-algebras and subspaces of Tychonoff cubes, endowed with the transformations that are definable in the language of MV-algebras. We then show that this dual adjunction restricts to a duality between semisimple MV-algebras and closed subspaces of Tychonoff cubes. The duality theorem for finitely presented objects is obtained by a (...) further specialisation. Our treatment is aimed at showing exactly which parts of the basic theory of MV-algebras are needed in order to establish these results, with an eye towards future generalisations. (shrink)

We study the extension 123) of the theory S21 by instances of the dual weak pigeonhole principle for p-time functions, dWPHPx2x. We propose a natural framework for formalization of randomized algorithms in bounded arithmetic, and use it to provide a strengthening of Wilkie's witnessing theorem for S21+dWPHP. We construct a propositional proof system WF , which captures the Π1b-consequences of S21+dWPHP. We also show that WF p-simulates the Unstructured Extended Nullstellensatz proof system of Buss et al. 256). We prove (...) that dWPHP is equivalent to a statement asserting the existence of a family of Boolean functions with exponential circuit complexity. Building on this result, we formalize the Nisan–Wigderson construction in a conservative extension of S21+dWPHP. (shrink)

The book presents logical foundations of dual tableaux together with a number of their applications both to logics traditionally dealt with in mathematics and philosophy (such as modal, intuitionistic, relevant, and many-valued logics) and to various applied theories of computational logic (such as temporal reasoning, spatial reasoning, fuzzy-set-based reasoning, rough-set-based reasoning, order-of magnitude reasoning, reasoning about programs, threshold logics, logics of conditional decisions). The distinguishing feature of most of these applications is that the corresponding dual tableaux are built (...) in a relational language which provides useful means of presentation of the theories. In this way modularity of dual tableaux is ensured. We do not need to develop and implement each dual tableau from scratch, we should only extend the relational core common to many theories with the rules specific for a particular theory. (shrink)

In this paper it is suggested to generalize our understanding of general (structural) proof theory and to consider it as a general theory of two kinds of derivations, namely proofs and dual proofs. The proposal is substantiated by (i) considerations on assertion, denial, and bi-lateralism, (ii) remarks on compositionality in proof-theoretic semantics, and (iii) comments on falsification and co-implication. The main formal result of the paper is a normal form theorem for the natural deduction proof system N2Int (...) of the bi-intuitionistic logic 2Int. The proof makes use of the faithful embedding of 2Int into intuitionistic logic with respect to validity and shows that conversions of dual proofs can be sidestepped. (shrink)

We present a relational proof system in the style of dual tableaux for the relational logic associated with a multimodal propositional logic for order of magnitude qualitative reasoning with a bidirectional relation of negligibility. We study soundness and completeness of the proof system and we show how it can be used for verification of validity of formulas of the logic.

We present a dual tableau system, RLK, which is itself a deterministic decision procedure verifying validity of K-formulas. The system is constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. Furthermore, we describe an implementation of the system RLK in Prolog, and we show some of its advantages.

Interval temporal logics provide both an insight into a nature of time and a framework for temporal reasoning in various areas of computer science. In this paper we present sound and complete relational proof systems in the style of dual tableaux for relational logics associated with modal logics of temporal intervals and we prove that the systems enable us to verify validity and entailment of these temporal logics. We show how to incorporate in the systems various relations between intervals (...) and/or various time orderings. (shrink)

We prove that the category of Nachbin’s compact ordered spaces and order-preserving continuous maps between them is dually equivalent to a variety of algebras, with operations of at most countable arity. Furthermore, we observe that the countable bound on the arity is the best possible: the category of compact ordered spaces is not dually equivalent to any variety of finitary algebras. Indeed, the following stronger results hold: the category of compact ordered spaces is not dually equivalent to any finitely accessible (...) category, any first-order definable class of structures, and any class of finitary algebras closed under products and subalgebras. An explicit equational axiomatisation of the dual of the category of compact ordered spaces is obtained; in fact, we provide a finite one, meaning that our description uses only finitely many function symbols and finitely many equational axioms. In preparation for the latter result, we establish a generalisation of a celebrated theorem by Mundici: our result—whose proof is independent of Mundici’s theorem—asserts that the category of unital commutative distributive lattice-ordered monoids is equivalent to the category of what we call MV-monoidal algebras.Abstract taken directly from the thesis.E-mail: [email protected]: https://air.unimi.it/retrieve/handle/2434/812809/1698986/phd_unimi_R11882.pdf. (shrink)

This paper contends that Stoic logic (i.e. Stoic analysis) deserves more attention from contemporary logicians. It sets out how, compared with contemporary propositional calculi, Stoic analysis is closest to methods of backward proof search for Gentzen-inspired substructural sequent logics, as they have been developed in logic programming and structural proof theory, and produces its proof search calculus in tree form. It shows how multiple similarities to Gentzen sequent systems combine with intriguing dissimilarities that may enrich contemporary discussion. Much of Stoic (...) logic appears surprisingly modern: a recursively formulated syntax with some truth-functional propositional operators; analogues to cut rules, axiom schemata and Gentzen’s negation-introduction rules; an implicit variable-sharing principle and deliberate rejection of Thinning and avoidance of paradoxes of implication. These latter features mark the system out as a relevance logic, where the absence of duals for its left and right introduction rules puts it in the vicinity of McCall’s connexive logic. Methodologically, the choice of meticulously formulated meta-logical rules in lieu of axiom and inference schemata absorbs some structural rules and results in an economical, precise and elegant system that values decidability over completeness. (shrink)

In the first chapter, we discuss Dummett’s idea that the notion of truth arises from the one of the correctness of an assertion. We argue that, in a first-order language, the need of defining truth in terms of the notion of satisfaction, which is yielded by the presence of quantifiers, is structurally analogous to the need of a notion of truth as distinct from the one of correctness of an assertion. In the light of the analogy between predicates in Frege (...) and open formulas in Tarksi, we concentrate on the semantic status of predicates. We register a dual attitude of Dummett towards Frege’s ascription of reference to predicates. On the one it is needed to endow quantifiers with their appropriate meaning. On the other hand, the introduction of concepts, as semantic correlate of predicates, smuggles a realist flavor in the overall semantic picture. In concluding the excursus (and with it the chapter), we stress Dummett’s will of developing a semantic picture free from this realist trait. In the second chapter, we present the idea of a proof-theoretic semantics. As for Frege true sentences denotes the truth-value True, so here closed' (i.e. categorical) valid argumentations denotes proofs. If a language contains implication-like operators, in order to characterize the condition of validity of a closed argumentation one has to introduce a notion of validity applying to ‘open’ (i.e. hypothetical) argumentations. We argue that this problem is analogous to the one posed by quantifiers in Frege-Tarksi’s style semantics. That is, implication forces one to introduce notion of validity for argumentations, which is more substantial than the correctness of the assertion of their conclusions. As we saw, the corresponding claim in the truth-based approach—that quantifiers require one to introduce a notion of truth, which is more substantial than the one of an assertion being correct—was the source of realism. Hence, Dummett proposes to reduce the semantic contribution of open argumentations to the one of their ‘closed instances’. In the truth-based perspective, this would correspond to the denial of the need of introducing concepts as the semantic correlates of predicates. We argue that Dummett’s fear, that an irreducible notion of function (represented by the need of ascribing validity to open argumentations) would lead to realism, turns out to be ill-founded. In the third chapter, we discuss the role played by the notion of truth in the anti-realist account. The notion of truth is what the anti-realist needs to cope with the so-called paradox of deduction. The analysis of the paradox yields to distinguishing between the truth of a sentence and the truth of a sentence being recognized. In terms of these conceptual couple, we reconsider the relationship between truth and assertion in an anti-realist perspective. Grounds are provided for a thesis (which was already advanced in chapter two), according to which the notion of the assertion of a sentence being correct is primarily connected only with the canonical means of establishing a sentence. The possibility of establishing a sentence by indirect means is conceptually dependent on the practice of establishing logical relationship of dependence among sentences. That is, the notion of a closed valid non-canonical argumentation is of any theoretical relevance only in presence of a notion of validity applying to open argumentations. In the fourth chapter, we discuss the possibility of characterizing in the proof-theoretic-semantics a notion of refutation. We develop an original characterization of refutations starting from an informal inductive specification of the condition of refutations of logically complex sentences. A sub-structural logic, called dual-intuitionistic logic, stands to this notion in the same relationship in which intuitionistic logic stands to the notion of proof so far consdered. All notions developed in chapter 2 have their corresponding (dual) ones in the framework developed. In particular, the distinctions canonical/non-canonical and closed/open argumentations. In the refutation based perspective, elimination rules have priority over introductions and the (only) assumption over the (many) conclusions. In the conclusions, we indicate the ingredients that an anti-realist approach to meaning should incorporate, in order to avoid the difficulties we registered. The core of an alternative view is a different conception of the relationship between categorical and hypothetical notions, in which the validity of open argumentations is not reduced to that of their instances, but rather it is directly defined. As a limit case, one would get a notion of validity applying to closed argumentations. (shrink)

This paper presents a sequent calculus and a dual domain semantics for a theory of definite descriptions in which these expressions are formalised in the context of complete sentences by a binary quantifier I. I forms a formula from two formulas. Ix[F, G] means ‘The F is G’. This approach has the advantage of incorporating scope distinctions directly into the notation. Cut elimination is proved for a system of classical positive free logic with I and it is shown to (...) be sound and complete for the semantics. The system has a number of novel features and is briefly compared to the usual approach of formalising ‘the F ’ by a term forming operator. It does not coincide with Hintikka’s and Lambert’s preferred theories, but the divergence is well-motivated and attractive. (shrink)

The logical formalism of abductive reasoning is still an open discussion and various theories have been presented about it. Abduction is a type of non-monotonic and defeasible reasonings, and the logic containing such a reasoning is one of the types of non-nonmonotonic and defeasible logics, such as inductive logic. Abduction is a kind of natural reasoning and it is a solution to the problems having this form "the phenomenon of φ cannot be explained by the theory of Θ" and we (...) need to search for (or to adduce) an explanation for φ. Taking α as the explanation and <Θ,φ> as the abductive problem, Θ∪{α}⊨φ is the logical format of a strong abductive reasoning. In this article, the proof theory for first-order abductive calculus is proposed based on Gentzen-type first-order proof theory. Considering its dual, i.e., the semantic tableaux, and without the need to translate the formulas, this calculation is sound and complete. After examining the structural rules of this calculus, some metalogical considerations and open problems such as consistency, completeness and undecidability of this account have been addressed. (shrink)

Beall and Restall’s Logical Pluralism (2006) characterises pluralism about logical consequence in terms of the different ways cases can be selected in the analysis of logical consequence as preservation of truth over a class of cases. This is not the only way to understand or to motivate pluralism about logical consequence. Here, I will examine pluralism about logical consequence in terms of different standards of proof. We will focus on sequent derivations for classical logic, imposing two different restrictions on classical (...) derivations to produce derivations for intuitionistic logic and for dual intuitionistic logic. The result is another way to understand the manner in which we can have different consequence relations in the same language. Furthermore, the proof-theoretic perspective gives us a different explanation of how the one concept of negation can have three different truth conditions, those in classical, intuitionistic and dual-intuitionistic models. (shrink)

We present relational proof systems for the four groups of theories of spatial reasoning: contact relation algebras, Boolean algebras with a contact relation, lattice-based spatial theories, spatial theories based on a proximity relation.

An Ockham lattice is defined to be a distributive lattice with 0 and 1 which is equipped with a dual homomorphic operation. In this paper we prove: (1) The lattice of all equational classes of Ockham lattices is isomorphic to a lattice of easily described first-order theories and is uncountable, (2) every such equational class is generated by its finite members. In the proof of (2) a characterization of orderings of with respect to which the successor function is decreasing (...) is given. (shrink)

Two examples of Galois connections and their dual forms are considered. One of them is applied to formulate a criterion when a given subset of a complete lattice forms a complete lattice. The second, closely related to the first, is used to prove in a short way the Knaster-Tarski’s fixed point theorem.

We present a proof of the equivalence between two deductive systems for constructive necessity, namely an axiomatic characterisation inspired by Hakli and Negri's system of derivations from assumptions for modal logic , a Hilbert-style formalism designed to ensure the validity of the deduction theorem, and the judgmental reconstruction given by Pfenning and Davies by means of a natural deduction approach that makes a distinction between valid and true formulae, constructively. Both systems and the proof of their equivalence are formally verified (...) using the state-of-the-art proof assistant Coq. The proof approach taken throughout the paper unveils the use of some alternative proof methods that allow for a smooth transition from the high-level mathematical proofs to their mechanised counterparts. (shrink)

In this article, I will discuss Mulla Sadrā's proof of ideas together with his evaluations of Fārābī, Ibn Sīnā and Suhrawardī's views. The aim of the article is to try to provide a certain opinion about the proof that Sadrā developed. It is seen that Sadrā generally exhibits a dual attitude about ideas. Sadrā's first attitude is to match the theologians' teaching of names, Suhrawardi's view of the master of genres, the sufists' a'yan al-sābita theory and the Peripatetics’ concept (...) of universal with ideas. His second attitude is that he is alone at the point of understanding Plato and reaching the clearness of the issue. In other words, he states that there has been no one who have understood and explained the issue as it should be. Sadrā attributes his own success on the subject both to discovery and inspiration, and to his intellectual research on existence. The aim of Sadrā is to try to unite between Plato and Aristotle. Therefore, he also follows Plotinos and Fārābī, who had this purpose before him. Sadrā, who criticizes Avicenna on the subject, sees Suhrawardī as the philosopher who comes closest to the truth, but states that he is also inadequate in some points. (shrink)

We combine intuitionistic logic and classical logic into a new, first-order logic called polarized intuitionistic logic. This logic is based on a distinction between two dual polarities which we call red and green to distinguish them from other forms of polarization. The meaning of these polarities is defined model-theoretically by a Kripke-style semantics for the logic. Two proof systems are also formulated. The first system extends Gentzenʼs intuitionistic sequent calculus LJ. In addition, this system also bears essential similarities to (...) Girardʼs LC proof system for classical logic. The second proof system is based on a semantic tableau and extends Dragalinʼs multiple-conclusion version of intuitionistic sequent calculus. We show that soundness and completeness hold for these notions of semantics and proofs, from which it follows that cut is admissible in the proof systems and that the propositional fragment of the logic is decidable. (shrink)

Peirce’s triadic logic has been under discussion since its discovery in the 1960s by Fisch and Turquette. The experiments with matrices of three-valued logic are recorded in a few pages of unpublished manuscripts dated 1909, a decade before similar systems have been developed by logicians. The purposes of Peirce’s work on such logic, as well as semantical aspects of his system, are disputable. In the most extensive work about it, Turquette suggested that the matrices are related in dual pairs (...) of axiomatic Hilbert-style systems. In this paper, we present a simple tableau proof for a fragment of Peirce three-valued logic, called P3, based on similar approaches in many-valued literature. We demonstrated that this proof is sound and complete. Besides that, taking the false as the only undesignated value and adding non-classical negations to the calculus, we can explore paraconsistent and paracompleteness theories into P3. Keywords: Charles S. Peirce, many-valued logics, theory of proof, tableau method. (shrink)

ABSTRACT This part of the series has a dual purpose. In the first place we will discuss two kinds of theories of proof. The first kind will be called a theory of linear proof. The second has been called a theory of suppositional proof. The term "natural deduction" has often and correctly been used to refer to the second kind of theory, but I shall not do so here because many of the theories so-called are not of the second (...) kind--they must be thought of either as disguised linear theories or theories of a third kind (see postscript below). The second purpose of this part is 25 to develop some of the main ideas needed in constructing a comprehensive theory of proof. The reason for choosing the linear and suppositional theories for this purpose is because the linear theory includes only rules of a very simple nature, and the suppositional theory can be seen as the result of making the linear theory more comprehensive. CORRECTION: At the time these articles were written the word ‘proof’ especially in the phrase ‘proof from hypotheses’ was widely used to refer to what were earlier and are now called deductions. I ask your forgiveness. I have forgiven Church and Henkin who misled me. (shrink)

Some commentators have worried that Descartes‘s ontological proof is a kind ofafterthought, redundancy, or even embarrassment. Descartes has everythingneeded to establish God as the ground of certainty by Meditation Three, so whybother with yet another proof in Meditation Five? Some have even gone so far asto doubt his sincerity.1Past literature on this topic is of daunting variety andmagnitude, dating back to the seventeenth century.2The current discussion hasfocused on Descartes‘s premises in relation to the coherence of his concept ofGod.3I wish to (...) take up this issue from a somewhat different tack, showing that Descartes‘s ontological proof actually involves a subtle change in the direction ofhis argument from a reflective to a recollective theory of innateness. In the FifthMeditation, Descartes does not simply expand on his previous discussion of God,which arose out of reflection on his self; rather, the ontological proof depends ona kind of recollection of God‘s being that could only be based on the causalpositivity, or ―power,‖ of His existence. God is the structural cause of our idea ofhim and thereby restricts the way in which we may think of Him, in the sameway as the essence of a triangle structurally determines the ways we must thinkof it.4We are not free to construct such ideas in any way we want, so there mustbe a cause, or a reason, that restricts such construction.The specific argument of Meditation Five, however, must be understoodin its larger context, for part of the structurally determined idea of God containsnecessary existence, which Descartes interprets in terms of causal power. In theprocess of explaining this causal power, first to Caterus and, later to Arnauld,Descartes develops a way of interpreting God‘s causal relationship to himself, interms of a scholastic distinction between God as causa sui and ens a se, whichpreserves the universality of the causal principle and allows us to understand whyGod can be considered as the formal cause of His own being—the self-groundingground of all existence—an idea of subsequent importance to Malebranche andSpinoza, among others. Understanding this position on God and cause allows usto see a complementarity between Mediations III and V that has previously beenoverlooked.5While the principle of eminent causality found in Meditation Threeis central to the structural causation argument of Meditation Five, it is God‘spower, the positivity of His causal relationship to himself, that allows theargument from his effects to his existence in the first place.The dualistic structure to Descartes‘s arguments for God‘s existence inMeditations Three and Five mirrors Anselm‘s approach in the Monologion andthe Proslogion. Appreciating this stylistic debt is crucial for understandingDescartes‘s attempts to improve on Anselm‘s arguments, as well as his attempt totruly ground all knowledge in the certainty of God‘s existence. Yet whileAnselm‘s dual argument is ultimately based on a negative intuition of God‘sbeing, described in the Monologion as that without which the world cannot be,Descartes‘s dual argument in Meditations Three and Five is based on a positiveintuition or recollection of God‘s being as a necessary structural restriction on our concepts of the world. The ontological proof is primarily based on thisrecollective theory of innateness. It is God as causa sui, recollected as thenecessary ground of all things, that is the sole efficient cause of the existence ofevery finite, limited thing—especially human beings and their clear and distinctideas. (shrink)

We introduce an Automatic Theorem Prover (ATP) of a dual tableau system for a relational logic for order of magnitude qualitative reasoning, which allows us to deal with relations such as negligibility, non-closeness and distance. Dual tableau systems are validity checkers that can serve as a tool for verification of a variety of tasks in order of magnitude reasoning, such as the use of qualitative sum of some classes of numbers. In the design of our ATP, we have (...) introduced some heuristics, such as the so called phantom variables, which improve the efficiency of the selection of variables used un the proof. (shrink)

In this paper we introduce a Gentzen calculus for (a functionally complete variant of) Belnap's logic in which establishing the provability of a sequent in general requires \emph{two} proof trees, one establishing that whenever all premises are true some conclusion is true and one that guarantees the falsity of at least one premise if all conclusions are false. The calculus can also be put to use in proving that one statement \emph{necessarily approximates} another, where necessary approximation is a natural (...) class='Hi'>dual of entailment. The calculus, and its tableau variant, not only capture the classical connectives, but also the `information' connectives of four-valued Belnap logics. This answers a question by Avron. (shrink)

The debate on how to interpret Kant's transcendental idealism has been prominent for several decades now. In his book Kant's Transcendental Proof of Realism (2004) Kenneth R. Westphal introduces and defends his version of the metaphysical dual-aspect reading. But his real aim lies deeper: to provide a sound transcendental proof for (unqualified) realism, based on Kant's work, without resorting to transcendental idealism. In this sense his aim is similar to that of Peter F. Strawson – although Westphal's approach is (...) far more sophisticated. First he attempts to show that noumenal causation – on the reality of which his argument partly rests – is coherent in and necessary for Kant's transcendental idealism. Westphal then aims to undermine transcendental idealism by two major claims: Kant can neither account for transcendental affinity nor satisfactorily counter Hume's causal scepticism. Finally Westphal defends his alternative for transcendental idealism by showing that it solves these problems and thus offers a genuine transcendental proof for realism. In this paper I will show that all the three steps outlined above suffer from decisive shortcomings, and that consequently, regardless of its merits, Westphal's transcendental argument for realism remains undemonstrated. (shrink)

The paper is a continuation of another paper published as Part I. Now, the case of “n=3” is inferred as a corollary from the Kochen and Specker theorem (1967): the eventual solutions of Fermat’s equation for “n=3” would correspond to an admissible disjunctive division of qubit into two absolutely independent parts therefore versus the contextuality of any qubit, implied by the Kochen – Specker theorem. Incommensurability (implied by the absence of hidden variables) is considered as dual to quantum contextuality. (...) The relevant mathematical structure is Hilbert arithmetic in a wide sense, in the framework of which Hilbert arithmetic in a narrow sense and the qubit Hilbert space are dual to each other. A few cases involving set theory are possible: (1) only within the case “n=3” and implicitly, within any next level of “n” in Fermat’s equation; (2) the identification of the case “n=3” and the general case utilizing the axiom of choice rather than the axiom of induction. If the former is the case, the application of set theory and arithmetic can remain disjunctively divided: set theory, “locally”, within any level; and arithmetic, “globally”, to all levels. If the latter is the case, the proof is thoroughly within set theory. Thus, the relevance of Yablo’s paradox to the statement of Fermat’s last theorem is avoided in both cases. The idea of “arithmetic mechanics” is sketched: it might deduce the basic physical dimensions of mechanics (mass, time, distance) from the axioms of arithmetic after a relevant generalization, Furthermore, a future Part III of the paper is suggested: FLT by mediation of Hilbert arithmetic in a wide sense can be considered as another expression of Gleason’s theorem in quantum mechanics: the exclusions about (n = 1, 2) in both theorems as well as the validity for all the rest values of “n” can be unified after the theory of quantum information. The availability (respectively, non-availability) of solutions of Fermat’s equation can be proved as equivalent to the non-availability (respectively, availability) of a single probabilistic measure as to Gleason’s theorem. (shrink)

Proust's madeleine illustrates the automatic nature of associative learning. Although we agree with Mitchell et al. that no compelling scientific proof for this effect has yet been reported in humans, evolutionary constraints suggest that it should not be discarded: There is no reason by which natural selection should favor individuals who lose a fast and automatic survival tool.

Girard introduced phase semantics as a complete set-theoretic semantics of linear logic, and Okada modified phase-semantic completeness proofs to obtain normal-form theorems. On the basis of these works, Okada and Takemura reformulated Girard’s phase semantics so that it became phase semantics for proof-terms, i.e., lambda-terms. They formulated phase semantics for proof-terms of Laird’s dual affine/intuitionistic lambda-calculus and proved the normal-form theorem for Laird’s calculus via a completeness theorem. Their semantics was obtained by an application of computability predicates. In (...) this paper, we first formulate phase semantics for proof-terms of second-order intuitionistic propositional logic by modifying Tait-Girard’s saturated sets method. Next, we prove the completeness theorem with respect to this semantics, which implies a strong normalization theorem. (shrink)

Public entities around the world are increasingly deploying artificial intelligence and algorithmic decision-making systems to provide public services or to use their enforcement powers. The rationale for the public sector to use these systems is similar to private sector: increase efficiency and speed of transactions and lower the costs. However, public entities are first and foremost established to meet the needs of the members of society and protect the safety, fundamental rights, and wellbeing of those they serve. Currently AI systems (...) are deployed by the public sector at various administrative levels without robust due diligence, monitoring, or transparency. This paper critically maps out the challenges in procurement of AI systems by public entities and the long-term implications necessitating AI-specific procurement guidelines and processes. This dual-prong exploration includes the new complexities and risks introduced by AI systems, and the institutional capabilities impacting the decision-making process. AI-specific public procurement guidelines are urgently needed to protect fundamental rights and due process. (shrink)

: Undoubtedly, in the formation of history, relations between religious structures and political powers, which are shaped within certain principles, have an important place. The course of these relations determines the strength and domain of both sides. This form of relationship, in some cases, evolves in favor of political power, and sometimes manifests itself as a political direction of religious interests. It is possible to see politics as a direction of religion or to use it in the direction of its (...) own interests in the politics that the Soviet Union has implemented since the Second World War. As a matter of fact, the Soviet Union, which has embraced the ideology of official atheism and struggled against religious beliefs, did not stop using religion/church for conjuration in its own interests. In this context, The Soviet leader Stalin has almost reconstructed the Russian Orthodox Church, which he had been trying to destroy since the early years of the Second World War. Even, Moscow has made serious attempts to make Patriarchate the pioneer of the Orthodox world. In this article, we aim to emphasize Stalin’s church politics and reasons. We will also stress the reasons behind the Council of the Orthodox Churches, which Stalin sought to achieve through the Moscow Patriarchate in 1947. Finally, we will touch on the policy of the Fener Greek Patriarch against these developments. Summary: Throughout history, politics of states have been under the influence of religion. Likewise, religions have directed political authority in the direction of their own interests. Sometimes a religion takes the state under its influence; sometimes under a state takes a religion under the influence and they try to use the other one in the interests of itself. Concepts that define religion-state relations have emerged under the influence of experiences experienced over time. Secularism is at the head of the concepts that determine religion-state relations today. What secularism is and how it is practiced is much debated in the scientific circles. Despite all these struggles, however, no binding definition has been reached for all political issues. Certainly, the subjective structure of states plays an important role in regulating religion-state relations. The political ideology adopted by this political structure and the world view varies. Sometimes political structures with official atheist ideology can break the principle of secularism. While these ideologies are ungodly in their nature, they benefit from political interests. As an example, it is possible to show the Soviet Union with an atheist ideology. Because the Soviet regime used religion in the direction of political interests between 1943-1948. The Russian Orthodox Church, which was very active and competent during the reign of Tsarist Russia, lost its power with the Bolshevik Revolution in 1917. The Soviet regime has made the Russian Orthodox Church an illegal institution. The struggle against the church by the regime continued until the Second World War. With the Second World War, Stalin's church politics changed. There is no doubt that this political change has become more than one reason. The first is that the state has entered into a war. Stalin did not want to continue the struggle with religion while the war was going on. Another reason for pushing Stalin for a policy change towards the Church is the anti-Soviet propaganda carried out by the Germans. As a matter of fact, the Germans defined themselves as the savior of the Russian people. It was also alleged that Germany was waging a war against the Soviets in order to free Russian people from communism. Even brochures were taken from the airplanes in this frame. The Germans aimed to break the resistance of the Russian people with this method. Stalin acted to ward off this propaganda of the Germans. Stalin therefore had to keep an eye on church politics and stopped the oppression against the church. In this framework, opportunities were provided for the Russian Orthodox Church. For example, have been approved to organize rites in churches. The priests are encouraged to strengthen hand the people. Also closed churches have been reopened by Stalin. In this way the German propaganda has been wasted. The Second World War ended with the victory of the Soviet Union. Stalin, however, continued to use the church after the war was over. So why did Stalin continue to support the church as an atheist? What were the reasons for pushing Stalin into this policy? Stalin's post-war church policy has multiple causes. The most important of these is spreading the Soviet influence over the entire Balkans and Middle East geography through the Russian Orthodox Church. Undoubtedly this is related to the long-term policies of the Soviets. Because the war has changed all the balances in the world. This has given new opportunities to the Soviets. At the beginning of these, the Orthodox world comes to the Soviet influence. It seems that the steps towards this have been started to be started from 1945. In this context, the Russian Orthodox Church found important activities. For example, the Moscow Patriarch has established relations with other Orthodox Churches. Jerusalem, Athens, Cyprus, Antakya churches were visited. In the end, an attempt was made to collect the Orthodox Council. The struggle of the Western and Eastern bloc emerged after the Second World War divided the Orthodox world into two camps. In this process, the Greek, Cyprus and Jerusalem Orthodox churches under the leadership of the Fener Patriarchate were under American influence. The Serbian, Bulgarian and Antiochian Orthodox Churches under the leadership of the Moscow Patriarchate were under Soviet influence. For these reasons, the Soviet regime, which has been fighting for the Church since the Bolshevik Revolution in 1917, has given up its position. It is understood from this historical fact that a regime adopting irreligion as an official ideology uses religion in its own interests as needed. This indicates that secularism is relative. This study will try to show how the Soviet Union uses the Russian Orthodox Church in its own interests despite the atheism ideology. (shrink)

We present a relational proof system in the style of dual tableaux for a multimodal propositional logic for order of magnitude qualitative reasoning to deal with relations of negligibility, non-closeness, and distance. This logic enables us to introduce the operation of qualitative sum for some classes of numbers. A relational formalization of the modal logic in question is introduced in this paper, i.e., we show how to construct a relational logic associated with the logic for order-of-magnitude reasoning and its (...) dual tableau system which is a validity checker for the modal logic. For that purpose, we define a validity preserving translation of the modal language into relational language. Then we prove that the system is sound and complete with respect to the relational logic defined as well as with respect to the logic for order of magnitude reasoning. Finally, we show that in fact relational dual tableau does more. It can be used for performing the four major reasoning tasks: verification of validity, proving entailment of a formula from a finite set of formulas, model checking, and verification of satisfaction of a formula in a finite model by a given object. (shrink)

In this paper I will show the problems that are encountered when dealing with uniqueness of connectives in a bilateralist setting within the larger framework of proof-theoretic semantics and suggest a solution. Therefore, the logic 2Int is suitable, for which I introduce a sequent calculus system, displaying - just like the corresponding natural deduction system - a consequence relation for provability as well as one dual to provability. I will propose a modified characterization of uniqueness incorporating such a duality (...) of consequence relations, with which we can maintain uniqueness in a bilateralist setting. (shrink)

The purpose of this paper is to introduce a bi-intuitionistic sequent calculus and to give proofs of admissibility for its structural rules. The calculus I will present, called SC2Int, is a sequent calculus for the bi-intuitionistic logic 2Int, which Wansing presents in [2016a]. There he also gives a natural deduction system for this logic, N2Int, to which SC2Int is equivalent in terms of what is derivable. What is important is that these calculi represent a kind of bilateralist reasoning, since (...) they do not only internalize processes of verifcation or provability but also the dual processes in terms of falsifcation or what is called dual provability. In [Wansing, 2017] a normal form theorem for N2Int is stated, here, I want to prove a cut-elimination theorem for SC2Int, i.e., if successful, this would extend the results existing so far. (shrink)

A dual-language edition presenting Descartes's original Latin text of his greatest work, with a facing-page authoritative English translation.

Dual arguments have become a standard tool for analysis of problems involving optimization by consumers and producers. The principal aim of this book is to provide a fairly systematic yet simple exposition of the basic structure of such arguments. The emphasis is not on providing mathematically general proofs; instead, a geometric approach is used to provide, in an informal way, an intuitive understanding of duality theory. This book introduces the most common alternative ways of representing preferences and technologies, (...) such as indirect utility and distance functions, expenditure and cost functions, and profit and revenue functions. and it discusses the assumptions under which alternative formulations contain precisely the same information. Results such as Roy's identity. the Hotelling-Wold identity, and Shephard's lemma are fully explained. as are their roles in facilitating analysis of behaviour. (shrink)

The purpose of this text is to analyze the social representations of feminism in divinatory practices. Our research in a few Moldavian counties has identified two main types of social representations of the relationship between magic/divination and feminism. Therefore, there are some dual representations of the feminine divinatory agents versus the masculine ones. Even though women are well represented among clairvoyants, clients, and spectators, these valorizations function as negative stereotypes and do not serve the women. Another representation of feminism (...) in divinatory practices that does not necessarily imply negativism and damnation is a more recent one. Old stereotypes are tamed and attenuated. The results of our research have shown that women continue to be associated with the survival of these practices. This is proof that old myths and representations are still alive. They are discretely present in social expressions. Finally, they will dominate us completely. (shrink)

Logical and philosophical literature provides different classifications of reasoning. In the Polish literature on the subject, for instance, there are three popular ones accepted by representatives of the Lvov-Warsaw School: Jan Łukasiewicz, Tadeusz Czeżowski and Kazimierz Ajdukiewicz (Ajdukiewicz in Logika pragmatyczna [Pragmatic Logic]. PWN, Warsaw (1965, 2nd ed. 1974). Translated as: Pragmatic Logic. Reidel & PWN, Dordrecht, 1975). The author of this paper, having modified those classifications, distinguished the following types of reasoning: (1) deductive and (2) non-deductive, and additionally two (...) types of them in each of the two, depending on the manner of combining their premises with the conclusion through the relation of classical logical entailment. Consequently, the four types of reasoning: unilateral deductive (incl. its sub-types: deductive inference and proof), bilateral deductive (incl. complete induction), and reductive (incl. the sub-types: explanation and verification), logically nonvaluable (incl. inference by analogy, statistic inference), correspond to four operators of derivability. They are defined formally on the ground of Tarski’s axiomatic theory of deductive systems, by means of the consequence operation _Cn_ (Tarski in Monatshefte Math Phys 37:361–404, 1930a, C R Soc Sci Lett Vars 23:22–29, 1930b). Also, certain metalogical properties of these operators are given, as well as their relations with Tarski’s consequence operations \(Cn^+\) ( \(Cn^+ = Cn\) ) and dual consequences \(Cn^{-1}\) (Słupecki in Zeszyty Naukowe Uniwersytetu Wrocławskiego Seria B Nr 3:33–40, 1959, Słupecki et al. in Stud Log 29:76–123, 1971, Wybraniec-Skardowska, in: Wybraniec-Skardowska, Bryll (eds) Z badań nad teorią zdań odrzuconych [Studies in the Theory of Rejected Propositions], Series B, Studia i Monografie, Zeszyty Naukowe Wyższej Szkoły Pedagogicznej w Opolu, Opole, 1969), and \(Cn^-\) (Wójcicki in Bull Sect Log 2(2):54–57, 1973)). (shrink)

The crossing property is perhaps the most subtle aspect of the particle-field relation. Although it is not difficult to state its content in terms of certain analytic properties relating different matrixelements of the S-matrix or formfactors, its relation to the localization- and positive energy spectral principles requires a level of insight into the inner workings of QFT which goes beyond anything which can be found in typical textbooks on QFT. This paper presents a recent account based on new ideas derived (...) from “modular localization” including a mathematic appendix on this subject. Its main achievement is the proof of the crossing property from a two-algebra generalization of the KMS condition.The main content is an in-depth criticism of the dual model and its string theoretic extension. The conceptual flaws of these models are closely related to misunderstandings of crossing. The correct interpretation of string theory is that of a dynamic infinite component one particle space where “dynamic” means that, unlike a mere collection of independent free fields, the formalism contains also operators which communicate between the different irreducible Poincaré representations and set the mass/spin spectrum. Whereas in pre-string times there were unsuccessful attempts to achieve this in analogy to the O(4,2) hydrogen spectrum by the use of higher noncompact groups, the superstring in d=9+1, which uses instead (bosonic/fermionic) oscillators obtained from multicomponent chiral currents, is the only known solution of the dynamical infinite component pointlike field (or pointlike generated wave function) project. (shrink)

Symmetic combinatory logic with the symmetric analogue of a combinatorially complete base (in the form of symmetric λ-calculus) is known to lack the Church-Rosser property. We prove a muchstrongertheorem that no symmetric combinatory logic that containsat least two proper symmetric combinatoryhas the Church-Rosser property. Although the statement of the result looks similar to an earlier one concerning dual combinatory logic,the proof is differentbecause symmetric combinators may form redexes in both left and right associated terms. Perhaps surprisingly, we are also (...) able to show that certain symmetric combinatory logics that include justone particular constantare not confluent. This result (beyond other differences) clearly sets apart symmetric combinatory logic from dual combinatory logic, since all dual combinatory systems with a single combinator or a single dual combinator are Church-Rosser. Lastly, we prove that a symmetric combinatory logic that contains the fixed point and the one-place identity combinator has the Church-Rosser property. (shrink)

It is well known that classical inferentialist semantics runs into problems regarding abnormal valuations. It is equally well known that the issues can be resolved if we construct the inference relation in a multiple-conclusion sequent calculus. The latter has been prominently developed in recent work by Restall, with the guiding interpretation that the valid sequent says that the simultaneous assertion of all of Γ with the denial of all of Δ is incoherent. However, such structures face significant interpretive challenges, and (...) they do not provide an adequate grasp on the machinery of the duality of assertions and denials that could provide an abstract account of inferential semantics; show why the dual treatment is semantically superior. This paper explores a slightly different tack by considering a dual-calculus framework consisting of two, single-conclusion, inference relations dealing with the preservation of assertion and the preservation of denial, respectively. In this context, I develop an abstract inferentialist semantics, before going on to show that the framework is equivalent to Restall’s, whilst providing a better grasp on the underlying proof-structure. (shrink)