Fernando Ferreira

Every model of IΔ0 is the tally part of a model of the stringlanguage theory Th‐FO (a main feature of which consists in having induction on notation restricted to certain AC0. sets). We show how to “smoothly” introduce in Th‐FO the binary length function, whereby it is possible to make exponential assumptions in models of Th‐FO. These considerations entail that every model of IΔ0 + ¬exp is a proper initial segment of a model of Th‐FO and that a modicum of bounded collection is true in these models. Mathematics Subject Classification: 03F30, 03C62, 68Q15.

© 2016 Elsevier B.V.The effect of energetic ion bombardment on the properties of tantalum thin films was investigated. To achieve such energetic ion bombardment during the process the Ta thin films were deposited by deep oscillation magnetron sputtering, an ionized physical vapor deposition technique related to high power impulse magnetron sputtering. The peak power was between 49 and 130 kW and the substrate was silicon at room temperature and ground potential. The directionality and the energy of the depositing species was controlled by changing the ionization fraction of the Ta species arriving at the substrate at different peak powers. In this work, the surface morphology, microstructure, structure and hardness and Young's modulus of the films were characterized. The ion energy distributions were measured using an electrostatic quadrupole ion energy and mass spectrometer. The IEDs showed that the DOMS process applies a very energetic ion bombardment on the growing tantalum films. Therefore, with such conditions it was possible to deposit pure α-Ta without the use of additional equipment, i.e., without substrate bias or substrate heating. Conditions are therefore significantly different than in previous works, offering a much simpler and cheaper solution to up-scale for industrial operation.

This commentary is a response to Patrícia Jerónimo’s article ‘Legal translation and the challenges of overcoming language barriers in court practice: Evidence from Portuguese courts’. It offers not only a detailed analysis of how to implement Directive 2010/64/EU in Portugal, but also provides a comprehensive overview of the socioprofessional background and institutional framework behind such implementation. Additionally, it presents concrete suggestions for improving the provision of legal interpretation and translation, focusing on quality standards, visibility, and professional recognition.

The unprecedented migration of populations to urban areas has created major challenges for municipalities and service providers. To address these issues, decision-makers must embrace smart city and Society 5.0 paradigms, both of which focus on adaptability and sustainable development. Artificial intelligence (AI) plays a pivotal role by expanding service capacity, enabling automation, and processing vast data to align urban development with the UN’s Sustainable Development Goals (SDGs). This paper develops a multi-criteria analysis system designed to support decision-making in complex socio-technological contexts. Using cognitive mapping and the Decision-Making Trial and Evaluation Laboratory (DEMATEL) technique within a neutrosophic environment, the study analyzes cause-and-effect relationships among critical factors that influence businesses’ adaptation to AI, smart cities, and Society 5.0. The results offer a holistic decision-support framework to guide policymakers, businesses, and urban planners toward inclusive, sustainable, and technologically integrated societies.

We consider some very robust semi-constructive theories related to Kripke–Platek set theory, with and without the powerset operation. These theories include the law of excluded middle for bounded formulas, a form of Markov’s principle, the unrestricted collection scheme and, also, the classical contrapositive of the bounded collection scheme. We analyse these theories using forms of a functional interpretation which work in tandem with the constructible hierarchy (or the cumulative hierarchy, if the powerset operation is present). The main feature of these functional interpretations is to treat bounded quantifications as “computationally empty.” Our analysis is extended to a second-order setting enjoying some forms of class comprehension, including strict- $$\Pi ^1_1$$ reflection. The key idea of the extended analysis is to treat second-order (class) quantifiers as bounded quantifiers and strict- $$\Pi ^1_1$$ reflection as a form of collection. We will be able to extract some effective bounds from proofs in these systems in terms of the constructive tree ordinals up to the Bachmann–Howard ordinal.

