Interactive theorem provers might seem particularly impractical in the history of philosophy. Journal articles in this discipline are generally not formalized. Interactive theorem provers involve a learning curve for which the payoffs might seem minimal. In this article I argue that interactive theorem provers have already demonstrated their potential as a useful tool for historians of philosophy; I do this by highlighting examples of work where this has already been done. Further, I argue that interactive theorem provers can continue to (...) be useful tools for historians of philosophy in the future; this claim is defended through a more conceptual analysis of what historians of philosophy do that identifies argument reconstruction as a core activity of such practitioners. It is then shown that interactive theorem provers can assist in this core practice by a description of what interactive theorem provers are and can do. If this is right, then computer verification for historians of philosophy is in the offing. (shrink)

Revised version of chapter in J. N. Mohanty and W. McKenna (eds.), Husserl’s Phenomenology: A Textbook, Lanham: University Press of America, 1989, 29–67. -/- Logic for Husserl is a science of science, a science of what all sciences have in common in their modes of validation. Thus logic deals with universal laws relating to truth, to deduction, to verification and falsification, and with laws relating to theory as such, and to what makes for theoretical unity, both on the side (...) of the propositions of a theory and on the side of the domain of objects to which these propositions refer. This essay presents a systematic overview of Husserl’s views on these matters as put forward in his Logical Investigations. It shows how Husserl’s theory of linguistic meanings as species of mental acts, his formal ontology of part, whole and dependence, his theory of meaning categories, and his theory of categorial intuition combine with his theory of science to form a single whole. Finally, it explores the ways in which Husserl’s ideas on these matters can be put to use in solving problems in the philosophy of language, logic and mathematics in a way which does justice to the role of mental activity in each of these domains while at the same time avoiding the pitfalls of psychologism. (shrink)

Over the last decade, multi-agent systems have come to form one of the key tech- nologies for software development. The Formal Approaches to Multi-Agent Systems (FAMAS) workshop series brings together researchers from the fields of logic, theoreti- cal computer science and multi-agent systems in order to discuss formal techniques for specifying and verifying multi-agent systems. FAMAS addresses the issues of logics for multi-agent systems, formal methods for verification, for example model check- ing, and formal approaches (...) to cooperation, multi-agent planning, communication, coordination, negotiation, games, and reasoning under uncertainty in a distributed environment. In 2007, the third FAMAS workshop, FAMAS'007, was one of the agent workshops gathered together under the umbrella of Multi-Agent Logics, Languages, and Organ- isations - Federated Workshops, MALLOW'007, taking place from 3 to 7 September 2007 in Durham. This current special issue of the Logic Journal of the IGPL gathers together the revised and updated versions of the five best FAMAS'007 contributions. (shrink)

The formal and empirical-generative perspectives of computation are demonstrated to be inadequate to secure the goals of simulation in the social sciences. Simulation does not resemble formal demonstrations or generative mechanisms that deductively explain how certain models are sufficient to generate emergent macrostructures of interest. The description of scientific practice implies additional epistemic conceptions of scientific knowledge. Three kinds of knowledge that account for a comprehensive description of the discipline were identified: formal, empirical and intentional knowledge. The (...) use of formal conceptions of computation for describing simulation is refuted; the roles of programming languages according to intentional accounts of computation are identified; and the roles of iconographic programming languages and aesthetic machines in simulation are characterized. The roles that simulation and intentional decision making may be able to play in a participative information society are also discussed. (shrink)

This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic with (...) implication, conjunction, disjunction, and falsity given in terms of a Hilbert-style axiomatization. As far as we know, our implementation is the first verified Henkin-style proof of completeness for intuitionistic logic following Troelstra and van Dalen's method in the literature. (shrink)

The field of AI has undergone a series of transformations, each marking a new phase of development. The initial phase emphasized curation of symbolic models which excelled in capturing reasoning but were fragile and not scalable. The next phase was characterized by machine learning models—most recently large language models (LLMs)—which were more robust and easier to scale but struggled with reasoning. Now, we are witnessing a return to symbolic models as complementing machine learning. Successes of LLMs contrast with their inscrutability, (...) inaccuracy, and hallucinations, which underwrite concerns over the reliability and trustworthiness of these systems, motivating investigations into commonsense reasoning, AI explainability, and formal verification techniques. Moreover, proper assessments of hybrid machine learning/symbolic systems require novel strategies to facilitate comparisons of performance and guide future AI progress. The EDGeS AAAI 2023 Spring symposium brought together researchers focusing on novel assessments and benchmarks for evaluating hybrid and artificial general intelligence (AGI) systems. This symposium revealed what was already suspected: research concerning evaluation of machine learning/symbolic hybrids and AGI is, unfortunately, lacking. Even so, the discussion was fruitful. (shrink)

