Rigorous proof is supposed to guarantee that the premises invoked imply the conclusion reached, and the problem of rigor may be described as that of bringing together the perspectives of formal logic and mathematical practice on how this is to be achieved. This problem has recently raised a lot of discussion among philosophers of mathematics. We survey some possible solutions and argue that failure to understand its terms properly has led to misunderstandings in the literature.

Criteria of acceptability for mathematical proofs are field-dependent. In topology, though not in most other domains, it is sometimes acceptable to appeal to visual intuition to support inferential steps. In previous work :829–842, 2014; Lolli, Panza, Venturi From logic to practice, Springer, Berlin, 2015; Larvor Mathematical cultures, Springer, Berlin, 2016) my co-author and I aimed at spelling out how topological proofs work on their own terms, without appealing to formal proofs which might be associated with them. In this article, I (...) address two criticisms that have been raised in Tatton-Brown against our approach: that it leads to a form of relativism according to which validity is equated with social agreement and that it implies an antiformalizability thesis according to which it is not the case that all rigorous mathematical proofs can be formalized. I reject both criticisms and suggest that our previous case studies provide insight into the plausibility of two related but quite different theses. (shrink)

A principle, according to which any scientific theory can be mathematized, is investigated. Social science, liberal arts, history, and philosophy are meant first of all. That kind of theory is presupposed to be a consistent text, which can be exhaustedly represented by a certain mathematical structure constructively. In thus used, the term “theory” includes all hypotheses as yet unconfirmed as already rejected. The investigation of the sketch of a possible proof of the principle demonstrates that it should be accepted rather (...) a metamathematical axiom about the relation of mathematics and reality. The main statement is formulated as follows: Any scientific theory admits isomorphism to some mathematical structure in a way constructive. Its investigation needs philosophical means. Husserl’s phenomenology is what is used, and then the conception of “bracketing reality” is modelled to generalize Peano arithmetic in its relation to set theory in the foundation of mathematics. The obtained model is equivalent to the generalization of Peano arithmetic by means of replacing the axiom of induction with that of transfinite induction. The sketch of the proof is organized in five steps: a generalization of epoché; involving transfinite induction in the transition between Peano arithmetic and set theory; discussing the finiteness of Peano arithmetic; applying transfinite induction to Peano arithmetic; discussing an arithmetical model of reality. Accepting or rejecting the principle, two kinds of mathematics appear differing from each other by its relation to reality. Accepting the principle, mathematics has to include reality within itself in a kind of Pythagoreanism. These two kinds are called in paper correspondingly Hilbert mathematics and Gödel mathematics. The sketch of the proof of the principle demonstrates that the generalization of Peano arithmetic as above can be interpreted as a model of Hilbert mathematics into Gödel mathematics therefore showing that the former is not less consistent than the latter, and the principle is an independent axiom. The present paper follows a pathway grounded on Husserl’s phenomenology and “bracketing reality” to achieve the generalized arithmetic necessary for the principle to be founded in alternative ontology, in which there is no reality external to mathematics: reality is included within mathematics. That latter mathematics is able to self-found itself and can be called Hilbert mathematics in honour of Hilbert’s program for self-founding mathematics on the base of arithmetic. The principle of universal mathematizability is consistent to Hilbert mathematics, but not to Gödel mathematics. Consequently, its validity or rejection would resolve the problem which mathematics refers to our being; and vice versa: the choice between them for different reasons would confirm or refuse the principle as to the being. An information interpretation of Hilbert mathematics is involved. It is a kind of ontology of information. The Schrödinger equation in quantum mechanics is involved to illustrate that ontology. Thus the problem which of the two mathematics is more relevant to our being is discussed again in a new way A few directions for future work can be: a rigorous formal proof of the principle as an independent axiom; the further development of information ontology consistent to both kinds of mathematics, but much more natural for Hilbert mathematics; the development of the information interpretation of quantum mechanics as a mathematical one for information ontology and thus Hilbert mathematics; the description of consciousness in terms of information ontology. (shrink)

We argue that Wittgenstein’s philosophical perspective on Gödel’s most famous theorem is even more radical than has commonly been assumed. Wittgenstein shows in detail that there is no way that the Gödelian construct of a string of signs could be assigned a useful function within (ordinary) mathematics. — The focus is on Appendix III to Part I of Remarks on the Foundations of Mathematics. The present reading highlights the exceptional importance of this particular set of remarks and, more specifically, emphasises (...) its refined composition and rigorous internal structure. (shrink)

Not focusing on the history of classical logic, this book provides discussions and quotes central passages on its origins and development, namely from a philosophical perspective. Not being a book in mathematical logic, it takes formal logic from an essentially mathematical perspective. Biased towards a computational approach, with SAT and VAL as its backbone, this is an introduction to logic that covers essential aspects of the three branches of logic, to wit, philosophical, mathematical, and computational.