"Each nation can do well, as in the life of individuals, only if things go equally well in all of her neighboring nations; the life of sciences is similar to that of states whose interest demands that everything be in order within individual states as properly as their relations be in good order among themselves. Understanding this correctly, the most important carriers of mathematical thoughts have always shown great interest in the law and order in neighboring sciences and, above all for the benefit of mathematics, have cultivated the relations to the neighboring sciences, in particular to physics and epistemology. The essence of these relations and the ground of their fertility will be made most distinct, I believe, if I sketch to you that general method of inquiry which appears to grow more and more significant in modern mathematics; the axiomatic method, I mean." (David Hilbert, 1917)

In finite type arithmetic, the real numbers are represented by rapidly converging Cauchy sequences of rational numbers. Ulrich Kohlenbach introduced abstract types for certain structures such as metric spaces, normed spaces, Hilbert spaces, etc. With these types, the elements of the spaces are given directly, not through the mediation of a representation. However, these abstract spaces presuppose the real numbers. In this paper, we show how to set up an abstract type for the real numbers. The appropriateness of our construction works in tandem with the bounded functional interpretation.

It is well-known that an element of a commutative ring with identity is nilpotent if, and only if, it lies in every prime ideal of the ring. A modification of this fact is amenable to a very simple proof mining analysis. We formulate a quantitative version of this modification and obtain an explicit bound. We present an application. This proof mining analysis is theleitmotiffor some comments and observations on the methodology of computational extraction. In particular, we emphasize that the formulation of quantitative versions of ordinary mathematical theorems is ofindependent interestfrom proof mining metatheorems.

We introduce a herbrandized functional interpretation of a first-order semi-intuitionistic extension of Heyting Arithmetic and study its main properties. We then extend the interpretation to a certain system of second-order arithmetic which includes a (classically false) formulation of the FAN principle and weak König's lemma. It is shown that any first-order formula provable in this system is classically true. It is perhaps worthy of note that, in our interpretation, second-order variables are interpreted by finite sets of natural numbers.

In Frege’s logicism, numbers are logical objects in the sense that they are extensions of certain concepts. Frege’s logical system is inconsistent, but Richard Heck showed that its restriction to predicative quantification is consistent. This predicative fragment is, nevertheless, too weak to develop arithmetic. In this paper, I will consider an extension of Heck’s system with impredicative quantifiers. In this extended system, both predicative and impredicative quantifiers co-exist but it is only permissible to take extensions of concepts formulated in the predicative fragment of the language. This system is consistent. Moreover, it proves the principle of reducibility applied to concepts true of only finitely many objects. With the aid of this form of reducibility, it is possible to develop arithmetic in a thoroughly Fregean way.

We introduce a new typed combinatory calculus with a type constructor that, to each type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}, associates the star type σ∗\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma ^*$$\end{document} of the nonempty finite subsets of elements of type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}. We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this star combinatory calculus, we define a functional interpretation of first-order predicate logic and prove a corresponding soundness theorem. It is seen that each theorem of classical first-order logic is connected with certain formulas which are tautological in character. As a corollary, we reprove Herbrand’s theorem on the extraction of terms from classically provable existential statements.

In this article we study applications of the bounded functional interpretation to theories of feasible arithmetic and analysis. The main results show that the novel interpretation is sound for considerable generalizations of weak König’s Lemma, even in the presence of very weak induction. Moreover, when this is combined with Cook and Urquhart’s variant of the functional interpretation, one obtains effective versions of conservation results regarding weak König’s Lemma which have been so far only obtained non-constructively

Commuting conversions were introduced in the natural deduction calculus as ad hoc devices for the purpose of guaranteeing the subformula property in normal proofs. In a well known book, Jean-Yves Girard commented harshly on these conversions, saying that ‘one tends to think that natural deduction should be modified to correct such atrocities.’ We present an embedding of the intuitionistic predicate calculus into a second-order predicative system for which there is no need for commuting conversions. Furthermore, we show that the redex and the conversum of a commuting conversion of the original calculus translate into equivalent derivations by means of a series of bidirectional applications of standard conversions.