We prove uniformly computable versions of the Implicit Function Theorem in its differentiable and non-differentiable forms. We show that the resulting operators are not computable if information about some of the partial derivatives of the implicitly defining function is omitted. Finally, as a corollary, we obtain a uniformly computable Inverse Function Theorem, first proven by M. Ziegler.

We extend the notion of absolute convergence for real series in several variables to a notion of convergence for series in a power series field ℝ((t Γ)) with coefficients in ℝ. Subsequently, we define a natural notion of analytic function at a point of ℝ((t Γ))m. Then, given a real function f analytic on a open box I of ℝ m , we extend f to a function f ★ which is analytic on a subset of ℝ((t (...) Γ)) m containing I. We prove that the functions f ★ share with real analytic functions certain basic properties: they are , they have usual Taylor development, they satisfy the inverse function theorem and the implicit function theorem. (shrink)

The Stone-Weierstrass Theorem for compact Hausdorff spaces is a basic result of functional analysis with far-reaching consequences. We introduce an equational logic ⊨Δ associated with an infinitary variety Δ and show that the Stone-Weierstrass Theorem is a consequence of the Beth definability property of ⊨Δ, stating that every implicit definition can be made explicit. Further, we define an infinitary propositional logic ⊢Δ by means of a Hilbert-style calculus and prove a strong completeness result whereby the semantic notion (...) of consequence associated with ⊢Δ coincides with ⊨Δ. (shrink)

In this article, we make analysis of the implicit fractional differential equations involving integral boundary conditions associated with Stieltjes integral and its corresponding coupled system. We use some sufficient conditions to achieve the existence and uniqueness results for the given problems by applying the Banach contraction principle, Schaefer’s fixed point theorem, and Leray–Schauder result of the cone type. Moreover, we present different kinds of stability such as Hyers–Ulam stability, generalized Hyers–Ulam stability, Hyers–Ulam–Rassias stability, and generalized Hyers–Ulam–Rassias stability by (...) using the classical technique of functional analysis. At the end, the results are verified with the help of examples. (shrink)

According to Relational Quantum Mechanics the wave function \ is considered neither a concrete physical item evolving in spacetime, nor an object representing the absolute state of a certain quantum system. In this interpretative framework, \ is defined as a computational device encoding observers’ information; hence, RQM offers a somewhat epistemic view of the wave function. This perspective seems to be at odds with the PBR theorem, a formal result excluding that wave functions represent knowledge of an (...) underlying reality described by some ontic state. In this paper we argue that RQM is not affected by the conclusions of PBR’s argument; consequently, the alleged inconsistency can be dissolved. To do that, we will thoroughly discuss the very foundations of the PBR theorem, i.e. Harrigan and Spekkens’ categorization of ontological models, showing that their implicit assumptions about the nature of the ontic state are incompatible with the main tenets of RQM. Then, we will ask whether it is possible to derive a relational PBR-type result, answering in the negative. This conclusion shows some limitations of this theorem not yet discussed in the literature. (shrink)

Just as intuitionistic proofs can be modeled by functions, linear logic proofs, being symmetric in the inputs and outputs, can be modeled by relations . However generic relations do not establish any functional dependence between the arguments, and therefore it is questionable whether they can be thought as reasonable generalizations of functions. On the other hand, in some situations one can speak in some precise sense about an implicit functional dependence defined by a relation. It turns out that it (...) is possible to model linear logic with implicit functions rather than general relations, an adequate language for such a semantics being differential calculus. This results in a non-degenerate model enjoying quite strong completeness properties. (shrink)

As a class of familiar nonlinear systems, nonaffine systems are frequently encountered in practical applications. Currently, in the context of learning control, there is a lack of research results about such general class of nonlinear systems, especially for the case of performing infinite interval tasks. This article focuses on the incremental adaptive control for nonlinear systems in nonaffine form, without requiring periodicity or repeatability. Instead of using the integral adaptation, incremental adaptive mechanisms are developed and the corresponding control schemes are (...) presented, by which the numerical integration for implementation can be avoided. With the proposed incremental adaptation, the implicit function theorem is introduced to solve the intractability problem of the nonaffine structure. The robustness of the tracking error is characterized, with the aid of a proposed key lemma, while the boundedness of all the variables is examined. Numerical results are presented to verify the effectiveness of the proposed control design. (shrink)

Traces the development of recursive functions from their origins in the late nineteenth century to the mid-1930s, with particular emphasis on the work and influence of Kurt Gödel.

