This paper considers two reasons that might support Russell’s choice of a ramified-type theory over a simple-type theory. The first reason is the existence of purported paradoxes that can be formulated in any simple-type language, including an argument that Russell considered in 1903. These arguments depend on certain converse-compositional principles. When we take account of Russell’s doctrine that a propositional function is not a constituent of its values, these principles turn out to be too implausible to make these arguments troubling. (...) The second reason is conditional on a substitutional interpretation of quantification over types other than that of individuals. This reason stands up to investigation: a simple-type language will not sustain such an interpretation, but a ramified-type language will. And there is evidence that Russell was tacitly inclined towards such an interpretation. A strong construal of that interpretation opens a way to make sense of Russell’s simultaneous repudiation of propositions and his willingness to quantify over them. But that way runs into trouble with Russell’s commitment to the finitude of human understanding. (shrink)

Øystein Linnebo has recently shown that the existence of successors cannot be proven in predicative Frege arithmetic, using Frege's definitions of arithmetical notions. By contrast, it is shown here that the existence of successor can be proven in ramified predicative Frege arithmetic.

The use of Extended Logics to replace ordinary second order definability in Kleene’s Ramified Analytical Hierarchy is investigated. This mirrors a similar investigation of Kennedy, Magidor and Väänänen [11] where Gödel’s universe L of constructible sets is subjected to similar variance. Enhancing second order definability allows models to be defined which may or may not coincide with the original Kleene hierarchy in domain. Extending the logic with game quantifiers, and assuming strong axioms of infinity, we obtain minimal correct models of (...) analysis. A wide spectrum of models can be so generated from abstract definability notions: one may take an abstract Spector Class and extract an extended logic for it. The resultant structure is then a minimal model of the given kind of definability. (shrink)

Øystein Linnebo has recently shown that the existence of successors cannot be proven in predicative Frege arithmetic, using Frege’s definitions of arithmetical notions. By contrast, it is shown here that the existence of successor can be proven in ramified predicative Frege arithmetic.

The Russell–Myhill theorem threatens a familiar structured conception of propositions according to which two sentences express the same proposition only if they share the same syntactic structure and their corresponding syntactic constituents share the same semantic value. Given the role of the principle of universal instantiation in the derivation of the theorem in simple type theory, one may hope to rehabilitate the core of the structured view of propositions in ramified type theory, where the principle is systematically restricted. We suggest (...) otherwise. The ramified core of the structured theory of propositions remains inconsistent in ramified type theory augmented with axioms of reducibility. This is significant because reducibility has been thought to be perfectly consistent with the ramified approach to the intensional antinomies. Nor is the addition of reducibility to ramified type theory sufficient to restore other intensional puzzles such as Prior’s paradox or Kripke’s puzzle about time and thought. (shrink)

“Ramified natural theology” can be defined as natural theology employed in the service not of general theism but of some particular theistic tradition. Examples of ramified natural theology in the Christian tradition include Anselm’s philosophical arguments for the incarnation, Pascal’s use of biblical prophecy to defend the deity of Christ, the use of contemporary miracle reports to substantiate the efficacy of prayer to Christ, and so forth. In the Christian context we normally think of ramified natural theology being used to (...) argue in favor of the claims of so-called mere Christianity over and against those of other religions or metaphysical naturalism. But historically they have also been prominent in debates between Christian denominations. It is this latter usage that I wish to explore here. I argue that the use of ramified natural theology in interdenominational debate is both unavoidable and entirely proper. I also ask which denomination, if any, are most likely to benefit from this usage. (shrink)

This book offers a rationale for a new 'ramified natural theology' that is in dialogue with both science and historical-critical study of the Bible. Traditionally, knowledge of God has been seen to come from two sources, nature and revelation. However, a rigid separation between these sources cannot be maintained, since what purports to be revelation cannot be accepted without qualification: rational argument is needed to infer both the existence of God from nature and the particular truth claims of the Christian (...) faith from the Bible. Hence the distinction between 'bare natural theology' and 'ramified natural theology.' The book begins with bare natural theology as background to its main focus on ramified natural theology. Bayesian confirmation theory is utilised to evaluate competing hypotheses in both cases, in a similar manner to that by which competing hypotheses in science can be evaluated on the basis of empirical data. In this way a case is built up for the rationality of a Christian theist worldview. Addressing issues of science, theology and revelation in a new framework, this book will be of keen interest to scholars working in Religion and Science, Natural Theology, Philosophy of Religion, Biblical Studies, Systematic Theology, and Science and Culture. (shrink)

