Gentzen’s approach by transfinite induction and that of intuitionist Heyting arithmetic to completeness and the self-foundation of mathematics are compared and opposed to the Gödel incompleteness results as to Peano arithmetic. Quantum mechanics involves infinity by Hilbert space, but it is finitist as any experimental science. The absence of hidden variables in it interpretable as its completeness should resurrect Hilbert’s finitism at the cost of relevant modification of the latter already hinted by intuitionism and Gentzen’s approaches for completeness. (...) This paper investigates both conditions and philosophical background necessary for that modification. The main conclusion is that the concept of infinity as underlying contemporary mathematics cannot be reduced to a single Peano arithmetic, but to at least two ones independent of each other. Intuitionism, quantum mechanics, and Gentzen’s approaches to completeness an even Hilbert’s finitism can be unified from that viewpoint. Mathematics may found itself by a way of finitism complemented by choice. The concept of information as the quantity of choices underlies that viewpoint. Quantum mechanics interpretable in terms of information and quantum information is inseparable from mathematics and its foundation. (shrink)

In their paper Nothing but the Truth Andreas Pietz and Umberto Rivieccio present Exactly True Logic, an interesting variation upon the four-valued logic for first-degree entailment FDE that was given by Belnap and Dunn in the 1970s. Pietz & Rivieccio provide this logic with a Hilbert-style axiomatisation and write that finding a nice sequent calculus for the logic will presumably not be easy. But a sequent calculus can be given and in this paper we will show that a calculus for (...) the Belnap-Dunn logic we have defined earlier can in fact be reused for the purpose of characterising ETL, provided a small alteration is made—initial assignments of signs to the sentences of a sequent to be proved must be different from those used for characterising FDE. While Pietz & Rivieccio define ETL on the language of classical propositional logic we also study its consequence relation on an extension of this language that is functionally complete for the underlying four truth values. On this extension the calculus gets a multiple-tree character—two proof trees may be needed to establish one proof. (shrink)

