Legal terms, such as “ownership,”“contract,”“validity,”“negligence,” are used as middle terms in legal deduction. The paper distinguishes two problems regarding this use. One is the logical function of terms for deduction within a normative system. Specific problems dealt with in this connection are meaning, definition, and economy of expression. The other problem connected with middle terms is the “moulding” and possible manipulation of the meaning of legal terms, for arriving at desired conclusions in a given scheme of inference. It is indicated (...) how the moulding of contested legal concepts, if not restricted, will obscure the ratio of legal rules. This problem is relevant, inter alia, to arguments ex analogia in the law. (shrink)

This paper deals with the system of modal logicGL, in particular with a formulation of it in terms of sequents. We prove some proof theoretical properties ofGL that allow to get the cut-elimination theorem according to Gentzen's procedure, that is, by double induction on grade and rank.

Peirce wrote in late 1901 a text on formal logic using a special Dragon-Head and Dragon-Tail notation in order to express the relation of logical consequence and its properties. These texts have not been referred to in the literature before. We provide a complete reconstruction and transcription of these previously unpublished sets of manuscript sheets and analyse their main content. In the reconstructed text, Peirce is seen to outline both a general theory of deduction and a general theory of consequence (...) relation. The two are the cornerstones of modern logic and have played a crucial role in its development. From the wider perspective, Peirce is led to these theories by three important generalizations: propositions to all signs, truth to scriptibility, and derivation to transformability. We provide an exposition of such proposed semiotic foundation for logical constants and point out a couple of further innovations in this rare text, including the sheet of assertion, correction as a dual of deduction and the nature of conditionals as variably strict conditionals. (shrink)

Linguistic inter-understanding is a communicative phenomenon that is well known and that has been studied in detail. It basically consists of the fact that an individual speaking a language is able to understand another person speaking a different language, and this without deeply knowing this last language or being able to express himself/herself in it. The phenomenon, which is especially frequent in the case of very similar languages, occurs because of certain inferential processes that can happen in the human mind (...) when people try to interpret information in a distinct language. In this way, the main aim of this paper is to show how such processes are very akin to some of those that the mental models theory attributes to the human reasoning ability, and that hence linguistic inter-understanding can be considered as evidence that this last theory is, at least partially, correct. (shrink)

The double negation has always been considered by the logical systems from ancient times to the present. In fact, that is an issue that the current syntactic theories studying human reasoning, for example, the mental logic theory, address today. However, in this paper, I claim that, in the case of some languages such as Spanish, the double negation causes problems for the cognitive theories mainly based on formal schemata and supporting the idea of a universal syntax of thought in the (...) human mind. Thus, I propose that, given those problems, semantic frameworks such as that of the mental models theory seem to be more appropriate for explaining the human inferential activity. (shrink)

The present endeavour aims at the clarification of the concept of the logical consequence. Initially we investigate the question: How was the concept of logical consequence discovered by the medieval philosophers? Which ancient philosophical foundations were necessary for the discovery of the logical relation of consequence and which explicit medieval contributions, such as the notion of the formality (formal validity), led to its discovery. Secondly we discuss which developments of modern philosophy effected the turn from the medieval concept of logical (...) consequence to its most recent conceptions, such as the semantic, syntactic, axiomatic and natural deductive approaches? Thirdly we examine which are the similarities and the differences between the logical concepts of consequence, inference, implication and entailment? Furthermore, we ask what kind of relation signifies the concept of the logical consequence? That is to say, which is the analytic definition of the consequence relation R between the premises p1, p2...pn and the conclusion c of a formally valid argument? Finally, we focus on the respective answers given through the developments in proof theory by David Hilbert and Gerhard Gentzen. (shrink)

Hilbert's conference lectures during the year 1922, Neuebegründung der Mathematik. Erste Mitteilung and Die logischen Grundlagen der Mathematik (both are published in (Hilbert [1935] 1965) pp. 157-195), contain his first public presentation of an axiom system for propositional logic, or at least for a fragment of propositional logic, which is largely influenced by the study on logical woks of Frege and Russell during the previous years.The year 1922 is at the beginning of Hilbert's foundational program in its definitive form. The (...) final public presentation by Hilbert of an axiom system for propositional logic is contained in the 1934 book Grundlagen der Mathematik, I (Hilbert and Bernays [1934] 1968). Sequent .. (shrink)

