Pierluigi Minari

The name “Becker’s rule” was coined by C. West Churchman in 1938 to denote the modal inference rule according to which the theoremhood of a strict implication of the form may be inferred from the theoremhood of a strict implication of the form. According to Churchman, such a rule was introduced explicitly by Oskar Becker in his On the Logic of Modalities (1930)—hence the name he gave to it, which is still current in the literature. The aim of this note is to point out that “Becker’s rule” is not at all Becker’s rule (a fact which has remained unnoticed until now, as far as we know) by explaining where and how Churchman misunderstood what Becker intended.

We aim at clarifying to what extent the work of the English mathematician George Boole on the algebra of logic is taken into consideration and discussed in the work of early Husserl, focusing in particular on Husserl’s lecture “Über die neueren Forschungen zur deduktiven Logik” of 1895, in which an entire section is devoted to Boole. We confront Husserl’s representation of the problem-solving processes with the analysis of “symbolic reasoning” proposed by George Boole in the Laws of Thought and try to show how and why Husserl, while praising Boole’s calculus, strongly criticizes his attempt at a philosophical clarification and justification of it.

We aim at clarifying to what extent the work of the German mathematician Ernst Schröder on the algebra of logic is taken into consideration and rehashed in the work of the early Husserl, focusing on Husserl’s 1891 Review of the first volume of Schröder’s monumental Vorlesungen über die Algebra der Logik and on Husserl’s text Der Folgerungskalkül und die Inhaltslogik written in the same year. We will try to show how and why Husserl, while praising Schröder’s calculus, strongly criticizes Schröder’s attempt at a philosophical clarification and justification of it.

The IOth International Congress of Logic, Methodology and Philosophy of Science, which took place in Florence in August 1995, offered a vivid and comprehensive picture of the present state of research in all directions of Logic and Philosophy of Science. The final program counted 51 invited lectures and around 700 contributed papers, distributed in 15 sections. Following the tradition of previous LMPS-meetings, some authors, whose papers aroused particular interest, were invited to submit their works for publication in a collection of selected contributed papers. Due to the large number of interesting contributions, it was decided to split the collection into two distinct volumes: one covering the areas of Logic, Foundations of Mathematics and Computer Science, the other focusing on the general Philosophy of Science and the Foundations of Physics. As a leading choice criterion for the present volume, we tried to combine papers containing relevant technical results in pure and applied logic with papers devoted to conceptual analyses, deeply rooted in advanced present-day research. After all, we believe this is part of the genuine spirit underlying the whole enterprise of LMPS studies.

The paper surveys ideas, results and applications of a novel proof-theoretical approach to equational theories of untyped operations (including combinatory logic CL and Lambda-calculus) we developed in the last 15 years. The approach is based on the introduction and the proof-theoretical investigation of “analytic” proof systems for such theories. Analyticity is due to a main result of transitivity elimination, yielding as a consequence a non trivial streamlining of the proof-theory of the corresponding theories and a number of applications. Among these, a positive solution to an open problem concerning the theory of combinatory strong reduction which was raised about 60 years ago by H.B. Curry.

For each ordinal $\alpha > 0, L(\alpha)$ is the intermediate predicate logic characterized by the class of all Kripke frames with the poset α and with constant domain. This paper will be devoted to a study of logics of the form L(α). It will be shown that for each uncountable ordinal of the form α + η with a finite or a countable $\eta (> 0)$ , there exists a countable ordinal of the form β + η such that L(α + η) = L(β + η). On the other hand, such a reduction of ordinals to countable ones is impossible for a logic L(α) if α is an uncountable regular ordinal. Moreover, it will be proved that the mapping L is injective if it is restricted to ordinals less than ω ω , i.e. α ≠ β implies L(α) ≠ L(β) for each ordinal $\alpha,\beta