It is widely taken that the first-order part of Frege's Begriffsschrift is complete. However, there does not seem to have been a formal verification of this received claim. The general concern is that Frege's system is one axiom short in the first-order predicate calculus comparing to, by now, the standard first-order theory. Yet Frege has one extra inference rule in his system. Then the question is whether Frege's first-order calculus is still deductively sufficient as far as the first-order (...) completeness is concerned. In this short note we confirm that the missing axiom is derivable from his stated axioms and inference rules, and hence the logic system in the Begriffsschrift is indeed first-order complete. (shrink)

Gödel's incompleteness theorems establish the stunning result that mathematics cannot be fully formalized and, further, that any formal system containing a modicum of number or set theory cannot establish its own consistency. Wilfried Sieg and Clinton Field, in their paper Automated Search for Gödel's Proofs, presented automated proofs of Gödel's theorems at an abstract axiomatic level; they used an appropriate expansion of the strategic considerations that guide the search of the automated theorem prover AProS. The representability conditions that allow (...) the syntactic notions of the metalanguage to be represented inside the object language were taken as axioms in the automated proofs. The concrete task I am taking on in this project is to extend the search by formally verifying these conditions. Using a formal metatheory defined in the language of binary trees, the syntactic objects of the metatheory lend themselves naturally to a direct encoding in Zermelo's theory of sets. The metatheoretic notions can then be inductively defined and shown to be representable in the object-theory using appropriate inductive arguments. Formal verification of the representability conditions is the first step towards an automated proof thereof which, in turn, brings the automated verification of Gödel's theorems one step closer to completion. (shrink)

Logic has pride of place in mathematics and its 20th century offshoot, computer science. Modern symbolic logic was developed, in part, as a way to provide a formal framework for mathematics: Frege, Peano, Whitehead and Russell, as well as Hilbert developed systems of logic to formalize mathematics. These systems were meant to serve either as themselves foundational, or at least as formal analogs of mathematical reasoning amenable to mathematical study, e.g., in Hilbert’s consistency program. Similar efforts continue, but (...) have been expanded by the development of sophisticated methods to study the properties of such systems using proof and model theory. In parallel with this evolution of logical formalisms as tools for articulating mathematical theories (broadly speaking), much progress has been made in the quest for a mechanization of logical inference and the investigation of its theoretical limits, culminating recently in the development of new foundational frameworks for mathematics with sophisticated computer-assisted proof systems. In addition, logical formalisms developed by logicians in mathematical and philosophical contexts have proved immensely useful in describing theories and systems of interest to computer scientists, and to some degree, vice versa. Three examples of the influence of logic in computer science are automated reasoning, computer verification, and type systems for programming languages. (shrink)

The classical theory of computation does not represent an adequate model of reality for simulation in the social sciences. The aim of this paper is to construct a methodological perspective that is able to conciliate the formal and empirical logic of program verification in computer science, with the interpretative and multiparadigmatic logic of the social sciences. We attempt to evaluate whether social simulation implies an additional perspective about the way one can understand the concepts of program and computation. (...) We demonstrate that the logic of social simulation implies at least two distinct types of program verifications that reflect an epistemological distinction in the kind of knowledge one can have about programs. Computer programs seem to possess a causal capability (Fetzer, 1999) and an intentional capability that scientific theories seem not to possess. This distinction is associated with two types of program verification, which we call empirical and intentional verification. We demonstrate, by this means, that computational phenomena are also intentional phenomena, and that such is particularly manifest in agent-based social simulation. Ascertaining the credibility of results in social simulation requires a focus on the identification of a new category of knowledge we can have about computer programs. This knowledge should be considered an outcome of an experimental exercise, albeit not empirical, acquired within a context of limited consensus. The perspective of intentional computation seems to be the only one possible to reflect the multiparadigmatic character of social science in terms of agent-based computational social science. We contribute, additionally, to the clarification of several questions that are found in the methodological perspectives of the discipline, such as the computational nature, the logic of program scalability, and the multiparadigmatic character of agent-based simulation in the social sciences. (shrink)

