Ordinal notations and induction

2021 ◽  
pp. 312-345
Author(s):  
Paolo Mancosu ◽  
Sergio Galvan ◽  
Richard Zach
Keyword(s):  
Simple Proof ◽  
Cut Elimination ◽  
Notation System ◽  
Ordinal Notations ◽  
Combinatorial System

In order to prove that the simplification process for arithmetic eventually reaches a simple proof, it is necessary to measure the complexity of proofs in a more sophisticated way than for the cut-elimination theorem. There, a pair of numbers suffices, and the proof proceeds by double induction on this measure. This chapter develops the system of ordinal notations up to ε0 which serve as this more sophisticated measure for proofs in arithmetic. Ordinal notations are presented as purely combinatorial system of symbols, so that from the outset there is no doubt about the constructive legitimacy of the associated principles of reasoning. The main properties of this notation system are presented, and it is shown that ordinal notations are well-ordered according to its associated less-than relation. The basics of the theory of set-theoretic ordinals is developed in the second half of the chapter, so that the reader can compare the infinitary, set-theoretic development of ordinals up to ε0 to the system of finitary ordinal notations. Finally, Paris-Kirby Hydra game and Goodstein sequences are presented as applications of induction up to ε0.

The consistency of arithmetic

2021 ◽  
pp. 268-311
Author(s):  
Paolo Mancosu ◽  
Sergio Galvan ◽  
Richard Zach
Keyword(s):  
Simple Proof ◽  
Sequent Calculus ◽  
Cut Elimination ◽  
Successor Function ◽  
Cut Rule ◽  
Original Proof ◽  
First Order ◽  
Successive Elimination ◽  
Pure Logic ◽  
Classical Arithmetic

This chapter opens the part of the book that deals with ordinal proof theory. Here the systems of interest are not purely logical ones, but rather formalized versions of mathematical theories, and in particular the first-order version of classical arithmetic built on top of the sequent calculus. Classical arithmetic goes beyond pure logic in that it contains a number of specific axioms for, among other symbols, 0 and the successor function. In particular, it contains the rule of induction, which is the essential rule characterizing the natural numbers. Proving a cut-elimination theorem for this system is hopeless, but something analogous to the cut-elimination theorem can be obtained. Indeed, one can show that every proof of a sequent containing only atomic formulas can be transformed into a proof that only applies the cut rule to atomic formulas. Such proofs, which do not make use of the induction rule and which only concern sequents consisting of atomic formulas, are called simple. It is shown that simple proofs cannot be proofs of the empty sequent, i.e., of a contradiction. The process of transforming the original proof into a simple proof is quite involved and requires the successive elimination, among other things, of “complex” cuts and applications of the rules of induction. The chapter describes in some detail how this transformation works, working through a number of illustrative examples. However, the transformation on its own does not guarantee that the process will eventually terminate in a simple proof.

scholarly journals A Simple Proof that Super-Consistency Implies Cut Elimination

2012 ◽  
Vol 53 (4) ◽  
pp. 439-456 ◽  
Author(s):  
Gilles Dowek ◽  
Olivier Hermant
Keyword(s):  
Simple Proof ◽  
Cut Elimination

Multi-focused cut elimination

2017 ◽  
Vol 28 (5) ◽  
pp. 614-650
Author(s):  
TAUS BROCK-NANNESTAD ◽  
NICOLAS GUENOT
Keyword(s):  
Simple Proof ◽  
Linear Logic ◽  
Cut Elimination ◽  
Sequent Calculi ◽  
Elimination Procedure ◽  
The Impact

We investigate cut elimination in multi-focused sequent calculi and the impact on the cut elimination proof of design choices in such calculi. The particular design we advocate is illustrated by a multi-focused calculus for full linear logic using an explicitly polarised syntax and incremental focus handling, for which we provide a syntactic cut elimination procedure. We discuss the effect of cut elimination on the structure of proofs, leading to a conceptually simple proof exploiting the strong structure of multi-focused proofs.

scholarly journals A FIELD GUIDE TO SONIC BOTANY: THOUGHTS ABOUT ECO-COMPOSITION

Tempo ◽  
2020 ◽  
Vol 75 (295) ◽  
pp. 31-44
Author(s):  
Maayan Tsadka
Keyword(s):  
Organic Matter ◽  
Performance Practice ◽  
Musical Instruments ◽  
Musical Composition ◽  
Notation System ◽  
Field Guide ◽  
The Past ◽  
Tuning Forks ◽  
Texture Size ◽  
Ongoing Project

AbstractSonic botany is an ongoing project that I have been developing over the past few years. It incorporates natural artefacts: dry leaves, pods, flowers, branches, rocks, bones and other organic findings. These are used as musical instruments that are played on with a scientific/musical tool: tuning forks in various frequencies. The vibration from the tuning forks resonates through the natural artefacts which amplify the vibration and – via sound – reveal the texture, size, material and condition of the organic matter. This process generates new sonic material, new context and new forms of musical composition. The practice developed into several compositions and projects, a performance practice, a notation system and a way of listening. Here I share some of the insights I gained through this process, the tools and the compositional framework.

scholarly journals A simple proof of Andrews’s 5 F 4 evaluation

2013 ◽  
Vol 36 (1-2) ◽  
pp. 165-170 ◽  
Author(s):  
Ira M. Gessel
Keyword(s):  
Simple Proof

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 simple proof of existence of weak and statistical solutions of Navier–Stokes equations

1992 ◽  
Vol 436 (1896) ◽  
pp. 1-11 ◽  
Keyword(s):  
Weak Solution ◽  
Initial Data ◽  
Natural Number ◽  
Simple Proof ◽  
Stokes Equations ◽  
Galerkin Approximation ◽  
Navier Stokes ◽  
Navier Stokes Equations ◽  
Existence Proofs ◽  
Statistical Solutions

The Galerkin approximation to the Navier–Stokes equations in dimension N , where N is an infinite non-standard natural number, is shown to have standard part that is a weak solution. This construction is uniform with respect to non-standard representation of the initial data, and provides easy existence proofs for statistical solutions.

Sign in / Sign up

Export Citation Format

Share Document