Gaisi Takeuti (1926–2017) is one of the most distinguished logicians in proof theory after Hilbert and Gentzen. He extensively extended Hilbert's program in the sense that he formulated Gentzen's sequent calculus, conjectured that cut-elimination holds for it (Takeuti's conjecture), and obtained several stunning results in the 1950–60s towards the solution of his conjecture. Though he has been known chiefly as a great mathematician, he wrote many papers in English and Japanese where he expressed his philosophical thoughts. In (...) particular, he used several keywords such as "active intuition" and "self-reflection" from Nishida's philosophy. In this paper, we aim to describe a general outline of our project to investigate Takeuti's philosophy of mathematics. In particular, after reviewing Takeuti's proof-theoretic results briefly, we describe some key elements in Takeuti's texts. By explaining these texts, we point out the connection between Takeuti's proof theory and Nishida's philosophy and explain the future goals of our project. (shrink)

Chapter 1 constitutes an introduction to Gentzen calculi from two perspectives, logical and philosophical. It introduces the notion of generalisations of Gentzen sequent calculus and the discussion on properties that characterize good inferential systems. Among the variety of Gentzen-style sequent calculi, I divide them in two groups: syntactic and semantic generalisations. In the context of such a discussion, the inferentialist philosophy of the meaning of logical constants is introduced, and some potential objections – mainly concerning the choice (...) of working with semantic generalizations – are addressed. Finally, I’ll introduce the case studies that I’ll be dealing with in part II. Chapter 2 is concerned with the origins and development of Jaśkowski’s discussive logic. The main idea of this chapter is to systematize the various stages of the development of discussive logic related researches from two different angles, i.e., its connections to modal logics and its proof theory, by highlighting virtues and vices. Chapter 3 focuses on the Gentzen-style proof theory of discussive logic, by providing a characterization of it in terms of labelled sequent calculi. Chapter 4 deals with the Gentzen-style proof theory of relevant logics, again by employing the methodology of labelled sequent calculi. This time, instead of working with a single logic, I’ll deal with a whole family of them. More precisely, I’ll study in terms of proof systems those relevant logics that can be characterised, at the semantic level, by reduced Routley-Meyer models, i.e., relational structures with a ternary relation between states and a unique base element. Chapter 5 investigates the proof theory of a modal expansion of intuitionistic propositional logic obtained by adding an ‘actuality’ operator to the connectives. This logic was introduced also using Gentzen sequents. Unfortunately, the original proof system is not cut-free. This chapter shows how to solve this problem by moving to hypersequents. Chapter 6 concludes the investigations and discusses the future of the research presented throughout the dissertation. (shrink)

This paper contends that Stoic logic (i.e. Stoic analysis) deserves more attention from contemporary logicians. It sets out how, compared with contemporary propositional calculi, Stoic analysis is closest to methods of backward proof search for Gentzen-inspired substructural sequent logics, as they have been developed in logic programming and structural proof theory, and produces its proof search calculus in tree form. It shows how multiple similarities to Gentzen sequent systems combine with intriguing dissimilarities that may enrich (...) contemporary discussion. Much of Stoic logic appears surprisingly modern: a recursively formulated syntax with some truth-functional propositional operators; analogues to cut rules, axiom schemata and Gentzen’s negation-introduction rules; an implicit variable-sharing principle and deliberate rejection of Thinning and avoidance of paradoxes of implication. These latter features mark the system out as a relevance logic, where the absence of duals for its left and right introduction rules puts it in the vicinity of McCall’s connexive logic. Methodologically, the choice of meticulously formulated meta-logical rules in lieu of axiom and inference schemata absorbs some structural rules and results in an economical, precise and elegant system that values decidability over completeness. (shrink)

In this paper we introduce a Gentzen calculus for (a functionally complete variant of) Belnap's logic in which establishing the provability of a sequent in general requires \emph{two} proof trees, one establishing that whenever all premises are true some conclusion is true and one that guarantees the falsity of at least one premise if all conclusions are false. The calculus can also be put to use in proving that one statement \emph{necessarily approximates} another, where necessary approximation is a (...) natural dual of entailment. The calculus, and its tableau variant, not only capture the classical connectives, but also the `information' connectives of four-valued Belnap logics. This answers a question by Avron. (shrink)

As the 19th century drew to a close, logicians formalized an ideal notion of proof. They were driven by nothing other than an abiding interest in truth, and their proofs were as ethereal as the mind of God. Yet within decades these mathematical abstractions were realized by the hand of man, in the digital stored-program computer. How it came to be recognized that proofs and programs are the same thing is a story that spans a century, a chase with (...) as many twists and turns as a thriller. At the end of the story is a new principle for designing programming languages that will guide computers into the 21st century. -/- For my money, Gentzen’s natural deduction and Church’s lambda calculus are on a par with Einstein’s relativity and Dirac’s quantum physics for elegance and insight. And the maths are a lot simpler. I want to show you the essence of these ideas. I’ll need a few symbols, but not too many, and I’ll explain as I go along. -/- To simplify, I’ll present the story as we understand it now, with some asides to fill in the history. First, I’ll introduce Gentzen’s natural deduction, a formalism for proofs. Next, I’ll introduce Church’s lambda calculus, a formalism for programs. Then I’ll explain why proofs and programs are really the same thing, and how simplifying a proof corresponds to executing a program. Finally, I’ll conclude with a look at how these principles are being applied to design a new generation of programming languages, particularly mobile code for the Internet. (shrink)

Gaisi Takeuti extended Gentzen's work to higher-order case in 1950's–1960's and proved the consistency of impredicative subsystems of analysis. He has been chiefly known as a successor of Hilbert's school, but we pointed out in the previous paper that Takeuti's aimed to investigate the relationships between "minds" by carrying out his proof-theoretic project rather than proving the "reliability" of such impredicative subsystems of analysis. Moreover, as briefly explained there, his philosophical ideas can be traced back to Nishida's philosophy (...) in Kyoto's school. For the proving the consistency of such systems, it is crucial to prove the well-foundedness of ordinals called "ordinal diagrams" developed for it. Takeuti presented such arguments several times in order to show that they are admitted in his stand point. As a starting point of investigating his finitist stand point, we formulate the system of ordinal notations up to ε0 and reconstruct the well-foundedness arguments of them. (shrink)

An adequate semantics for generic sentences must stake out positions across a range of contested territory in philosophy and linguistics. For this reason the study of generic sentences is a venue for investigating different frameworks for understanding human rationality as manifested in linguistic phenomena such as quantification, classification of individuals under kinds, defeasible reasoning, and intensionality. Despite the wide variety of semantic theories developed for generic sentences, to date these theories have been almost universally model-theoretic and representational. This essay outlines (...) a range of proof-theoretic analyses for characterizing generics. Particular attention is given to an expressivist proof-theory that can be traced to 1) work on logical syntax that Carnap undertook prior to his turn toward truth-conditional model theory in the late 1930s, and 2) research on sequent calculi and natural deduction systems that originate in work from Gentzen and Prawitz.1. (shrink)

