We formulate an abstract version of the finite injury method in the form of the Baire category theorem. The theorem has the following corollaries: The Friedberg-Muchnik pair of recursively enumerable degrees, the Sacks splitting theorem, the existence of a minimal degree below 0′ and the Shoenfield jump theorem.

Working in the language of first-order arithmetic we consider models of the base theory P - . Suppose M is a model of P - and let M satisfy induction for σ 1 -formulas. First it is shown that the Friedberg-Muchnik finite injury argument can be performed inside M, and then, using a blocking method for the requirements, we prove that the Sacks splitting construction can be done in M. So, the "amount" of induction needed to perform (...) the known finite injury priority arguments is Σ 1 -induction. (shrink)

We develop a bounded version of the finite injury priority method in recursion theory. We use this to study the learnability of unions of rectangles over the domain {0, …, n − 1}d with only equivalence queries. Applying this method, we show three main results:1. The class of unions of rectangles is polynomial time learnable for constant dimension d.2. The class of unions of rectangles whose projections at some unknown dimension are pairwise-disjoint is polynomial time learnable.3. (...) The class of unions of two disjoint rectangles is polynomial time learnable with unions of two rectangles as hypotheses. (shrink)

Given a reducibility ⩽r, we say that an infinite set A is r-introimmune if A is not r-reducible to any of its subsets B with |A\B| = ∞. We consider the many-one reducibility ⩽m and we prove the existence of a low1 m-introimmune set in Π01 and the existence of a low1 bi-m-introimmune set.

Contents: Recursive Enumerability and the Jump Operator; On the Degrees Less Than 0'; A Simple Set Which Is Not Effectively Simple; The Recursively Enumerable Degrees Are Dense; Metarecursive Sets (with G Kreisel); Post's Problem, Admissible Ordinals and Regularity; On a Theorem of Lachlan and Marlin; A Minimal Hyperdegree (with R O Gandy); Measure-Theoretic Uniformity in Recursion Theory and Set Theory; Forcing with Perfect Closed Sets; Recursion in Objects of Finite Type; The a-Finite Injury Method (with S (...) G Simpson); Remarks Against Foundational Activity; Countable Admissible Ordinals and Hyperdegrees; The 1-Section of a Type n Object; The k-Section of a Type n Object; Post's Problem, Absoluteness and Recursion in Finite Types; Effective Bounds on Morley Rank; On the Number of Countable Models; Post's Problem in E-Recursion; The Limits of E-Recursive Enumerability; Effective Versus Proper Forcing. (shrink)

This paper is a sequel to our [7]. In that paper we constructed a Π1 0 tree of avoidable points. Here we construct a Π1 0 tree of shadow points. This tree is a tree of sharp filters, where a sharp filter is a nested sequence of basic open sets converging to a point. In the construction we assign to each basic open set on the tree an address in 2<ω. One interesting fact is that while our Π1 0 tree (...) of sharp filters (a subtree of Δ<ω) is isomorphic to the tree of addresses (a subtree of 2<ω), the tree of addresses is recursively enumerable but not recursive. To achieve this end we use a finite injury priority argument. (shrink)

This research partially answers the question raised by Goncharov about the size of the class of positive elements of a Roger's semilattice. We introduce a notion of effective infinity of classes of computable enumerations. Then, using finite injury priority method, we prove five theorems which give sufficient conditions to be effectively infinite for classes of all enumerations without repetitions, positive undecidable enumerations, negative undecidable enumerations and all computable enumerations of a family of r.e. sets. These theorems permit (...) to strengthen the results of Pour-El, Pour-El and Howard, Ershov and Khutoretskii about existence of enumerations without repetitions and positive undecidable enumerations. (shrink)

Based on the heterogeneous multiscale method, this paper presents a finite volume method to solve multiscale convection-diffusion-reaction problem. The paper constructs an algorithm of the optimal order convergence rate in H1-norm under periodic medias.

Despite being one of the most dependable methods used by applied mathematicians and engineers in handling complex systems, the finite element method commits variational crimes. This paper contextualizes the concept of variational crime within a broader account of mathematical practice by explaining the tradeoff between complexity and accuracy involved in the construction of numerical methods. We articulate two standards of accuracy used to determine whether inexact solutions are good enough and show that, despite violating the justificatory principles of (...) one, the finite element method nevertheless succeeds in obtaining its legitimacy from the other. (shrink)

