Completed in 1983, this work culminates nearly half a century of the late Alfred Tarski's foundational studies in logic, mathematics, and the philosophy of science. Written in collaboration with Steven Givant, the book appeals to a very broad audience, and requires only a familiarity with first-order logic. It is of great interest to logicians and mathematicians interested in the foundations of mathematics, but also to philosophers interested in logic, semantics, algebraic logic, or the methodology of the deductive sciences, and to (...) computer scientists interested in developing very simple computer languages rich enough for mathematical and scientific applications. The authors show that set theory and number theory can be developed within the framework of a new, different, and simple equational formalism, closely related to the formalism of the theory of relation algebras. There are no variables, quantifiers, or sentential connectives. Predicates are constructed from two atomic binary predicates (which denote the relations of identity and set-theoretic membership) by repeated applications of four operators that are analogues of the well-known operations of relative product, conversion, Boolean addition, and complementation. All mathematical statements are expressed as equations between predicates. There are ten logical axiom schemata and just one rule of inference: the one of replacing equals by equals, familiar from high school algebra. Though such a simple formalism may appear limited in its powers of expression and proof, this book proves quite the opposite. The authors show that it provides a framework for the formalization of practically all known systems of set theory, and hence for the development of all classical mathematics. The book contains numerous applications of the main results to diverse areas of foundational research: propositional logic; semantics; first-order logics with finitely many variables; definability and axiomatizability questions in set theory, Peano arithmetic, and real number theory; representation and decision problems in the theory of relation algebras; and decision problems in equational logic. (shrink)

The Narrative Gravity operator (Ng) has been criticized as lacking operational definition — as a conceptual label rather than a calculable variable. This paper provides the complete mathematical formalization of Ng = Ma / Sn squared, operationalizes its input variables, and demonstrates calculability through three benchmark cases. -/- Narrative Mass (Ma) is operationalized through four sub-variables scored 0.0-2.5: Causal Density (Cd), Informational Opacity (Io), Temporal Persistence (Tp), and Structural Centrality (Sc). Ma = Cd + Io + Tp + Sc, (...) range 0.0-10.0. -/- Narrative Entropy (Sn) is operationalized through Information Friction (If, scored 0.0-5.0) and Causal Branching (Cb, scored 0.0-5.0). Sn = If x Cb. Three benchmark calculations demonstrate the formula's calculability: Pulp Fiction (Ma=10.0, Sn=18.0, Ng=0.031 — edge of structural collapse through maximum entropy and maximum Vacuum Variable attractor), Crime and Punishment (Ma=7.8, Sn=5.0, Ng=0.312 — high stability through controlled entropy), and Moby Dick (Ma=9.4, Sn=7.5, Ng=0.167). -/- The Vacuum Variable is formally defined as an attractor with Io=2.5 (maximum informational opacity) and distinguished from Hitchcock's MacGuffin through precise mathematical criteria. Four testable predictions are derived, falsifiable through standard reader response methodology without biometric equipment. -/- The paper demonstrates that Ng constitutes a genuine structural contribution distinct from Shannon's Information Theory through three mathematical elements absent from Shannon: temporal integration of entropy, a formal counterforce mechanism, and a squared denominator capturing exponential attractor requirements of high-entropy systems. (shrink)

In this paper I attempt a formalization of Descartes’ causal argument for the existence of God presented in the Third Meditation. By taking into account the philosophical setting of Descartes’ Meditations, I argue that the best logical theory to carry out the formalization is quantified modal logic where free logic is used for the first-order axioms. This fact is related to Descartes’ distinction between formal and objective reality which — to my mind — suggests both the adoption of (...) modality (e.g. true in formal vs true in objective reality) and the possibility of using empty names (i.e. names which lack reference in “formal reality”). After presenting the formal system and the reconstruction of Descartes’ proof, I will discuss some issues related to the philosophical import of the formalization, such as the understanding of rigid designation and lack of reference. I will argue that the formalization of Descartes’ argument has an intrinsic philosophical value for it sheds light on the structure of argument, its implicit difficulties, and the use of logic itself to understand the philosophical tradition. (shrink)