The “four-color” theorem seems to be generalizable as follows. The four-letter alphabet is sufficient to encode unambiguously any set of well-orderings including a geographical map or the “map” of any logic and thus that of all logics or the DNA plan of any alive being. Then the corresponding maximally generalizing conjecture would state: anything in the universe or mind can be encoded unambiguously by four letters. That admits to be formulated as a “four-letter theorem”, and thus one can search for (...) a properly mathematical proof of the statement. It would imply the “four colour theorem”, the proof of which many philosophers and mathematicians believe not to be entirely satisfactory for it is not a “human proof”, but intermediated by computers unavoidably since the necessary calculations exceed the human capabilities fundamentally. It is furthermore rather unsatisfactory because it consists in enumerating and proving all cases one by one. Sometimes, a more general theorem turns out to be much easier for proving including a general “human” method, and the particular and too difficult for proving theorem to be implied as a corollary in certain simple conditions. The same approach will be followed as to the four colour theorem, i.e. to be deduced more or less trivially from the “four-letter theorem” if the latter is proved. References are only classical and thus very well-known papers: their complete bibliographic description is omitted. (shrink)

Growing technological advances in intelligent artifacts and bitter experiences of the past have emphasized the need to use and operate ethics in this field. Accordingly, it is vital to discuss the ethical integrity of having intelligent artifacts. Concerning the method of gathering materials, the current study uses library and documentary research followed by attribution style. Moreover, descriptive analysis is employed in order to analyze data. Explaining and criticizing the opposing views in this field and reviewing the related literature, it is (...) concluded that the proof of the ethical integrity of the intelligent artifacts is possible due to the specific features of these artifacts and their own moral system. (shrink)

The suggestion of something akin to a ‘relativist solution to the Mind-Body problem’ has recently been held by some scientists and philosophers; either explicitly (Galadí, 2023; Lahav & Neemeh, 2022; Ludwig, 2015) or in more implicit terms (Solms, 2018; Velmans, 2002, 2008). In this paper I provide an argument in favor of a relativist approach to the Mind-Body problem, more specifically, an argument for ‘1st/3rd person relativism’, the claim that ‘The truth value of some sentences or propositions is relative to (...) 1st and 3rd person perspectives’. The argument for 1st/3rd person relativism is close to a forma proof. It is shown that, just by assuming the 1st/3rd person distinction itself and using first order logic and set theory, ‘1st/3rd person relativism’ follows as a theorem. Some consequences of ‘1st/3rd person relativism’ to the Mind-Body Problem are evaluated. It is shown that ‘1st/3rd person relativism’ predicts the existence of an (apparent) Explanatory Gap; explains why the Explanatory Gap is just apparent (and the origins of such illusion); dissolves the Hard-Problem; provides a possible solution the problem of Mental Causation; explains why Mental Causation looks like a problem in the first place and accurately predicts the actual empirically found correlation and covariation between conscious experiences and brain states. This explanatory power of ‘1st/3rd person relativism’ is particularly impressive since it was not designed as a possible solution to the Mind-Body problem in the first place. (shrink)

Infectious logics are systems that have a truth-value that is assigned to a compound formula whenever it is assigned to one of its components. This paper studies four-valued infectious logics as the basis of transparent theories of truth. This take is motivated as a way to treat different pathological sentences differently, namely, by allowing some of them to be truth-value gluts and some others to be truth-value gaps and as a way to treat the semantic pathology suffered by at least (...) some of these sentences as infectious. This leads us to consider four distinct four-valued logics: one where truth-value gaps are infectious, but gluts are not; one where truth-value gluts are infectious, but gaps are not; and two logics where both gluts and gaps are infectious, in some sense. Additionally, we focus on the proof theory of these systems, by offering a discussion of two related topics. On the one hand, we prove some limitations regarding the possibility of providing standard Gentzen sequent calculi for these systems, by dualizing and extending some recent results for infectious logics. On the other hand, we provide sound and complete four-sided sequent calculi, arguing that the most important technical and philosophical features taken into account to usually prefer standard calculi are, indeed, enjoyed by the four-sided systems. (shrink)

This paper is an English version of the paper that was published in German under the title: "Über die Aussichten erfolgreicher Beweise für Theismus oder Atheismus". My English paper was translated into German by Gabriele Schlegel. -/- The aim of this paper is to examine the prospects for proofs or successful arguments for the existence or non-existence of God.