The mathematical model of physical problems interprets physical phenomena closely. This research work is focused on numerical solution of a nonlinear mathematical model of fractional Maxwell nanofluid with the finite difference element method. Addition of nanoparticles in base fluids such as water, sodium alginate, kerosene oil, and engine oil is observed, and velocity profile and heat transfer energy profile of solutions are investigated. The finite difference method involving the discretization of time and distance parameters is applied (...) for numerical results by using the Caputo time fractional operator. These results are plotted against different physical parameters under the effects of magnetic field. These results depicts that a slight decrease occurs for velocity for a high value of Reynolds number, while a small value of Re provides more dominant effects on velocity and temperature profile. It is observed that fractional parameters α and β show inverse behavior against u y, t and θ y, t. An increase in volumetric fraction of nanoparticles in base fluids decreases the temperature profile of fractional Maxwell nanofluids. Using mathematical software of MAPLE, codes are developed and executed to obtain these results. (shrink)

In this paper, we present an intensive investigation of the finite volume method compared to the finite difference methods. In order to show the main difference in the way of approaching the solution, we take the Burgers equation and the Buckley–Leverett equation as examples to simulate the previously mentioned methods. On the one hand, we simulate the results of the finite difference methods using the schemes of Lax–Friedrichs and Lax–Wendroff. On the other hand, we apply Godunov’s (...) scheme to simulate the results of the finite volume method. Moreover, we show how starting with a variational formulation of the problem, the finite element technique provides piecewise formulations of functions defined by a collection of grid data points, while the finite difference technique begins with a differential formulation of the problem and continues to discretize the derivatives. Finally, some graphical and numerical comparisons are provided to illustrate and corroborate the differences between these two main methods. (shrink)

Annually, more than ten million people in all age groups in the world experience an acquired brain injury, which is a brain injury caused after birth by external forces or certain internal factors. Brain injury survivors are often left with long-term impairments in cognitive, social, or emotional functioning. Despite a promising outset, research on the effectiveness of philosophical dialogues as an educational method for persons with ABI to increase their cognitive, social, and emotional functioning has, to (...) our knowledge, been virtually non-existent. The present research project targets this and uses a pretest-posttest and mixed-method triangulation design and attempts to measure effects of two small-scale interventions carried out in the northern part of Sweden. In this text, the project’s research design, data production, and data processing are described. (shrink)

This work investigates the finite-time control problem for a nonlinear four-tank cross-coupled liquid level system by the port-controlled Hamiltonian model. A fixed-free methodology is exhibited which can be used to simplify the controller design procedure. To get an adjustable convergent gain of the finite-time control, a feasible technique named damping normalization is proposed. A novel parameter autotuning algorithm is given to clarify the principle of choosing parameters of the PCH method. Furthermore, a finite-time controller is designed (...) by a state-error desired Hamiltonian function, and the relationship between the settling time and a parameter is given, which can be applied in practical engineering easily to adjust the settling time according to the industrial need. Finally, simulation and experimental results verify the effectiveness of the proposed algorithm. (shrink)

In the present contribution we look at the legacy of Hilbert's programme in some recent developments in mathematics. Hilbert's ideas have seen new life in generalised and relativised forms by the hands of proof theorists and have been a source of motivation for the so--called reverse mathematics programme initiated by H. Friedman and S. Simpson. More recently Hilbert's programme has inspired T. Coquand and H. Lombardi to undertake a new approach to constructive algebra in which strong emphasis is laid on (...) the use of finite methods. The main aim is to eliminate the ideal objects and in so doing obtain more elementary and informative proofs. We survey some work in commutative algebra---mainly about and around the Zariski spectrum and the Krull dimension of a commutative ring---which witnesses the feasibility of such a revised Hilbert's programme. (shrink)

We discuss the possibility of applying the compactness theorem to the study of finite structures. Given a class of finite structures, it is important to determine whether it can be expressed by a particular category of sentences. We are interested in this type of problem, and use nonstandard method for showing the non‐expressibility of certain classes of finite graphs by an existential monadic second order sentence.

Measuring neuronal activity with electrophysiological methods may be useful in detecting neurological dysfunctions, such as mild traumatic brain injury (mTBI). This approach may be particularly valuable for rapid detection in at-risk populations including military service members and athletes. Electrophysiological methods, such as quantitative electroencephalography (qEEG) and recording event-related potentials (ERPs) may be promising; however, the field is nascent and significant controversy exists on the efficacy and accuracy of the approaches as diagnostic tools. For example, the specific measures derived from (...) an electroencephalogram (EEG) that are most suitable as markers of dysfunction have not been clearly established. A study was conducted to summarize and evaluate the statistical rigor of evidence on the overall utility of qEEG as an mTBI detection tool. The analysis evaluated qEEG measures/parameters that may be most suitable as fieldable diagnostic tools, identified other types of EEG measures and analysis methods of promise, recommended specific measures and analysis methods for further development as mTBI detection tools, identified research gaps in the field, and recommended future research and development thrust areas. The qEEG study group formed the following conclusions: 1. Individual qEEG measures provide limited diagnostic utility for mTBI. However, many measures can be important features of qEEG discriminant functions, which do show significant promise as mTBI detection tools. 2. ERPs offer utility in mTBI detection. In fact, evidence indicates that ERPs can identify abnormalities in cases where EEGs alone are nondisclosing. 3. The standard mathematical procedures used in the characterization of mTBI EEGs should be expanded to incorporate newer methods of analysis including nonlinear dynamical analysis, complexity measures, analysis of causal interactions, graph theory and information dynamics. 4. and 5. are too long to include here. (shrink)