This paper is concerned with the construction of theories of software systems yielding adequate predictions of their target systems’ computations. It is first argued that mathematical theories of programs are not able to provide predictions that are consistent with observed executions. Empirical theories of software systems are here introduced semantically, in terms of a hierarchy of computational models that are supplied by formal methods and testing techniques in computer science. Both deductive top-down and inductive bottom-up approaches in the discovery (...) of semantic software theories are refused to argue in favour of the abductive process of hypothesising and refining models at each level in the hierarchy, until they become satisfactorily predictive. Empirical theories of computational systems are required to be modular, as modular are most software verification and testing activities. We argue that logic relations must be thereby defined among models representing different modules in a semantic theory of a modular software system. We exclude that scientific structuralism is able to define module relations needed in software modular theories. The algebraic Theory of Institutions is finally introduced to specify the logic structure of modular semantic theories of computational systems. (shrink)

Logical and philosophical literature provides different classifications of reasoning. In the Polish literature on the subject, for instance, there are three popular ones accepted by representatives of the Lvov-Warsaw School: Jan Łukasiewicz, Tadeusz Czeżowski and Kazimierz Ajdukiewicz (Ajdukiewicz in Logika pragmatyczna [Pragmatic Logic]. PWN, Warsaw (1965, 2nd ed. 1974). Translated as: Pragmatic Logic. Reidel & PWN, Dordrecht, 1975). The author of this paper, having modified those classifications, distinguished the following types of reasoning: (1) deductive and (2) non-deductive, and additionally two (...) types of them in each of the two, depending on the manner of combining their premises with the conclusion through the relation of classical logical entailment. Consequently, the four types of reasoning: unilateral deductive (incl. its sub-types: deductive inference and proof), bilateral deductive (incl. complete induction), and reductive (incl. the sub-types: explanation and verification), logically nonvaluable (incl. inference by analogy, statistic inference), correspond to four operators of derivability. They are defined formally on the ground of Tarski’s axiomatic theory of deductive systems, by means of the consequence operation _Cn_ (Tarski in Monatshefte Math Phys 37:361–404, 1930a, C R Soc Sci Lett Vars 23:22–29, 1930b). Also, certain metalogical properties of these operators are given, as well as their relations with Tarski’s consequence operations \(Cn^+\) ( \(Cn^+ = Cn\) ) and dual consequences \(Cn^{-1}\) (Słupecki in Zeszyty Naukowe Uniwersytetu Wrocławskiego Seria B Nr 3:33–40, 1959, Słupecki et al. in Stud Log 29:76–123, 1971, Wybraniec-Skardowska, in: Wybraniec-Skardowska, Bryll (eds) Z badań nad teorią zdań odrzuconych [Studies in the Theory of Rejected Propositions], Series B, Studia i Monografie, Zeszyty Naukowe Wyższej Szkoły Pedagogicznej w Opolu, Opole, 1969), and \(Cn^-\) (Wójcicki in Bull Sect Log 2(2):54–57, 1973)). (shrink)

The host of SUSY(supersymmetry) based string theories is considered. Superstrings are comprehended as possible candidates on Quantum Gravity basic objects. It is argued that superstring theories constitute mainly mathematical progress and can reconcile general relativity with quantum field theory at best. Yet they cannot provide the genuine synthesis. Superstring unification of all the four forces at hand is a formal one . It is contended that genesis and proliferation of superstrings can better be described not by philosophy of science (...) models but in terms of modern sociology of science. The formal character of gravity and quantum fields fusion and the lack of experimental verification make the transition to superstring theories ad hoc in Lakatosian standards. Possible way of explanation is proposed based on social interests conception of Andrew Pickering. -/- Key words: superstrings, unification, Kaluza-Klein, sociology of science . (shrink)

The connection between science and mathematics is often considered necessary and insoluble. Therefore, a relationship between mathematics and humanities or arts is deemed exceptional or sometimes unnatural. Nevertheless, on the basis of historical, ontological and epistemological researches it can be noted that it’s impossible to warrant the immediate identification between mathematics and sciences on a deeper level than the practical one. Given the instrumentality and then the unnecessity of this connection, the relationship between mathematics and not-scientific disciplines is undeniable, even (...) if the mathematics in the explicit formalisms which we know doesn’t appear in them. It’s possible to demonstrate this relationship not only with philosophical argumentations, but also whit empirical verifications, e.g. in the music and in particular in the music of J. S. Bach. Such an epistemological thought finally leads to the question on the possibility of knowledge in the art in comparison to the epistemological characteristics of the Galilean and Post-Galilean science. (shrink)

