 In the twenties and in the early thirties, the orthodox view of logic among mathematical logicians was more or less type- or set theoretic. However, there was an effort to develop new grand logics as substitutes for the logic of Principia Mathematica. These frameworks arose both as attempts to recover the simplicity of the type-free approach, as derived from the so-called naive comprehension principle, as well as in order to satisfy metamathematical needs, such as the clarification of fundamental concepts underlying the notions of “formal system,” “formalism,” “rule,” etc. In particular, Church and Curry proposed theories which (i) assume as primitive the notions of self-applicable function-in-intension (operation), and (ii) stress the very mechanism of definition/combination of concepts. If one looks closely at the development of these systems, one can see that paradoxical constructions have become essential tools for defining objects and proving non-trivial logical mathematical facts. Following ideas of Schönfinkel and aiming at a mathematical analysis of the substitution process, Curry’s 1930 thesis introduced a formal language based on basic general operators, the so-called combinators \(B\) (composition), \(C\) (permutation), \(W\) (duplication), \(K\) (cancellation), \(Q\) (equality), and logical constants like the universal quantifier and implication. Expressions are then inductively generated by application from constants; intuitively, a term \(M\) stands for a function, and the applicative term \(MN\) (juxtaposition plays the role of application and parentheses are associated to the left) denotes the value of the term obtained by replacing the first variable of \(M\) with \(N\). Self-application \(MM\) is admissible and this feature tells us that the objects of combinatory logic cannot be simply interpreted as set-theoretic functions. The formal system consists of standard equations on combinators (e.g, \(Bxyz=x(yz), Wxy=xyy\), or \(Cxyz=xzy)\), rules for equality and the logical constants; its main goal is to derive equalities \(X=Y\) and to make assertions of the form \(\vdash X (= X\) is provable). Combinatory logic is a theory which analyzes the modes of combinations of formal objects, substitution, and the notions of proposition and propositional function (see the entry on  combinatory logic  for a proper introduction to variants of the formalism and an overview of the properties of related calculi). For Curry, the root of the paradoxes is found in assuming that combinations of concepts are always propositions. The notion of proposition becomes a theoretical concept, which is decided by the theory. Types are not assigned to the expressions of the formal system at the outset, but are instead inferred by means of the system itself, which has a dual nature: it can derive identities, but also truths. In particular, if \(\vdash MN\) is derived, this can be read as “\(N\) is of type \(M\)” or “\(N\) is an element of \(M\)”. These ideas foreshadow fundamental developments such as the so-called formulas-as types interpretation (see Howard 1968).