By formalizing Berry's paradox, Vopěnka, Chaitin, Boolos and others proved the incompleteness theorems without using the diagonal argument. In this paper, we shall examine these proofs closely and show their relationships. Firstly, we shall show that we can use the diagonal argument for proofs of the incompleteness theorems based on Berry's paradox. Then, we shall show that an extension of Boolos' proof can be considered as a special case of Chaitin's proof by defining a suitable Kolmogorov complexity. We shall show (...) also that Vopěnka's proof can be reformulated in arithmetic by using the arithmetized completeness theorem. (shrink)
Within a weak subsystem of second-order arithmetic , that is -conservative over , we reformulate Kreisel's proof of the Second Incompleteness Theorem and Boolos' proof of the First Incompleteness Theorem.
We present a version of Herbelin’s image-calculus in the call-by-name setting to study the precise correspondence between normalization and cut-elimination in classical logic. Our translation of λμ-terms into a set of terms in the calculus does not involve any administrative redexes, in particular η-expansion on μ-abstraction. The isomorphism preserves β,μ-reduction, which is simulated by a local-step cut-elimination procedure in the typed case, where the reduction system strictly follows the “ cut=redex” paradigm. We show that the underlying untyped calculus is confluent (...) and enjoys the PSN property for the isomorphic image of λμ-calculus, which in turn yields a confluent and strongly normalizing local-step cut-elimination procedure for classical logic. (shrink)
We define a liar-type paradox as a consistent proposition in propositional modal logic which is obtained by attaching boxes to several subformulas of an inconsistent proposition in classical propositional logic, and show several famous paradoxes are liar-type. Then we show that we can generate a liar-type paradox from any inconsistent proposition in classical propositional logic and that undecidable sentences in arithmetic can be obtained from the existence of a liar-type paradox. We extend these results to predicate logic and discuss Yablo’s (...) Paradox in this framework. Furthermore, we define explicit and implicit self-reference in paradoxes in the incompleteness phenomena. (shrink)
On applique ici la méthode de l’analyse de réseau pour comprendre les temporalités de la construction de l’imprimerie, comme activité économique associant des hommes de lettres et des acteurs économiques. À partir des informations contenues dans l’Incunabula Short Title Catalogue, deux types de réseaux sont construits pour les éditions imprimées à Venise entre 1469 et 1500. Le premier permet d’observer le vivier des noms d’auteurs présents dans les éditions. Le second permet d’aller plus loin dans les notions de centralité et (...) d’autorité dans le réseau. Les presses vénitiennes se sont construites par l’utilisation réciproque des ateliers et des grands noms lettrés, dont le prestige légitimait les grandes entreprises typographiques. Avec le développement de l’imprimerie, les noms d’auteurs contemporains se font plus nombreux. Pour l’ensemble des lettrés impliqués dans l’imprimerie, cela se traduit par un rapport de force en leur défaveur. Les imprimeurs organisent eux-mêmes leurs collaborations en choisissant dans un vivier qui ne fait que s’accroître. Le prestige des auteurs est plus diffus et se nourrit de l’association de plusieurs noms dans une édition. Mais certains ont su particulièrement bien en jouer, comme le montre l’exemple d’Antonio Mancinelli. Ces réseaux éditoriaux, analysés dans leur épaisseur chronologique, permettent ainsi de redonner une vraie dimension temporelle à la construction d’une nouvelle industrie culturelle. (shrink)
We introduce a dual-context style sequent calculus which is complete with respectto Kripke semantics where implication is interpreted as strict implication in the modal logic K. The cut-elimination theorem for this calculus is proved by a variant of Gentzen's method.
We consider a set-theoretic version of mereology based on the inclusion relation ⊆ and analyze how well it might serve as a foundation of mathematics. After establishing the non-definability of ∈ from ⊆, we identify the natural axioms for ⊆-based mereology, which constitute a finitely axiomatizable, complete, decidable theory. Ultimately, for these reasons, we conclude that this form of set-theoretic mereology cannot by itself serve as a foundation of mathematics. Meanwhile, augmented forms of set-theoretic mereology, such as that obtained by (...) adding the singleton operator, are foundationally robust. (shrink)
Bear bile has long been used in the Asian traditional pharmacopoeia. Bear farming first started in China ~30 years ago in terms of reducing the number of poached bears and ensuring the supply of bear bile. Approximately 13,000 bears are today captivated on Asia’s bear farms: their teeth are broken and the claws are also pulled out for the sake of human safety; the bears are imprisoned in squeeze cages for years; and a catheter is daily inserted into a bear’s (...) gall bladder or a tube is implanted inside its body in order to collect the dripped bile—captive bears moan in severe pain whenever the bile is extracted. When the bears cannot produce sufficient bile, they are often left to die of starvation. It must be impossible to justify the bile extraction from living bears because (1) medicinal/herbal alternatives are similar to bear bile; (2) there is no evidence to suggest that bear farming has any beneficial effects on wild bear populations; and (3) ethical problems lie not only in the painful bile extraction but also the whole lifecycle of captive bears. In conclusion, human welfare (health care) based on traditional medicine is upheld by sacrificing bear welfare. Since a trial calculation suggests that it is economically unfeasible to keep a proper balance between bear welfare and the traditional pharmacopeia, the cultivation of herbal alternatives seems to be a possible solution to phase out bear faming and maintain the practice of traditional medicine in Asia. (shrink)
We introduce a Gentzen style formulation of Basic Propositional Calculus(BPC), the logic that is interpreted in Kripke models similarly tointuitionistic logic except that the accessibility relation of eachmodel is not necessarily reflexive. The formulation is presented as adual-context style system, in which the left hand side of a sequent isdivided into two parts. Giving an interpretation of the sequents inKripke models, we show the soundness and completeness of the system withrespect to the class of Kripke models. The cut-elimination theorem isproved (...) in a syntactic way by modifying Gentzen's method. Thisdual-context style system exemplifies the effectiveness of dual-contextformulation in formalizing various non-classical logics. (shrink)
Since the beginning of Christianity, the understanding of Christ’s sonship has played an essential role in soteriology. According to the Church Fathers and to the medieval theologians, the human person can become a son of God by the grace of adoption through the sonship of Christ. However, the German Dominican, Meister Eckhart , uses the theological concept 'the Only-begotten Son', which stands for the divine sonship of Christ himself, to describe the human condition and demonstrates the equality between Christ and (...) the human person. This quite unusual understanding drew the attention of the Church authorities in his time, because it could be associated with the doctrines of heretics in the late Middle Ages who insisted on the perfect identity between Christ and the human person. In the end, Eckhart’s teaching including the understanding of the sonship was condemned by the papal bull In agro dominico together with his other teachings. The present article attempts to reconstruct this one of the most challenging teachings of Eckhart by the analysis of his text, mainly the text of his German homilies, and to examine how he understands the relationship between Christ and the human person regarding the sonship. (shrink)
This paper introduces sequent systems for Visser's two propositional logics: Basic Propositional Logic (BPL) and Formal Propositional Logic (FPL). It is shown through semantical completeness that the cut rule is admissible in each system. The relationships with Hilbert-style axiomatizations and with other sequent formulations are discussed. The cut-elimination theorems are also demonstrated by syntactical methods.