Developing a suggestion by Russell, Prawitz showed how the usual natural deduction inference rules for disjunction, conjunction and absurdity can be derived using those for implication and the second order quantifier in propositional intuitionistic second order logic NI\. It is however well known that the translation does not preserve the relations of identity among derivations induced by the permutative conversions and immediate expansions for the definable connectives, at least when the equational theory of NI\ is assumed to consist only of (...) \- and \-equations. On the basis of the categorial interpretation of NI\, we introduce a new class of equations expressing what in categorial terms is a naturality condition satisfied by the transformations interpreting NI\-derivations. We show that the Russell–Prawitz translation does preserve identity of proof with respect to the enriched system by highlighting the fact that naturality corresponds to a generalized permutation principle. Finally we sketch how these results could be used to investigate the properties of connectives definable in the framework of higher-level rules. (shrink)

In a previous paper we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative translation into System F. Our key idea was to introduce an extended equational theory for System F codifying at a syntactic level some properties found in parametric models of polymorphic type theory. A different approach to extract proof-theoretic properties of natural deduction derivations was proposed in a recent series of papers on the basis of an embedding of intuitionistic propositional logic into a (...) predicative fragment of System F, called atomic System F. In this paper we show that this approach finds a general explanation within our equational study of second-order natural deduction, and a clear semantic justification in terms of parametricity. (shrink)

The question of xing has received much attention in the revival of Neo-Confucian philosophy (called Contemporary Neo-Confucianism) in present-day Taiwan, Hong Kong, and China and among scholars of Chinese philosophy in the United States. It also has much to do with a critical consciousness of both the difference and the affinity between the Chinese philosophy of man and morality and the contemporary Western philosophy of human existence and moral virtues. The study of this has great meaning for the development of (...) a global onto-ethics and an onto-ethics of the future of humankind. (shrink)

We have become estranged from the cosmic movements, according to Bataille. We are confined by the error linked to the representation of ‘the stationary earth’. We have negated the immersive immanence of the whole and made nature into a fixed world of tools and things. How then do we recognise ourselves as part of the ‘rapture of the heavens’? Bataille urges us to consider life as a solar phenomenon, the free play of solar energy on the earth. This paper argues (...) how Bataille’s cosmic vision anticipates both planetary and ecological thinking. This entails a base materialism of difference based on a radical Nietzschean and Heraclitean theory of becoming and flux. This thought is developed along Bataillean concepts such as the movement of the whole, the labyrinthine, and compound beings, ipseity, as well as the concept of a communifying movement. This materialism paired with Vladimir Vernadsky’s biosphere lays the foundation for the laws of the general economy, which also constitutes an economy inclusive of a general ecology: a tragic vision of Gaia and Dionysos. Finally, poetry is considered, as a way we might reconnect with the universe and stimulate ecological imagination. (shrink)