Researchers often pursue proof of concept research, but criteria for evaluating such research remain poorly specified. This article proposes a general framework for proof of concept research that k...

We study a fragment of Intuitionistic Linear Logic combined with non-normal modal operators. Focusing on the minimal modal logic, we provide a Gentzen-style sequent calculus as well as a semantics in terms of Kripke resource models. We show that the proof theory is sound and complete with respect to the class of minimal Kripke resource models. We also show that the sequent calculus allows cut elimination. We put the logical framework to use by instantiating it as a logic (...) of agency. In particular, we apply it to reason about the resource-sensitive use of artefacts. (shrink)

This paper presents proof that Buss's S22 can prove the consistency of a fragment of Cook and Urquhart's PV from which induction has been removed but substitution has been retained. This result improves Beckmann's result, which proves the consistency of such a system without substitution in bounded arithmetic S12. Our proof relies on the notion of "computation" of the terms of PV. In our work, we first prove that, in the system under consideration, if an equation is proved (...) and either its left- or right-hand side is computed, then there is a corresponding computation for its right- or left-hand side, respectively. By carefully computing the bound of the size of the computation, the proof of this theorem inside a bounded arithmetic is obtained, from which the consistency of the system is readily proven. This result apparently implies the separation of bounded arithmetic because Buss and Ignjatović stated that it is not possible to prove the consistency of a fragment of PV without induction but with substitution in Buss's S12. However, their proof actually shows that it is not possible to prove the consistency of the system, which is obtained by the addition of propositional logic and other axioms to a system such as ours. On the other hand, the system that we have considered is strictly equational, which is a property on which our proof relies. (shrink)

Proofs of God in Early Modern Europe offers a fascinating window into early modern efforts to prove God’s existence. Assembled here are twenty-two key texts, many translated into English for the first time, which illustrate the variety of arguments that philosophers of the seventeenth and eighteenth centuries offered for God. These selections feature traditional proofs—such as various ontological, cosmological, and design arguments—but also introduce more exotic proofs, such as the argument from eternal truths, the argument from universal aseity, and the (...) argument ex consensu gentium. Drawn from the work of eighteen philosophers, this book includes both canonical figures (such as Descartes, Spinoza, Newton, Leibniz, Locke, and Berkeley) and noncanonical thinkers (such as Norris, Fontenelle, Voltaire, Wolff, Du Châtelet, and Maupertuis). -/- Lloyd Strickland provides fresh translations of all selections not originally written in English and updates the spelling and grammar of those that were. Each selection is prefaced by a lengthy headnote, giving a biographical account of its author, an analysis of the main argument(s), and important details about the historical context. Strickland’s introductory essay provides further context, focusing on the various reasons that led so many thinkers of early modernity to develop proofs of God’s existence. -/- Proofs of God is perfect for both students and scholars of early modern philosophy and philosophy of religion. (shrink)

“Proof of concept” is a phrase frequently used in descriptions of research sought in program announcements, in experimental studies, and in the marketing of new technologies. It is often coupled with either a short definition or none at all, its meaning assumed to be fully understood. This is problematic. As a phrase with potential implications for research and technology, its assumed meaning requires some analysis to avoid it becoming a descriptive category that refers to all things scientifically exciting. I (...) provide a short analysis of proof of concept research and offer an example of it within synthetic biology. I suggest that not only are there activities that circumscribe new epistemological categories but there are also associated normative ethical categories or principles linked to the research. I examine these and provide an outline for an alternative ethical account to describe these activities that I refer to as “extended agency ethics”. This view is used to explain how the type of research described as proof of concept also provides an attendant proof of principle that is the result of decision-making that extends across practitioners, their tools, techniques, and the problem solving activities of other research groups. (shrink)

It is shown how the schema of equivalence can be used to obtain short proofs of tautologies A , where the depth of proofs is linear in the number of variables in A .

Introduction to the Scientific Proof of the Natural Moral Law This paper proves that Aquinas has a means of demonstrating and deriving both moral goodness and the natural moral law from human nature alone. Aquinas scientifically proves the existence of the natural moral law as the natural rule of human operations from human nature alone. The distinction between moral goodness and transcendental goodness is affirmed. This provides the intellectual tools to refute the G.E. Moore (Principles of Ethics) attack against (...) the natural law as committing a "naturalistic fallacy". This article proves that instead Moore commits the fallacy of equivocation between moral goodness and transcendental goodness in his very assertion of a "naturalistic fallacy" by the proponents of the natural moral law. In the process the new deontological/kantian theory of natural law as articulated by John Finnis, Robert George, and Germain Grisez is false historically and philosophically. Ethical naturalism is affirmed as a result. (shrink)

