This paper discusses the relation between the minimal positive relevant logic B and intersection and union type theories. There is a marvelous coincidence between these very differently motivated research areas. First, we show a perfect fit between the Intersection Type Discipline ITD and the tweaking BT of B, which saves implication and conjunction but drops disjunction . The filter models of the -calculus (and its intimate partner Combinatory Logic CL) of the first author and her coauthors then become theory models (...) of these calculi. (The logician's "theory" is the algebraist's "filter".) The coincidence extends to a dual interpretation of key particles—the subtype translates to provable , type intersection to conjunction , function space to implication, and whole domain to the (trivially added but trivial) truth T. This satisfying ointment contains a fly. For it is right, proper, and to be expected that type union should correspond to the logical disjunction of B. But the simulation of functional application by a fusion (or modus ponens product) operation on theories leaves the key Bubbling lemma of work on ITD unprovable for the -prime theories now appropriate for the modeling. The focus of the present paper lies in an appeal to Harrop theories which are (a) prime and (b) closed under fusion. A version of the Bubbling lemma is then proved for Harrop theories, which accordingly furnish a model of and CL. (shrink)

Miller, D., G. Nadathur, F. Pfenning and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic 51 125–157. A proof-theoretic characterization of logical languages that form suitable bases for Prolog-like programming languages is provided. This characterization is based on the principle that the declarative meaning of a logic program, provided by provability in a logical system, should coincide with its operational meaning, provided by interpreting logical connectives as simple and fixed search instructions. The (...) operational semantics is formalized by the identification of a class of cut-free sequent proofs called uniform proofs. A uniform proof is one that can be found by a goal-directed search that respects the interpretation of the logical connectives as search instructions. The concept of a uniform proof is used to define the notion of an abstract logic programming language, and it is shown that first-order and higher-order Horn clauses with classical provability are examples of such a language. Horn clauses are then generalized to hereditary Harrop formulas and it is shown that first-order and higher-order versions of this new class of formulas are also abstract logic programming languages if the inference rules are those of either intuitionistic or minimal logic. The programming language significance of the various generalizations to first-order Horn clauses is briefly discussed. (shrink)

The paper proves refined feasibility properties for the disjunction property of intuitionistic propositional logic. We prove that it is possible to eliminate all cuts from an intuitionistic proof, propositional or first-order, without increasing the Horn closure of the proof. We obtain a polynomial time, interactive, realizability algorithm for propositional intuitionistic proofs. The feasibility of the disjunction property is proved for sequents containing Harrop formulas. Under hardness assumptions for NP and for factoring, it is shown that the intuitionistic propositional (...) calculus does not always have polynomial size proofs and that the classical propositional calculus provides a superpolynomial speedup over the intuitionistic propositional calculus. The disjunction property for intuitionistic propositional logic is proved to be P-hard by a reduction to the circuit value problem. (shrink)

We study a range of issues connected with the idea of replacing one formula by another in a fixed context. The replacement core of a consequence relation ⊢ is the relation holding between a set of formulas {A1,..., Am,...} and a formula B when for every context C, we have C,..., C,... ⊢ C. Section 1 looks at some differences between which inferences are lost on passing to the replacement cores of the classical and intuitionistic consequence relations. For example, (...) we find that while the inference from A and B to \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$A \land B$\end{document}, sanctioned by both these initial consequence relations, is retained on passage to the replacement core in the classical case, it is lost in the intuitionistic case. Further discussion of these two logics occupies Sections 3 and 4. Section 2 looks at the m = 1 case, describing A as replaceable by B according to ⊢ when B is a consequence of A by the replacement core of ⊢, and inquiring as to which choices of ⊢ render this induced replaceability relation symmetric. Section 5 investigates further conceptual refinements— such as a contrast between horizontal and vertical replaceability—suggested by some work of R. B. Angell and R. Harrop in the 1950s and 1960s. Appendix 1 examines a related aspect of term-for-term replacement in connection with identity in predicate logic. Appendix 2 is a repository for proofs which would otherwise clutter up Section 3. (shrink)

In the 80's Pierangelo Miglioli, starting from motivations in the framework of Abstract Data Types and Program Synthesis, introduced semiconstructive theories, a family of “large subsystems” of classical theories that guarantee the computability of functions and predicates represented by suitable formulas. In general, the above computability results are guaranteed by algorithms based on a recursive enumeration of the theorems of the whole system. In this paper we present a family of semiconstructive systems, we call uniformly semiconstructive, that provide computational (...) procedures only involving formulas with bounded complexity. We present several examples of uniformly semiconstructive systems containing Harrop theories, induction principles and some well-known predicate intermediate principles. Among these, we give an account of semiconstructive and uniformly semiconstructive systems which lie between Intuitionistic and Classical Arithmetic and we discuss their constructive incompatibility. (shrink)

In the 80's Pierangelo Miglioli, starting from motivations in the framework of Abstract Data Types and Program Synthesis, introduced semiconstructive theories, a family of large subsystems of classical theories that guarantee the computability of functions and predicates represented by suitable formulas. In general, the above computability results are guaranteed by algorithms based on a recursive enumeration of the theorems of the whole system. In this paper we present a family of semiconstructive systems, we call uniformly semiconstructive, that provide computational (...) procedures only involving formulas with bounded complexity. We present several examples of uniformly semiconstructive systems containing Harrop theories, induction principles and some well-known predicate intermediate principles. Among these, we give an account of semiconstructive and uniformly semiconstructive systems which lie between Intuitionistic and Classical Arithmetic and we discuss their constructive incompatibility. (shrink)

