Logics without the contraction rule

1985 ◽  
Vol 50 (1) ◽  
pp. 169-201 ◽  
Author(s):  
Hiroakira Ono ◽  
Yuichi Komori
Keyword(s):  
Intuitionistic Logic ◽  
Formal System ◽  
The Other ◽  
Promising Tool ◽  
Nonclassical Logics ◽  
Relevant Logics ◽  
Exchange Rule ◽  
Distributive Law ◽  
Image Position ◽  
Partially Ordered Monoids

We will study syntactical and semantical properties of propositional logics weaker than the intuitionistic, in which the contraction rule (or, the exchange rule or the weakening rule, in some cases) does not hold. Here, the contraction rule means the rule of inference of the formif we formulate our logics in a Gentzen-type formal system. Some syntactical properties of these logics have been studied firstly by the second author in [11], in connection with the study of BCK-algebras (for information on BCK-algebras, see [9]). There, it turned out that such a syntactical method is a powerful and promising tool in studying BCK-algebras. Using this method, considerable progress has been made since then (see, e.g., [8], [18], [27]).In this paper, we will study these logics more comprehensively. We notice here that the distributive lawdoes not hold necessarily in these logics. By adding some axioms (or initial sequents) and rules of inference to these basic logics, we can obtain a lot of interesting nonclassical logics such as Łukasiewicz's many-valued logics, relevant logics, the intuitionistic logic and logics related to BCK-algebras, which have been studied separately until now. Thus, our approach will give a uniform way of dealing with these logics. One of our two main tools in doing so is Gentzen-type formulation of logics in syntax, and the other is semantics defined by using partially ordered monoids.

Completeness of global intuitionistic set theory

1997 ◽  
Vol 62 (2) ◽  
pp. 506-528 ◽  
Author(s):  
Satoko Titani
Keyword(s):  
Set Theory ◽  
Intuitionistic Logic ◽  
Classical Logic ◽  
Mathematical Object ◽  
The Other ◽  
Logical System ◽  
Logical Operators ◽  
Logical Symbol ◽  
Image Position ◽  
Intuitionistic Set Theory

Gentzen's sequential system LJ of intuitionistic logic has two symbols of implication. One is the logical symbol → and the other is the metalogical symbol ⇒ in sequentsConsidering the logical system LJ as a mathematical object, we understand that the logical symbols ∧, ∨, →, ¬, ∀, ∃ are operators on formulas, and ⇒ is a relation. That is, φ ⇒ Ψ is a metalogical sentence which is true or false, on the understanding that our metalogic is a classical logic. In other words, we discuss the logical system LJ in the classical set theory ZFC, in which φ ⇒ Ψ is a sentence.The aim of this paper is to formulate an intuitionistic set theory together with its metatheory. In Takeuti and Titani [6], we formulated an intuitionistic set theory together with its metatheory based on intuitionistic logic. In this paper we postulate that the metatheory is based on classical logic.Let Ω be a cHa. Ω can be a truth value set of a model of LJ. Then the logical symbols ∧, ∨, →, ¬, ∀x, ∃x are interpreted as operators on Ω, and the sentence φ ⇒ Ψ is interpreted as 1 (true) or 0 (false). This means that the metalogical symbol ⇒ also can be expressed as a logical operators such that φ ⇒ Ψ is interpreted as 1 or 0.

On derivability

1937 ◽  
Vol 2 (3) ◽  
pp. 113-119 ◽  
Author(s):  
W. V. Quine
Keyword(s):  
Formal System ◽  
Free Variable ◽  
The Other ◽  
Free Variables ◽  
Image Position ◽  
Positive Integers

1. The notion of derivability. Italic capitals, with or without subscripts, will be used as variables. They are to take as values some manner of elements which may for the present be left undetermined. Now let us consider abstractly the notion of the derivability of an element X from one or more specified elements by a series of steps of a specified kind. This involves reference to two conditions upon elements. One of these conditions, expressible by some statement form containing a single free variable, determines the elements from which X is said to be derivable. The other condition, expressed say by a statement form containing k + 1 free variables, determines the kind of steps by which the derivation is to proceed; it is the condition which any elements Z1, … Zk, Y must fulfill if progress from Zi, …, Zk to Y is to constitute a step of derivation in the intended sense. Supposing “f(Y)” supplanted by the first of these statement forms, whatever it may be, and “g(Z1, …, Zk, Y)” supplanted by the other, let us adopt the form of notationto express derivability of X in the suggested sense. The meaning of (1) can be formulated more accurately as follows:(i) There are elements Y1 to Ym (for some m) such that Ym = X and, for each i≦m, either f(Yi) or else there are numbers j1 to Ym, each less than i, for which g(Yj1, …, Yjk, Yi).(Variable subscripts are to be understood, here and throughout the paper, as referring only to positive integers.)The notion (1) is illustrated in the ancestral R* of a relation R;1 for,Another illustration is afforded by metamathematics. Suppose our elements are the expressions used in some formal system; suppose we have defined “Post(Y)”, meaning that Y is a postulate of that system; and suppose we have defined “Inf(ZI, …, Zk, Y)” (for some fixed k large enough for all purposes of the system in question), meaning that Y proceeds from Z1, …, Zk by one application of one or another of the rules of inference of the system. Thenwould mean that X is a theorem of the system.

