Epsilon substitution for $$\textit{ID}_1$$ ID 1 via cut-elimination

2017 ◽  
Vol 57 (5-6) ◽  
pp. 497-531
Author(s):  
Henry Towsner
Keyword(s):  
Cut Elimination ◽  
Epsilon Substitution

scholarly journals On the No-Counterexample Interpretation

1997 ◽  
Vol 4 (42) ◽  
Author(s):  
Ulrich Kohlenbach
Keyword(s):  
Normal Forms ◽  
Formal System ◽  
Modus Ponens ◽  
Order Type ◽  
Cut Elimination ◽  
Gamma Delta ◽  
Functional Interpretation ◽  
First Order ◽  
Epsilon Substitution ◽  
Definition Of

In [15],[16] Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano<br />arithmetic. In particular he proved, using a complicated epsilon-substitution method (due to<br />W. Ackermann), that for every theorem A (A prenex) of first-order Peano arithmetic (PA) one can find ordinal recursive functionals Phi_A of order type < epsilon_0 which realize the<br />Herbrand normal form A^H of A.<br /> Subsequently more perspicuous proofs of this fact via functional interpretation (combined<br />with normalization) and cut-elimination were found. These proofs however do not carry out the n.c.i. as a local proof interpretation and don't respect the modus<br />ponens on the level of the n.c.i. of formulas A and A -> B. Closely related to this phenomenon is the fact that both proofs do not establish the condition (delta) and - at<br />least not constructively - (gamma) which are part of the definition of an `interpretation of a<br />formal system' as formulated in [15].<br />In this paper we determine the complexity of the n.c.i. of the modus ponens rule for<br />(i) PA-provable sentences,<br />(ii) for arbitrary sentences A;B in L(PA) uniformly in functionals satisfying the n.c.i. of (prenex normal forms of) A and A -> B; and<br />(iii) for arbitrary A;B in L(PA) pointwise in given alpha(< epsilon_0)-recursive functionals satisfying the n.c.i. of A and A -> B. <br /> This yields in particular perspicuous proofs of new uniform versions of the conditions ( gamma), (delta). <br /> Finally we discuss a variant of the concept of an interpretation presented in [17] and<br />show that it is incomparable with the concept studied in [15],[16]. In particular we show<br />that the n.c.i. of PA_n by alpha(<omega_n(omega))-recursive functionals (n >= 1) is an interpretation in the sense of [17] but not in the sense of [15] since it violates the condition (delta).

Risperidone-treated Children and Adolescents with Behavioral Disorders: Do Drug Dose and Patients’ Gender and Age Relate to Drug and Metabolite Plasma Levels?

2017 ◽  
Vol 41 (S1) ◽  
pp. S104-S104
Author(s):  
D. Piacentino ◽  
M. Grözinger ◽  
A. Saria ◽  
F. Scolati ◽  
D. Arcangeli ◽  
...  
Keyword(s):  
Regression Analysis ◽  
Children And Adolescents ◽  
Behavioral Disorders ◽  
Plasma Levels ◽  
Linear Models ◽  
Parent Drug ◽  
Drug Dose ◽  
Cut Elimination ◽  
Younger Patients ◽  
Gender And Age

IntroductionBehavioral disorders, such as conduct disorder, influence choice of treatment and its outcome. Less is known about other variables that may have an influence.Objectives/AimsWe aimed to measure the parent drug and metabolite plasma levels in risperidone-treated children and adolescents with behavioral disorders and investigate the role of drug dose and patients’ gender and age.MethodsWe recruited 115 children/adolescents with DSM-5 behavioral disorders (females = 24; age range: 5–18 years) at the Departments of Psychiatry of the Hospitals of Bolzano, Italy, and Innsbruck, Austria. We measured risperidone and its metabolite 9-hydroxyrisperidone plasma levels and the parent drug-to-metabolite ratio in the plasma of all patients by using LC-MS/MS. A subsample of 15 patients had their risperidone doses measured daily. We compared risperidone and 9-hydroxyrisperidone plasma levels, as well as risperidone/9-hydroxyrisperidone ratio, in males vs. females and in younger (≤ 14 years) vs. older (15–18 years) patients by using Mann-Whitney U test. We fitted linear models for the variables “age” and “daily risperidone dose” by using log-transformation, regression analysis and applying the R2 statistic.ResultsFemales had significantly higher median 9-hydroxyrisperidone plasma levels (P = 0.000). Younger patients had a slightly lower median risperidone/9-hydroxyrisperidone ratio (P = 0.052). At the regression analysis, daily risperidone doses and metabolite, rather than parent drug–plasma levels were correlated (R2 = 0.35).ConclusionsGender is significantly associated with plasma levels, with females being slower metabolizers than males. Concerning age, younger patients seem to be rapid metabolizers, possibly due to a higher activity of CYP2D6. R2 suggests a clear-cut elimination of the metabolite.Disclosure of interestThe authors have not supplied their declaration of competing interest.

A proof of the cut-elimination theorem in simple type theory

1973 ◽  
Vol 38 (2) ◽  
pp. 215-226
Author(s):  
Satoko Titani
Keyword(s):  
Boolean Algebra ◽  
Type Theory ◽  
Arbitrary Number ◽  
Formal System ◽  
Cut Elimination ◽  
Simple Type ◽  
Inductive Definition ◽  
Simple Type Theory ◽  
Maximal Ideals ◽  
Definition Of

In [4], I introduced a quasi-Boolean algebra, and showed that in a formal system of simple type theory, from which the cut rule is omitted, wffs form a quasi-Boolean algebra, and that the cut-elimination theorem can be formulated in algebraic language. In this paper we use the result of [4] to prove the cut-elimination theorem in simple type theory. The theorem was proved by M. Takahashi [2] in 1967 by using the concept of Schütte's semivaluation. We use maximal ideals of a quasi-Boolean algebra instead of semivaluations.The logical system we are concerned with is a modification of Schütte's formal system of simple type theory in [1] into Gentzen style.Inductive definition of types.0 and 1 are types.If τ1, …, τn are types, then (τ1, …, τn) is a type.Basic symbols.a1τ, a2τ, … for free variables of type τ.x1τ, x2τ, … for bound variables of type τ.An arbitrary number of constants of certain types.An arbitrary number of function symbols with certain argument places.

Cut-Elimination for SBL

2020 ◽  
pp. 265-298
Author(s):  
Toshiyasu Arai
Keyword(s):  
Cut Elimination

scholarly journals One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity

2020 ◽  
Author(s):  
Paweł Płaczek
Keyword(s):  
Analogous Result ◽  
Cut Elimination ◽  
Sequent Systems ◽  
Natural Symmetry ◽  
Sequent System

Bilinear Logic of Lambek [10] amounts to Noncommutative MALL of Abrusci [1]. Lambek [10] proves the cut–elimination theorem for a onesided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek [10], we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTIME complexity of the multiplicative fragment of NBL.

Sign in / Sign up

Export Citation Format

Share Document