Implicational logics in natural deduction systems

1982 ◽  
Vol 47 (1) ◽  
pp. 184-186 ◽  
Author(s):  
E.G.K. López-Escobar
Keyword(s):  
Natural Deduction ◽  
Short Note ◽  
Direct Proof ◽  
Modus Ponens ◽  
Implicational Logics

In 1959 M. Dummett [3] introduced the logic LC obtained by adding the axiom ACpqCqp to the formalization of the intuitionistic prepositional calculus having modus ponens and substitution as its rules of inference. Later on R. A. Bull [1] showed, by quite a roundabout way, that the implicational theses of LC were precisely the theses of the implicational calculus obtained by adding the axiom CCCpqrCCCqprr to the system of positive implication. In 1964 Bull [2] gave another proof, this time using results of Birkhoff concerning subdirectly reducible algebras.The aim of this short note is to emphasize that the use of Gentzen's natural deduction systems (see Prawitz [4]) allows us to give a much more direct proof.

Gentzen's Proof of Normalization for Natural Deduction

2008 ◽  
Vol 14 (2) ◽  
pp. 240-257 ◽  
Author(s):  
Jan von Plato
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Direct Proof ◽  
Cut Elimination ◽  
Doctoral Thesis ◽  
Detailed Proof ◽  
Normalization Theorem ◽  
The One ◽  
The Right ◽  
Special Case

AbstractGentzen writes in the published version of his doctoral thesis Untersuchungen über das logische Schliessen (Investigations into logical reasoning) that he was able to prove the normalization theorem only for intuitionistic natural deduction, but not for classical. To cover the latter, he developed classical sequent calculus and proved a corresponding theorem, the famous cut elimination result. Its proof was organized so that a cut elimination result for an intuitionistic sequent calculus came out as a special case, namely the one in which the sequents have at most one formula in the right, succedent part. Thus, there was no need for a direct proof of normalization for intuitionistic natural deduction. The only traces of such a proof in the published thesis are some convertibilities, such as when an implication introduction is followed by an implication elimination [1934–35, II.5.13]. It remained to Dag Prawitz in 1965 to work out a proof of normalization. Another, less known proof was given also in 1965 by Andres Raggio.We found in February 2005 an early handwritten version of Gentzen's thesis, with exactly the above title, but with rather different contents: Most remarkably, it contains a detailed proof of normalization for what became the standard system of natural deduction. The manuscript is located in the Paul Bernays collection at the ETH-Zurichwith the signum Hs. 974: 271. Bernays must have gotten it well before the time of his being expelled from Göttingen on the basis of the racial laws in April 1933.

scholarly journals An analog of Thompson's triangle inequality in Euclidean Jordan algebras

2021 ◽  
Vol 37 (37) ◽  
pp. 156-159
Author(s):  
Jiyuan Tao
Keyword(s):  
Linear Algebra ◽  
Jordan Algebra ◽  
Triangle Inequality ◽  
Short Note ◽  
Direct Proof ◽  
Case Analysis ◽  
Euclidean Jordan Algebra ◽  
Jordan Algebras ◽  
Euclidean Jordan Algebras

In a recent paper [Linear Algebra Appl., 461:92--122, 2014], Tao et al. proved an analog of Thompson's triangle inequality for a simple Euclidean Jordan algebra by using a case-by-case analysis. In this short note, we provide a direct proof that is valid on any Euclidean Jordan algebras.

SHEFFER’S STROKE: A STUDY IN PROOF-THEORETIC HARMONY

1999 ◽  
Vol 34 (1) ◽  
pp. 7-23 ◽  
Author(s):  
Stephen Read
Keyword(s):  
Classical Logic ◽  
Natural Deduction ◽  
Complete System ◽  
Direct Proof ◽  
Double Negation ◽  
Logical Constants ◽  
Indirect Proof ◽  
Deduction Rules

In order to explicate Gentzen’s famous remark that the introduction-rules for logical constants give their meaning, the elimination-rules being simply consequences of the meaning so given, we develop natural deduction rules for Sheffer’s stroke, alternative denial. The first system turns out to lack Double Negation. Strengthening the introduction-rules by allowing the introduction of Sheffer’s stroke into a disjunctive context produces a complete system of classical logic, one which preserves the harmony between the rules which Gentzen wanted: all indirect proof reduces to direct proof.