Many authors have noted that there are types of English modal sentences cannot be formalized in the language of basic first-order modal logic. Some widely discussed examples include “There could have been things other than there actually are” and “Everyone who is actually rich could have been poor.” In response to this lack of expressive power, many authors have discussed extensions of first-order modal logic with two-dimensional operators. But claims about the relative expressive power of these extensions are often justified (...) only by example rather than by rigorous proof. In this paper, we provide proofs of many of these claims and present a more complete picture of the expressive landscape for such languages. (shrink)

I was quite excited when I first read Restall and Russell’s (2010) paper. For two reasons. First, because the paper provides rigorous formulations and formal proofs of implication barrier the- ses, namely “theses [which] deny that one can derive sentences of one type from sentences of another”. Second (and primarily), because the paper proves a general theorem, the Barrier Con- struction Theorem, which unifies implication barrier theses concerning four topics: generality, necessity, time, and normativity. After thinking about the paper, I (...) am satisfied with its treatment of the first three topics, namely generality, necessity, and time. But I am not satisfied with its treatment of normativity, so my comments are exclusively on that topic. (shrink)

I was quite excited when I first read Restall and Russell’s (2010) paper. For two reasons. First, because the paper provides rigorous formulations and formal proofs of implication barrier theses, namely “theses [which] deny that one can derive sentences of one type from sentences of another”. Second (and primarily), because the paper proves a general theorem, the Barrier Construction Theorem, which unifies implication barrier theses concerning four topics: generality, necessity, time, and normativity. After thinking about the paper, I am satisfied (...) with its treatment of the first three topics, namely generality, necessity, and time. But I am not satisfied with its treatment of normativity, so my comments are exclusively on that topic. (shrink)

Could the intersection of [formal proofs of mathematical logic] and [sound deductive inference] specify formal systems having [deductively sound formal proofs of mathematical logic]? All that we have to do to provide [deductively sound formal proofs of mathematical logic] is select the subset of conventional [formal proofs of mathematical logic] having true premises and now we have [deductively sound formal proofs of mathematical logic].

When adopting a sound logical system, reasonings made within this system are correct. The situation with reasonings expressed, at least in part, with natural language is much more ambiguous. One way to be certain of the correctness of these reasonings is to provide a logical model of them. To conclude that a reasoning process is correct we need the logical model to be faithful to the reasoning. In this case, the reasoning inherits, so to speak, the correctness of the logical (...) model. There is a weak link in this procedure, which we call the faithfulness problem: how do we decide that the logical model is faithful to the reasoning that it is supposed to model? That is an issue external to logic, and we do not have rigorous formal methods to make the decision. The purpose of this paper is to expose the faithfulness problem (not to solve it). For that purpose, we will consider two examples, one from the geometrical reasoning in Euclid’s Elements and the other from a study on deductive reasoning in the psychology of reasoning. (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)

Since the time of Aristotle's students, interpreters have considered Prior Analytics to be a treatise about deductive reasoning, more generally, about methods of determining the validity and invalidity of premise-conclusion arguments. People studied Prior Analytics in order to learn more about deductive reasoning and to improve their own reasoning skills. These interpreters understood Aristotle to be focusing on two epistemic processes: first, the process of establishing knowledge that a conclusion follows necessarily from a set of premises (that is, on the (...) epistemic process of extracting information implicit in explicitly given information) and, second, the process of establishing knowledge that a conclusion does not follow. Despite the overwhelming tendency to interpret the syllogistic as formal epistemology, it was not until the early 1970s that it occurred to anyone to think that Aristotle may have developed a theory of deductive reasoning with a well worked-out system of deductions comparable in rigor and precision with systems such as propositional logic or equational logic familiar from mathematical logic. When modern logicians in the 1920s and 1930s first turned their attention to the problem of understanding Aristotle's contribution to logic in modern terms, they were guided both by the Frege-Russell conception of logic as formal ontology and at the same time by a desire to protect Aristotle from possible charges of psychologism. They thought they saw Aristotle applying the informal axiomatic method to formal ontology, not as making the first steps into formal epistemology. They did not notice Aristotle's description of deductive reasoning. Ironically, the formal axiomatic method (in which one explicitly presents not merely the substantive axioms but also the deductive processes used to derive theorems from the axioms) is incipient in Aristotle's presentation. Partly in opposition to the axiomatic, ontically-oriented approach to Aristotle's logic and partly as a result of attempting to increase the degree of fit between interpretation and text, logicians in the 1970s working independently came to remarkably similar conclusions to the effect that Aristotle indeed had produced the first system of formal deductions. They concluded that Aristotle had analyzed the process of deduction and that his achievement included a semantically complete system of natural deductions including both direct and indirect deductions. Where the interpretations of the 1920s and 1930s attribute to Aristotle a system of propositions organized deductively, the interpretations of the 1970s attribute to Aristotle a system of deductions, or extended deductive discourses, organized epistemically. The logicians of the 1920s and 1930s take Aristotle to be deducing laws of logic from axiomatic origins; the logicians of the 1970s take Aristotle to be describing the process of deduction and in particular to be describing deductions themselves, both those deductions that are proofs based on axiomatic premises and those deductions that, though deductively cogent, do not establish the truth of the conclusion but only that the conclusion is implied by the premise-set. Thus, two very different and opposed interpretations had emerged, interestingly both products of modern logicians equipped with the theoretical apparatus of mathematical logic. The issue at stake between these two interpretations is the historical question of Aristotle's place in the history of logic and of his orientation in philosophy of logic. This paper affirms Aristotle's place as the founder of logic taken as formal epistemology, including the study of deductive reasoning. A by-product of this study of Aristotle's accomplishments in logic is a clarification of a distinction implicit in discourses among logicians--that between logic as formal ontology and logic as formal epistemology. (shrink)