his paper presents a unified treatment of the propositional and first-order many-valued logics through the method of tableaux. It is shown that several important results on the proof theory and model theory of those logics can be obtained in a general way. We obtain, in this direction, abstract versions of the completeness theorem, model existence theorem (using a generalization of the classical analytic consistency properties), compactness theorem and Lowenheim-Skolem theorem. The paper is completely self-contained and includes examples of application (...) to particular many-valued formal systems. (shrink)

A method of constructing Hilbert-type axiom systems for standard many-valued propositional logics was offered by Rosser and Turquette. Although this method is considered to be a solution of the problem of axiomatisability of a wide class of many-valued logics, the article demonstrates that it fails to produce adequate axiom systems. The article concerns finitely many-valued propositional logics of Łukasiewicz. It proves that if standard propositional connectives of the Rosser–Turquette axiom systems are definable in terms of the propositional connectives (...) of Łukasiewicz’s logics, and thus, they are normal ones, then every Rosser–Turquette axiom system for a finite-valued Łukasiewicz’s logic is semantically incomplete. (shrink)

Familiar proof theoretical and especially automated deduction methods sometimes accept infinity where, in fact, it can be omitted. Our first example deals with the infinite supply of individual variables admitted in 1-order deductions, the second one deals with infinite-branching rules in sequent calculi with number-theoretical induction. The contents of Section 1 summarize and extend basic ideas and results published elsewhere, whereas basic ideas and results of Section 2 are exposed for the first time in the present paper. We consider classical (...) formalisms only, to which constructive formalisms can be reduced by Shanin-style interpretations. (shrink)

Finite-state methods are applied to determine the consequences of events, represented as strings of sets of fluents. Developed to flesh out events used in natural language semantics, the approach supports reasoning about action in AI, including the frame problem and inertia. Representational and inferential aspects of the approach are explored, centering on conciseness of language, context update and constraint application with bias.

We use the apparatus of the canonical formulas introduced by Zakharyaschev [10] to prove that all finitely axiomatizable normal modal logics containing K4.3 are decidable, though possibly not characterized by classes of finite frames. Our method is purely frame-theoretic. Roughly, given a normal logic L above K4.3, we enumerate effectively a class of frames with respect to which L is complete, show how to check effectively whether a frame in the class validates a given formula, and then apply (...) a Harropstyle argument to establish the decidability of L, provided of course that it has finitely many axioms. (shrink)

In [4], I proved that the product-free fragment L of Lambek's syntactic calculus (cf. Lambek [2]) is not finitely axiomatizable if the only rule of inference admitted is Lambek's cut-rule. The proof (which is rather complicated and roundabout) was subsequently adapted by Kandulski [1] to the non-associative variant NL of L (cf. Lambek [3]). It turns out, however, that there exists an extremely simple method of non-finite-axiomatizability proofs which works uniformly for different subsystems of L (in particular, for (...) NL). We present it below to the use of those who refer to the results of [1] and [4]. (shrink)

In order to modelize the reasoning of intelligent agents represented by a poset T, H. Rasiowa introduced logic systems called “Approximation Logics”. In these systems a set of constants constitutes a fundamental tool. In this paper, we consider logic systems called L'T without this kind of constants but limited to the case where T is a finite poset. We study the tableau method for this system and we prove its completeness for a class of formulas with respect to (...) an algebraic semantics. (shrink)

Finite-state methods are applied to the Russell-Wiener notion of time (based on events) and developed into an account of interval relations and temporal propositions. Strings are formed and collected in regular languages and regular relations that are argued to embody temporal relations in their various underspecified guises. The regular relations include retractions that reduce computations by projecting strings down to an appropriate level of granularity, and non-deterministic relations defining notions of partiality within and across such levels.

The article explores the following question: which among the most often examined in the literature method of constructing Hilbert-type axiom systems for finite-valued propositional logics of Łukasi...

Finite-state methods are applied to the Russell-Wiener-Kamp notion of time (based on events) and developed into an account of interval relations and semi-intervals. Strings are formed and collected in regular languages and regular relations that are argued to embody temporal relations in their various underspecified guises. The regular relations include retractions that reduce computations by projecting strings down to an appropriate level of granularity, and notions of containment for partiality within and across such levels.