An alternative consensus algorithm to both proof-of-work and proof-of-stake, proof-of-loss addresses all their deficiencies, including the lack of an organic block size limit, the risks of mining centralization, and the "nothing at stake" problem.

This chapter discusses Kant's 1763 "possibility proof" for the existence of God. I first provide a reconstruction of the proof in its two stages, and then revisit my earlier argument according to which the being the proof delivers threatens to be a Spinozistic-panentheistic God—a being whose properties include the entire spatio-temporal universe—rather than the traditional, ontologically distinct God of biblical monotheism. I go on to evaluate some recent alternative readings that have sought to avoid this result by (...) arguing that the relevant facts about real modality can be ultimately grounded in God’s powers or thoughts – or that Kant just leaves the grounding relations mysterious. I argue that the textual and philosophical costs of each of these alternative readings are formidable. The chapter concludes with a discussion of the fate of the proof in the critical period. Some commentators think that it disappears altogether, or that it is downgraded such that it produces a mere regulative idea of God as the most real being. I suggest that the proof survives but that the mode of assent it licenses towards its conclusion changes from knowledge to a certain kind of Belief (Glaube). (shrink)

In this article, I argue that it is impossible to complete infinitely many tasks in a finite time. A key premise in my argument is that the only way to get to 0 tasks remaining is from 1 task remaining, when tasks are done 1-by-1. I suggest that the only way to deny this premise is by begging the question, that is, by assuming that supertasks are possible. I go on to present one reason why this conclusion (that supertasks are (...) impossible) is important, namely that it implies a new verdict on a decision puzzle propounded by Jeffrey Barrett and Frank Arntzenius. (shrink)

The current industrial revolution is said to be driven by the digitization that exploits connected information across all aspects of manufacturing. Standards have been recognized as an important enabler. Ontology-based information standard may provide benefits not offered by current information standards. Although there have been ontologies developed in the industrial manufacturing domain, they have been fragmented and inconsistent, and little has received a standard status. With successes in developing coherent ontologies in the biological, biomedical, and financial domains, an effort called (...) Industrial Ontologies Foundry (IOF) has been formed to pursue the same goal for the industrial manufacturing domain. However, developing a coherent ontology covering the entire industrial manufacturing domain has been known to be a mountainous challenge because of the multidisciplinary nature of manufacturing. To manage the scope and expectations, the IOF community kicked-off its effort with a proof-of-concept (POC) project. This paper describes the developments within the project. It also provides a brief update on the IOF organizational set up. (shrink)

PARC is an "appended numeral" system of natural deduction that I learned as an undergraduate and have taught for many years. Despite its considerable pedagogical strengths, PARC appears to have never been published. The system features explicit "tracking" of premises and assumptions throughout a derivation, the collapsing of indirect proofs into conditional proofs, and a very simple set of quantificational rules without the long list of exceptions that bedevil students learning existential instantiation and universal generalization. The system can be used (...) with any Copi-style set of inference rules, so it is quite adaptable to many mainstream symbolic logic textbooks. Consequently, PARC may be especially attractive to logic teachers who find Jaskowski/Gentzen-style introduction/elimination rules to be far less "natural" than Copi-style rules. The PARC system is also keyboard-friendly in comparison to the widely adopted Jaskowski-style graphical subproof system of natural deduction, viz., Fitch diagrams and Copi "bent arrow" diagrams. (shrink)

The problem of resurrection, one of the most important issues in the philosophy and theology. Some of Muslim philosophers and the vast majority of theologians always discussed about this topic. Some of Muslim philosophers accepted this problem and prove it, but, in quality of occurrence of them, they have differ believe from each other. However, some of Muslim theologians except those who believe in transmogrification, they consider the resurrection to be one of the principle of religion, beside monotheism and prophecy. (...) Moreover, they proved the principle of resurrection through reasons, and explanations them elaborates through the Holy Quran and Prophetic saying (Traditions- Hadith). Avicenna and Suhrawardi have been proving resurrection. Of course, for prove of this problem, they adopted of different manner from Muslim Theologians. Both of philosophers according to codify of ordinary psychological system, have proved and explanation this issue. Thus, for understand of Avicenna and Suhrawardi’s eschatology. First of all, we must understand of their psychological system. Furthermore, in this paper, we will discuss about survival of the soul according to immaterial soul and perfecting of soul as two premises for prove of resurrection. (shrink)