The notion of “ramifiability” , usually applied to cardinals, can be extended to directed sets and is put in relation here with familiar “large cardinal” properties.

In this paper I examine the nature of Russell's ramified type theory resolution of paradoxes. In particular, I consider the effect of construing the types in Church's cumulative sense, that is, the range of a variable of a given type includes the range of every variable of directly lower type. Contrary to what seems to be generally assumed, I show that the decision to make the levels cumulative and allow this to be reflected in the semantics is not neutral with (...) respect to the solution of the paradoxes. I introduce a distinction between syntactical and semantical cumulativeness. It turns out that noncumulative type theories (in either sense) are equally capable of dealing with the paradoxes. Furthermore, whether cumulativeness is appropriate appears to be context dependent. (shrink)

Ramified natural theology concerns arguments for or against distinctively Christian theism, using only our natural endowments of reason and sense perception, without appealing to the authority of divine revelation. Before ramified natural theology’s arguments and evidence can be evaluated properly, first its methodology must be clear, impartial, settled, and effective. This paper defends three theses regarding methodology. First, ramified natural theology and science share the same core methodology, namely, the PEL model, specifying that conclusions about the world require three resources: (...) Presuppositions, Evidence, and Logic. Second, ramified natural theology, especially when implemented with the PEL model, provides a suitable methodology for investigating miracles. Third, despite methodological differences, there is a fruitful synergy between natural and revealed theology. Ramified natural theology has its own intrinsic importance, and yet its full value emerges from its synergy with revealed theology. (shrink)

This paper uses an atomistic ontology of universals, individuals, and facts to provide a semantics for ramified type theory. It is shown that with some natural constraints on the sort of universals and facts admitted into a model, the axiom of reducibility is made valid.

We consider the impact of negative natural theology on the prospects of Christian ramified natural theology with reference to Richard Swinburne’s argument for the Incarnation and Resurrection. We argue that Swinburne’s pivotal claim—that God would not allow deceptive evidence to exist for the Incarnation and Resurrection—is refuted by key evidence from negative natural theology. We argue, further, that Swinburne’s argument omits dominating items of evidence of negative natural theology which seem to critically weaken the probability of the Incarnation and Resurrection. (...) Negative natural theology thus serves as a formidable obstacle to Christian ramified natural theology. (shrink)

The tree-property and its variants make sense also for directed sets and even for partially ordered sets. A combinatoria approach is developed here, with characterizations and criteria involving adequate families of special substructures of directed sets. These substructures form a natural hierarchy that is also investigated.

Traditionally, knowledge of God has been considered to arise from two sources: our innate human capacities of reason and intuition, and special divine revelation. The former is the subject of natural theology and the latter of systematic or dogmatic theology. In this article I argue that this rigid distinction should be dispensed with, both because of the need to respond to the criticisms of atheists that religious beliefs are not grounded on evidence, and because different religions make different and contradictory (...) claims to truth. Thus, what is purported to be revelation needs to be evaluated on commonly accepted criteria of rationality. Such criteria will exclude both a priori religious assumptions, so as to avoid circularity, and a priori atheistic assumptions, so as to avoid excluding what is being investigated by fiat. The project of evaluating specific Christian claims in this way, such as the resurrection of Jesus, is what has been dubbed “ramified natural theology.”. (shrink)

The paper first formalizes the ramified type theory as (informally) described in the Principia Mathematica [32]. This formalization is close to the ideas of the Principia, but also meets contemporary requirements on formality and accuracy, and therefore is a new supply to the known literature on the Principia (like [25], [19], [6] and [7]).As an alternative, notions from the ramified type theory are expressed in a lambda calculus style. This situates the type system of Russell and Whitehead in a modern (...) setting. Both formalizations are inspired by current developments in research on type theory and typed lambda calculus; see [3]. (shrink)