Although traditionally neglected, mathematical diagrams have recently begun to attract attention from philosophers of mathematics. By now, the literature includes several case studies investigating the role of diagrams both in discovery and justification. Certain preliminary questions have, however, been mostly bypassed. What are diagrams exactly? Are there different types of diagrams? In the scholarly literature, the term “mathematical diagram” is used in diverse ways. I propose a working definition that carves out the phenomena that are of most importance for a (...) taxonomy of diagrams in the context of a practice-based philosophy of mathematics, privileging examples from contemporary mathematics. In doing so, I move away from vague, ordinary notions. I define mathematical diagrams as forming notational systems and as being geometric/topological representations or two-dimensional representations. I also examine the relationship between mathematical diagrams and spatiotemporal intuition. By proposing an explication of diagrams, I explain certain controversies in the existing literature. Moreover, I shed light on why mathematical diagrams are so effective in certain instances, and, at other times, dangerously misleading. (shrink)

The aim of this article is to investigate the roles of commutative diagrams (CDs) in a specific mathematical domain, and to unveil the reasons underlying their effectiveness as a mathematical notation; this will be done through a case study. It will be shown that CDs do not depict spatial relations, but represent mathematical structures. CDs will be interpreted as a hybrid notation that goes beyond the traditional bipartition of mathematical representations into diagrammatic and linguistic. It will be argued that one (...) of the reasons why CDs form a good notation is that they are highly mathematically tractable: experts can obtain valid results by ‘calculating’ with CDs. These calculations, take the form of ‘diagram chases’. In order to draw inferences, experts move algebraic elements around the diagrams. It will be argued that these diagrams are dynamic. It is thanks to their dynamicity that CDs can externalize the relevant reasoning and allow experts to draw conclusions directly by manipulating them. Lastly, it will be shown that CDs play essential roles in the context of proof as well as in other phases of the mathematical enterprise, such as discovery and conjecture formation. (shrink)

In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the natural deduction system (...) of Wansing's bi-intuitionistic logic 2Int, which I will turn into a term-annotated form. Therefore, we need a type theory that extends to a two-sorted typed lambda-calculus. I will present such a term-annotated proof system for 2Int and prove a Dualization Theorem relating proofs and refutations in this system. On the basis of these formal results I will argue that this gives us interesting insights into questions about sense and denotation as well as synonymy and identity of proofs from a bilateralist point of view. (shrink)

Mathematical diagrams are frequently used in contemporary mathematics. They are, however, widely seen as not contributing to the justificatory force of proofs: they are considered to be either mere illustrations or shorthand for non-diagrammatic expressions. Moreover, when they are used inferentially, they are seen as threatening the reliability of proofs. In this paper, I examine certain examples of diagrams that resist this type of dismissive characterization. By presenting two diagrammatic proofs, one from topology and one from algebra, I show that (...) diagrams form genuine notational systems, and I argue that this explains why they can play a role in the inferential structure of proofs without undermining their reliability. I then consider whether diagrams can be essential to the proofs in which they appear. (shrink)

The traditional view of evidence in mathematics is that evidence is just proof and proof is just derivation. There are good reasons for thinking that this view should be rejected: it misrepresents both historical and current mathematical practice. Nonetheless, evidence, proof, and derivation are closely intertwined. This paper seeks to tease these concepts apart. It emphasizes the role of argumentation as a context shared by evidence, proofs, and derivations. The utility of argumentation theory, in general, and argumentation schemes, in particular, (...) as a methodology for the study of mathematical practice is thereby demonstrated. Argumentation schemes represent an almost untapped resource for mathematics education. Notably, they provide a consistent treatment of rigorous and non-rigorous argumentation, thereby working to exhibit the continuity of reasoning in mathematics with reasoning in other areas. Moreover, since argumentation schemes are a comparatively mature methodology, there is a substantial body of existing work to draw upon, including some increasingly sophisticated software tools. Such tools have significant potential for the analysis and evaluation of mathematical argumentation. The first four sections of the paper address the relationships of evidence to proof, proof to derivation, argument to proof, and argument to evidence, respectively. The final section directly addresses some of the educational implications of an argumentation scheme account of mathematical reasoning. (shrink)