The new phase of science evolution is characterized by totality of subject and object of cognition and technology (high-hume). As a result, forming of network structure in a disciplinary matrix modern are «human dimensional» natural sciences and two paradigmal «nuclei» (attraktors). As a result, the complication of structure of disciplinary matrix and forming a few paradigm nuclei in modern «human dimensional» natural sciences are observed. In the process of social verification integration of scientific theories into the existent system of (...) mental and valued options of spiritual culture takes place. The attribute of classical science – ethics neutrality of scientific knowledge becomes an unattainable ideal. One of the trends in the evolution of theoretical epistemology is the study of migration mechanisms of generation of scientific knowledge from the sphere of its own logic and methodology of science in the field of sociology - the consideration of this process, as the resulting system of interactions of social structures and institutions. Ensuing ideas and settings become the dominant worldview of philosophical and technological civilization. -/- . (shrink)

The new phase of science evolution is characterized by totality of subject and object of cognition and technology (high-hume). As a result, forming of network structure in a disciplinary matrix modern are «human dimensional» natural sciences and two paradigmal «nuclei» (attraktors). As a result, the complication of structure of disciplinary matrix and forming a few paradigm nuclei in modern «human dimensional» natural sciences are observed. In the process of social verification integration of scientific theories into the existent system of (...) mental and valued options of spiritual culture takes place. The attribute of classical science – ethics neutrality of scientific knowledge becomes an unattainable ideal. One of the trends in the evolution of theoretical epistemology is the study of migration mechanisms of generation of scientific knowledge from the sphere of its own logic and methodology of science in the field of sociology - the consideration of this process, as the resulting system of interactions of social structures and institutions. Ensuing ideas and settings become the dominant worldview of philosophical and technological civilization. -/- . (shrink)

This paper investigates the strange case of an argument that was directed against a positivist verification principle. We find an early occurrence of the argument in a talk by the phenomenologist Roman Ingarden at the 1934 International Congress of Philosophy in Prague, where Carnap and Neurath were present and contributed short rejoinders. We discuss the underlying presuppositons of the argument, and we evaluate whether the attempts by Carnap (especially) actually succeed in answering this argument. We think they don’t, and (...) offer instead a few sociological thoughts about why the argument seems to have disappeared from the profession’s evaluaton of the positivist criterion of verifiability. (shrink)

This article explores some open questions related to the problem of verification of theories in the context of empirical sciences by contrasting three epistemological frameworks. Each of these epistemological frameworks is based on a corresponding central metaphor, namely: (a) Neo-empiricism and the gambling metaphor; (b) Popperian falsificationism and the scientific tribunal metaphor; (c) Cognitive constructivism and the object as eigen-solution metaphor. Each of one of these epistemological frameworks has also historically co-evolved with a certain statistical theory and method for (...) testing scientific hypotheses, respectively: (a) Decision theoretic Bayesian statistics and Bayes factors; (b) Frequentist statistics and p-values; (c) Constructive Bayesian statistics and e-values. This article examines with special care the Zero Probability Paradox (ZPP), related to the verification of sharp or precise hypotheses. Finally, this article makes some remarks on Lakatos’ view of mathematics as a quasi-empirical science. (shrink)

The new phase of science evolution is characterized by totality of subject and object of cognition and technology (high-hume). As a result, forming of network structure in a disciplinary matrix modern are «human dimensional» natural sciences and two paradigmal «nuclei» (attraktors). As a result, the complication of structure of disciplinary matrix and forming a few paradigm nuclei in modern «human dimensional» natural sciences are observed.

Every person has his/her own unique signature that is used mainly for the purposes of personal identification and verification of important documents or legal transactions. There are two kinds of signature verification: static and dynamic. Static(off-line) verification is the process of verifying an electronic or document signature after it has been made, while dynamic(on-line) verification takes place as a person creates his/her signature on a digital tablet or a similar device. Offline signature verification is not (...) efficient and slow for a large number of documents. To overcome the drawbacks of offline signature verification, we have seen a growth in online biometric personal verification such as fingerprints, eye scan etc. In this paper we created CNN model using python for offline signature and after training and validating, the accuracy of testing was 99.70%. (shrink)