It is well known that Russell abandoned his multiple-relation theory of judgment, which provided the philosophical foundations for _PM_'s ramified type-theory, in response to criticisms by Wittgenstein. Their exact nature has remained obscure. An influential interpretation, put forth by Sommerville and Griffin, is that Wittgenstein showed that the theory must appeal to the very hierarchy it is intended to generate and thus collapses into circularity. I argue that this rests on a mistaken interpretation of type-theory and suggest an alternative one (...) to explain Russell's reaction. (shrink)

In this article we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell’s reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematical analysis in the style of Bishop. We present a ramified type theory suitable for this purpose. One may regard the results of this (...) article as an alternative solution to the problem of the proliferation of levels of real numbers in Russell’s theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here also suggests that there is a natural associated notion of predicative elementary topos. (shrink)

It is already known that Fitch’s knowability paradox can be solved by typing knowledge within ramified theory of types. One of the aims of this paper is to provide a greater defence of the approach against recently raised criticism. My second goal is to make a sufficient support for an assumption which is needed for this particular application of typing knowledge but which is not inherent to ramified theory of types as such.

In Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have a strong correlation with predicativity, predicative (...) logic still plays an influential role in Computer Science.An important example is the proof checker Nuprl, which is basedon Martin-Löf''s Type Theory which uses type universes. Those type universes,and also degrees of expressions in AUTOMATH, are closely related toorders. In this paper, we show that orders have not disappeared from modern logic and computer science, rather, orders play a crucial role in understanding the hierarchy of modern systems. In order to achieve our goal, we concentrate on a subsystem of Nuprl.The novelty of our paper lies in: (1) a modest revival of Russell's orders, (2) the placing of the historical system RTT underlying the famous Principia Mathematica in a context with a modern system of computer mathematics (Nuprl) and modern type theories (Martin-Löf''s type theory and PTSs), and (3) the presentation of acomplex type system (Nuprl) as a simple and compact PTS. (shrink)

Taking seriously Richard Swinburne’s distinction between “bare” natural theology and “ramified” natural theology, this article contends that the moral argument for God’s existence helps to flesh out distinctively moral aspects of God’s character, reflective of and resonant with a specifically Anselmian concept of God. This article argues that the project of ramified natural theology not only helps distinguish the Christian conception from other theisms, it also helps to clarify important distinctions made among Christians concerning their understanding of God, resulting in (...) an argumentative strategy we call “doubly ramified natural theology.”. (shrink)

This dissertation constitutes an inquiry into the formal aspects of a particular form of conceptual intentional realism: Holistic Realist Ramified Conceptualism. Several axiomatic systems, which have this theory as their philosophical background are developed and/or studied from a syntactical and semantical point of view. ;Among systems studied are Cocchiarella's RRC$\sbsp{\lambda}{\*}$ and HRRC$\sbsp{\lambda}{\*}$. A set theoretical semantics for these systems is developed. Also, completeness theorems with respect to certain extensions of RRC$\sbsp{\lambda}{\*}$ and HRRC$\sbsp{\lambda}{\*}$ and certain notions of validity related to that (...) semantics are proved. A relative consistency proof of RRC$\sbsp{\lambda}{\*}$, HRRC$\sbsp{\lambda}{\*}$ and other systems is given. ;An axiomatic system for identity free realist ramified conceptualism involving indiscernibility relative to constructive concepts is developed. A set theoretical semantics for this system is constructed. A completeness theorem with respect to certain extensions of the identity-free system and a notion of validity related to that semantics is proved. ;Epistemic considerations are brought into this inquiry by introducing an epistemic operator into the logical syntax. Such an operator corresponds intuitively to the idea of constructive knowability. A philosophical discussion of this idea is presented and on the basis of this discussion an epistemic logical theory is formulated. It is shown that this system has HRRC$\sbsp{\lambda}{\*}$ as a proper subsystem. On the basis of the epistemic logical theory, an axiomatic system is introduced from which Peano's arithmetic is deduced. In this way, it is shown that arithmetic can be developed axiomatically on conceptualist foundations. (shrink)

ABSTRACT We characterize those binary ramified frames for which propositional modal logic is as expressive as the corresponding first-order logic.