A polynomial translation of S4 into intuitionistic logic

2006 ◽  
Vol 71 (3) ◽  
pp. 989-1001 ◽  
Author(s):  
David Fernandez
Keyword(s):  
Model Checking ◽  
Intuitionistic Logic ◽  
The Other ◽  
Kripke Semantics ◽  
Topological Semantics ◽  
Finite Set ◽  
Image Position ◽  
Polynomial Translation

It is known that both S4 and the Intuitionistic prepositional calculus Int are P-SPACE complete. This guarantees that there is a polynomial translation from each system into the other.However, no sound and faithful polynomial translation from S4 into Int is commonly known. The problem of finding one was suggested by Dana Scott during a very informal gathering of logicians in February 2005 at UCLA. Grigori Mints then brought it to my attention, and in this paper I present a solution. It is based on Kripke semantics and describes model-checking for S4 using formulas of Int.A simple translation from Int into S4, the Gödel-Tarski translation, is wellknown; given a formula φ of Int, one obtains by prefixing □ to every subformula. For example,.That the translation is sound and faithful can be seen by considering topological semantics, which assign open sets both to □-formulas of S4 and arbitrary formulas of Int; the interpretation of φ and turn out to be identical. See Tarski's paper [6] for details. Gödel's original paper can be found in [3].In [2], Friedman and Flagg present a kind of inverse to Gödel-Tarski. Given a formula φ of S4 and a finite set of formulas Γ of Int, for each ε ∈ Γ one gets an intuitionistic formula given recursively by

TRANSLATIONS BETWEEN LINEAR AND TREE NATURAL DEDUCTION SYSTEMS FOR RELEVANT LOGICS

2021 ◽  
pp. 1-22
Author(s):  
SHAWN STANDEFER
Keyword(s):  
Natural Deduction ◽  
The Other ◽  
Relevant Logics

Abstract Anderson and Belnap presented indexed Fitch-style natural deduction systems for the relevant logics R, E, and T. This work was extended by Brady to cover a range of relevant logics. In this paper I present indexed tree natural deduction systems for the Anderson–Belnap–Brady systems and show how to translate proofs in one format into proofs in the other, which establishes the adequacy of the tree systems.

scholarly journals The Dissociation of the Compound of Iodine and Thio-urea

1904 ◽  
Vol 24 ◽  
pp. 233-239 ◽  
Author(s):  
Hugh Marshall
Keyword(s):  
Nitric Acid ◽  
General Formula ◽  
Free Acid ◽  
The Other ◽  
Image Position

When thio-urea is treated with suitable oxidising agents in presence of acids, salts are formed corresponding to the general formula (CSN2H4)2X2:—Of these salts the di-nitrate is very sparingly soluble, and is precipitated on the addition of nitric acid or a nitrate to solutions of the other salts. The salts, as a class, are not very stable, and their solutions decompose, especially on warming, with formation of sulphur, thio-urea, cyanamide, and free acid. A corresponding decomposition results immediately on the addition of alkali, and this constitutes a very characteristic reaction for these salts.

Extremely undecidable sentences

1982 ◽  
Vol 47 (1) ◽  
pp. 191-196 ◽  
Author(s):  
George Boolos
Keyword(s):  
Modal Logic ◽  
The Other ◽  
Propositional Modal Logic ◽  
Image Position