Formal ontology as a main branch of metaphysics investigates categories of being. In the formal ontological approach to metaphysics, these ontological categories are analysed by ontological forms. This analysis, which we illustrate by some category systems, provides a tool to assess the clarity, exactness and intelligibility of different category systems or formal ontologies. We discuss critically different accounts of ontological form in the literature. Of ontological form, we propose a character- neutral relational account. In this metatheory, ontological (...) forms of entities are their standings in internal relations whose holding is neutral on the character of their relata. These relations are “formal ontological relations”. Entities belong to ontological categories because they stand in the same formal ontological relations. We hold a nominalist relationalism about ontological categories and forms. We conclude by showing that our metatheory is useful for understanding categorial fundamentality/non- fundamentality, different formal ontologies, and for unifying metaphysical questions. (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)

Two interconnected surveys are presented, one of artifacts and one of designometry. Artifacts are objects, which have an originator and do not exist in nature. Designometry is a new field of study, which aims to identify the originators of artifacts. The space of artifacts is described and also domains, which pursue designometry, yet currently doing so without collaboration or common methodologies. On this basis, synergies as well as a generic axiom and heuristics for the quest of the creators of artifacts (...) are introduced. While designometry has various areas of applications, the research of methods to detect originators of artificial minds, which constitute a subgroup of artifacts, can be seen as particularly relevant and, in the case of malevolent artificial minds, as contribution to AI safety. (shrink)

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)

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.

I argue that normative formal epistemology (NFE) is best understood as modelling, in the sense that this is the reconstruction of its methodology on which NFE is doing best. I focus on Bayesianism and show that it has the characteristics of modelling. But modelling is a scientific enterprise, while NFE is normative. I thus develop an account of normative models on which they are idealised representations put to normative purposes. Normative assumptions, such as the transitivity of comparative credence, are (...) characterised as modelling idealisations motivated normatively. I then survey the landscape of methodological options: what might formal epistemologists be up to? I argue the choice is essentially binary: modelling or theorising. If NFE is theorising it is doing very poorly: generating false claims with no clear methodology for separating out what is to be taken seriously. Modelling, by contrast, is a successful methodology precisely suited to the management of useful falsehoods. Regarding NFE as modelling is not costless, however. First, our normative inferences are less direct and are muddied by the presence of descriptive idealisations. Second, our models are purpose-specific and limited in their scope. I close with suggestions for how to adapt our practice. (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)

In the era of “big data,” science is increasingly information driven, and the potential for computers to store, manage, and integrate massive amounts of data has given rise to such new disciplinary fields as biomedical informatics. Applied ontology offers a strategy for the organization of scientific information in computer-tractable form, drawing on concepts not only from computer and information science but also from linguistics, logic, and philosophy. This book provides an introduction to the field of applied ontology that is of (...) particular relevance to biomedicine, covering theoretical components of ontologies, best practices for ontology design, and examples of biomedical ontologies in use. After defining an ontology as a representation of the types of entities in a given domain, the book distinguishes between different kinds of ontologies and taxonomies, and shows how applied ontology draws on more traditional ideas from metaphysics. It presents the core features of the Basic Formal Ontology (BFO), now used by over one hundred ontology projects around the world, and offers examples of domain ontologies that utilize BFO. The book also describes Web Ontology Language (OWL), a common framework for Semantic Web technologies. Throughout, the book provides concrete recommendations for the design and construction of domain ontologies. (shrink)

Inspired by impossibility theorems of social choice theory, many democratic theorists have argued that aggregative forms of democracy cannot lend full democratic justification for the collective decisions reached. Hence, democratic theorists have turned their attention to deliberative democracy, according to which “outcomes are democratically legitimate if and only if they could be the object of a free and reasoned agreement among equals” (Cohen 1997a, 73). However, relatively little work has been done to offer a formal theory of democratic deliberation. (...) This article helps fill that gap by offering a formal theory of three different modes of democratic deliberation: myopic discussion, constructive discussion, and debate. We show that myopic discussion suffers from indeterminacy of long run outcomes, while constructive discussion and debate are conclusive. Finally, unlike the other two modes of deliberation, debate is path independent and converges to a unique compromise position, irrespective of the initial status quo. (shrink)

Ontology and theology cannot be combined if ontology excludes non physical causes. This paper examines some possibilities for ontology to be combined with theology in so far as non physical causes are permitted. The paper builds on metaphysical findings that shows that separate ontological domains can interact causally indirectly via interfaces. As interfaces are not universes a first universe is allowed to be caused by an interface without violating the principle of causal closure of any universe. Formal theology can (...) therefore be based on the assumption that the (first) universe is caused by God if God is defined as the first cause. Given this, formal theology and science can have the same ontological base. (shrink)