Machine intelligence already helps medical staff with a number of tasks. Ethical decision-making, however, has not been handed over to computers. In this proof-of-concept study, we show how an algorithm based on Beauchamp and Childress’ prima-facie principles could be employed to advise on a range of moral dilemma situations that occur in medical institutions. We explain why we chose fuzzy cognitive maps to set up the advisory system and how we utilized machine learning to train it. We report on (...) the difficult task of operationalizing the principles of beneficence, non-maleficence and patient autonomy, and describe how we selected suitable input parameters that we extracted from a training dataset of clinical cases. The first performance results are promising, but an algorithmic approach to ethics also comes with several weaknesses and limitations. Should one really entrust the sensitive domain of clinical ethics to machine intelligence? (shrink)

This paper draws attention to a proof of the necessity of identity given by Arthur Prior. In its simplicity, it is comparable to a proof of Quine's, popularised by Kripke, but it is slightly different. Prior's Polish notation is transcribed into a more familiar idiom. Prior's proof is followed by a proof of the necessity of difference, possibly the first such proof in the literature, which is also repeated here and transcribed. The paper concludes with (...) a brief discussion of Prior's views on identity and difference over time. (shrink)

The essay argues that while there is no general agreement on whether moral realism is true, there is general agreement on at least some of the moral obligations that we have if moral realism is true. Given that moral realism might be true, and given that we know some of the things we ought to do if it is true, we have a reason to do those things. Furthermore, this reason is itself an objective moral reason. Thus, if moral realism (...) might be true, then it is true. (shrink)

In this paper, I develop a quasi-transcendental argument to justify Kant’s infamous claim “man is evil by nature.” The cornerstone of my reconstruction lies in drawing a systematic distinction between the seemingly identical concepts of “evil disposition” (böseGesinnung) and “propensity to evil” (Hang zumBösen). The former, I argue, Kant reserves to describe the fundamental moral outlook of a single individual; the latter, the moral orientation of the whole species. Moreover, the appellative “evil” ranges over two different types of moral failure: (...) while an “evil disposition” is a failure to realize the good (i.e., to adopt the motive of duty as limiting condition for all one’s desires), an “evil propensity” is a failure to realize the highest good (i.e., to engage in the collective project of transforming the legal order into an ethical community). This correlation between units of moral analysis and types of obligation suggests a way to offer a deduction of the universal propensity on behalf of Kant. It consists in tracing the source of radical evil to the same subjective necessity that gives rise to the doctrine of the highest good. For, at the basis of Kant’s two doctrines lies the same natural dialectic between happiness and morality. While the highest good brings about the critically acceptable resolution of this dialectic, the propensity to evil perpetuates and aggravates it. Instead of connecting happiness and morality in an objective relation, the human will subordinatesmorality to the pursuit of happiness according to the subjective order of association. If this reading is correct, it would explain why prior attempts at a transcendental deduction have failed: interpreters have looked for the key to the deduction in the body of Kant’s text, where it is not to be found, for it is tucked, instead, in the Preface to the first edition. (shrink)

Paley’s ‘proof’ of the existence of God, or some supposed version of it, is well known. In this paper I offer the real thing and two objections to it. One objection is my own, and the other is provided by Darwin.

Considered in light of the reader’s expectation of a thoroughgoing criticism of the pretensions of the rational psychologist, and of the wealth of discussions available in the broader 18th century context, which includes a variety of proofs that do not explicitly turn on the identification of the soul as a simple substance, Kant’s discussion of immortality in the Paralogisms falls lamentably short. However, outside of the Paralogisms (and the published works generally), Kant had much more to say about the arguments (...) for the soul’s immortality as he devoted considerable time to the topic throughout his career in his lectures on metaphysics. In fact, as I show in this paper, the student lecture notes prove to be an indispensable supplement to the treatment in the Paralogisms, not only for illuminating Kant’s criticism of the rational psychologist’s views on the immortality of the soul, but also in reconciling this criticism with Kant’s own positive claims regarding certain theoretical proofs of immortality. (shrink)

Some people think that grounding is a type of identity. And some people think that grounding connections hold necessarily. I show that, under plausible assumptions, if grounding is a type of identity, then grounding connections hold necessarily.