Background: Benzodiazepines have been widely used in clinical practice for over four decades and continue to be one of the most consumed and highly prescribed class of drugs available in the treatment of anxiety, depression, and insomnia. The literature indicates that Benzodiazepine users at a significantly increased risk of Motor Vehicle accidents compared to non-users but the impact on injuries at workplace is not well-defined. We aimed to investigate whether use of benzodiazepine is associated with increased risk of occupational injuries.Methods: (...) PubMed, Embase, and Scopus databases were searched. A meta-analysis was performed to calculate odds ratio and 95% confidence interval among case controls, cross-sectional studies, either questionnaire or laboratory exams based.Results: A total of 13 studies met inclusion criteria, involving 324,168 OI from seven different countries, with an estimated occurrence of benzodiazepine positivity of 2.71%. A total of 14 estimates were retrieved. Of them, 10 were based on laboratory analyses, three on institutional databases, while one study was based on questionnaires. Regarding the occupational groups, three estimates focused on commercial drivers, that exhibited a reduced risk ratio for benzodiazepine positivity compared to other occupational groups. Eventually, no increased risk for benzodiazepine positivity was identified, either from case control studies, or cross sectional studies, when only laboratory based estimates were taken in account.Conclusions: Even though benzodiazepines have the potential to increase injury rates among casual and chronic users, available evidence are insufficient to sustain this hypothesis, particularly when focusing on laboratory-based studies. (shrink)

We show that the existence of a recursively enumerable set whose Turing degree is neither low nor complete cannot be proven from the basic axioms of first order arithmetic (P -) together with Σ 2 -collection (BΣ 2 ). In contrast, a high (hence, not low) incomplete recursively enumerable set can be assembled by a standard application of the infinite injury priority method. Similarly, for each n, the existence of an incomplete recursively enumerable set that is neither low (...) n nor high n - 1 , while true, cannot be established in P - + BΣ n + 1 . Consequently, no bounded fragment of first order arithmetic establishes the facts that the high n and low n jump hierarchies are proper on the recursively enumerable degrees. (shrink)

The importance of including performance-related body mechanics into music education to improve performance quality and prevent performance-related injuries has been stressed by many researchers recently. However, it is unclear how this information could be delivered most effectively. The somatic method ‘Timani’ provides a practical solution by combining expertise in music performance and functional body mechanics with the goal of achieving a more efficient playing technique. Since no in-depth study has been conducted to assess the method before, we explored (...) the impact of this method on young musicians’ performance through an online, 4-week-long Timani intervention with a mixed-methodology design. 17 students were recruited from the Norwegian Academy of Music. They participated in two group workshops at the beginning and the end of the project and received four individual Timani sessions administered by certified teachers. We collected survey data at the workshops about performance-related pain and self-efficacy, and qualitative feedback after each session. In addition, all sessions were observed by the researcher and semi-structured interviews were conducted with the teachers about the perceived outcomes and their experiences with teaching the method online. Our findings show that the intervention had a positive impact on a physical, professional, and to some extent, psychological and behavioral level. The improvements included better posture when playing, enhanced control and dexterity in the upper extremities, and improved breathing mechanisms. The seven students who had performance-related pain pre-intervention reported a reduction in the discomfort. The positive results were achieved by the dual expertise of the teachers in music performance and functional body mechanics, the structure of the sessions, the communication, and the pedagogical tools used. Both students and teachers felt that administering the sessions online was satisfactory and produced good results. Timani is a promising method to establish healthy playing and singing habits thus improving performance quality and preventing performance-related problems and has great potential in reducing pre-existing injuries and pain. Also, it can be effectively taught online which has further implications for the logistics of delivery. (shrink)

In this article, I undertake three main tasks. First, I argue that, contrary to the standard view, moral injury is not a species of PTSD (post-traumatic stress disorder) but rather, on the most coherent conception of moral injury, PTSD is (in effect) a species of moral injury. In doing so, I make use of the notion of caring deeply about something or someone worthy of being cared deeply about. Second, I consider so-called “dirty hands” actions in police (...) work and in war, and distinguish these from the morally legitimate, but harmful, actions of police officers and of war fighters, such as the morally legitimate use of coercive force and lethal force (respectively). While the morally legitimate use of harmful methods is constitutive of these occupational roles, “dirty hands” methods are not. Roughly speaking, a “dirty hands” action is one that is morally wrong and (typically) unlawful but done for the sake of a good outcome. Both categories of action are conducive to moral injury, but “dirty hands” actions much more so, especially given the slippery moral slope from “dirty hands” actions to egregious moral wrongdoing. Third, I offer some recommendations for reducing moral injury among police officers and war fighters. (shrink)