The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of finite-valued first order (...) logics in a general way, and to present some of the more important results in this area. In Systems covered are the resolution calculus, sequent calculus, tableaux, and natural deduction. This report is actually a template, from which all results can be specialized to particular logics. (shrink)

In his article “Insight: Genesis and Ongoing Context,” Fred Crowe calls out Lonergan’s line “the diagram is more important than…is ordinarily believed” as the “philosophical understatement of the century.” Sixteen pages later he identifies elaborating an invariant cognitional theory to underlie generalized emergent probability and thus “the immanent order of the universe of proportionate being,” as “our challenge,” “but given the difficulty” he does not “see any prospect for an immediate answer.” Could this have something to do with the lack (...) of a comprehensive diagram of cognitional theory? Appendix A of The Boston College Lectures on Mathematical Logic and Existentialism offers diagrams of the dynamics of knowing and doing perhaps copied from Lonergan’s own blackboard work, but they do not distinguish explanatory and descriptive insights, let alone statistical insights, and do not illustrate the pull upwards or the fusing of routinized insights. Before we can effectively relate cognitional theory to generalized emergent probability, we must have an adequately rigorous and precise cognitional theory. I firmly believe in the truth of Lonergan’s fundamental insights, but in order to rigorously undergird generalized emergent probability there are many pertinent questions about his cognitional theory which must be asked and answered. In this paper I (1) review some of Lonergan’s attempts to diagram cognitional theory and discuss what insights they do and do not express, (2) elaborate and defend principles for making our formulations of insight into insight rigorous and clear, and (3) attempt to build up a diagram which makes full use of those principles in a maximally expressive way. (shrink)

Robert Brandom’s expressivism argues that not all semantic content may be made fully explicit. This view connects in interesting ways with recent movements in philosophy of mathematics and logic (e.g. Brown, Shin, Giaquinto) to take diagrams seriously - as more than a mere “heuristic aid” to proof, but either proofs themselves, or irreducible components of such. However what exactly is a diagram in logic? Does this constitute a semiotic natural kind? The paper will argue that such a natural kind does (...) exist in Charles Peirce’s conception of iconic signs, but that fully understood, logical diagrams involve a structured array of normative reasoning practices, as well as just a “picture on a page”. (shrink)

A close interrelationship between logic and religious faith is confirmed in many places of the Bible. In the paper, special attention is paid to the dialogue of Jesus and a Samaritan woman (John 4). In a proposed outline of a logical formalization, religious faith is described as a pragmatic function through which the linguistic and logical content is contextually realized. In the continuation of the paper, Gödel's ontological proof is commented, which in a logically rigorous way describes the ontology (...) where we can detect the systematic place of religious faith as an ontological force. (shrink)

There is a long tradition of logic, from Aristotle to Gödel, of understanding a proof from the concepts of necessity and causality. Gödel's attempts to define provability in terms of necessity led him to the distinction of formal and absolute (abstract) provability. Turing's definition of mechanical procedure by means of a Turing machine (TM) and Gödel's definition of a formal system as a mechanical procedure for producing formulas prompt us to understand formal provability as a mechanical causality. We propose a (...) formalism which makes explicit the mechanical causal nature of a TM's work. We claim that Gödel's axiomatised ontotheology and his ontological proof give a clue for the understanding of the concept of absolute provability and the pattern of the corresponding absolute completeness proof, respectively. (shrink)

Kurt Gödel wrote (1964, p. 272), after he had read Husserl, that the notion of objectivity raises a question: “the question of the objective existence of the objects of mathematical intuition (which, incidentally, is an exact replica of the question of the objective existence of the outer world)”. This “exact replica” brings to mind the close analogy Husserl saw between our intuition of essences in Wesensschau and of physical objects in perception. What is it like to experience a mathematical proving (...) process? What is the ontological status of a mathematical proof? Can computer assisted provers output a proof? Taking a naturalized world account, I will assess the relationship between mathematics, the physical world and consciousness by introducing a significant conceptual distinction between proving and proof. I will propose that proving is a phenomenological conscious experience. This experience involves a combination of what Kurt Gödel called intuition, and what Husserl called intentionality. In contrast, proof is a function of that process — the mathematical phenomenon — that objectively self-presents a property in the world, and that results from a spatiotemporal unity being subject to the exact laws of nature. In this essay, I apply phenomenology to mathematical proving as a performance of consciousness, that is, a lived experience expressed and formalized in language, in which there is the possibility of formulating intersubjectively shareable meanings. (shrink)

