Related Research Articles
Analysis is the process of breaking a complex topic or substance into smaller parts in order to gain a better understanding of it. The technique has been applied in the study of mathematics and logic since before Aristotle, though analysis as a formal concept is a relatively recent development.
Discrete mathematics is the study of mathematical structures that can be considered "discrete" rather than "continuous". Objects studied in discrete mathematics include integers, graphs, and statements in logic. By contrast, discrete mathematics excludes topics in "continuous mathematics" such as real numbers, calculus or Euclidean geometry. Discrete objects can often be enumerated by integers; more formally, discrete mathematics has been characterized as the branch of mathematics dealing with countable sets. However, there is no exact definition of the term "discrete mathematics".
Mathematics is an area of knowledge, which includes the study of such topics as numbers, formulas and related structures (algebra), shapes and spaces in which they are contained (geometry), and quantities and their changes. There is no general consensus about its exact scope or epistemological status.
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.
Proof theory is a major branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.
Johann Peter Gustav Lejeune Dirichlet was a German mathematician who made deep contributions to number theory, and to the theory of Fourier series and other topics in mathematical analysis; he is credited with being one of the first mathematicians to give the modern formal definition of a function.
Errett Albert Bishop was an American mathematician known for his work on analysis. He expanded constructive analysis in his 1967 Foundations of Constructive Analysis, where he proved most of the important theorems in real analysis by constructive methods.
In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early part of the 20th century, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies. As a solution, Hilbert proposed to ground all existing theories to a finite, complete set of axioms, and provide a proof that these axioms were consistent. Hilbert proposed that the consistency of more complicated systems, such as real analysis, could be proven in terms of simpler systems. Ultimately, the consistency of all of mathematics could be reduced to basic arithmetic.
In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005).
Newton Carneiro Affonso da Costa is a Brazilian mathematician, logician, and philosopher. He studied engineering and mathematics at the Federal University of Paraná in Curitiba and the title of his 1961 Ph.D. dissertation was Topological spaces and continuous functions.
In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.
Computational mathematics involves mathematical research in mathematics as well as in areas of science where computation plays a central and essential role, and emphasizes algorithms, numerical methods, and symbolic computations.
In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way that knowledge of the realizer gives knowledge about the truth of the formula. There are many variations of realizability; exactly which class of formulas is studied and which objects are realizers differ from one variation to another.
Markov's principle, named after Andrey Markov Jr, is a conditional existence statement for which there are many equivalent formulations, as discussed below.
In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic arithmetic into a finite type extension of primitive recursive arithmetic, the so-called System T. It was developed by Kurt Gödel to provide a consistency proof of arithmetic. The name of the interpretation comes from the journal Dialectica, where Gödel's paper was published in a 1958 special issue dedicated to Paul Bernays on his 70th birthday.
Alexandra Bellow is a Romanian-American mathematician, who has made contributions to the fields of ergodic theory, probability and analysis.
Ulrich Wilhelm Kohlenbach is a German mathematician and professor of algebra and logic at the Technische Universität Darmstadt. His research interests lie in the field of proof mining.
Steven George Krantz is an American scholar, mathematician, and writer. He has authored more than 280 research papers and more than 135 books. Additionally, Krantz has edited journals such as the Notices of the American Mathematical Society and The Journal of Geometric Analysis.
Bar recursion is a generalized form of recursion developed by C. Spector in his 1962 paper. It is related to bar induction in the same fashion that primitive recursion is related to ordinary induction, or transfinite recursion is related to transfinite induction.
Validated numerics, or rigorous computation, verified computation, reliable computation, numerical verification is numerics including mathematically strict error evaluation, and it is one field of numerical analysis. For computation, interval arithmetic is used, and all results are represented by intervals. Validated numerics were used by Warwick Tucker in order to solve the 14th of Smale's problems, and today it is recognized as a powerful tool for the study of dynamical systems.
References
- ↑ Ulrich Kohlenbach (2008). Applied Proof Theory: Proof Interpretations and Their Use in Mathematics . Springer Verlag, Berlin. pp. 1–536.