Traditional logical reconstruction of arguments aims at assessing the validity of ordinary language arguments. It involves several tasks: extracting argumentations from texts, breaking up complex argumentations into individual arguments, framing arguments in standard form, as well as formalizing arguments and showing their validity with the help of a logical formalism. These tasks are guided by a multitude of partly antagonistic goals, they interact in various feedback loops, and they are intertwined with the development of theories of valid inference and adequate (...) formalization. This paper explores how the method of reflective equilibrium can be used for modelling the complexity of such reconstructions and for justifying the various steps involved. The proposed approach is illustrated and tested in a detailed reconstruction of the beginning of Anselm’s De casu diaboli. (shrink)

The tools of logic are used properly or improperly relative to two interrelated purposes. Logic is both a symbolism for the expression of the formal structures of thought and an inference mechanism. Formalization in philosophical logic is justified to the extent that it contributes to our understanding of logical properties and the conceptual problems they may help to state, clarify, or resolve. This view of the value and limits of formalization in logic affords a pragmatic perspective that in (...) principle should selectively support the development of particular formal systems, while excluding others as unjustified. Yet the pragmatic grounds are so liberal as to disallow virtually no exercises in formalization as entirely useless. Logic is abused in another sense, when it is wrongly used, not by violating logical canons generally, but by presupposing that substantive metaphysical, normative, or scientific content can be derived from purely formal logical relations. (shrink)

The article addresses two closely related questions: What are the criteria of adequacy of logical formalization of natural language arguments, and what gives logic the authority to decide which arguments are good and which are bad? Our point of departure is the criticism of the conception of logical formalization put forth, in a recent paper, by M. Baumgartner and T. Lampert. We argue that their account of formalization as a kind of semantic analysis brings about more problems (...) than it solves. We also argue that the criteria of adequate formalization need not be based on truth conditions associated with logical formulas; in our view, they are better based on structural (inferential) grounds. We then put forward our own version of the criteria. The upshot of the discussion that follows is that the quest for an adequate formalization in a suitable logical language is best conceived of as the search for a Goodmanian reflective equilibrium. (shrink)

This article discusses the philosophy of Alain Badiou from the perspective of a formulation that we believe represents it succinctly: the dialectic of formalization. The main thesis of the article is that Badiou’s doctrine of the four truth procedures can be understood as a doctrine of a dialectical realization of new and universal forms in the world. The dialectic of formalization announces a double procedure – an autonomous and creative procedure for the production of a new true form (...) in the world and a process of the formation of continuity in discontinuity. Moreover, the dialectic of formalization represents a connection between Badiou’s mature work and his early writings from the late 1960s. Even though in the 1960s and 1970s Badiou had not yet introduced the concepts of subject and truth in the sense that he understands them today, it is possible to support the thesis that there is an indisputable connection between Badiou’s early concept of formalization and his later concept of generic truth procedure. We will try to show that the dialectic of formalization designates the continuity between Badiou’s early and mature work. (shrink)