scholarly journals Redirecting Proofs by Contradiction

10.29007/wm8b ◽  
2018 ◽  
Author(s):  
Jasmin Christian Blanchette
Keyword(s):  
Natural Deduction ◽  
Direct Proof ◽  
Theorem Prover ◽  
Automatic Theorem

This paper presents an algorithm that redirects proofs by contradiction. The input is a refutation graph, as produced by an automatic theorem prover (e.g., E, SPASS, Vampire, Z3); the output is a direct proof expressed in natural deduction extended with case analyses and nested subproofs. The algorithm is implemented in Isabelle’s Sledgehammer, where it enhances the legibility of machine-generated proofs.

A lambda proof of the P-W theorem

2000 ◽  
Vol 65 (4) ◽  
pp. 1841-1849
Author(s):  
Sachio Hirokawa ◽  
Yuichi Komori ◽  
Misao Nagayama
Keyword(s):  
Intuitionistic Logic ◽  
Natural Deduction ◽  
Modus Ponens ◽  
Logical System ◽  
System P

AbstractThe logical system P-W is an implicational non-commutative intuitionistic logic denned by axiom schemes B − (b → c) → (a → b) → a → c. B′ = (a → b) → (b → c) → a → c. I - a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α - β holds if α → β and β → α are both provable in P-W. The answer is affirmative. The first to prove this was E. P. Martin by a semantical method.In this paper, we give the first proof of Martin's theorem based on the theory of simply typed λ-calculus. This proof is obtained as a corollary to the main theorem of this paper, shown without using Martin's Theorem, that any closed hereditary right-maximal linear (HRML) λ-term of type α → α is βη-reducible to λxx. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style.

The proofs of α → α in P – W

1996 ◽  
Vol 61 (1) ◽  
pp. 195-211 ◽  
Author(s):  
Sachio Hirokawa
Keyword(s):  
Normal Form ◽  
Natural Deduction ◽  
Syntactic Structure ◽  
Modus Ponens ◽  
Relevant Logic

AbstractThe syntactic structure of the system of pure implicational relevant logic P − W is investigated. This system is defined by the axioms B = (b → c) → (a → b) → a → c, B′ = (a → b) → (b → c)→ a → c, I = a → a, and the rules of substitution and modus ponens. A class of λ-terms, the closed hereditary right-maximal linearλ-terms, and a translation of such λ-terms M to BB′ I-combinators M+ is introduced. It is shown that a formula a is provable in P − W if and only if α is a type of some λ-term in this class. Hence these λ-terms represent proof figures in the Natural Deduction version of P − W.Errol Martin (1982) proved that no formula with form α → α is provable in P − W without using the axiom I. We show that a β-normal form λ-term M in the class is η reducible to λx.x if the translated BB′ I-combinator M+ contains I. Using this theorem and Martin's result, we prove that a λ-term in the class is βη-reducible to λx.x if the λ-term has a type α → α. Hence the structure of proofs of α → α in P − W is determined.

scholarly journals The Laws of Natural Deduction in Inference by DNA Computer

2014 ◽  
Vol 2014 ◽  
pp. 1-10 ◽  
Author(s):  
Łukasz Rogowski ◽  
Petr Sosík
Keyword(s):  
Restriction Enzyme ◽  
Propositional Logic ◽  
Natural Deduction ◽  
Reaction System ◽  
Modus Ponens ◽  
Simultaneous Occurrence ◽  
Modus Tollens ◽  
Inference Process ◽  
Basic Facts ◽  
Improved Design

We present a DNA-based implementation of reaction system with molecules encoding elements of the propositional logic, that is, propositions and formulas. The protocol can perform inference steps using, for example,modus ponensandmodus tollensrules and de Morgan’s laws. The set of the implemented operations allows for inference of formulas using the laws of natural deduction. The system can also detect whether a certain propositionacan be deduced from the basic facts and given rules. The whole protocol is fully autonomous; that is, after introducing the initial set of molecules, no human assistance is needed. Only one restriction enzyme is used throughout the inference process. Unlike some other similar implementations, our improved design allows representing simultaneously a factaand its negation ~a, including special reactions to detect the inconsistency, that is, a simultaneous occurrence of a fact and its negation. An analysis of correctness, completeness, and complexity is included.

Convergent-bceam diffraction studies on lead zirconate titanate Ceramics