This short essay seeks to identify and prevent a pitfall that attends less careful inquiries into “physiosemiosis.” It is emphasized that, in order to truly establish the presence of sign-action in the non-living world, all the components of a triadic sign - including the interpretant - would have to be abiotic (that is, not dependent on a living organism). Failure to heed this necessary condition can lead one to hastily confuse a natural sign (like smoke coming from fire) for an (...) instance of abiotic semiosis. A more rigorous and reserved approach to the topic is called for. (shrink)

The Born’s rule to interpret the square of wave function as the probability to get a specific value in measurement has been accepted as a postulate in foundations of quantum mechanics. Although there have been so many attempts at deriving this rule theoretically using different approaches such as frequency operator approach, many-world theory, Bayesian probability and envariance, literature shows that arguments in each of these methods are circular. In view of absence of a convincing theoretical proof, recently some researchers (...) have carried out experiments to validate the rule up-to maximum possible accuracy using multi-order interference (Sinha et al, Science, 329, 418 [2010]). But, a convincing analytical proof of Born’s rule will make us understand the basic process responsible for exact square dependency of probability on wave function. In this paper, by generalizing the method of calculating probability in common experience into quantum mechanics, we prove the Born’s rule for statistical interpretation of wave function. (shrink)

This article presents modal versions of resource-conscious logics. We concentrate on extensions of variants of linear logic with one minimal non-normal modality. In earlier work, where we investigated agency in multi-agent systems, we have shown that the results scale up to logics with multiple non-minimal modalities. Here, we start with the language of propositional intuitionistic linear logic without the additive disjunction, to which we add a modality. We provide an interpretation of this language on a class of Kripke resource models (...) extended with a neighbourhood function: modal Kripke resource models. We propose a Hilbert-style axiomatisation and a Gentzen-style sequent calculus. We show that the proof theories are sound and complete with respect to the class of modal Kripke resource models. We show that the sequent calculus admits cut elimination and that proof-search is in PSPACE. We then show how to extend the results when non-commutative connectives are added to the language. Finally, we put the l.. (shrink)

Leibniz proposed the ‘Most Determined Path Principle’ in seventeenth century. According to it, ‘ease’ of travel is the end purpose of motion. Using this principle and his calculus method he demonstrated Snell’s Laws of reflection and refraction. This method shows that light follows extremal (local minimum or maximum) time path in going from one point to another, either directly along a straight line path or along a broken line path when it undergoes reflection or refraction at plane or spherical (concave (...) or convex) surfaces. The extremal time path avoided the criticism that Fermat’s least time path was subjected to, by Cartesians who cited examples of reflections at spherical surfaces where light took the path of longest time. Thereby it became the standard method of demonstration of Snell’s Laws. Ptolemy’s theorem is a fundamental theorem in geometry. A special case of it offers a method of finding the minimum sum of the two distances of a point from two given fixed points. We show in this paper that Leibniz’s calculus proof of Snell’s Laws violates Ptolemy’s theorem, whereby Leibniz’s proof becomes invalid. (shrink)

Euclid's classic proof about the infinitude of prime numbers has been a standard model of reasoning in student textbooks and books of elementary number theory. It has withstood scrutiny for over 2000 years but we shall prove that despite the deceptive appearance of its analytical reasoning it is tautological in nature. We shall argue that the proof is more of an observation about the general property of a prime numbers than an expository style of natural deduction of the (...) proof of their infinitude. (shrink)

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting (...) to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants. (shrink)

The paper suggests that Kafka's writings offer a conception of freedom that is incompatible with the free will and it is not reducible to either compatibilism or incompatibilism.

Edward Feser defends the ‘Neo-Platonic proof ’ for the existence of the God of classical theism. After articulating the argument and a number of preliminaries, I first argue that premise three of Feser’s argument—the causal principle that every composite object requires a sustaining efficient cause to combine its parts—is both unjustified and dialectically ill-situated. I then argue that the Neo-Platonic proof fails to deliver the mindedness of the absolutely simple being and instead militates against its mindedness. Finally, I (...) uncover two tensions between Trinitarianism and the Neo-Platonic proof. (shrink)

