In recent years, the e ffort to formalize erotetic inferences (i.e., inferences to and from questions) has become a central concern for those working in erotetic logic. However, few have sought to formulate a proof theory for these inferences. To fill this lacuna, we construct a calculus for (classes of) sequents that are sound and complete for two species of erotetic inferences studied by Inferential Erotetic Logic (IEL): erotetic evocation and regular erotetic implication. While an attempt has been made (...) to axiomatize the former in a sequent system, there is currently no proof theory for the latter. Moreover, the extant axiomatization of erotetic evocation fails to capture its defeasible character and provides no rules for introducing or eliminating question-forming operators. In contrast, our calculus encodes defeasibility conditions on sequents and provides rules governing the introduction and elimination of erotetic formulas. We demonstrate that an elimination theorem holds for a version of the cut rule that applies to both declarative and erotetic formulas and that the rules for the axiomatic account of question evocation in IEL are admissible in our system. (shrink)
I am presenting a sequentcalculus that extends a nonmonotonic consequence relation over an atomic language to a logically complex language. The system is in line with two guiding philosophical ideas: (i) logical inferentialism and (ii) logical expressivism. The extension defined by the sequent rules is conservative. The conditional tracks the consequence relation and negation tracks incoherence. Besides the ordinary propositional connectives, the sequentcalculus introduces a new kind of modal operator that marks implications that (...) hold monotonically. Transitivity fails, but for good reasons. Intuitionism and classical logic can easily be recovered from the system. (shrink)
We provide a logical matrix semantics and a Gentzen-style sequentcalculus for the first-degree entailments valid in W. T. Parry’s logic of Analytic Implication. We achieve the former by introducing a logical matrix closely related to that inducing paracomplete weak Kleene logic, and the latter by presenting a calculus where the initial sequents and the left and right rules for negation are subject to linguistic constraints.
This paper contends that Stoic logic (i.e. Stoic analysis) deserves more attention from contemporary logicians. It sets out how, compared with contemporary propositional calculi, Stoic analysis is closest to methods of backward proof search for Gentzen-inspired substructural sequent logics, as they have been developed in logic programming and structural proof theory, and produces its proof search calculus in tree form. It shows how multiple similarities to Gentzen sequent systems combine with intriguing dissimilarities that may enrich contemporary discussion. (...) Much of Stoic logic appears surprisingly modern: a recursively formulated syntax with some truth-functional propositional operators; analogues to cut rules, axiom schemata and Gentzen’s negation-introduction rules; an implicit variable-sharing principle and deliberate rejection of Thinning and avoidance of paradoxes of implication. These latter features mark the system out as a relevance logic, where the absence of duals for its left and right introduction rules puts it in the vicinity of McCall’s connexive logic. Methodologically, the choice of meticulously formulated meta-logical rules in lieu of axiom and inference schemata absorbs some structural rules and results in an economical, precise and elegant system that values decidability over completeness. (shrink)
We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequentcalculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without (...) resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants. (shrink)
The aim of this paper is to emphasize the fact that for all finitely-many-valued logics there is a completely systematic relation between sequent calculi and tableau systems. More importantly, we show that for both of these systems there are al- ways two dual proof sytems (not just only two ways to interpret the calculi). This phenomenon may easily escape one’s attention since in the classical (two-valued) case the two systems coincide. (In two-valued logic the assignment of a truth value (...) and the exclusion of the opposite truth value describe the same situation.). (shrink)
In their paper Nothing but the Truth Andreas Pietz and Umberto Rivieccio present Exactly True Logic, an interesting variation upon the four-valued logic for first-degree entailment FDE that was given by Belnap and Dunn in the 1970s. Pietz & Rivieccio provide this logic with a Hilbert-style axiomatisation and write that finding a nice sequentcalculus for the logic will presumably not be easy. But a sequentcalculus can be given and in this paper we will show (...) that a calculus for the Belnap-Dunn logic we have defined earlier can in fact be reused for the purpose of characterising ETL, provided a small alteration is made—initial assignments of signs to the sentences of a sequent to be proved must be different from those used for characterising FDE. While Pietz & Rivieccio define ETL on the language of classical propositional logic we also study its consequence relation on an extension of this language that is functionally complete for the underlying four truth values. On this extension the calculus gets a multiple-tree character—two proof trees may be needed to establish one proof. (shrink)
In this paper we introduce a Gentzen calculus for (a functionally complete variant of) Belnap's logic in which establishing the provability of a sequent in general requires \emph{two} proof trees, one establishing that whenever all premises are true some conclusion is true and one that guarantees the falsity of at least one premise if all conclusions are false. The calculus can also be put to use in proving that one statement \emph{necessarily approximates} another, where necessary approximation is (...) a natural dual of entailment. The calculus, and its tableau variant, not only capture the classical connectives, but also the `information' connectives of four-valued Belnap logics. This answers a question by Avron. (shrink)
Hilbert's ε-calculus is based on an extension of the language of predicate logic by a term-forming operator εx. Two fundamental results about the ε-calculus, the first and second epsilon theorem, play a rôle similar to that which the cut-elimination theorem plays in sequentcalculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of (...) Herbrand disjunctions of existential theorems obtained by this elimination procedure. (shrink)
We employ a recently developed methodology -- called "structural refinement" -- to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. This method can be seen as a means by which labelled sequent systems can be transformed into nested sequent systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. The nested systems we obtain incorporate propagation rules that are (...) parameterized with formal grammars, and which encode certain frame conditions expressible as first-order Horn formulae that correspond to a subclass of the Scott-Lemmon axioms. We show that our nested systems are sound, cut-free complete, and admit hp-admissibility of typical structural rules. (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 sequentcalculus, 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, sequentcalculus, tableaux, and natural deduction. This report is actually a template, from which all results can be specialized to particular logics. (shrink)
This paper presents a sequentcalculus and a dual domain semantics for a theory of definite descriptions in which these expressions are formalised in the context of complete sentences by a binary quantifier I. I forms a formula from two formulas. Ix[F, G] means ‘The F is G’. This approach has the advantage of incorporating scope distinctions directly into the notation. Cut elimination is proved for a system of classical positive free logic with I and it is shown (...) to be sound and complete for the semantics. The system has a number of novel features and is briefly compared to the usual approach of formalising ‘the F ’ by a term forming operator. It does not coincide with Hintikka’s and Lambert’s preferred theories, but the divergence is well-motivated and attractive. (shrink)
This paper presents rules in sequentcalculus for a binary quantifier I to formalise definite descriptions: Ix[F, G] means ‘The F is G’. The rules are suitable to be added to a system of positive free logic. The paper extends the proof of a cut elimination theorem for this system by Indrzejczak by proving the cases for the rules of I. There are also brief comparisons of the present approach to the more common one that formalises definite descriptions (...) with a term forming operator. In the final section rules for I for negative free and classical logic are also mentioned. (shrink)
An exact truthmaker for A is a state which, as well as guaranteeing A’s truth, is wholly relevant to it. States with parts irrelevant to whether A is true do not count as exact truthmakers for A. Giving semantics in this way produces a very unusual consequence relation, on which conjunctions do not entail their conjuncts. This feature makes the resulting logic highly unusual. In this paper, we set out formal semantics for exact truthmaking and characterise the resulting notion of (...) entailment, showing that it is compact and decidable. We then investigate the effect of various restrictions on the semantics. We also formulate a sequent-style proof system for exact entailment and give soundness and completeness results. (shrink)
This paper presents and motivates a new philosophical and logical approach to truth and semantic paradox. It begins from an inferentialist, and particularly bilateralist, theory of meaning---one which takes meaning to be constituted by assertibility and deniability conditions---and shows how the usual multiple-conclusion sequentcalculus for classical logic can be given an inferentialist motivation, leaving classical model theory as of only derivative importance. The paper then uses this theory of meaning to present and motivate a logical system---ST---that conservatively (...) extends classical logic with a fully transparent truth predicate. This system is shown to allow for classical reasoning over the full (truth-involving) vocabulary, but to be non-transitive. Some special cases where transitivity does hold are outlined. ST is also shown to give rise to a familiar sort of model for non-classical logics: Kripke fixed points on the Strong Kleene valuation scheme. Finally, to give a theory of paradoxical sentences, a distinction is drawn between two varieties of assertion and two varieties of denial. On one variety, paradoxical sentences cannot be either asserted or denied; on the other, they must be both asserted and denied. The target theory is compared favourably to more familiar related systems, and some objections are considered. (shrink)
A uniform construction for sequent calculi for finite-valued first-order logics with distribution quantifiers is exhibited. Completeness, cut-elimination and midsequent theorems are established. As an application, an analog of Herbrand’s theorem for the four-valued knowledge-representation logic of Belnap and Ginsberg is presented. It is indicated how this theorem can be used for reasoning about knowledge bases with incomplete and inconsistent information.
In this paper, we present a non-trivial and expressively complete paraconsistent naïve theory of truth, as a step in the route towards semantic closure. We achieve this goal by expressing self-reference with a weak procedure, that uses equivalences between expressions of the language, as opposed to a strong procedure, that uses identities. Finally, we make some remarks regarding the sense in which the theory of truth discussed has a property closely related to functional completeness, and we present a sound and (...) complete three-sided sequentcalculus for this expressively rich theory. (shrink)
Methods available for the axiomatization of arbitrary finite-valued logics can be applied to obtain sound and complete intelim rules for all truth-functional connectives of classical logic including the Sheffer stroke and Peirce’s arrow. The restriction to a single conclusion in standard systems of natural deduction requires the introduction of additional rules to make the resulting systems complete; these rules are nevertheless still simple and correspond straightforwardly to the classical absurdity rule. Omitting these rules results in systems for intuitionistic versions of (...) the connectives in question. (shrink)
Restall set forth a "consecution" calculus in his "An Introduction to Substructural Logics." This is a natural deduction type sequentcalculus where the structural rules play an important role. This paper looks at different ways of extending Restall's calculus. It is shown that Restall's weak soundness and completeness result with regards to a Hilbert calculus can be extended to a strong one so as to encompass what Restall calls proofs from assumptions. It is also shown (...) how to extend the calculus so as to validate the metainferential rule of reasoning by cases, as well as certain theory-dependent rules. (shrink)
Many prominent writers on the philosophy of logic, including Michael Dummett, Dag Prawitz, Neil Tennant, have held that the introduction and elimination rules of a logical connective must be ‘in harmony ’ if the connective is to possess a sense. This Harmony Thesis has been used to justify the choice of logic: in particular, supposed violations of it by the classical rules for negation have been the basis for arguments for switching from classical to intuitionistic logic. The Thesis has also (...) had an influence on the philosophy of language: some prominent writers in that area, notably Dummett and Robert Brandom, have taken it to be a special case of a more general requirement that the grounds for asserting a statement must cohere with its consequences. This essay considers various ways of making the Harmony Thesis precise and scrutinizes the most influential arguments for it. The verdict is negative: all the extant arguments for the Thesis are weak, and no version of it is remotely plausible. (shrink)
In this paper we define intensional models for the classical theory of types, thus arriving at an intensional type logic ITL. Intensional models generalize Henkin's general models and have a natural definition. As a class they do not validate the axiom of Extensionality. We give a cut-free sequentcalculus for type theory and show completeness of this calculus with respect to the class of intensional models via a model existence theorem. After this we turn our attention to (...) applications. Firstly, it is argued that, since ITL is truly intensional, it can be used to model ascriptions of propositional attitude without predicting logical omniscience. In order to illustrate this a small fragment of English is defined and provided with an ITL semantics. Secondly, it is shown that ITL models contain certain objects that can be identified with possible worlds. Essential elements of modal logic become available within classical type theory once the axiom of Extensionality is given up. (shrink)
Gaisi Takeuti (1926–2017) is one of the most distinguished logicians in proof theory after Hilbert and Gentzen. He extensively extended Hilbert's program in the sense that he formulated Gentzen's sequentcalculus, conjectured that cut-elimination holds for it (Takeuti's conjecture), and obtained several stunning results in the 1950–60s towards the solution of his conjecture. Though he has been known chiefly as a great mathematician, he wrote many papers in English and Japanese where he expressed his philosophical thoughts. In particular, (...) he used several keywords such as "active intuition" and "self-reflection" from Nishida's philosophy. In this paper, we aim to describe a general outline of our project to investigate Takeuti's philosophy of mathematics. In particular, after reviewing Takeuti's proof-theoretic results briefly, we describe some key elements in Takeuti's texts. By explaining these texts, we point out the connection between Takeuti's proof theory and Nishida's philosophy and explain the future goals of our project. (shrink)
We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.
We study a fragment of Intuitionistic Linear Logic combined with non-normal modal operators. Focusing on the minimal modal logic, we provide a Gentzen-style sequentcalculus as well as a semantics in terms of Kripke resource models. We show that the proof theory is sound and complete with respect to the class of minimal Kripke resource models. We also show that the sequentcalculus allows cut elimination. We put the logical framework to use by instantiating it as (...) a logic of agency. In particular, we apply it to reason about the resource-sensitive use of artefacts. (shrink)
This article presents modal versions of resource-conscious logics. We concentrate on extensions of variants of linear logic with one minimal non-normal modality. In earlier work, where we investigated agency in multi-agent systems, we have shown that the results scale up to logics with multiple non-minimal modalities. Here, we start with the language of propositional intuitionistic linear logic without the additive disjunction, to which we add a modality. We provide an interpretation of this language on a class of Kripke resource models (...) extended with a neighbourhood function: modal Kripke resource models. We propose a Hilbert-style axiomatisation and a Gentzen-style sequentcalculus. We show that the proof theories are sound and complete with respect to the class of modal Kripke resource models. We show that the sequentcalculus admits cut elimination and that proof-search is in PSPACE. We then show how to extend the results when non-commutative connectives are added to the language. Finally, we put the l.. (shrink)
The first-order temporal logics with □ and ○ of time structures isomorphic to ω (discrete linear time) and trees of ω-segments (linear time with branching gaps) and some of its fragments are compared: the first is not recursively axiomatizable. For the second, a cut-free complete sequentcalculus is given, and from this, a resolution system is derived by the method of Maslov.
In [5], Béziau provides a means by which Gentzen’s sequentcalculus can be combined with the general semantic theory of bivaluations. In doing so, according to Béziau, it is possible to construe the abstract “core” of logics in general, where logical syntax and semantics are “two sides of the same coin”. The central suggestion there is that, by way of a modification of the notion of maximal consistency, it is possible to prove the soundness and completeness for any (...) normal logic. However, the reduction to bivaluation may be a side effect of the architecture of ordinary sequents, which is both overly restrictive, and entails certain expressive restrictions over the language. This paper provides an expansion of Béziau’s completeness results for logics, by showing that there is a natural extension of that line of thinking to n-sided sequent constructions. Through analogical techniques to Béziau’s construction, it is possible, in this setting, to construct abstract soundness and completeness results for n-valued logics. (shrink)
We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special (...) form that is translatable to a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics. (shrink)
A general class of labeled sequent calculi is investigated, and necessary and sufficient conditions are given for when such a calculus is sound and complete for a finite -valued logic if the labels are interpreted as sets of truth values. Furthermore, it is shown that any finite -valued logic can be given an axiomatization by such a labeled calculus using arbitrary "systems of signs," i.e., of sets of truth values, as labels. The number of labels needed is (...) logarithmic in the number of truth values, and it is shown that this bound is tight. (shrink)
An introductory textbook on metalogic. It covers naive set theory, first-order logic, sequentcalculus and natural deduction, the completeness, compactness, and Löwenheim-Skolem theorems, Turing machines, and the undecidability of the halting problem and of first-order logic. The audience is undergraduate students with some background in formal logic.
In this essay I give a complete join semi-lattice of possible display-equivalence schemes for Display Logic, using the standard connectives, and leaving fixed only the schemes governing the star. In addition to proving the completeness of this list, I offer a discussion of the basic properties of these schemes.
This thesis is about the metaphysics of logic. I argue against a view I refer to as ‘logical realism’. This is the view that the logical constants represent a particular kind of metaphysical structure, which I dub ‘logico-metaphysical structure’. I argue instead for a more metaphysically lightweight view of logic which I dub ‘logical expressivism’. -/- In the first part of this thesis (Chapters I and II) I argue against a number of arguments that Theodore Sider has given for logical (...) realism. In Chapter I, I present an argument of his to the effect that logico-metaphysical structure provides the only good explanation of the semantic determinacy of the logical constants. I argue that other explanations are possible. In Chapter II, I present another argument of his to the effect that logico-metaphysical structure is something that comes along with ontological realism: the view that there is a non-language-relative fact of the matter about what exists. I argue that the connection between logical and ontological realism is not as close as Sider makes it out to be. -/- In the second part of this thesis (Chapters III – V) I set out a positive view of the logical constants that can explain both why their meanings are semantically determinate, and why they form part of our vocabulary. On that view, the primary bearers of logical structure are propositional attitudes, and the logical constants are in our language as vehicles for the expression of logically complex propositional attitudes. In Chapter III, I set out an expressivist theory of propositional logic. In Chapter IV, I use this theory to explain how the logical connectives end up having determinate meanings. In Chapter V, I extend the expressivist theory to predicate logic. (shrink)
This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable proof-theoretic properties from its (...) associated labelled calculus. (shrink)
The first learning game to be developed to help students to develop and hone skills in constructing proofs in both the propositional and first-order predicate calculi. It comprises an autotelic (self-motivating) learning approach to assist students in developing skills and strategies of proof in the propositional and predicate calculus. The text of VALIDITY consists of a general introduction that describes earlier studies made of autotelic learning games, paying particular attention to work done at the Law School of Yale University, (...) called the ALL Project (Accelerated Learning of Logic). Following the introduction, the game of VALIDITY is described, first with reference to the propositional calculus, and then in connection with the first-order predicate calculus with identity. Sections in the text are devoted to discussions of the various rules of derivation employed in both calculi. Three appendices follow the main text; these provide a catalogue of sequents and theorems that have been proved for the propositional calculus and for the predicate calculus, and include suggestions for the classroom use of VALIDITY in university-level courses in mathematical logic. (shrink)
This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cut-free calculi in possession of desirable proof-theoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly incorporates (...) the semantics of the associated logic, and such systems typically violate the subformula property to a high degree. By contrast, nested sequent calculi employ a simpler syntax and adhere to a strict reading of the subformula property, making such systems useful in the design of automated reasoning algorithms. However, the downside of the nested sequent paradigm is that a general theory concerning the automated construction of such calculi (as in the labelled setting) is essentially absent, meaning that the construction of nested systems and the confirmation of their properties is usually done on a case-by-case basis. The refinement method connects both paradigms in a fruitful way, by transforming labelled systems into nested (or, refined labelled) systems with the properties of the former preserved throughout the transformation process. To demonstrate the method of refinement and some of its applications, we consider grammar logics, first-order intuitionistic logics, and deontic STIT logics. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics. Furthermore, we employ our refined labelled calculi for grammar logics to show that every logic in the class possesses the effective Lyndon interpolation property. (shrink)
We examine the set of formula-to-formula valid inferences of Classical Logic, where the premise and the conclusion share at least a propositional variable in common. We review the fact, already proved in the literature, that such a system is identical to the first-degree entailment fragment of R. Epstein's Relatedness Logic, and that it is a non-transitive logic of the sort investigated by S. Frankowski and others. Furthermore, we provide a semantics and a calculus for this logic. The semantics is (...) defined in terms of a Rp-matrix built on top of a 5-valued extension of the 3-element weak Kleene algebra, whereas the calculus is defined in terms of a Gentzen-style sequent system where the left and right negation rules are subject to linguistic constraints. (shrink)
In this paper I introduce a sequent system for the propositional modal logic S5. Derivations of valid sequents in the system are shown to correspond to proofs in a novel natural deduction system of circuit proofs (reminiscient of proofnets in linear logic, or multiple-conclusion calculi for classical logic). -/- The sequent derivations and proofnets are both simple extensions of sequents and proofnets for classical propositional logic, in which the new machinery—to take account of the modal vocabulary—is directly motivated (...) in terms of the simple, universal Kripke semantics for S5. The sequent system is cut-free and the circuit proofs are normalising. (shrink)
This paper examines systematically which features of a life story (or history) make it good for the subject herself - not aesthetically or morally good, but prudentially good. The tentative narrative calculus presented claims that the prudential narrative value of an event is a function of the extent to which it contributes to her concurrent and non-concurrent goals, the value of those goals, and the degree to which success in reaching the goals is deserved in virtue of exercising agency. (...) The narrative value of a life is a simple sum of the values of individual events that comprise it. I claim that this view best explains and support common intuitions about the significance of the shape of a life. (shrink)
To explore the extent of embeddability of Leibnizian infinitesimal calculus in first-order logic (FOL) and modern frameworks, we propose to set aside ontological issues and focus on pro- cedural questions. This would enable an account of Leibnizian procedures in a framework limited to FOL with a small number of additional ingredients such as the relation of infinite proximity. If, as we argue here, first order logic is indeed suitable for developing modern proxies for the inferential moves found in Leibnizian (...) infinitesimal calculus, then modern infinitesimal frameworks are more appropriate to interpreting Leibnizian infinitesimal calculus than modern Weierstrassian ones. (shrink)
A new proof style adequate for modal logics is defined from the polynomial ring calculus. The new semantics not only expresses truth conditions of modal formulas by means of polynomials, but also permits to perform deductions through polynomial handling. This paper also investigates relationships among the PRC here defined, the algebraic semantics for modal logics, equational logics, the Dijkstra???Scholten equational-proof style, and rewriting systems. The method proposed is throughly exemplified for S 5, and can be easily extended to other (...) modal logics. (shrink)
Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using a three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. We solve this (...) problem by applying recent methods from sorted logics. This paper presents a tableau calculus that combines the proper treatment of partial functions with the efficiency of sorted calculi. (shrink)
The derivative is a basic concept of differential calculus. However, if we calculate the derivative as change in distance over change in time, the result at any instant is 0/0, which seems meaningless. Hence, Newton and Leibniz used the limit to determine the derivative. Their method is valid in practice, but it is not easy to intuitively accept. Thus, this article describes the novel method of differential calculus based on the double contradiction, which is easier to accept intuitively. (...) Next, the geometrical meaning of the double contradiction is considered as follows. A tangent at a point on a convex curve is iterated. Then, the slope of the tangent at the point is sandwiched by two kinds of lines. The first kind of line crosses the curve at the original point and a point to the right of it. The second kind of line crosses the curve at the original point and a point to the left of it. Then, the double contradiction can be applied, and the slope of the tangent is determined as a single value. Finally, the meaning of this method for the foundation of mathematics is considered. We reflect on Dehaene’s notion that the foundation of mathematics is based on the intuitions, which evolve independently. Hence, there may be gaps between intuitions. In fact, the Ancient Greeks identified inconsistency between arithmetic and geometry. However, Eudoxus developed the theory of proportion, which is equivalent to the Dedekind Cut. This allows the iteration of an irrational number by rational numbers as precisely as desired. Simultaneously, we can define the irrational number by the double contradiction, although its existence is not guaranteed. Further, an area of a curved figure is iterated and defined by rectilinear figures using the double contradiction. (shrink)
The paper is an introduction to geometric algebra and geometric calculus for those with a knowledge of undergraduate mathematics. No knowledge of physics is required. The section Further Study lists many papers available on the web.
Vector models of language are based on the contextual aspects of language, the distributions of words and how they co-occur in text. Truth conditional models focus on the logical aspects of language, compositional properties of words and how they compose to form sentences. In the truth conditional approach, the denotation of a sentence determines its truth conditions, which can be taken to be a truth value, a set of possible worlds, a context change potential, or similar. In the vector models, (...) the degree of co-occurrence of words in context determines how similar the meanings of words are. In this paper, we put these two models together and develop a vector semantics for language based on the simply typed lambda calculus models of natural language. We provide two types of vector semantics: a static one that uses techniques familiar from the truth conditional tradition and a dynamic one based on a form of dynamic interpretation inspired by Heim’s context change potentials. We show how the dynamic model can be applied to entailment between a corpus and a sentence and provide examples. (shrink)
Building on the work of Peter Hinst and Geo Siegwart, we develop a pragmatised natural deduction calculus, i.e. a natural deduction calculus that incorporates illocutionary operators at the formal level, and prove its adequacy. In contrast to other linear calculi of natural deduction, derivations in this calculus are sequences of object-language sentences which do not require graphical or other means of commentary in order to keep track of assumptions or to indicate subproofs. (Translation of our German paper (...) "Ein Redehandlungskalkül. Ein pragmatisierter Kalkül des natürlichen Schließens nebst Metatheorie"; online available at http://philpapers.org/rec/CORERE.). (shrink)
John Venn has the “uneasy suspicion” that the stagnation in mathematical logic between J. H. Lambert and George Boole was due to Kant’s “disastrous effect on logical method,” namely the “strictest preservation [of logic] from mathematical encroachment.” Kant’s actual position is more nuanced, however. In this chapter, I tease out the nuances by examining his use of Leonhard Euler’s circles and comparing it with Euler’s own use. I do so in light of the developments in logical calculus from G. (...) W. Leibniz to Lambert and Gottfried Ploucquet. While Kant is evidently open to using mathematical tools in logic, his main concern is to clarify what mathematical tools can be used to achieve. For without such clarification, all efforts at introducing mathematical tools into logic would be blind if not complete waste of time. In the end, Kant would stress, the means provided by formal logic at best help us to express and order what we already know in some sense. No matter how much mathematical notations may enhance the precision of this function of formal logic, it does not change the fact that no truths can, strictly speaking, be revealed or established by means of those notations. (shrink)
The formalisation of Natural Language arguments in a formal language close to it in syntax has been a central aim of Moss’s Natural Logic. I examine how the Quantified Argument Calculus (Quarc) can handle the inferences Moss has considered. I show that they can be incorporated in existing versions of Quarc or in straightforward extensions of it, all within sound and complete systems. Moreover, Quarc is closer in some respects to Natural Language than are Moss’s systems – for instance, (...) is does not use negative nouns. The process also sheds light on formal properties and presuppositions of some inferences it formalises. Directions for future work are outlined. (shrink)
Create an account to enable off-campus access through your institution's proxy server.
Monitor this page
Be alerted of all new items appearing on this page. Choose how you want to monitor it:
Email
RSS feed
About us
Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.