This paper reviews the central points and presents some recent developments of the epistemic approach to paraconsistency in terms of the preservation of evidence. Two formal systems are surveyed, the basic logic of evidence (BLE) and the logic of evidence and truth (LET J ), designed to deal, respectively, with evidence and with evidence and truth. While BLE is equivalent to Nelson’s logic N4, it has been conceived for a different purpose. Adequate valuation semantics that provide decidability are given (...) for both BLE and LET J . The meanings of the connectives of BLE and LET J , from the point of view of preservation of evidence, is explained with the aid of an inferential semantics. A formalization of the notion of evidence for BLE as proposed by M. Fitting is also reviewed here. As a novel result, the paper shows that LET J is semantically characterized through the so-called Fidel structures. Some opportunities for further research are also discussed. (shrink)

We propose a formal framework for interpretable machine learning. Combining elements from statistical learning, causal interventionism, and decision theory, we design an idealised explanation game in which players collaborate to find the best explanation for a given algorithmic prediction. Through an iterative procedure of questions and answers, the players establish a three-dimensional Pareto frontier that describes the optimal trade-offs between explanatory accuracy, simplicity, and relevance. Multiple rounds are played at different levels of abstraction, allowing the players to explore overlapping (...) causal patterns of variable granularity and scope. We characterise the conditions under which such a game is almost surely guaranteed to converge on a optimal explanation surface in polynomial time, and highlight obstacles that will tend to prevent the players from advancing beyond certain explanatory thresholds. The game serves a descriptive and a normative function, establishing a conceptual space in which to analyse and compare existing proposals, as well as design new and improved solutions. (shrink)

Although formal thought disorder (FTD) has been for long a clinical label in the assessment of some psychiatric disorders, in particular of schizophrenia, it remains a source of controversy, mostly because it is hard to say what exactly the “formal” in FTD refers to. We see anomalous processing of terminological knowledge, a core construct of human knowledge in general, behind FTD symptoms and we approach this anomaly from a strictly formal perspective. More specifically, we present here a (...) symbolic computational model of storage in, and activation of, a human semantic network, or semantic memory, whose core element is logical form; this is normalized by description logic (DL), namely by CL, a DL-based language – Conception Language – designed to formalize conceptualization from the viewpoint of individual cognitive agency. In this model, disruptions in the rule-based implementation of the logical form account for the apparently semantic anomalies symptomatic of FTD, which are detected by means of a CL-based algorithmic assessment. (shrink)

I argue that Aristotle’s account of scientific demonstrations in the Posterior Analytics is centred upon formal causation, understood as a demonstration in terms of essence (and as innocent of the distinction between form and matter). While Aristotle says that all four causes can be signified by the middle term in a demonstrative syllogism, and he discusses at some length efficient causation, much of Aristotle’s discussion is foremost concerned with the formal cause. Further, I show that Aristotle had very (...) detailed procedures for identifying the formal cause, and that he is aware of several problems which might lead one to erroneously identify the wrong form as the cause of a property. Finally, I show that Aristotle’s account can easily be adapted to material causation, and through some modifications (introduction of process universals related through parthood), hinted at in II 11-12 and 16-17, to efficient and final causation. (shrink)

This book is a collection of articles dealing with criticisms of Robert S. Hartman’s theory of formal axiology. During his lifetime, Hartman wrote responses to many of his critics. Some of these were previously published but many are published here for the first time. In particular, published here are Hartman’s replies to such critics as Hector Neri Castañeda, Charles Hartshorne, Rem B. Edwards, Robert E. Carter, G. R. Grice, Nicholas Rescher, Robert W. Mueller, Gordon Welty, Pete Gunter, George Kimball (...) Plochmann, William Eckhardt, and Robert S. Brumbaugh. Crticial essays and responses to them developed by Rem B. Edwards, Frank G. Forrest, and Mark A. Moore after Hartman’s untimely death in 1973 are also included. (shrink)

It is commonly said that some standards, such as morality, are ‘normatively authoritative’ in a way that other standards, such as etiquette, are not; standards like etiquette are said to be ‘not really normative’. Skeptics deny the very possibility of normative authority, and take claims like ‘etiquette is not really normative’ to be either empty or confused. I offer a different route to defeat skeptics about authority: instead of focusing on what makes standards like morality special, we should focus on (...) what makes standards like etiquette ‘not really normative’. I defend a fictionalist theory on which etiquette is ‘not really normative’ in roughly the same way that Sherlock is ‘not really a detective’, and show that fictionalism about some normative standards helps us explain the possibility of normative authority. (shrink)

