We present well-ordering proofs for Martin-Löf's type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in Setzer show that the proof theoretical strength of the type theory is precisely ψΩ1Ω1 + ω, which is slightly more than the strength of Feferman's theory T0, classical set theory KPI and the subsystem of analysis + . The strength of intensional and extensional version, of the version (...) à la Tarski and à la Russell are shown to be the same. (shrink)

We define a type theory MLM, which has proof theoretical strength slightly greater then Rathjen's theory KPM. This is achieved by replacing the universe in Martin-Löf's Type Theory by a new universe V having the property that for every function f, mapping families of sets in V to families of sets in V, there exists a universe inside V closed under f. We show that the proof theoretical strength of MLM is $\geq \psi_{\Omega_1}\Omega_{{\rm M}+\omega}$ . This is slightly greater than (...) $|{\rm KPM}|$ , and shows that V can be considered to be a Mahlo-universe. Together with [Se96a] it follows $|{\rm MLM}|=\psi_{\Omega_1}(\Omega_{{\rm M}+\omega})$. (shrink)

This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories $\widehat{ID}_\alpha and \widehat{ID}_{ the exact proof-theoretic ordinals of these systems are presented.

This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories $\widehat{ID}_\alpha and \widehat{ID}_{<\alpha};$ the exact proof-theoretic ordinals of these systems are presented.

Previous research shows that females use more exclamation marks than males, often to establish rapport. The purpose of the present studies was to test whether people associate texters’ use of exclamation marks with friendliness and femaleness. If this association is due to normative expectations, we hypothesized that females would appear less friendly if they did not use an exclamation mark in texting. In Study 1, participants rated a texter using an exclamation mark to be highly female and highly friendly. The (...) gender results disappeared when friendliness was controlled for. In Study 2, we tested whether friendliness ratings decreased if texters violated gender-associated punctuation. Participants rated a texter with a gendered name on friendliness. Regardless of gender, participants inferred greater friendliness to texters using an exclamation mark. That is, there was no evidence of a cost for violating this gender expectation. We conclude that people predict that a texter using an exclamation mark is likely to be female, but do not penalize females for not using an exclamation mark. (shrink)

Induction–recursion is a powerful definition method in intuitionistic type theory. It extends inductive definitions and allows us to define all standard sets of Martin-Löf type theory as well as a large collection of commonly occurring inductive data structures. It also includes a variety of universes which are constructive analogues of inaccessibles and other large cardinals below the first Mahlo cardinal. In this article we give a new compact formalization of inductive–recursive definitions by modeling them as initial algebras in slice categories. (...) We give generic formation, introduction, elimination, and equality rules generalizing the usual rules of type theory. Moreover, we prove that the elimination and equality rules are equivalent to the principle of the existence of initial algebras for certain endofunctors. We also show the equivalence of the current formulation with the formulation of induction–recursion as a reflection principle given in Dybjer and Setzer 93). Finally, we discuss two type-theoretic analogues of Mahlo cardinals in set theory: an external Mahlo universe which is defined by induction–recursion and captured by our formalization, and an internal Mahlo universe, which goes beyond induction–recursion. We show that the external Mahlo universe, and therefore also the theory of inductive–recursive definitions, have proof-theoretical strength of at least Rathjen's theory KPM. (shrink)

The idea of the genetic unity of all mankind is an integral part of Christian teaching. The purpose of this brief survey is to illustrate its role within the Greek patristic tradition, and then to point to a few examples from modern science which lend support to this ancient idea.

Some recent Christian thinkers have made attempts to harmonize Christianity and science by trying to show a positive correlation between current cosmologyand a literal reading of the account of creation in Genesis. This essay argues that this approach is mistaken since it misunderstands the practices of scienceand hermeneutics. Instead it is argued that Scripture and tradition make only very broad claims about the nature of creation which must be respected when thinking about the universe. Those broad claims are decribed here.

As variants of the Christian tradition have emerged through the centuries they have given rise to distinct versions of Christian metaphysics with divergent cosmological commitments. In the early Church, the Cappodocian fathers constructed a theological framework which focuses on the “personal” nature of reality. The personal nature of reality is central not only to understanding key theological doctrines, such as the Trinity, but also the cosmos itself. This essay explores the Cappodocian conception of the cosmos as personal both in its (...) origin and as a medium for an interpersonal relationship between God and creatures. (shrink)

As variants of the Christian tradition have emerged through the centuries they have given rise to distinct versions of Christian metaphysics with divergent cosmological commitments. In the early Church, the Cappodocian fathers constructed a theological framework which focuses on the “personal” nature of reality. The personal nature of reality is central not only to understanding key theological doctrines, such as the Trinity, but also the cosmos itself. This essay explores the Cappodocian conception of the cosmos as personal both in its (...) origin and as a medium for an interpersonal relationship between God and creatures. (shrink)

Russian Orthodoxy during the twentieth century presented a rich and varied body of thought about the nature of humanity and the human condition. This article surveys the major thinkers within this tradition, beginning with its background in the Slavophile movement and culminating in the work of more recent Orthodox thinkers such as Sergei Bulgakov, Georges Florovsky, Vladimir Lossky, and Alexander Schmemann.

The future of salmon aquaculture depends on the adoption of alternative feed resources in order to reduce the need for fish meal and fish oil. This may include resources such as species from lower trophic levels, by-products and by-catch from fisheries and aquaculture, animal by-products, plants, genetically modified (GM) plants, nutritionally enhanced GM plants and products from microorganisms and GM microorganisms. Here, we report on a deliberative assessment of these alternative feed resources, involving 18 participants from different interest groups within (...) Norwegian salmon aquaculture. The participants defined a broad range of appraisal criteria concerning health and welfare issues, economical issues, environmental issues, and knowledge and social issues. A number of uncertainties, in the form of incomplete knowledge, diverging opinions, and context specific factors were identified when the participants evaluated the alternatives. Our findings support the need for more research on the suitability of alternative feed resources for farmed salmon. Additionally, the study underlines the importance of facilitating deliberative assessments in order to map the plurality of perspectives and explore qualitative aspects of uncertainty. Such initiatives improve the information base upon which decisions on future feed resources for farmed salmon are made. (shrink)