We present nested sequent systems for propositional Gödel-Dummett logic and its first-order extensions with non-constant and constant domains, built atop nested calculi for intuitionistic logics. To obtain nested systems for these Gödel-Dummett logics, we introduce a new structural rule, called the linearity rule, which (bottom-up) operates by linearising branching structure in a given nested sequent. In addition, an interesting feature of our calculi is the inclusion of reachability rules, which are special logical rules that operate by propagating data and/or checking (...) if data exists along certain paths within a nested sequent. Such rules require us to generalise our nested sequents to include signatures (i.e. finite collections of variables) in the first-order cases, thus giving rise to a generalisation of the usual nested sequent formalism. Our calculi exhibit favourable properties, admitting the height-preserving invertibility of every logical rule and the (height-preserving) admissibility of a large collection of structural and reachability rules. We prove all of our systems sound and cut-free complete, and show that syntactic cut-elimination obtains for the intuitionistic systems. We conclude the paper by discussing possible extensions and modifications, putting forth an array of structural rules that could be used to provide a sizable class of intermediate logics with cut-free nested sequent systems. (shrink)

Šiuo straipsniu mėginama parodyti, jog Indijos ir stoikų logika yra panašesnės viena į kitą nei į standartinę logiką. Šiuo tikslu analizuojama ištrauka iš Kathāvatthu, kurioje pateikiamas sąlyginio teiginio apibrėžimas dažnai interpretuojamas kaip atitinkantis modernioje teiginių logikoje vartojamą materialiosios implikacijos sampratą. Teigiama, jog tokia interpretacija nėra visiškai pagrįsta. Todėl daroma išvada, jog tai, kas iš tiesų sakoma aptariamoje ištraukoje, nuosekliai susiję su Chrisipo Soliečio pasiūlytu sąlyginio teiginio teisingumo kriterijumi.

In this paper we examine two approaches to the formal treatment of the notion of problem in the paradigm of algorithmic semantics. Namely, we will explore an approach based on Martin-Löf’s Constructive Type Theory, which can be seen as a direct continuation of Kolmogorov’s original calculus of problems, and an approach utilizing Tichý’s Transparent Intensional Logic, which can be viewed as a non-constructive attempt of interpreting Kolmogorov’s logic of problems. In the last section we propose Kolmogorov and CTT-inspired modifications to (...) TIL-based approach. The focus will be on non-empirical problems only. (shrink)

In this note, we will study four implicational logicsB, BI, BB and BBI. In [5], Martin and Meyer proved that a formula is provable inBB if and only if is provable inBBI and is not of the form of » . Though it gave a positive solution to theP - W problem, their method was semantical and not easy to grasp. We shall give a syntactical proof of the syntactical relation betweenBB andBBI logics. It also includes a syntactical proof of (...) Powers and Dwyer's theorem that is proved semantically in [5]. Moreover, we shall establish the same relation betweenB andBI logics asBB andBBI logics. This relation seems to say thatB logic is meaningful, and so we think thatB logic is the weakest among meaningful logics. Therefore, by Theorem 1.1, our Gentzentype system forBI logic may be regarded as the most basic among all meaningful logics. It should be mentioned here that the first syntactical proof ofP - W problem is given by Misao Nagayama [6]. (shrink)

Non-classical negations may fail to be contradictory-forming operators in more than one way, and they often fail also to respect fundamental meta-logical properties such as the replacement property. Such drawbacks are witnessed by intricate semantics and proof systems, whose philosophical interpretations and computational properties are found wanting. In this paper we investigate congruential non-classical negations that live inside very natural systems of normal modal logics over complete distributive lattices; these logics are further enriched by adjustment connectives that may be used (...) for handling reasoning under uncertainty caused by inconsistency or undeterminedness. Using such straightforward semantics, we study the classes of frames characterized by seriality, reflexivity, functionality, symmetry, transitivity, and some combinations thereof, and discuss what they reveal about sub-classical properties of negation. To the logics thereby characterized we apply a general mechanism that allows one to endow them with analytic ordinary sequent systems, most of which are even cut-free. We also investigate the exact circumstances that allow for classical negation to be explicitly defined inside our logics. (shrink)