In my old manuscript “Formal Theology” that now is out as a preprint I show that science and theology can be founded upon the same set of basic assumptions. I now follow up this idea with the thought that Formal Theology may be used to ground also a religion. “Religion“, in this regard, as related to beliefs. I’m not going into any details, neither concerning the original manuscript, nor this new idea. The important thing, I think, is to explore if (...) this kind of “religion”, in any way, can be accommodated with “ordinary” religions. I leave more rigorous work to myself or to others for the future. (shrink)

One of the most fundamental questions in the philosophy of mathematics concerns the relation between truth and formal proof. The position according to which the two concepts are the same is called deflationism, and the opposing viewpoint substantialism. In an important result of mathematical logic, Kurt Gödel proved in his first incompleteness theorem that all consistent formal systems containing arithmetic include sentences that can neither be proved nor disproved within that system. However, such undecidable Gödel sentences can be established to (...) be true once we expand the formal system with Alfred Tarski s semantical theory of truth, as shown by Stewart Shapiro and Jeffrey Ketland in their semantical arguments for the substantiality of truth. According to them, in Gödel sentences we have an explicit case of true but unprovable sentences, and hence deflationism is refuted. -/- Against that, Neil Tennant has shown that instead of Tarskian truth we can expand the formal system with a soundness principle, according to which all provable sentences are assertable, and the assertability of Gödel sentences follows. This way, the relevant question is not whether we can establish the truth of Gödel sentences, but whether Tarskian truth is a more plausible expansion than a soundness principle. In this work I will argue that this problem is best approached once we think of mathematics as the full human phenomenon, and not just consisting of formal systems. When pre-formal mathematical thinking is included in our account, we see that Tarskian truth is in fact not an expansion at all. I claim that what proof is to formal mathematics, truth is to pre-formal thinking, and the Tarskian account of semantical truth mirrors this relation accurately. -/- However, the introduction of pre-formal mathematics is vulnerable to the deflationist counterargument that while existing in practice, pre-formal thinking could still be philosophically superfluous if it does not refer to anything objective. Against this, I argue that all truly deflationist philosophical theories lead to arbitrariness of mathematics. In all other philosophical accounts of mathematics there is room for a reference of the pre-formal mathematics, and the expansion of Tarkian truth can be made naturally. Hence, if we reject the arbitrariness of mathematics, I argue in this work, we must accept the substantiality of truth. Related subjects such as neo-Fregeanism will also be covered, and shown not to change the need for Tarskian truth. -/- The only remaining route for the deflationist is to change the underlying logic so that our formal languages can include their own truth predicates, which Tarski showed to be impossible for classical first-order languages. With such logics we would have no need to expand the formal systems, and the above argument would fail. From the alternative approaches, in this work I focus mostly on the Independence Friendly (IF) logic of Jaakko Hintikka and Gabriel Sandu. Hintikka has claimed that an IF language can include its own adequate truth predicate. I argue that while this is indeed the case, we cannot recognize the truth predicate as such within the same IF language, and the need for Tarskian truth remains. In addition to IF logic, also second-order logic and Saul Kripke s approach using Kleenean logic will be shown to fail in a similar fashion. (shrink)

A detailed axiomatisation of diagrams (in affine geometry) is presented, which supports typing of geometric objects, calculation of geometric quantities and automated proof of theorems.

How does one formalize the structure of structures necessary for the foundations of physics? This work is an attempt at conceptualizing the metaphysics of pregeometric structures, upon which new and existing notions of quantum geometry may find a foundation. We discuss the philosophy of pregeometric structures due to Wheeler, Leibniz as well as modern manifestations in topos theory. We draw attention to evidence suggesting that the framework of formal language, in particular, homotopy type theory, provides the conceptual building blocks for (...) a theory of pregeometry. This work is largely a synthesis of ideas that serve as a precursor for conceptualizing the notion of space in physical theories. In particular, the approach we espouse is based on a constructivist philosophy, wherein ``structureless structures'' are syntactic types realizing formal proofs and programs. Spaces and algebras relevant to physical theories are modeled as type-theoretic routines constructed from compositional rules of a formal language. This offers the remarkable possibility of taxonomizing distinct notions of geometry using a common theoretical framework. In particular, this perspective addresses the crucial issue of how spatiality may be realized in models that link formal computation to physics, such as the Wolfram model. (shrink)

Although Kant (1998) envisaged a prominent role for logic in the argumentative structure of his Critique of Pure Reason, logicians and philosophers have generally judged Kantgeneralformaltranscendental logics is a logic in the strict formal sense, albeit with a semantics and a definition of validity that are vastly more complex than that of first-order logic. The main technical application of the formalism developed here is a formal proof that Kants logic is after all a distinguished subsystem of first-order logic, namely what (...) is known as geometric logic. (shrink)