Adaptation to novel visuomotor transformations for example when navigating a cursor on a computer monitor by using a computer mouse, can be explicit or implicit. Explicit adjustments are made when people are informed about the occurrence and the type of a novel visuomotor transformation and intentionally modify their movements. Implicit adjustments, in contrast, are made without reportable knowledge of a novel visuomotor transformation and without a change intention. The relation of implicit adjustments to explicit adjustments needs further (...) clarification. Here we show that these two types of adjustment occur at the same time and remain functionally independent. The size of total adjustment turned out to be the sum of explicit and implicit adjustments measured in isolation, even when both processes produce opposite outcomes. In perspective our results demonstrate that automatic, implicit processes of motor control are not superseded by intentional, explicit ones, but only superposed. (shrink)

The propositional account of explicit and implicit knowledge interprets cognitive differences between direct and indirect test performance as emerging from the elements in different hierarchical levels of the propositional representation that have been made explicit. The hierarchical nature of explicitness is challenged, however, on the basis of neuropsychological dissociations between direct and indirect tests of memory, as well as the stochastic independence that has been observed between these two types of tests. Furthermore, format specificity on indirect test of memory (...) challenges the basic notion of a propositional theory of implicit and explicit knowledge. (shrink)

This paper addresses the strength of Ramsey's theorem for pairs ($RT^2_2$) over a weak base theory from the perspective of 'proof mining'. Let $RT^{2-}_2$ denote Ramsey's theorem for pairs where the coloring is given by an explicit term involving only numeric variables. We add this principle to a weak base theory that includes weak König's Lemma and a substantial amount of $\Sigma^0_1$-induction (enough to prove the totality of all primitive recursive functions but not of all primitive recursive functionals). (...) In the resulting theory we show the extractability of primitive recursive programs and uniform bounds from proofs of $\forall\exists$-theorems. There are two components of this work. The first component is a general proof-theoretic result, due to the second author, that establishes conservation results for restricted principles of choice and comprehension over primitive recursive arithmetic PRA as well as a method for the extraction of primitive recursive bounds from proofs based on such principles. The second component is the main novelty of the paper: it is shown that a proof of Ramsey's theorem due to Erdős and Rado can be formalized using these restricted principles. So from the perspective of proof unwinding the computational content of concrete proofs based on $RT^2_2$ the computational complexity will, in most practical cases, not go beyond primitive recursive complexity. This even is the case when the theorem to be proved has function parameters f and the proof uses instances of $RT^2_2$ that are primitive recursive in f. (shrink)

We develop a version of Herbrand's theorem for continuous logic and use it to prove that definable functions in infinite-dimensional Hilbert spaces are piecewise approximable by affine functions. We obtain similar results for definable functions in Hilbert spaces expanded by a group of generic unitary operators and Hilbert spaces expanded by a generic subspace. We also show how Herbrand's theorem can be used to characterize definable functions in absolutely ubiquitous structures from classical logic.

Central limit theorem for the functional of jump Markov process. Nguyễn Văn Hữu, Vương Quân Hoàng và Trần Minh Ngọc. Báo cáo: Hội nghị toàn quốc lần thứ III “Xác suất - Thống kê: Nghiên cứu, ứng dụng và giảng dạy” (tr. 34). Ba Vì, Hà Tây, ngày 12-14 tháng 05 năm 2005. Viện Toán học / Trường Đại học Khoa học tự nhiên / Đại học Quốc gia Hà Nội.

Computer assisted theorem proving is an increasingly important part of mathematical methodology, as well as a long-standing topic in artificial intelligence (AI) research. However, the current generation of theorem proving software have limited functioning in terms of providing new proofs. Importantly, they are not able to discriminate interesting theorems and proofs from trivial ones. In order for computers to develop further in theorem proving, there would need to be a radical change in how the software functions. Recently, (...) machine learning results in solving mathematical tasks have shown early promise that deep artificial neural networks could learn symbolic mathematical processing. In this paper, I analyze the theoretical prospects of such neural networks in proving mathematical theorems. In particular, I focus on the question how such AI systems could be incorporated in practice to theorem proving and what consequences that could have. In the most optimistic scenario, this includes the possibility of autonomous automated theorem provers (AATP). Here I discuss whether such AI systems could, or should, become accepted as active agents in mathematical communities. (shrink)