I examine the (mediated) correspondence between Spinoza and Robert Boyle concerning the latter’s account of fluidity and his experiments on reconstitution of niter in the light of the epistemology and doctrine of method contained in the Treatise on the Emendation of the Intellect. I argue that both the Treatise and the correspondence reveal that for Spinoza, the proper method of science is not experimental, and that he accepted a powerful under-determination thesis. I argue that, in contrast to modern versions, Spinoza’s (...) form of naturalism was a highly rationalist and anti-empirical one. I conclude with a brief account of the value of experience and experimentation for Spinoza’s scientific method. (shrink)

Leibniz often refers to the Principle of Sufficient Reason (PSR) as something like a first principle. In some texts, however, he attempts to give positive arguments in its favor. I examine two such arguments, and find them wanting. The first argument has two defects. First, it is question-begging; and second, when the question-begging step is excised, the principle one can in fact derive is highly counter-intuitive. The second argument is valid, but has the defect of only reaching a nearly trivial (...) conclusion. (shrink)

Priority monism is the doctrine that there is only one basic object: the entire cosmos. Priority monists often take this to be a metaphysically necessary thesis. I explore the consequences of modalizing the priority monist thesis. I argue that, modulo some assumptions, the modalized thesis entails the necessary existence of the actual cosmos. I further argue that, if the modalized thesis is true, and the actual cosmos necessarily exists, then the only possible concrete objects are the actually existing ones.

This paper takes as its starting point an examination of the current status of some of the concerns that were raised in the mid?1980s about methodological problems faced by educational researchers using the behavioural approach in schools. These concerns included the measurement of agreement between observers, the interpretation of raw data extracted, the potential influences of observers and the inherent properties of research designs. Subsequently, some more wide?ranging concerns are considered, in particular the kinds of behaviour selected for treatment, the (...) lack of analysis of what is involved in teachers? positive responses to pupils? behaviour and the relatively uninvestigated effects of teachers? negative responses. The conclusions are presented as a series of points that are listed, as far as possible, in the order in which they confront the investigator. (shrink)

Kearns (2021) argues that there is a parody version of Anselm's ontological argument (a "gontological argument") which shows that God does not exist. I show that Anselm considers one of the key premises in Kearns' gontological argument, and explicitly gives an argument which entails its falsity, and hence the unsoundness of the supposed parody argument. -/- .

There have been a number of earlier investigations, using differing methodologies, into the extent to which teachers in the secondary school interact with boys and girls and the results have suggested an imbalance in the teachers? verbal behaviour towards the genders that is quite similar to the imbalance found in teachers? behaviour in the primary school. The main aim of this study was to devise an investigation using the same methodology as that used in a recent primary school investigation in (...) order to be able to make a fair comparison between the two levels. The results showed considerable differences in the teachers? verbal behaviour towards the genders in the secondary school from that of teachers in the primary school. Where the primary school data showed teachers interacting more with the boys than the girls and the boys being less on?task than the girls, the secondary school data showed no such differences. (shrink)

Much of the research in higher education has treated student bodies as homogeneous groups with a consequent neglect of any consideration of gender differences. To test the validity of such research a questionnaire was administered to 255 psychology students. The results showed some important differences in responses between the genders. In particular, the female students reported attaching more importance than males to pre?course aims, rated various learning activities as more valuable and interesting than males and reported more improvement in nine (...) of the 12 skills surveyed than the males. The males rated experiencing less difficulty for various aspects of the course than anticipated than did the females for 11 of 12 potential difficulties listed. As a consequence, it is suggested that researchers ought to be wary of conducting research into various aspects of higher education without considering potential gender differences. (shrink)

In the second chapter of her <i>Institutions de Physique</i> Emilie Du Chatelet gives two cosmological arguments for the existence of God. In this chapter I focus on the first of these arguments. I argue that, while it bears some significant similarities to arguments given by John Locke and Christian Wolff, it improves on these arguments in at least two ways. First, it avoids a potential equivocation in Locke's argument; and second, it avoids Wolff's mere stipulation that whoever claims that there (...) cannot be an infinite regress of contingent beings does not understand what a sufficient reason is. I finally argue that her argument avoids a related objection, considered by David Hume, on which to explain a causal chain is merely to explain each link in the chain. (shrink)

I examine the views of Thomas Reid with respect to a certain version of the problem of induction: Why are inductions using natural kinds successful, and what justifies them? I argue that while both Reid holds a kind of conventionalist view about natural kinds, this conventionalism has a realistic component which allows him to answer both questions.

Nineteen teachers took part in a brief, one session, in?service course in which they were trained in behavioural techniques with the main aim of helping them increase their rates of approval contingent upon required behaviours from their pupils and to decrease their rates of disapproval. Subsidiary aims were that the teachers would be enabled to alter the balance of approval/disapproval given to academic and social behaviours, to increase the rate of approval given to group behaviours, to increase the rate of (...) description given to behaviours approved/disapproved, to use pupils' names more frequently and increase redirections given to behaviours following disapproval. From observations taken before and after training, it was seen that the main aim was achieved, with teachers showing increased levels of approval contingent upon required behaviour and decreased levels of disapproval, these changes being accompanied by increased pupil on?task behaviour. For the subsidiary aims, the data showed an encouraging shift in the balance of the teachers' verbal behaviour towards social and academic behaviours but the results were rather mixed for the other subsidiary aims. (shrink)