Substructural logics are logics obtained from a sequent formulation of intuitionistic or classical logic by rejecting some structural rules. The substructural logics considered here are linear logic, relevant logic and BCK logic. It is proved that first-order variants of these logics with an intuitionistic negation can be embedded by modal translations into S4-type extensions of these logics with a classical, involutive, negation. Related embeddings via translations like the double-negation translation are also considered. Embeddings into analogues of S4 are obtained with (...) the help of cut elimination for sequent formulations of our substructural logics and their modal extensions. These results are proved for systems with equality too. (shrink)

The current formal theories trying to account for reasoning and language often need to resort to the thesis of the pragmatic or implicit premises to explain the real role pragmatics plays in the human inferential activity. The main aim of this paper is to show that, although they did not propose theories in this way, the Stoics, by means of their concept of ‘sign’, already offered the essential arguments and foundations necessary to describe the real action of both pragmatics and (...) the premises coming from general knowledge when we make inferences. (shrink)

ABSTRACTIn this paper, we present a generalisation of proof simulation procedures for Frege systems by Bonet and Buss to some logics for which the deduction theorem does not hold. In particular, we study the case of finite-valued Łukasiewicz logics. To this end, we provide proof systems and which augment Avron's Frege system HŁuk with nested and general versions of the disjunction elimination rule, respectively. For these systems, we provide upper bounds on speed-ups w.r.t. both the number of steps in proofs (...) and the length of proofs. We also consider Tamminga's natural deduction and Avron's hypersequent calculus GŁuk for 3-valued Łukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued Łukasiewicz logics. (shrink)

We expose some basic elements of a style of programming supported by functional languages like Haskell by relating them to a coherent set of notions and techniques from Curry’s work in combinatory logic and formal systems, and their algebraic and categorical interpretations. Our account takes the form of a commentary to a simple fragment of Haskell code attempting to isolate the conceptual sources of the linguistic abstractions involved.

In this paper we give a new proof of cut elimination in Gentzen's sequent system for intuitionistic first-order predicate logic. The point of this proof is that the elimination procedure eliminates the cut rule itself, rather than the mix rule.

Recientemente, se ha propuesto que la lógica no es el único factor que incide en el razonamiento condicional y que el valor y la utilidad son otros dos elementos importantes en este sentido. Al respecto, Bonnefon y Sloman añadieron en 2013 que la estructura de los condicionales es, del mismo modo, relevante en la actividad inferencial con condicionales de utilidad y trataron de demostrarlo por medio de varios experimentos. Sus resultados parecieron mostrar que, efectivamente, sus tesis eran correctas. No obstante, (...) plantearon igualmente que su propuesta y, por tanto, sus resultados eran compatibles con una teoría contemporánea de amplio alcance, la teoría de los modelos mentales, y en este artículo se trata de desarrollar esta idea con el propósito de comprobar si es cierta. (shrink)

The seminal book on graph theory by Dénes Kőnig, published in the year 1936, collected notions and results from precursory works from the mid to late nineteenth century by Hamilton, Cayley, Sylvester and others. More importantly, Kőnig himself contributed many of his own results that he had obtained in the more than twenty years that he had been working on this subject matter. What is noteworthy is the fact that the fundamentals of what he calls directed graphs are taken almost (...) exhaustively from Paul Hertz' 1922 article on structural reasoning about sentences of the form a→b. This is not a fact that is well known in logical circles, even though Kőnig fully acknowledges this in his book. In view of the numerous trends in the recent decades to describe and explicate logical matters by means of graphs, the fact that it was Hertz' foundation of structural reasoning that informed basic notions of graph theory in the first place is highly significant. The main goal of this paper is to summarize Hertz' article and demonstrate how Kőnig integrates the notions and results presented therein in his book. This is followed by an exposition of how and when Hertz' results were reinvented in terms of graph theory. A critical discussion of the opinion expressed by both Hertz and Kőnig that the more general sentences of the form (a1,…,an)→b, introduced by Hertz in a companion article in 1923, cannot be interpreted by graphs concludes this paper. (shrink)