Although the Four Colour Theorem is passe, we give an elementary pre-formal proof that transparently illustrates why four colours suffice to chromatically differentiate any set of contiguous, simply connected and bounded, planar spaces; by showing that there is no minimal 4-coloured planar map M. We note that such a pre-formal proof of the Four Colour Theorem highlights the significance of differentiating between: (a) Plato's knowledge as justified true belief, which seeks a formal proof in a first-order mathematical (...) language in order to justify a belief as true; and (b) Piccinini's knowledge as factually grounded belief, which seeks a pre-formal proof, in Pantsar's sense, in order to justify the axioms and rules of inference of a first-order mathematical language which can, then, formally prove the belief as justifiably true under a well-defined interpretation of the language. (shrink)

Andrew Wiles' analytic proof of Fermat's Last Theorem FLT, which appeals to geometrical properties of real and complex numbers, leaves two questions unanswered: (i) What technique might Fermat have used that led him to, even if only briefly, believe he had `a truly marvellous demonstration' of FLT? (ii) Why is x^n+y^n=z^n solvable only for n<3? In this inter-disciplinary perspective, we offer insight into, and answers to, both queries; yielding a pre-formal proof of why FLT can be treated as (...) a true arithmetical proposition (one which, moreover, might not be provable formally in the first-order Peano Arithmetic PA), where we admit only elementary (i.e., number-theoretic) reasoning, without appeal to analytic properties of real and complex numbers. We cogently argue, further, that any formal proof of FLT needs---as is implicitly suggested by Wiles' proof---to appeal essentially to formal geometrical properties of formal arithmetical propositions. (shrink)

A review of Edward Feser's Five Proofs of the Existence of God.

We develop a reading of Moore’s “Proof of an External World” that emphasizes the connections between this paper and Moore’s earlier concerns and strategies. Our reading has the benefit of explaining why the claims that Moore advances in “Proof of an External World” would have been of interest to him, and avoids attributing to him arguments that are either trivial or wildly unsuccessful. Part of the evidence for our view comes from unpublished drafts which, we believe, contain important (...) clues concerning Moore’s aims and intent. While our approach to PEW may be classified alongside other broadly "metaphysical" readings, we believe that a proper recognition of the continuity in Moore’s philosophical concerns and strategies across his philosophical career shows that the customary distinction between "epistemological" and "metaphysical" interpretative approaches to PEW is at best superficial. (shrink)

All accepted proofs of the Four Colour Theorem (4CT) are computer-dependent; and appeal to the existence, and manual identification, of an ‘unavoidable’ set containing a sufficient number of explicitly defined configurations—each evidenced only by a computer as ‘reducible’—such that at least one of the configurations must occur in any chromatically distinguished, minimal, planar map. For instance, Appel and Haken ‘identified’ 1,482 such configurations in their 1977, computer-dependent, proof of 4CT; whilst Neil Robertson et al ‘identified’ 633 configurations as sufficient (...) in their 1997, also computer-dependent, proof of 4CT. However, treating any specific number of ‘reducible’ configurations in an ‘unavoidable’ set as sufficient entails a minimum number as necessary and sufficient. We now show that the minimum number of such configurations can only be the one corresponding to the ‘unavoidable’ set of a ‘reducible’, 4-sided configuration identified by Alfred Kempe in his, seemingly fatally flawed, 1879 ‘proof’ of 4CT. Although Kempe appealed to putative properties of ‘Kempe’ chains in a graphical representation to fallaciously argue that a 5-sided configuration was also in the ‘unavoidable’ set, and ‘reducible’, we shall show why the flaw in his ‘proof’ is not fatal when the argument is expressed geometrically; and that, essentially, Kempe correctly argued that any planar map which admits a chromatic differentiation with a five-sided area C that shares non-zero boundaries with four, all differently coloured, neighbours can be 4-coloured. (shrink)

This paper discusses critically what simulation models of the evolution of cooperation can possibly prove by examining Axelrod’s “Evolution of Cooperation” (1984) and the modeling tradition it has inspired. Hardly any of the many simulation models in this tradition have been applicable empirically. Axelrod’s role model suggested a research design that seemingly allowed to draw general conclusions from simulation models even if the mechanisms that drive the simulation could not be identified empirically. But this research design was fundamentally flawed. At (...) best such simulations can claim to prove logical possibilities, i.e. they prove that certain phenomena are possible as the consequence of the modeling assumptions built into the simulation, but not that they are possible or can be expected to occur in reality. I suggest several requirements under which proofs of logical possibilities can nevertheless be considered useful. Sadly, most Axelrod-style simulations do not meet these requirements. It would be better not to use this kind of simulations at all. (shrink)