It has often been remarked that the metatheory of strong reduction $\succ$ , the combinatory analogue of βη-reduction ${\twoheadrightarrow_{\beta\eta}}$ in λ-calculus, is rather complicated. In particular, although the confluence of $\succ$ is an easy consequence of ${\twoheadrightarrow_{\beta\eta}}$ being confluent, no direct proof of this fact is known. Curry and Hindley’s problem, dating back to 1958, asks for a self-contained proof of the confluence of $\succ$ , one which makes no detour through λ-calculus. We answer positively to this question, by extending and exploiting the technique of transitivity elimination for ‘analytic’ combinatory proof systems, which has been introduced in previous papers of ours. Indeed, a very short proof of the confluence of $\succ$ immediately follows from the main result of the present paper, namely that a certain analytic proof system G e [ $\mathbb {C}$ ] , which is equivalent to the standard proof system CL ext of Combinatory Logic with extensionality, admits effective transitivity elimination. In turn, the proof of transitivity elimination—which, by the way, we are able to provide not only for G e [ $\mathbb {C}$ ] but also, in full generality, for arbitrary analytic combinatory systems with extensionality—employs purely proof-theoretical techniques, and is entirely contained within the theory of combinators

We introduce a certain extension of -calculus, and show that it has the Church-Rosser property. The associated open-term extensional combinatory algebra is used as a basis to construct models for theories of Explict Mathematics (formulated in the language of "types and names") with positive stratified comprehension. In such models, types are interpreted as collections of solutions (of terms) w.r. to a set of numerals. Exploiting extensionality, we prove some consistency results for special ontological axioms which are refutable under elementary comprehension.

It is well known that Lukasiewicz’s three-valued-logic L3 admits – unlike classical logic – the definition of two non trivial, truth-functional modal operators and ∆. We address the question of finding a convenient syntactic characterization of the “modal content” of L3. To this aim, we consider Wajsberg’s axiomatization of L3 and prove its equivalence with a modal calculus W_ which, essentially, includes: the BCK+double negation schemas, the characteristic modal schemas of S5 , full contraction for boxed formulas and the “partial collapse” schema α → . As applications, we obtain a simple and natural completeness proof à la Lindenbaum for W, as well as a considerable simplification of Wajsberg’s original, ingenious completeness proof

The paper settles an open question concerning Negri-style labeled sequent calculi for modal logics and also, indirectly, other proof systems which make (more or less) explicit use of semantic parameters in the syntax and are thus subsumed by labeled calculi, like Brünnler’s deep sequent calculi, Poggiolesi’s tree-hypersequent calculi and Fitting’s prefixed tableau systems. Specifically, the main result we prove (through a semantic argument) is that labeled calculi for the modal logics K and D remain complete w.r.t. valid sequents whose relational part encodes a tree-like structure, when the unique rule which contains an harmful implicit contraction—by which the condition that the premises be less complex than the conclusion is violated—is modified into a contraction-free one respecting the latter condition, thus making the proof-search space finite.

We introduce, in a general setting, an ‘‘analytic’’ version of standard equational calculi of combinatory logic. Analyticity lies on the one side in the fact that these calculi are characterized by the presence of combinatory introduction rules in place of combinatory axioms, and on the other side in that the transitivity rule proves to be eliminable. Apart from consistency, which follows immediately, we discuss other almost direct consequences of analyticity and the main transitivity elimination theorem; in particular the Church−Rosser and the leftmostreduction theorems for the associated notions of reduction. The last two sections deal with analytic combinatory calculi with the extensionality rule added. Here, as far as the elimination of transitivity is concerned, we have only partial results, which unfortunately do not cover, at present, full CL + Ext. Yet, they are sufficient to prove the decidability of weaker combinatory calculi with extensionality, including e.g. BCK + Ext

We introduce new proof systems G[β] and G ext[β], which are equivalent to the standard equational calculi of λβ- and λβη- conversion, and which may be qualified as ‘analytic’ because it is possible to establish, by purely proof-theoretical methods, that in both of them the transitivity rule admits effective elimination. This key feature, besides its intrinsic conceptual significance, turns out to provide a common logical background to new and comparatively simple demonstrations—rooted in nice proof-theoretical properties of transitivity-free derivations—of a number of well-known and central results concerning β- and βη-reduction. The latter include the Church–Rosser theorem for both reductions, the Standardization theorem for β- reduction, as well as the Normalization (Leftmost reduction) theorem and the Postponement of η-reduction theorem for βη-reduction