I defend J. L. Austin's direct realism against the colour delusion argument by employing epistemic logic to demonstrate that perceiving colours does not necessitate an intermediary such as sense-data, thus preserving the directness of perception.

(This is for the Cambridge Handbook of Analytic Philosophy, edited by Marcus Rossberg) In this handbook entry, I survey the different ways in which formal mathematical methods have been applied to philosophical questions throughout the history of analytic philosophy. I consider: formalization in symbolic logic, with examples such as Aquinas’ third way and Anselm’s ontological argument; Bayesian confirmation theory, with examples such as the fine-tuning argument for God and the paradox of the ravens; foundations of mathematics, with examples such (...) as Hilbert’s programme and Gödel’s incompleteness theorems; social choice theory, with examples such as Condorcet’s paradox and Arrow’s theorem; ‘how possibly’ results, with examples such as Condorcet’s jury theorem and recent work on intersectionality theory; and the application of advanced mathematics in philosophy, with examples such as accuracy-first epistemology. (shrink)

This paper offers a response to William’s Hanson’s criticism of Sher’s formal-structural conception of logical consequence and logical constants.

Très souvent, on compte sur la science pour nous sauver. Le rapport qu'on établit avec elle peut donner à penser que la science parlerait ainsi de choses, validerait quelque chose comme des évidences immédiates. La connaissance scientifique est inférentielle. Si elle a un objet, ce qu'en rigueur de termes la philosophie n'a pas, elle doit néanmoins se mettre à distance de lui pour se faire science. Elle valide ainsi des schèmes abstraits, qui ne sont scientifiques que dans cette mesure. Nous (...) prendrons la mesure du fait que pour nous aider à retrouver le concret, l'intuition est meilleure guide que la science, et puis nous convoquerons certaines idées de l'algébriste et métaphysicien Alfred North Whitehead dont l'actualité ne cesse d'étonner, lorsqu'il inverse l'accès direct au réel, à l'envers de la vulgate reçue concernant les rapports entre science et religion. (shrink)

The purpose of this introduction is to give a rough overview of the discussion of the formalization of arguments, focusing on deductive arguments. The discussion is structured around four important junctions: i) the notion of support, which captures the relation between the conclusion and premises of an argument, ii) the choice of a formal language into which the argument is translated in order to make it amenable to evaluation via formal methods, iii) the question of quality criteria for (...) such formalizations, and finally iv) the choice of the underlying logic. This introductory discussion is supplemented by a brief description of the genesis of the special issue, acknowledgements, and summaries of each article. (shrink)

What is a fact ? Are there such things ?

This paper introduces the special issue on Formal Approaches to the Ontological Argument of the Journal of Applied Logics (College Publications). The issue contains the following articles: Formal Approaches to the Ontological Argument, by Ricardo Sousa Silvestre and Jean-Yves Béziau; A Brief Critical Introduction to the Ontological Argument and its Formalization: Anselm, Gaunilo, Descartes, Leibniz and Kant, by Ricardo Sousa Silvestre; A Mechanically Assisted Examination of Begging the Question in Anselm’s Ontological Argument, by John Rushby; A Tractarian Resolution (...) to the Ontological Argument, by Erik Thomsen; On Kant’s Hidden Ambivalence Toward Existential Generalization in his Critique of the Ontological Argument, by Giovanni Mion; The Totality of Predicates and the Possibility of the Most Real Being, by Srećko Kovač; An Even More Leibnizian Version of Gödel’s Ontological Argument, by Kordula Świętorzecka and Marcin Łyczak; A Case Study On Computational Hermeneutics: E. J. Lowe’s Modal Ontological Argument, by David Fuenmayor. (shrink)

In this paper we examine whether and how powers ontologies can back formal causation. We attempt to answer three questions: i) what is formal causation; ii) whether we need formal causation, and iii) whether formal causation need powers and whether it can be grounded in powers. We take formal causal explanations to be explanations in which something's essence features prominently in the explanans. Three kinds of essential explanations are distinguished: constitutive, consequential, and those singling out (...) something's propria. This last kind of explanation has been somewhat overlooked in the literature, but we argue that it features in much of the most relevant uses of formal explanations in philosophy and science. These are the explanations for why an object has certain propertis that are not, properly speaking, parts of its essence, but that belong to it more intimately than just being part of its consequential essence: they are the properties that ‘flow’ from something's essence. It is argued that a powers metaphysics is uniquely placed to make sense of this last phenomenon. We then distinguish three grades of involvement in which powers might be salient for formal causal explanations: i) powers might be the subject matter of the essence operator, ii) the essence of something might include (or be exhausted) by powers, or iii) powers can explain how propria can flow from something's constitutive existence. (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)