Any theory of information needs to comply with what we call the implementation, formalization, and representation constraints. These constraints are justified by basic considerations concerning scientific modelling and methodology. In the first part of this paper, we argue that the implementation and formalization constraints cannot be satisfied because the relation between Shannon information and IIT must be clarified. In the second part of the paper, we focus on the representation constraint. We argue that IIT cannot succeed in satisfying (...) this constraint for semantic contents without offering models for concepts, conceptual roles, and context sensitivity. In the final part of the paper, further complications are raised with respect to the distinction between consciousness and attention, which apply more specifically to the representation constraint. We conclude with some recommendations as to how IIT may succeed in solving these problems, highlighting the advantages and enormous potential of IIT as a scientific theory. (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.

This paper offers a conceptually novel contribution to the understanding of the distinctive governance challenges arising from the increasing reliance on formalized knowledge in the governance of research activities. It uses the current Australian research governance system as an example – a system which exhibits a comparatively strong degree of formalization as to its knowledge mechanisms. Combining theoretical reflections on the political-administrative and epistemic dimensions of processes of formalization with analyses of interview data gathered at Australian universities, it (...) is suggested that such a strong reliance on formalized knowledge has rather ambivalent governance ramifications. On the one hand, it allows for a seemingly rational and efficient form of the control and coordination of research activities. Yet on the other hand, it also increases the risk that knowledge is used in governance contexts in superficial, unconsidered and ultimately unreasonable ways. It is further suggested that there are a range of indications that precisely such use elicits and reinforces a range of dysfunctional behaviors on part of relevant individual and organizational actors in the public science system. (shrink)

Although Kant envisaged a prominent role for logic in the argumentative structure of his Critique of pure reason [12], logicians and philosophers have generally judged Kant’s logic negatively. What Kant called ‘general’ or ‘formal’ logic has been dismissed as a fairly arbitrary subsystem of first order logic, and what he called ‘transcendental logic’ is considered to be not a logic at all: no syntax, no semantics, no definition of validity. Against this, we argue that Kant’s ‘transcendental logic’ 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 Kant’s Table of Judgements in §9 of the Critique of pure reason, is indeed, as Kant claimed, complete for the kind of semantics he had in mind. This result implies that Kant’s ’general’ logic is after all a distinguished subsystem of first order logic, namely what is known as geometric logic. (shrink)

I make an attempt at the description of the delicate role of the standard model of arithmetic for the syntax of formal systems. I try to assess whether the possible instability in the notion of finiteness deriving from the nonstandard interpretability of arithmetic affects the very notions of syntactic metatheory and of formal system. I maintain that the crucial point of the whole question lies in the evaluation of the phenomenon of formalization. The ideas of Skolem, Zermelo, Beth and (...) Carnap (among others) on the problem are discussed. ‘A tries to explain to B the meaning of negation. Finally A gives up, saying: “You don’t understand what I mean, and I am not going to explain any longer,” to which B replies: “Yes, I see what you mean, and I am glad you are willing to continue your explanations”’. G. Mannoury, reported by E. W. Beth (Beth, 1963, 489). (shrink)

This work examines the importance of distinguishing different levels of psychological explanation and the primacy of the computational level over implementational levels. The framework of levels allows us to recognize the role of formal theories as tools for specifying reasoning tasks at the computational level. It is shown that formal specifications of reasoning tasks allow us to analyze the complexity of the specified tasks and also serve to define reasoning competence and performance errors. Complexity analysis helps us identify tractable, practically (...) significant, subclasses of inference. The identification of these subclasses provides useful ante hoc and post hoc specifications for AI programming projects and psychological modeling. Formalization and complexity analysis also enable us to examine tradeoffs between tractability and range of applicability of implementations of a reasoning task. It is undesirable to obtain tractability at the expense of limiting the applicability of a cognitive mechanism to an unreal situation or a toy domain. It is argued that this undesirable result can be avoided if we examine the structure of the environment in which a mechanism is supposed to work and the environmental assumptions that make the computation tractable. Finally, it is demonstrated that many problems the human mind needs to solve in normal environments are indeed tractable and that the mind is equipped with adaptive mechanisms to solve them efficiently. This demonstration undermines a skeptical challenge to human rationality based on claims that many problems are intractable and that the capacity of the human mind is limited. (shrink)

Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different such tools are being increasingly used in order to accelerate and simplify proof checking, and the Coq proof assistant is one of the most well known and used in large-scale projects. Language and automata theory is a well-established area of mathematics, relevant to computer science foundations and information technology. In particular, context-free language (...) theory is of fundamental importance in the analysis, design, and implementation of computer programming languages. This work describes a formalization effort, using the Coq proof assistant, of fundamental results of the classical theory of contextfree grammars and languages. These include closure properties (union, concatenation, and Kleene star), grammar simplification (elimination of useless symbols, inaccessible symbols, empty rules, and unit rules), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. As it turns out, this is a comprehensive formalization of the classical context-free language theory in the Coq proof assistant and includes the formalization of the Pumping Lemma for context-free languages. The perspectives for the further development of this work are diverse and can be grouped in three different areas: inclusion of new devices and results, code extraction, and general enhancements of its libraries. (shrink)

he general theme of this paper is the issue of formalization in philosophy; in a more specific way, it deals with the issue of formalization of arguments in analytic philosophy of religion. One argument in particular – Anselm’s Proslogion II ontological argument – and one specific attempt to formalize it – Robert Adams’ formalization found in his paper “The Logical Structure of Anselm’s Arguments”, published in The Philosophical Review in 1971 – are taken as study cases. The purpose (...) of the paper is to critically analyze Adams’ formalization with the intent to shed some light on the following questions: What are the virtues of formally analyzing arguments and the contributions, if any, of such an enterprise to the debate on Anselm’s argument? Which lessons can Adam’s work teach us about the dangers and limitations of formalization? Do these virtues and dangers teach us something about analysis of arguments in general? (shrink)

This chapter examines three ways of formalizing the law of non-contradiction. The key feature of such a way is the enforcement of consistency of the formal system concerned. The first formalization is as a formula of form, ∼(A&∼A), favoured by textbooks. The presence of this as a logical law is shown to be completely independent of the consistency of the logical system. The second formalization is as a rule, A,∼A → B, called the Spread Law. This rule is (...) somewhat better as its presence prevents contradictions from occurring in the logic, through pain of triviality. However, paraconsistent logics are without the rule, and something needs to be done for them. The third formalization uses rejection in two forms, one rejecting contradictions and one rejecting negations of provable formulae, but these too have their problems. (shrink)

This paper compares several models of formalization. It articulates criteria of correct formalization and identifies their problems. All of the discussed criteria are so called “semantic” criteria, which refer to the interpretation of logical formulas. However, as will be shown, different versions of an implicitly applied or explicitly stated criterion of correctness depend on different understandings of “interpretation” in this context.

This paper can be treated as a simplification of the Gentzen formalization of SCI-tautologies presented by A. Michaels in [1].

This paper contains a careful derivation of principles of Interpretability Logic valid in extensions of I0+1.

Model makers often find themselves in the following situation: in order for the model to be able to represent the dynamics of the target system, they have to make certain assumptions that pertain to the system. The problem with these assumptions is not that they are wrong, but that they cannot be derived from observations and experiments. Thus, alternative modeling assumptions can also be used, and the data does not adjudicate between the sets of assumptions. Since a decision must be (...) made, the decision derives from considerations such as the theoretical commitments of the modeler. Focusing on assumptions of this sort, the article examines the assumptions of evolutionary game theory (EGT). Following previous authors who noticed that there were in fact two strands of EGT, the current work compares the set of modeling assumptions made in each. The attempt here is not to adjudicate between the two sets, but to demonstrate that for each strand of EGT, an alternative set of assumptions was available. My hope is that the examination of the chosen assumptions will reveal the theoretical commitments that motivated the choice. Focusing on the latter strand of EGT, the article addresses the following question: What assumptions about evolution did EGT embody that align this modeling tradition with sociobiology? By demonstrating these similarities, I hope to support a broader argument, namely, that models are not neutral structures with respect to their target system. (shrink)

Proof requires a dialogue between agents to clarify obscure inference steps, fill gaps, or reveal implicit assumptions in a purported proof. Hence, argumentation is an integral component of the discovery process for mathematical proofs. This work presents how argumentation theories can be applied to describe specific informal features in the development of proof-events. The concept of proof-event was coined by Goguen who described mathematical proof as a public social event that takes place in space and time. This new meta-methodological concept (...) is designed to cover not only “traditional” formal proofs but all kinds of proofs and inference steps, including incomplete or purported proofs. Our approach attempts to make proof-events more comprehensive to express the complete trajectory of a mathematical proof-event until the ultimate validation of the proving outcome. Thus, we advance an extended version of proof-event calculus which is built on argumentation theories designed to capture the internal and external structure of collaborative mathematical practice and highlight the relationship between proof, human reasoning, and cognitive processes. In addition, another area in which argumentation can make a significant contribution is dealing with the defeasible knowledge of the Web which is a product of its open and ubiquitous nature. This approach seems to be sufficient for the presentation of Web-based proving processes as manifested in the case of the Mini-Polymath 4 project. (shrink)

The question, what a given statement is “about,” often occurs in philosophic discussion. I shall use this question in the hope of illustrating how a relatively simple application of symbolic logic can clarify a problem which might otherwise turn into a maze of complications.

Within a weak subsystem of second-order arithmetic , that is -conservative over , we reformulate Kreisel's proof of the Second Incompleteness Theorem and Boolos' proof of the First Incompleteness Theorem.

The idea at the basis of this special issue is that reopening the old debate about the logical status of Hegel’s dialectics is extremely interesting, for various reasons.1 The first reason is that...

Mainstream economics has been accused of excessive mathematization, whereas the rejection of mathematical and other formal methods is often cited as a crucial trait of Austrian economics. Based on a systematic discussion of potential benefits and drawbacks of formalization, this paper corroborates legitimate concerns that predominant types of mathematization induce a shift of attention away from the key concepts of Austrian economics. Taking this shift to the extreme, predominant modes of mathematization tend to accompany a detachment from ‘reality’ incompatible (...) with Austrian pleas for realisticness. Contrary to popular prejudice however, the most prominent representatives of the Austrian School including Carl Menger, Ludwig Mises, Friedrich Hayek, Israel Kirzner, and Peter Boettke neither provide a justification for a wholesale rejection of formalization nor actually reject it. Adequate formalization can serve as a remedy for lacking logical and semantic rigor in standard mathematical economics as well as in murky verbal chains of reasoning. (shrink)

Explication is the conceptual cornerstone of Carnap’s approach to the methodology of scientific analysis. From a philosophical point of view, it gives rise to a number of questions that need to be addressed, but which do not seem to have been fully addressed by Carnap himself. This paper reconsiders Carnapian explication by comparing it to a different approach: the ‘formalisms as cognitive tools’ conception. The comparison allows us to discuss a number of aspects of the Carnapian methodology, as well as (...) issues pertaining to formalization in general. We start by introducing Carnap’s conception of explication, arguing that there is a tension between his proposed criteria of fruitfulness and similarity; we also argue that his further desideratum of exactness is less crucial than might appear at first. We then bring in the general idea of formalisms as cognitive tools, mainly by discussing the reliability of so-called statistical prediction rules, i.e. simple algorithms used to make predictions across a range of areas. SPRs allow for a concrete instantiation of Carnap’s fruitfulness desideratum, which is arguably the most important desideratum for him. Finally, we elaborate on what we call the ‘paradox of adequate formalization’, which for the Carnapian corresponds to the tension between similarity and fruitfulness. We conclude by noting that formalization is an inherently paradoxical enterprise in general, but one worth engaging in given the ‘cognitive boost’ it affords as a tool for discovery. (shrink)

Jim Griesemer papers are typically rich, creative, and challenging. One of my favorite things about a Griesemer paper is that some of the best bits are doing double duty as framing. That is well on display in his 2013 “Formalization and the Meaning of ‘Theory’ in the Inexact Biological Sciences,” where we find epistemological stances operationalized as methodological tools and guides. This makes Griesemer’s papers richly layered. Here, for example, the proximate topic is formalization of theories in exact (...) and inexact sciences. Yet to get there we travel through a pragmatic conception of theories, framed by some of Griesemer’s distinctive stances and approaches to science and philosophy. A reader singularly focused on the end goal risks missing some of the value laid out along the way. (shrink)

We combine linear temporal logic (with both past and future modalities) with a deontic version of justification logic to provide a framework for reasoning about time and epistemic and normative reasons. In addition to temporal modalities, the resulting logic contains two kinds of justification assertions: epistemic justification assertions and deontic justification assertions. The former presents justification for the agent’s knowledge and the latter gives reasons for why a proposition is obligatory. We present two kinds of semantics for the logic: one (...) based on Fitting models and the other based on neighborhood models. The use of neighborhood semantics enables us to define the dual of deontic justification assertions properly, which corresponds to a notion of permission in deontic logic. We then establish the soundness and completeness of an axiom system of the logic with respect to these semantics. Further, we formalize the Protagoras versus Euathlus paradox in this logic and present a precise analysis of the paradox, and also briefly discuss Leibniz’s solution. (shrink)

It may be useful to summarize the information on studied individuals using a small number of parameters which make it possible to find the correct overall distribution. Apart from the saving thus made, these parameters can provide us with a simple demographic interpretation clarifying the process observed.

In this paper, we provide a logical formalization of the emotion triggering process and of its relationship with mental attitudes, as described in Ortony, Clore, and Collins’s theory. We argue that modal logics are particularly adapted to represent agents’ mental attitudes and to reason about them, and use a specific modal logic that we call Logic of Emotions in order to provide logical definitions of all but two of their 22 emotions. While these definitions may be subject to debate, (...) we show that they allow to reason about emotions and to draw interesting conclusions from the theory. (shrink)