1986 ◽  
Vol 44 ◽  
pp. 482-483
Author(s):  
M.L.A. Dass ◽  
T.A. Bielicki ◽  
G. Thomas ◽  
T. Yamamoto ◽  
K. Okazaki
Keyword(s):  
Lead Zirconate Titanate ◽  
Direct Proof ◽  
Lead Zirconate ◽  
Subsolidus Phase ◽  
Pzt Ceramics ◽  
Subsolidus Phase Diagram ◽  
Zirconate Titanate ◽  
Two Phases ◽  
Cbd Method ◽  
Titanate Ceramics

Lead zirconate titanate, Pb(Zr,Ti)O3 (PZT), ceramics are ferroelectrics formed as solid solutions between ferroelectric PbTiO3 and ant iferroelectric PbZrO3. The subsolidus phase diagram is shown in figure 1. PZT transforms between the Ti-rich tetragonal (T) and the Zr-rich rhombohedral (R) phases at a composition which is nearly independent of temperature. This phenomenon is called morphotropism, and the boundary between the two phases is known as the morphotropic phase boundary (MPB). The excellent piezoelectric and dielectric properties occurring at this composition are believed to.be due to the coexistence of T and R phases, which results in easy poling (i.e. orientation of individual grain polarizations in the direction of an applied electric field). However, there is little direct proof of the coexistence of the two phases at the MPB, possibly because of the difficulty of distinguishing between them. In this investigation a CBD method was found which would successfully differentiate between the phases, and this was applied to confirm the coexistence of the two phases.

Introduction

2018 ◽  
Author(s):  
Peter Hopkins
Keyword(s):  
Final Section ◽  
Short Note ◽  
Current Situation ◽  
Research Projects ◽  
Everyday Lives ◽  
Early Settlement ◽  
The Everyday ◽  
Initial Research

The chapters in this collection explore the everyday lives, experiences, practices and attitudes of Muslims in Scotland. In order to set the context for these chapters, in this introduction I explore the early settlement of Muslims in Scotland and discuss some of the initial research projects that charted the settlement of Asians and Pakistanis in Scotland’s main cities. I then discuss the current situation for Muslims in Scotland through data from the 2011 Scottish Census. Following a short note about the significance of the Scottish context, in the final section, the main themes and issues that have been explored in research about Muslims in Scotland.

THE HEXOSAMINE CONTENT OF THE ORBIT IN RELATION TO ANTI-THYROTROPHIN ANTIBODY TITRES IN SERA OF THYROTROPHIN-TREATED RABBITS WITH AND WITHOUT CORTISONE ADMINISTRATION

1962 ◽  
Vol 41 (3) ◽  
pp. 474-480 ◽  
Author(s):  
Otto Wegelius ◽  
E. J. Jokinen
Keyword(s):  
Connective Tissue ◽  
Guinea Pigs ◽  
Antibody Formation ◽  
Direct Proof ◽  
Significant Rise ◽  
Extraocular Muscles ◽  
Concomitant Treatment ◽  
Antibody Titres ◽  
Hexosamine Content ◽  
Synergetic Action

ABSTRACT In all previous investigations on experimental exophthalmos, heterologous thyrotrophic pituitary extracts have been used. These protein hormones stimulate antihormone formation in the test animals. Cortisone has been reported to effectively block antibody formation. In addition, it has been shown to potentiate TSH-induced exophthalmos in guinea-pigs. With rabbits as test animals, the hexosamine content of the orbital tissues was determined and used as an index of exophthalmos development and at the same time the antibody titres in the sera were followed. TSH injections for six weeks led to a highly significant accumulation of hexosamine in the retrobulbar connective tissue and in the extraocular muscles, i. e. an increase of up to 400% as compared with the control animals. At the same time a significant rise in antihormonal titres was detectable in the sera. Concomitant treatment with cortisone brought about an equal or higher accumulation of hexosamine but significantly lower antibody titres. The known opposite peripheral actions of TSH and cortisone can be reconciled with the synergy in producing experimental exophthalmos by attributing the synergetic action of cortisone to the blocking of antihormone formation. If less antihormones are produced, the effect of TSH is enhanced. Our experiments do not provide direct proof for this hypothesis. High hexosamine values in the orbit and low antihormone titres in the serum are, however, concomitant phenomena.

Sign in / Sign up

Export Citation Format

Share Document