One shortcoming of the chain rule is that it does not iterate: it gives the derivative of f(g(x)), but not (directly) the second or higher-order derivatives. We present iterated differentials and a version of the multivariable chain rule which iterates to any desired level of derivative. We first present this material informally, and later discuss how to make it rigorous (a discussion which touches on formal foundations of calculus). We also suggest a finite calculus chain rule (contrary to Graham, Knuth (...) and Patashnik's claim that "there's no corresponding chain rule of finite calculus"). (shrink)

The central hypothesis of the collaboration between Language and Computing (L&C) and the Institute for Formal Ontology and Medical Information Science (IFOMIS) is that the methodology and conceptual rigor of a philosophically inspired formal ontology greatly benefits application ontologies. To this end r®, L&C’s ontology, which is designed to integrate and reason across various external databases simultaneously, has been submitted to the conceptual demands of IFOMIS’s Basic Formal Ontology (BFO). With this project we aim to move beyond the level of (...) controlled vocabularies to yield an ontology with the ability to support reasoning applications. Our general procedure has been the implementation of a meta-ontological definition space in which the definitions of all the concepts and relations in LinKBase® are standardized in a framework of first-order logic. In this paper we describe how this standardization has already led to an improvement in the LinKBase® structure that allows for a greater degree of internal coherence than ever before possible. We then show the use of this philosophical standardization for the purpose of mapping external databases to one another, using LinKBase® as translation hub, with a greater degree of success than possible hitherto. We demonstrate how this offers a genuine advance over other application ontologies that have not submitted themselves to the demands of philosophical scrutiny. LinKBase® is one of the world’s largest applications-oriented medical domain ontologies, and BFO is one of the world’s first philosophically driven reference ontologies. The collaboration of the two thus initiates a new phase in the quest to solve the so-called “Tower of Babel”. (shrink)

This article discusses some of Chateaubriand’s views on the connections between the ideas of formalization and infinity, as presented in chapters 19 and 20 of Logical Forms. We basically agree with his criticisms of the standard construal of these connections, a view we named “formal proofs as ultimate provings”, but we suggest an alternative way of picturing that connection based on some ideas of the late Wittgenstein.

The classification of algebraic surfaces by the Italian School of algebraic geometry is universally recognized as a breakthrough in 20th-century mathematics. The methods by which it was achieved do not, however, meet the modern standard of rigor and therefore appear dubious from a contemporary viewpoint. In this article, we offer a glimpse into the mathematical practice of the three leading exponents of the Italian School of algebraic geometry: Castelnuovo, Enriques, and Severi. We then bring into focus their distinctive conception of (...) rigor and intuition. Unlike what is often assumed today, from their perspective, rigor is neither opposed to intuition nor understood as a unitary phenomenon – Enriques distinguishes between small-scale rigor and large-scale rigor and Severi between formal rigor and substantial rigor. Finally, we turn to the notion of mathematical objectivity. We draw from our case study in order to advance a multi-dimensional analysis of objectivity. Specifically, we suggest that various types of rigor may be associated with different conceptions of objectivity: namely, objectivity as faithfulness to facts and objectivity as intersubjectivity. (shrink)

This article explores aspects of Rosenzweig’s Star of Redemption from the perspective of systems theory. Mosès, Pollock, and others have noted the systematic character of the Star. While “systematic” does not mean “systems theoretic,” the philosophical theology of the Star encompasses ideas that are salient in systems theory. The Magen David star to which the title refers, and which deeply structures Rosenzweig’s thought, fits the classic definition of “system” – a set of elements (God, World, Human) and relations between the (...) elements (Creation, Revelation, Redemption). The Yes and No of the elements and their reversals illustrate the bridging of element and relation with the third category of “attribute,” a notion also central to the definition of “system.” In the diachronics of “the All,” the relations actualize what is only potential in the elements in their primordial state and thus remedy the incompleteness of these elements, fusing them into an integrated whole. Incompleteness is a major theme of systems theory, which also explicitly examines the relations between wholes and parts and offers a formal framework for expressing such fusions. In this article, the systems character of Parts I & II of the Star is explored through extensive use of diagrams; a systems exploration of Part III is left for future work. Remarkably, given its highly architectonic character, diagrams are absent in Rosenzweig’s book, except for the triangle of elements, the triangle of relations, and the hexadic star, which are presented on the opening page of each part of the book. While structures can be explicated entirely in words, diagrams are a visual medium of communication that supplements words and supports a nonverbal understanding that structures both thought and experience. (shrink)

Is there a notion of contradiction—let us call it, for dramatic effect, “absolute”—making all contradictions, so understood, unacceptable also for dialetheists? It is argued in this paper that there is, and that spelling it out brings some theoretical benefits. First it gives us a foothold on undisputed ground in the methodologically difficult debate on dialetheism. Second, we can use it to express, without begging questions, the disagreement between dialetheists and their rivals on the nature of truth. Third, dialetheism has an (...) operator allowing it, against the opinion of many critics, to rule things out and manifest disagreement: for unlike other proposed exclusion-expressing-devices (for instance, the entailment of triviality), the operator used to formulate the notion of absolute contradiction appears to be immune both from crippling expressive limitations and from revenge paradoxes—pending a rigorous nontriviality proof for a formal dialetheic theory including it. (shrink)

The central hypothesis of the collaboration between Language and Computing (L&C) and the Institute for Formal Ontology and Medical Information Science (IFOMIS) is that the methodology and conceptual rigor of a philosophically inspired formal ontology will greatly benefit software application ontologies. To this end LinKBase®, L&C’s ontology, which is designed to integrate and reason across various external databases simultaneously, has been submitted to the conceptual demands of IFOMIS’s Basic Formal Ontology (BFO). With this, we aim to move beyond the level (...) of controlled vocabularies to yield an ontology with the ability to support reasoning applications. (shrink)

In a first part, I defend that formal semantics can be used as a guide to ontological commitment. Thus, if one endorses an ontological view \(O\) and wants to interpret a formal language \(L\) , a thorough understanding of the relation between semantics and ontology will help us to construct a semantics for \(L\) in such a way that its ontological commitment will be in perfect accordance with \(O\) . Basically, that is what I call constructing formal semantics from an (...) ontological perspective. In the rest of the paper, I develop rigorously and put into practice such a method, especially concerning the interpretation of second-order quantification. I will define the notion of ontological framework: it is a set-theoretical structure from which one can construct semantics whose ontological commitments correspond exactly to a given ontological view. I will define five ontological frameworks corresponding respectively to: (i) predicate nominalism, (ii) resemblance nominalism, (iii) armstrongian realism, (iv) platonic realism, and (v) tropism. From those different frameworks, I will construct different semantics for first-order and second-order languages. Notably I will present different kinds of nominalist semantics for second-order languages, showing thus that we can perfectly quantify over properties and relations while being ontologically committed only to individuals. I will show in what extent those semantics differ from each other; it will make clear how the disagreements between the ontological views extend from ontology to logic, and thus why endorsing an ontological view should have an impact on the kind of logic one should use. (shrink)

Cantor’s proof that the powerset of the set of all natural numbers is uncountable yields a version of Richard’s paradox when restricted to the full definable universe, that is, to the universe containing all objects that can be defined not just in one formal language but by means of the full expressive power of natural language: this universe seems to be countable on one account and uncountable on another. We argue that the claim that definitional contexts impose restrictions on the (...) scope of quantifiers reveals a natural way out. (shrink)

This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of Hughes and Cresswell, but the system, based on a different choice of axioms, is better described as a Mendelson system augmented with axiom schemes for K, T, S4, and B, and the necessitation rule as a rule of inference. The language has the false and implication as the only primitive (...) logical connectives and necessity as the only primitive modal operator. The full source code is available online and has been typechecked with Lean 3.4.2. (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)

A teaching document I've used in my courses on truth and on incompleteness. Aimed at students who have a good grasp of basic logic, and decent math skills, it attempts to give them the background they need to understand a proper statement of the classic results due to Gödel and Tarski, and sketches their proofs. Topics covered include the notions of language and theory, the basics of formal syntax and arithmetization, formal arithmetic (Q and PA), representability, diagonalization, and the incompleteness (...) and undefinability theorems. (shrink)

This paper considers logics which are formally dual to intuitionistic logic in order to investigate a co-constructive logic for proofs and refutations. This is philosophically motivated by a set of problems regarding the nature of constructive truth, and its relation to falsity. It is well known both that intuitionism can not deal constructively with negative information, and that defining falsity by means of intuitionistic negation leads, under widely-held assumptions, to a justification of bivalence. For example, we do not want to (...) equate falsity with the non-existence of a proof since this would render a statement such as “pi is transcendental” false prior to 1882. In addition, the intuitionist account of negation as shorthand for the derivation of absurdity is inadequate, particularly outside of purely mathematical contexts. To deal with these issues, I investigate the dual of intuitionistic logic, co-intuitionistic logic, as a logic of refutation, alongside intuitionistic logic of proofs. Direct proof and refutation are dual to each other, and are constructive, whilst there also exist syntactic, weak, negations within both logics. In this respect, the logic of refutation is weakly paraconsistent in the sense that it allows for statements for which, neither they, nor their negation, are refuted. I provide a proof theory for the co-constructive logic, a formal dualizing map between the logics, and a Kripke-style semantics. This is given an intuitive philosophical rendering in a re-interpretation of Kolmogorov’s logic of problems. (shrink)

The discussions which follow rest on a distinction, first expounded by Husserl, between formal logic and formal ontology. The former concerns itself with (formal) meaning-structures; the latter with formal structures amongst objects and their parts. The paper attempts to show how, when formal ontological considerations are brought into play, contemporary extensionalist theories of part and whole, and above all the mereology of Leniewski, can be generalised to embrace not only relations between concrete objects and object-pieces, but also relations between what (...) we shall call dependent parts or moments. A two-dimensional formal language is canvassed for the resultant ontological theory, a language which owes more to the tradition of Euler, Boole and Venn than to the quantifier-centred languages which have predominated amongst analytic philosophers since the time of Frege and Russell. Analytic philosophical arguments against moments, and against the entire project of a formal ontology, are considered and rejected. The paper concludes with a brief account of some applications of the theory presented. (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)

I explain why model theory is unsatisfactory as a semantic theory and has drawbacks as a tool for proofs on logic systems. I then motivate and develop an alternative, the truth-valuational substitutional approach (TVS), and prove with it the soundness and completeness of the first order Predicate Calculus with identity and of Modal Propositional Calculus. Modal logic is developed without recourse to possible worlds. Along the way I answer a variety of difficulties that have been raised against TVS and show (...) that, as applied to several central questions, model-theoretic semantics can be considered TVS in disguise. The conclusion is that the truth-valuational substitutional approach is an adequate tool for many of our logic inquiries, conceptually preferable over model-theoretic semantics. Another conclusion is that formal logic is independent of semantics, apart from its use of the notion of truth, but that even with respect to it its assumptions are minimal. (shrink)

Husserl (a mathematician by education) remained a few famous and notable philosophical “slogans” along with his innovative doctrine of phenomenology directed to transcend “reality” in a more general essence underlying both “body” and “mind” (after Descartes) and called sometimes “ontology” (terminologically following his notorious assistant Heidegger). Then, Husserl’s tradition can be tracked as an idea for philosophy to be reinterpreted in a way to be both generalized and mathenatizable in the final analysis. The paper offers a pattern borrowed from the (...) theory of information and quantum information (therefore relating philosophy to both mathematics and physics) to formalize logically a few key concepts of Husserl’s phenomenology such as “epoché” “eidetic, phenomenological, and transcendental reductions” as well as the identification of “phenomenological, transcendental, and psychological reductions” in a way allowing for that identification to be continued to “eidetic reduction” (and thus to mathematics). The approach is tested by an independent and earlier idea of Husserl, “logical arithmetic” (parallelly implemented in mathematics by Whitehead and Russell’s Principia) as what “Hilbert arithmetic” generalizing Peano arithmetics is interpreted. A basic conclusion states for the unification of philosophy, mathematics, and physics in their foundations and fundamentals to be the Husserl tradition both tracked to its origin (in the being itself after Heidegger or after Husserl’s “zu Sache selbst”) and embodied in the development of human cognition in the third millennium. (shrink)

In this paper we give some formal examples of ideas developed by Penco in two papers on the tension inside Frege's notion of sense (see Penco 2003). The paper attempts to compose the tension between semantic and cognitive aspects of sense, through the idea of sense as proof or procedure – not as an alternative to the idea of sense as truth condition, but as complementary to it (as it happens sometimes in the old tradition of procedural semantics).

From the beginning of the 16th century to the end of the 18th century, there were not less than ten philosophers who focused extensively on Venn’s ostensible analytical diagrams, as noted by modern historians of logic (Venn, Gardner, Baron, Coumet et al.). But what was the reason for early modern philosophers to use logic or analytical diagrams? Among modern historians of logic one can find two theses which are closely connected to each other: M. Gardner states that since the Middle (...) Ages certain logic diagrams were used just in order to teach “dull-witted students”. Therefore, logic diagrams were just a means to an end. According to P. Bernhard, the appreciation of logic diagrams had not started prior to the 1960s, therefore the fact that logic diagrams become an end the point of research arose very late. The paper will focus on the question whether logic resp. analytical diagrams were just means in the history of (early) modern logic or not. In contrast to Gardner, I will argue that logic diagrams were not only used as a tool for “dull-witted students”, but rather as a tool used by didactic reformers in early modern logic. In predating Bernhard’s thesis, I will argue that in the 1820s logic diagrams had already become a value in themselves in Arthur Schopenhauer’s lectures on logic, especially in proof theory. (shrink)

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 conventional notion of a formal system is adapted to conform to the sound deductive inference model operating on finite strings. Finite strings stipulated to have the semantic property of Boolean true provide the sound deductive premises. Truth preserving finite string transformation rules provide valid the deductive inference. Conclusions of sound arguments are derived from truth preserving finite string transformations applied to true premises.