When we ask ourselves about the meaning of life, two analyses are possible in principle: 1. that we are asking something about the purpose or the reason of being of life or of a life, or 2. that we are asking something the value of life or of a life. At the present article, I do not approach 1 neither the life as a whole, but I take the individual lives in the context of 2. I briefly explain what would (...) be to someone to have an objectivist conception of the meaning of life and what would be to someone to have a subjectivist one; and, then, I try to show how we can think in formulas that can capture the intuitions of those conceptions, without acquiring commitment with none of them. My way is to show that both objectivist and subjectivist conceptions think the meaning of life as related to projects or realizations that fulfill principles of value (the value can be objective or subjective according to the adopted conception), and ten I try to indicate that the projects or realizations from a person’s life come together through a simple sum to make the meaning of life of such a person’s life. The way I suggested for us to find the value of one of those realizations does not seem to present none theoretical problem. But the simple sum of realizations (and/or projects) to represent the value of the meaning of a person’s life simply did not work. That’s because it seems to lack some kind of index that is able to formalize the relations between realizations. Thus, although we couldn’t properly formalize the relation between the realizations that achieve the meaning of someone’s life at a certain moment, we get a good intuitive formalization of the value of a realization and we hope to have started an interesting investigation for future logicians, metaphysicians, mathematicians and theorists of value. (shrink)

The formal sciences - mathematical as opposed to natural sciences, such as operations research, statistics, theoretical computer science, systems engineering - appear to have achieved mathematically provable knowledge directly about the real world. It is argued that this appearance is correct.

The terms ‘verification’ and ‘validation’ are widely used in science, both in the natural and the social sciences. They are extensively used in simulation, often associated with the need to evaluate models in different stages of the simulation development process. Frequently, terminological ambiguities arise when researchers conflate, along the simulation development process, the technical meanings of both terms with other meanings found in the philosophy of science and the social sciences. This article considers the problem of verification and (...) validation in social science simulation along five perspectives: The reasons to address terminological issues in simulation; the meaning of the terms in the philosophical sense of the problem of “truth”; the observation that some debates about these terms in simulation are inadvertently more terminological than epistemological; the meaning of the terms in the technical context of the simulation development process; and finally, a comprehensive outline of the relation between terminology used in simulation, different types of models used in the development process and different epistemological perspectives. (shrink)

Formalizing Euclid’s first axiom. Bulletin of Symbolic Logic. 20 (2014) 404–5. (Coauthor: Daniel Novotný) -/- Euclid [fl. 300 BCE] divides his basic principles into what came to be called ‘postulates’ and ‘axioms’—two words that are synonyms today but which are commonly used to translate Greek words meant by Euclid as contrasting terms. -/- Euclid’s postulates are specifically geometric: they concern geometric magnitudes, shapes, figures, etc.—nothing else. The first: “to draw a line from any point to any point”; the last: the (...) parallel postulate. -/- Euclid’s axioms are general principles of magnitude: they concern geometric magnitudes and magnitudes of other kinds as well even numbers. The first is often translated “Things that equal the same thing equal one another”. -/- There are other differences that are or might become important. -/- Aristotle [fl. 350 BCE] meticulously separated his basic principles [archai, singular archê] according to subject matter: geometrical, arithmetic, astronomical, etc. However, he made no distinction that can be assimilated to Euclid’s postulate/axiom distinction. -/- Today we divide basic principles into non-logical [topic-specific] and logical [topic-neutral] but this too is not the same as Euclid’s. In this regard it is important to be cognizant of the difference between equality and identity—a distinction often crudely ignored by modern logicians. Tarski is a rare exception. The four angles of a rectangle are equal to—not identical to—one another; the size of one angle of a rectangle is identical to the size of any other of its angles. No two angles are identical to each other. -/- The sentence ‘Things that equal the same thing equal one another’ contains no occurrence of the word ‘magnitude’. This paper considers the problem of formalizing the proposition Euclid intended as a principle of magnitudes while being faithful to the logical form and to its information content. (shrink)