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)

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 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.

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)

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

This paper deals with Tarski's first axiomatic presentations of the syntax of deductive system. Andrzej Grzegorczyk's significant results which laid the foundations for the formalization of metalogic, are touched upon briefly. The results relate to Tarski's theory of concatenation, also called the theory of strings, and to Tarski's ideas on the formalization of metamathematics. There is a short mention of author's research in the field. The main part of the paper surveys research on the theory of deductive systems (...) initiated by Tarski, in particular research on the axiomatization of the general notion of consequence operation, axiom systems for the theories of classic consequence and for some equivalent theories, and axiom systems for the theories of nonclassic consequence. In this paper the results of Jerzy Supecki's research are taken into account, and also the author's and other people belonging to his circle of scientific research. Particular study is made of his dual characterization of deductive systems, both as systems in regard to acceptance and systems in regard to rejection . Comparison is made, therefore, with axiomatizations of the theories of rejection and dual consequence, and the theory of the usual consequence operation. (shrink)

This article summarizes the main ideas for formalizing categorial languages genrated by classical categorial grammar originated by K. Ajdukiewicz [1935,1960].This formalization is presented in detail in the author's monographs in Polish "Teorie Języków Syntaktycznie Kategorialnych" ("Theories of Syntactically Categorical Languages"), PWN, Warszawa-Wrocław 1985 and in English "Theory of Language Syntax, Categorial Approach", Kluwer Academic Publishers, Boston-London-Dordrecht 1991.

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.

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)

Tom Eyers contrasts the different “movements” of the novel and the lyric poem: while moments of stasis in the novel are swept up in its narrative trajectory, atemporal moments in poetry can be juxtaposed against other kinds of temporality — for Eyers’s purposes, most importantly the temporalities of politics and history. The Theory of the Novelbecomes a theory of the lyric, undoing the persistent belief that history can only be made to appear in narrative.

Deontic logic, as traditionally conceived, provides only a deductive theory that constrains the states or possible worlds within which an agent should try to remain.

On September 6, 2004, using the Isabelle proof assistant, I verified the following statement: (%x. pi x * ln (real x) / (real x)) ----> 1 The system thereby confirmed that the prime number theorem is a consequence of the axioms of higher-order logic together with an axiom asserting the existence of an infinite set. All told, our number theory session, including the proof of the prime number theorem and supporting libraries, constitutes 673 pages of proof scripts, or roughly 30,000 (...) lines. This count includes about 65 pages of elementary number theory that we had at the outset, developed by Larry Paulson and others; also about 50 pages devoted to a proof of the law of quadratic reciprocity and properties of Euler’s ϕ function, neither of which are used in the proof of the prime number theorem. The page count does not include the basic HOL library, or properties of the real numbers that we obtained from the HOL-Complex library. (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)

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...

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

The purpose of this paper is twofold. First, it aims at introducing the ontological argument through the analysis of five historical developments: Anselm’s argument found in the second chapter of his Proslogion, Gaunilo’s criticism of it, Descartes’ version of the ontological argument found in his Meditations on First Philosophy, Leibniz’s contribution to the debate on the ontological argument and his demonstration of the possibility of God, and Kant’s famous criticisms against the (cartesian) ontological argument. Second, it intends to critically examine (...) the enterprise of formally analyzing philosophical arguments and, as such, contribute in a small degree to the debate on the role of formalization in philosophy. My focus will be mainly on the drawbacks and limitations of such enterprise; as a guideline, I shall refer to a Carnapian, or Carnapian-like theory of argument analysis. (shrink)

We present a formalization of first-order predicate calculus with equality which, unlike traditional systems with axiom schemata or substitution rules, is finitely axiomatized in the sense that each step in a formal proof admits only finitely many choices. This formalization is primarily based on the inference rule of condensed detachment of Meredith. The usual primitive notions of free variable and proper substitution are absent, making it easy to verify proofs in a machine-oriented application. Completeness results are presented. The (...) example of Zermelo-Fraenkel set theory is shown to be finitely axiomatized under the formalization. The relationship with resolution-based theorem provers is briefly discussed. A closely related axiomatization of traditional predicate calculus is shown to be complete in a strong metamathematical sense. (shrink)

This paper sketches or signals some ideas, results, and proposals connected with the theoretical issues related to the categorial approach to language which originated from the first author and which form the basis for further research by the second author. The main aims are the following: 1) to bring into common use some Polish ideas concerned with classical categorial grammar; 2) to take into consideration a universal and simultaneously formal-logical perspective; 3) to consider Peirce's well-known differentiation of linguistic objects, i.e. (...) their twofold ontological status as tokens and types and, according to this, to consider the biaspectual formalization of language dealing with the two main orientations in the controversy between nominalism and Platonism; 4) to characterize language according to Frege's ontological canons, according to which each expression of language corresponds to its denotation. All of these factors make possible not only the syntactic characterization of language but also the introduction of syntactic and semantic definitions of a true expression and its denotation. These notions correspond here to the old classical, but not necessarily standard, understanding of semantic concepts. The paper is divided into four sections: the first contains a brief characterization of the categorial approach to syntax; the second presents two strains of this approach; the third touches on certain general semantic issues connected with the notion of truth; and the last gives some final remarks. (shrink)