Gleason-type theorems derive the density operator and the Born rule formalism of quantum theory from the measurement postulate, by considering additive functions which assign probabilities to measurement outcomes. Additivity is also the defining property of solutions to Cauchy’s functional equation. This observation suggests an alternative proof of the strongest known Gleason-type theorem, based on techniques used to solve functional equations.

For a wave packet evolving quantum mechanically, the rates of change of the expectations and uncertainties of the position and momentum are exactly the same as if Wigner's function instantaneously obeyed a classical Liouville equation (whatever the Hamiltonian). This extension of Ehrenfest's theorem should be useful for dealing with the evolution and manipulation of quantum states.

It is well known that in any nonstandard model of $\mathsf{PA}$ (Peano arithmetic) neither addition nor multiplication is recursive. In this paper we focus on the recursiveness of unary functions and find several pairs of unary functions which cannot be both recursive in the same nonstandard model of $\mathsf{PA}$ (e.g., $\{2x,2x+1\}$, $\{x^2,2x^2\}$, and $\{2^x,3^x\}$). Furthermore, we prove that for any computable injection $f(x)$, there is a nonstandard model of $\mathsf{PA}$ in which $f(x)$ is recursive.

R. M. Friedberg demonstrated the existence of a recursive functional that agrees with no Banach-Mazur functional on the class of recursive functions. In this paper Friedberg's result is generalized to both α-recursive functionals and weak α-recursive functionals for all admissible ordinals α such that $\lambda , where α * is the Σ 1 -projectum of α and λ is the Σ 2 -cofinality of α. The theorem is also established for the metarecursive case, α = ω 1 , where (...) α * = λ = ω. (shrink)

ABSTRACT A computational logic, PLPR (Predicate Logic using Polymorphism and Recursion) is presented. Actually this logic is the object language of an automated deduction system designed as a tool for proving mathematical theorems as well as specify and verify properties of functional programs. A useful denotationl semantics and two general deduction methods for PLPR are defined. The first one is a tableau algorithm proved to be complete and also used as a guideline for building complete calculi. The second is a (...) sound and complete natural deduction system. Moreover a fixed point induction rule is introduced for formulas called continuous. The strategies for mechanizing the proofs of the final automated system are based on the previous deduction methods. As the examples of the use of the system show, the implemented theorem prover outperforms humans to a certain extent, retaining logic and calculi generality. (shrink)

We recapitulate (Section 1) some basic details of the system of implicative BCSK logic, which has two primitive binary implicational connectives, and which can be viewed as a certain fragment of the modal logic S5. From this modal perspective we review (Section 2) some results according to which the pure sublogic in either of these connectives (i.e., each considered without the other) is an exact replica of the material implication fragment of classical propositional logic. In Sections 3 and 5 we (...) show that for the pure logic of one of these implicational connectives two – in general distinct – consequence relations (global and local) definable in the Kripke semantics for modal logic turn out to coincide, though this is not so for the pure logic of the other connective, and that there is an intimate relation between formulas constructed by means of the former connective and the local consequence relation. (Corollary 5.8. This, as we show in an Appendix, is connected to the fact that the ‘propositional operations’ associated with both of our implicational connectives are close to being what R. Quackenbush has called pattern functions.) Between these discussions Section 4 examines some of the replacement-of-equivalents properties of the two connectives, relative to these consequence relations, and Section 6 closes with some observations about the metaphor of identical twins as applied to such pairs of connectives. (shrink)

A large number of scholars have conducted detailed studies on the effectiveness of commercial advertising by using neuroimaging methods, but only a few scholars have used this method to study the effectiveness of public service announcements. To research the relationship between the effectiveness of PSAs and the audience’s implicit awareness, functional near-infrared spectroscopy was employed to record the neural activity data of participants in this study. The results showed that there was a correlation between activation of dorsolateral prefrontal cortex (...) and the effectiveness of PSAs; The activation of the dlPFC could also be used as an indicator to represent the appeal of advertising content. The results means that neuroimaging tool can also be used to investigate the effectiveness of PSAs, not just commercial advertisements and a few PSAs study, and that neural activity can predict and improve the effectiveness of PSAs before they are released. (shrink)

Some conditions are given to ensure that for a jump homogeneous Markov process $\{X(t),t\ge 0\}$ the law of the integral functional of the process $T^{-1/2} \int^T_0\varphi(X(t))dt$ converges to the normal law $N(0,\sigma^2)$ as $T\to \infty$, where $\varphi$ is a mapping from the state space $E$ into $\bbfR$.

The authors would like to make the corrections to the original article described below.