Let ‘ϕ’, ‘χ’, and ‘ψ’ be variables ranging over functions from the sentence letters P0, P1, … Pn, … of (propositional) modal logic to sentences of P(eano) Arithmetic), and for each sentence A of modal logic, inductively define Aϕ by[and similarly for other nonmodal propositional connectives]; andwhere Bew(x) is the standard provability predicate for PA and ⌈F⌉ is the PA numeral for the Gödel number of the formula F of PA. Then for any ϕ, (−□⊥)ϕ = −Bew(⌈⊥⌉), which is the consistency assertion for PA; a sentence S is undecidable in PA iff both and , where ϕ(p0) = S. If ψ(p0) is the undecidable sentence constructed by Gödel, then ⊬PA (−□⊥→ −□p0 & − □ − p0)ψ and ⊢PA(P0 ↔ −□⊥)ψ. However, if ψ(p0) is the undecidable sentence constructed by Rosser, then the situation is the other way around: ⊬PA(P0 ↔ −□⊥)ψ and ⊢PA (−□⊥→ −□−p0 & −□−p0)ψ. We call a sentence S of PA extremely undecidable if for all modal sentences A containing no sentence letter other than p0, if for some ψ, ⊬PAAψ, then ⊬PAAϕ, where ϕ(p0) = S. (So, roughly speaking, a sentence is extremely undecidable if it can be proved to have only those modal-logically characterizable properties that every sentence can be proved to have.) Thus extremely undecidable sentences are undecidable, but neither the Godel nor the Rosser sentence is extremely undecidable. It will follow at once from the main theorem of this paper that there are infinitely many inequivalent extremely undecidable sentences.

On functional Nörlund methods

1970 ◽  
Vol 67 (1) ◽  
pp. 47-60 ◽  
Author(s):  
B. Choudhary
Keyword(s):  
The Other ◽  
Integral Transformations ◽  
Other Hand ◽  
Nörlund Means ◽  
The One ◽  
Image Position

Integral transformations analogous to the Nörlund means have been introduced and investigated by Kuttner, Knopp and Vanderburg(6), (5), (4). It is known that with any regular Nörlund mean (N, p) there is associated a functionregular for |z| < 1, and if we have two Nörlund means (N, p) and (N, r), where (N, pr is regular, while the function is regular for |z| ≤ 1 and different) from zero at z = 1, then q(z) = r(z)p(z) belongs to a regular Nörlund mean (N, q). Concerning Nörlund means Peyerimhoff(7) and Miesner (3) have recently obtained the relation between the convergence fields of the Nörlund means (N, p) and (N, r) on the one hand and the convergence field of the Nörlund mean (N, q) on the other hand.

scholarly journals Distribution of rational points on the real line

1973 ◽  
Vol 15 (2) ◽  
pp. 243-256 ◽  
Author(s):  
T. K. Sheng
Keyword(s):  
Algebraic Number ◽  
Rational Number ◽  
Real Line ◽  
Rational Points ◽  
The Other ◽  
Liouville Numbers ◽  
The Real ◽  
Other Hand ◽  
Image Position

It is well known that no rational number is approximable to order higher than 1. Roth [3] showed that an algebraic number is not approximable to order greater than 2. On the other hand it is easy to construct numbers, the Liouville numbers, which are approximable to any order (see [2], p. 162). We are led to the question, “Let Nn(α, β) denote the number of distinct rational points with denominators ≦ n contained in an interval (α, β). What is the behaviour of Nn(α, + 1/n) as α varies on the real line?” We shall prove that and that there are “compressions” and “rarefactions” of rational points on the real line.

3. Laboratory Notes by Professor Tait (a.) Measurement of the Potential, required to produce Sparks of various lengths, in Air at different pressures, by a Holtz Machine

1878 ◽  
Vol 9 ◽  
pp. 332-333
Author(s):  
Messrs Macfarlane ◽  
Paton
Keyword(s):  
General Result ◽  
The Other ◽  
Considerable Distance ◽  
Image Position

The general result of these strictly preliminary experiments appears to show that for sparks not exceeding a decimetre in length (L), taken in air at different pressures (P), between two metal balls of 7mm·5 radius, the requisite potential (V), is expressed by the formulaThe Holtz machine employed is a double one, made by Ruhmkorff, and it was used with its small Leyden jars attached. The measurements had to be made with a divided-ring electrometer, so that two insulated balls, at a considerable distance from one another, were connected, one with the machine, the other with the electrometer.

scholarly journals Certain Mathematical Instruments for Graphically Indicating the Direction of Refracted and Reflected Light Rays

1906 ◽  
Vol 25 (2) ◽  
pp. 806-812
Author(s):  
J.R. Milne
Keyword(s):  
Optical System ◽  
The Other ◽  
Reflected Light ◽  
Light Rays ◽  
Image Position

The refraction equation sin i == μ sin r, though simple in itself, is apt to give rise, in problems connected with refraction, to formulæ too involved for arithmetical computation. In such cases it may be necessary to trace the course through the optical system in question of a certain number of arbitrarily chosen rays, and thence to find the course of the other rays by interpolation. Thelinkage about to be described affords a rapid and accurate means of determining the paths of the rays through any optical system.

Sign in / Sign up

Export Citation Format

Share Document