Citizendia
Your Ad Here

Mathematical logic is a subfield of logic and mathematics. Logic is the study of the principles of valid demonstration and Inference. Mathematics is the body of Knowledge and Academic discipline that studies such concepts as Quantity, Structure, Space and [1] It consists both of the mathematical study of logic and the application of this study to other areas of mathematics. Mathematical logic has close connections to computer science and philosophical logic, as well. Computer science (or computing science) is the study and the Science of the theoretical foundations of Information and Computation and their This article is about Philosophical logic not Philosophy of logic Philosophical logic is the study of the more specifically philosophical aspects of Unifying themes in mathematical logic include the expressive power of formal logics and the deductive power of formal proof systems. In formal logic, a formal system (also called a logical system, a logistic system, or simply a logic Formal systems in mathematics consist In Mathematics, a proof is a convincing demonstration (within the accepted standards of the field that some Mathematical statement is necessarily true

Since its inception, mathematical logic has contributed to, and has been motivated by, the study of foundations of mathematics. Foundations of mathematics is a term sometimes used for certain fields of Mathematics, such as Mathematical logic, Axiomatic set theory, Proof theory This study began in the late 19th century with the development of axiomatic frameworks for geometry, arithmetic, and analysis. In the early 20th century it was shaped by David Hilbert's program to prove the consistency of foundational theories. David Hilbert ( January 23, 1862 &ndash February 14, 1943) was a German Mathematician, recognized as one of the most Hilbert's program, formulated by German mathematician David Hilbert in the 1920s was to formalize all existing theories to a finite complete set of axioms and provide Results of Kurt Gödel, Gerhard Gentzen, and others provided partial resolution to the program, and clarified the issues involved in proving consistency. Kurt Gödel (kʊɐ̯t ˈgøːdl̩ (April 28 1906 – January 14 1978 was an Austrian American Logician, Mathematician and Philosopher Gerhard Karl Erich Gentzen ( November 24, 1909, Greifswald, Germany &ndash August 4, 1945, Prague, Czechoslovakia Work in set theory showed that almost all ordinary mathematics can be formalized in terms of sets, although there are some theorems that cannot be proven in common axiom systems for set theory. Contemporary work in the foundations of mathematics often focuses on establishing which parts of mathematics can be formalized in particular formal systems, rather than trying to find theories in which all of mathematics can be developed. In formal logic, a formal system (also called a logical system, a logistic system, or simply a logic Formal systems in mathematics consist

Mathematical logic is often divided into the subfields of set theory, model theory, recursion theory, and proof theory and constructive mathematics. In Mathematics, model theory is the study of (classes of mathematical structures such as groups, Fields graphs or even models Recursion theory, also called computability theory, is a branch of Mathematical logic that originated in the 1930s with the study of Computable functions Proof theory is a branch of Mathematical logic that represents proofs as formal Mathematical objects facilitating their analysis by mathematical techniques In the Philosophy of mathematics These areas share basic results on logic, particularly first-order logic, and definability. First-order logic (FOL is a formal Deductive system used in mathematics philosophy linguistics and computer science In Mathematical logic, a definable set is an n-ary relation on the domain of a structure whose elements are precisely those elements

Contents

History

Mathematical logic began to diverge as a distinct field in the mid-19th century (Ferreirós 2001, p. 443). Until then, logic was studied with rhetoric, through the syllogism, and with philosophy (see History of logic). Rhetoric has had many definitions no simple definition can do it justice A syllogism, or logical appeal, (συλλογισμός &mdash "conclusion" "inference" (usually the categorical syllogism) is a kind of Philosophy is the study of general problems concerning matters such as existence knowledge truth beauty justice validity mind and language The history of logic traces the development of the science of valid inference ( Logic) Sophisticated theories of logic were developed in many cultures; the works most familiar to western mathematicians were Aristotle's theory of syllogisms and Euclid's axioms for planar geometry. Aristotle (Greek Aristotélēs) (384 BC – 322 BC was a Greek philosopher a student of Plato and teacher of Alexander the Great. A syllogism, or logical appeal, (συλλογισμός &mdash "conclusion" "inference" (usually the categorical syllogism) is a kind of Euclid ( Greek:.) fl 300 BC also known as Euclid of Alexandria, is often referred to as the Father of Geometry Euclidean geometry is a mathematical system attributed to the Greek Mathematician Euclid of Alexandria. In the 1700s, attempts to treat the operations of formal logic in a symbolic or algebraic way had been made by philosophical mathematicians including Leibniz and Lambert, but their labors remained isolated and little known. Johann Heinrich Lambert ( August 26, 1728 &ndash September 25 1777) was a Swiss Mathematician, Physicist and

19th century

In the middle of the nineteenth century, George Boole and then Augustus De Morgan presented systematic mathematical treatments of logic. George Boole (buːl ( November 2, 1815 &ndash December 8, 1864) was a British Mathematician and Philosopher. Augustus De Morgan ( 27 June, 1806 &ndash 18 March, 1871) was a British Mathematician and Logician. Their work, building on work by algebraists such as George Peacock, reformed and extended the traditional Aristotelian doctrine of logic and developed an adequate instrument for investigating the fundamental concepts of mathematics (Katz 1998, p. George Peacock ( April 9, 1791 – November 8, 1858) was an English Mathematician. Foundations of mathematics is a term sometimes used for certain fields of Mathematics, such as Mathematical logic, Axiomatic set theory, Proof theory 686).

Charles Peirce built upon the work of Boole to develop a logical system for relations and quantifiers, which he published in several papers from 1870 to 1885. Charles Sanders Peirce (pronounced purse) (September 10 1839 &ndash April 19 1914 was an American Logician mathematician, philosopher Gottlob Frege presented an independent development of logic with quantifiers in his Begriffsschrift, published in 1879. Friedrich Ludwig Gottlob Frege ( 8 November 1848, Wismar, Grand Duchy of Mecklenburg-Schwerin  &ndash 26 July 1925 Begriffsschrift is the title of a short book on Logic by Gottlob Frege, published in 1879, and is also the name of the Formal system Frege's work remained obscure, however, until Russell began to promote it near the turn of the century. The two-dimensional notation Frege developed was never widely adopted and is unused in contemporary texts.

From 1890 to 1905, Ernst Schröder published Vorlesungen über die Algebra der Logik in three volumes. For the actor see Ernst Schröder (actor. Ernst Schröder ( 25 November, 1841 Mannheim Germany – This work summarized and extended the work of Boole, De Morgan, and Peirce, and was a comprehensive reference to symbolic logic as it was understood at the end of the 19th century.

Foundational theories

The development of formal logic, together with concerns that mathematics had not been built on a proper foundation, led to the development of axiom systems for fundamental areas of mathematics such as arithmetic, analysis, and geometry.

In logic, the term arithmetic refers to the theory of the natural numbers. In Mathematics, a natural number (also called counting number) can mean either an element of the set (the positive Integers or an Giuseppe Peano (1888) published a set of axioms for arithmetic that came to bear his name, using a variation of the logical system of Boole and Schröder but adding quantifiers. Giuseppe Peano ( August 27, 1858 &ndash April 20, 1932) was an Italian Mathematician, whose work was of exceptional Peano was unaware of Frege's work at the time. Around the same time Richard Dedekind showed that the natural numbers are uniquely characterized by their induction properties. Julius Wilhelm Richard Dedekind ( October 6, 1831 &ndash February 12, 1916) was a German mathematician who did important Dedekind (1888) proposed a different characterization, which lacked the formal logical character of Peano's axioms. Dedekind's work, however, proved theorems inaccessible in Peano's system, including the uniqueness of the set of natural numbers (up to isomorphism) and the recursive definitions of addition and multiplication from the successor function and mathematical induction. The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict Subset of the recursive Mathematical induction is a method of Mathematical proof typically used to establish that a given statement is true of all Natural numbers It is done by proving that

In the mid-19th century, flaws in Euclid's axioms for geometry became known (Katz 1998, p. 774). In addition to the independence of the parallel postulate, established by Nikolai Lobachevsky in 1826 (Lobachevsky 1840), mathematicians discovered that certain theorems taken for granted by Euclid were not in fact provable from his axioms. In Geometry, the parallel postulate, also called Euclid 's fifth postulate since it is the fifth postulate in Euclid's ''Elements'', is a distinctive Nikolai Ivanovich Lobachevsky (Никола́й Ива́нович Лобаче́вский ( December 1 1792 &ndash February 24 1856 ( N Among these is the theorem that a line contains at least two points, or that circles of the same radius whose centers are separated by that radius must intersect. Hilbert (1899) developed a complete set of axioms for geometry, building on previous work by Pasch (1882). Hilbert's axioms are a set of 20 assumptions (originally 21 David Hilbert proposed in 1899 as the foundation for a modern treatment of Euclidean geometry. In Geometry, Pasch's axiom, is a result of Plane geometry used by Euclid, but yet which cannot be derived from Euclid's postulates. The success in axiomatizing geometry motivated Hilbert to seek complete axiomatizations of other areas of mathematics, such as the real line and the natural numbers. This would prove to be a major area of research in the first half of the 20th century.

The 19th century saw great advances in the theory of real analysis, including theories of convergence of functions and Fourier series. Real analysis is a branch of Mathematical analysis dealing with the set of Real numbers In particular it deals with the analytic properties of real In Mathematics, a Fourier series decomposes a periodic function into a sum of simple oscillating functions Mathematicians such as Karl Weierstrass began to construct functions that stretched intuition, such as nowhere-differentiable continuous functions. Karl Theodor Wilhelm Weierstrass ( Weierstraß) ( October 31, 1815 &ndash February 19, 1897) was a German mathematician Previous conceptions of a function as a rule for computation, or a smooth graph, were no longer adequate. Weierstrass began to advocate the arithmetization of analysis, which sought to axiomatize analysis using properties of the natural numbers. The arithmetization of analysis was a research program in the Foundations of mathematics carried out in the second half of the 19th century The modern "ε-δ" definition of limits and continuous functions was developed by Bolzano and Cauchy between 1817 and 1823 (Felscher 2000). In Mathematics, the concept of a " limit " is used to describe the Behavior of a function as its argument either "gets close" In Mathematics, a continuous function is a function for which intuitively small changes in the input result in small changes in the output In 1858, Dedekind proposed a definition of the real numbers in terms of Dedekind cuts of rational numbers (Dedekind 1872), a definition still employed in contemporary texts. In Mathematics, a Dedekind cut, named after Richard Dedekind, in a Totally ordered set S is a partition of it into two non-empty

Georg Cantor developed the fundamental concepts of infinite set theory. Georg Ferdinand Ludwig Philipp Cantor ( – January 6 1918) was a German Mathematician, born in Russia. His early results developed the theory of cardinality and proved that the reals and the natural numbers have different cardinalities (Cantor 1874). In Mathematics, the cardinality of a set is a measure of the "number of elements of the set" Over then next twenty years, Cantor developed a theory of transfinite numbers in a series of publications. Transfinite numbers are Cardinal numbers or Ordinal numbers that are larger than all finite numbers yet not necessarily absolutely infinite. In 1891, he published a new proof of the uncountability of the real numbers that introduced the diagonal argument, and used this method to prove Cantor's theorem that no set can have the same cardinality as its powerset. Note in order to fully understand this article you may want to refer to the Set theory portion of the Table of mathematical symbols. In Mathematics, given a set S, the power set (or powerset) of S, written \mathcal{P}(S P ( S) Cantor believed that every set could be well-ordered, but was unable to produce a proof for this result, leaving it as an open problem in 1895 (Katz 1998, p. 807).

20th century

In the early decades of the 20th century, the main areas of study were set theory and formal logic. The discovery of paradoxes in informal set theory caused some to wonder whether mathematics itself is inconsistent, and to look for proofs of consistency.

In 1900, Hilbert posed a famous list of 23 problems for the next century. Hilbert's problems are a list of twenty-three problems in Mathematics put forth by German Mathematician David Hilbert at the Paris The first two of these were to resolve the continuum hypothesis and prove the consistency of elementary arithmetic, respectively; the tenth was to produce a method that could decide whether a multivariate polynomial equation over the integers has a solution. In Mathematics, the continuum hypothesis (abbreviated CH) is a Hypothesis, advanced by Georg Cantor, about the possible sizes of Infinite The integers (from the Latin integer, literally "untouched" hence "whole" the word entire comes from the same origin but via French Subsequent work to resolve these problems shaped the direction of mathematical logic, as did the effort to resolve Hilbert's Entscheidungsproblem, posed in 1928. In Mathematics, the Entscheidungsproblem ( German for ' Decision problem ' is a challenge posed by David Hilbert in 1928 This problem asked for a procedure that would decide, given a formalized mathematical statement, whether the statement is true or false.

Set theory and paradoxes

Ernst Zermelo (1904) gave a proof that every set could be well-ordered, a result Georg Cantor had been unable to obtain. Ernst Friedrich Ferdinand Zermelo ( July 27 1871, Berlin, German Empire – May 21 1953, Freiburg im Breisgau Georg Ferdinand Ludwig Philipp Cantor ( – January 6 1918) was a German Mathematician, born in Russia. To achieve the proof, Zermelo introduced the axiom of choice, which drew heated debate and research among mathematicians and the pioneers of set theory. In Mathematics, the axiom of choice, or AC, is an Axiom of Set theory. The immediate criticism of the method led Zermelo to publish a second exposition of his result, restating the proof and then directly addressing criticisms of the first proof (Zermelo 1908). This paper led to the general acceptance of the axiom of choice in the mathematics community.

Skepticism about the axiom of choice was reinforced by recently discovered paradoxes in naive set theory. Cesare Burali-Forti (1897) was the first to state a paradox: the Burali-Forti paradox shows that the collection of all ordinal numbers cannot form a set. Cesare Burali-Forti ( 13 august 1861 Arezzo - 21 january 1931 Turin) was an Italian Mathematician In Set theory, a field of Mathematics, the Burali-Forti paradox demonstrates that naively constructing "the set of all Ordinal numbers quot leads to In Set theory, an ordinal number, or just ordinal, is the Order type of a Well-ordered set. Very soon thereafter, Bertrand Russell discovered Russell's paradox in 1901, and Jules Richard (1905) discovered Richard's paradox. Bertrand Arthur William Russell 3rd Earl Russell, OM, FRS (18 May 1872 – 2 February 1970 was a British Philosopher, Historian Part of the Foundations of mathematics, Russell's paradox (also known as Russell's antinomy) discovered by Bertrand Russell in 1901 showed that the Jules Richard (born 12 Aug, 1862 in Blet, Département Cher died 14 Oct, 1956 in Châteauroux, Département Indre was Richard's paradox is a fallacious Paradox of mathematical mapping first described by the French Mathematician Jules Richard in 1905

Zermelo (1908) provided the first set of axioms for set theory. These axioms, together with the additional axiom of replacement proposed by Abraham Fraenkel, are now called Zermelo–Fraenkel set theory (ZF). In Set theory, the axiom schema of replacement is a schema of Axioms in Zermelo-Fraenkel set theory (ZFC that asserts that the image Abraham Halevi (Adolf Fraenkel (אברהם הלוי (אדולף פרנקל February 17 1891 Munich, Germany – October 15 Zermelo–Fraenkel set theory with the axiom of choice, commonly abbreviated ZFC, is the standard form of Axiomatic set theory and as such is the most common Zermelo's axioms incorporated the principle of limitation of size to avoid Russell's paradox. In the Philosophy of mathematics, specifically the philosophical foundations of Set theory, limitation of size is a concept developed by Philip Jourdain

In 1910, the first volume of Principia Mathematica by Russell and Alfred North Whitehead was published. The Principia Mathematica is a 3-volume work on the Foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell Alfred North Whitehead, OM ( February 15 1861, Ramsgate, Kent, England &ndash December 30 1947, This seminal work developed the theory of functions and cardinality in a completely formal framework of type theory, which Russell and Whitehead developed in an effort to avoid the paradoxes. In Mathematics, Logic and Computer science, type theory is any of several Formal systems that can serve as alternatives to Naive set theory Principia Mathematica is considered one of the most influential works of the 20th century, although the framework of type theory did not prove popular as a foundational theory for mathematics (Ferreirós 2001, p. 445).

Fraenkel (1922) proved that the axiom of choice cannot be proved from the remaining axioms of Zermelo's set theory with urelements. In Set theory, a branch of Mathematics, an urelement or ur-element (from the German prefix ur-, 'primordial' is an object (concrete Later work by Paul Cohen (1966) showed that the addition of urelements is not needed, and the axiom of choice is unprovable in ZF. Paul Cohen may refer to Paul Cohen (mathematician (1934&ndash2007 American (middle initial J professor at Stanford University Paul Cohen Cohen's proof developed the method of forcing, which is now an important tool for establishing independence results in set theory. In the mathematical discipline of Set theory, forcing is a technique invented by Paul Cohen, for proving Consistency and independence results

Symbolic logic

Leopold Löwenheim (1918) and Thoralf Skolem (1919) obtained the Löwenheim–Skolem theorem, which says that first-order logic cannot control the cardinalities of infinite structures. Leopold Löwenheim (1878 Krefeld Germany - 1957 Berlin) was a German Mathematician, known for his work in Mathematical logic. Thoralf Albert Skolem ( May 23, 1887 – March 23, 1963) (ˈtɔɾɑlf ˈskuləm was a Norwegian Mathematician known In Mathematical logic, the Löwenheim–Skolem theorem states that if a countable first-order theory has an infinite model then for every infinite Cardinal number Skolem realized that this theorem would apply to first-order formalizations of set theory, and that it implies any such formalization has a countable model. In Universal algebra and in Model theory, a structure consists of an underlying set along with a collection of Finitary functions and relations This counterintuitive fact became known as Skolem's paradox. Skolem's paradox is the mathematical fact that every countable Axiomatisation of Set theory in First-order logic, if Consistent, has

In his doctoral thesis, Gödel (1929) proved the completeness theorem, which establishes a correspondence between syntax and semantics in first-order logic. Gödel's completeness theorem is a fundamental theorem in Mathematical logic that establishes a correspondence between semantic truth and syntactic provability in First-order logic (FOL is a formal Deductive system used in mathematics philosophy linguistics and computer science Gödel used the completeness theorem to prove the compactness theorem, demonstrating the finitary nature of first-order logical consequence. In Mathematical logic, the compactness theorem states that a (possibly Infinite) set of first-order sentences has a model, Iff every "Therefore" redirects here For the symbol see Therefore sign. These results helped establish first-order logic as the dominant logic used by mathematicians.

In 1931, Gödel published On Formally Undecidable Propositions of Principia Mathematica and Related Systems, which proved the incompleteness (in a different meaning of the word) of all sufficiently strong, effective first-order theories. This article describes the publication details of a famous paper in mathematical logic In Mathematical logic, Gödel's incompleteness theorems, proved by Kurt Gödel in 1931 are two Theorems stating inherent limitations of all but the most This result established severe limitations on axiomatic foundations for mathematics, striking a strong blow to Hilbert's program. It showed the impossibility of providing a consistency proof of arithmetic within any formal theory of arithmetic. Hilbert, however, did not acknowledge the importance of the incompleteness theorem for some time.

Gödel's theorem shows that a consistency proof of any sufficiently strong, effective axiom system cannot be obtained in the system itself, if the system is consistent, nor in any weaker system. This leaves open the possibility of consistency proofs that cannot be formalized within the system they consider. Gentzen (1936) proved the consistency of arithmetic using a finitistic system together with a principle of transfinite induction. Transfinite induction is an extension of Mathematical induction to well-ordered sets, for instance to sets of ordinals or cardinals. Gentzen's result introduced the ideas of cut elimination and proof-theoretic ordinals, which became key tools in proof theory. The cut-elimination theorem is the central result establishing the significance of the Sequent calculus. In Proof theory, ordinal analysis assigns ordinals (often Large countable ordinals) to mathematical theories as a measure of their strength Gödel (1958) gave a different consistency proof, which reduces the consistency of classical arithmetic to that of intutitionistic arithmetic in higher types.

Beginnings of the other branches

Alfred Tarski developed the basics of model theory. Alfred Tarski ( January 14, 1901, Warsaw, Russian ruled Poland – October 26, 1983, Berkeley California In Mathematics, model theory is the study of (classes of mathematical structures such as groups, Fields graphs or even models

Beginning in 1935, a group of prominent mathematicians collaborated under the pseudonym Nicolas Bourbaki to publish a series of encyclopedic mathematics texts. Nicolas Bourbaki is the collective Pseudonym under which a group of (mainly French) 20th-century Mathematicians wrote a series of books presenting an exposition These texts, written in an austere and axiomatic style, emphasized rigorous presentation and set-theoretic foundations. Terminology coined by these texts, such as the words bijection, injection, and surjection, and the set-theoretic foundations the texts employed, were widely adopted throughout mathematics. In Mathematics and related technical fields the term map or mapping is often a Synonym for function.

The study of computability came to be known as recursion theory, because early formalizations by Gödel and Kleene relied on recursive definitions of functions. [2] When these definitions were shown equivalent to Turing's formalization involving Turing machines, it became clear that a new concept – the computable function – had been discovered, and that this definition was robust enough to admit numerous independent characterizations. Computable functions are the basic objects of study in computability theory. In his work on the incompleteness theorems in 1931, Gödel lacked a rigorous concept of an effective formal system; he immediately realized that the new definitions of computability could be used for this purpose, allowing him to state the incompleteness theorems in generality that could only be implied in the original paper.

Numerous results in recursion theory were obtained in the 1940s by Stephen Cole Kleene and Emil Leon Post. Stephen Cole Kleene ( January 5, 1909, Hartford Connecticut, USA &ndash January 25, 1994, Madison Wisconsin Emil Leon Post, PhD, ( February 11 1897, Augustów – April 21 1954, New York City) was a Mathematician Kleene (1943) introduced the concepts of relative computability, foreshadowed by Turing (1939), and the arithmetical hierarchy. In Mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene hierarchy classifies certain sets based on the complexity of formulas Kleene later generalized recursion theory to higher-order functionals. Kleene and Kreisel studied formal versions of intuitionistic mathematics, particularly in the context of proof theory.

Subfields and scope

Contemporary mathematical logic is roughly divided into four areas: set theory, model theory, recursion theory, and proof theory and constructive mathematics. In Mathematics, model theory is the study of (classes of mathematical structures such as groups, Fields graphs or even models Recursion theory, also called computability theory, is a branch of Mathematical logic that originated in the 1930s with the study of Computable functions Proof theory is a branch of Mathematical logic that represents proofs as formal Mathematical objects facilitating their analysis by mathematical techniques In the Philosophy of mathematics Each area has a distinct focus, although many techniques and results are shared between multiple areas. The border lines between these fields, and the lines between mathematical logic and other fields of mathematics, are not always sharp. Gödel's incompleteness theorem marks not only a milestone in recursion theory and proof theory, but has also led to Loeb's theorem in modal logic. In Mathematical logic, Gödel's incompleteness theorems, proved by Kurt Gödel in 1931 are two Theorems stating inherent limitations of all but the most In Mathematical logic, Löb's theorem states that in a theory with Peano arithmetic, for any formula P if it is provable that "if P is provable then The method of forcing is employed in set theory, model theory, and recursion theory, as well as in the study of intuitionistic mathematics. In the mathematical discipline of Set theory, forcing is a technique invented by Paul Cohen, for proving Consistency and independence results

The mathematical field of category theory uses many formal axiomatic methods, but category theory is not ordinarily considered a subfield of mathematical logic. In Mathematics, category theory deals in an abstract way with mathematical Structures and relationships between them it abstracts from sets Because of its applicability in diverse fields of mathematics, mathematicians including Saunders Mac Lane have proposed category theory as a foundational system for mathematics, independent of set theory. Saunders Mac Lane ( 4 August 1909, Taftville, Connecticut – 14 April 2005, San Francisco) was an American These foundations use toposes, which resemble generalized models of set theory that may employ classical or nonclassical logic. In Mathematics, a topos (plural "topoi" or "toposes" is a type of category that behaves like the category of sheaves of sets

Formal logic

At its core, mathematical logic deals with mathematical concepts expressed using formal logical systems. These systems, though they differ in many details, share the common property of considering only expressions in a fixed formal language, or signature. In Mathematics, signature can refer to The signature of a Permutation is ±1 according to whether it is an even/odd permutation The system of first-order logic is the most widely studied today, because of its applicability to foundations of mathematics and because of its desirable proof-theoretic properties. First-order logic (FOL is a formal Deductive system used in mathematics philosophy linguistics and computer science Foundations of mathematics is a term sometimes used for certain fields of Mathematics, such as Mathematical logic, Axiomatic set theory, Proof theory [3] Stronger classical logics such as second-order logic or infinitary logic are also studied, along with nonclassical logics such as intuitionistic logic. In Logic and Mathematics second-order logic is an extension of First-order logic, which itself is an extension of Propositional logic. Those unfamiliar with Mathematical logic or the concept of Ordinals are advised to consult those articles first Intuitionistic logic, or constructivist logic, is the Symbolic logic system originally developed by Arend Heyting to provide a formal basis for Brouwer

First-order logic

Main article: First-order logic

First-order logic is a particular formal system of logic. First-order logic (FOL is a formal Deductive system used in mathematics philosophy linguistics and computer science In formal logic, a formal system (also called a logical system, a logistic system, or simply a logic Formal systems in mathematics consist Its syntax involves only finite expressions as well-formed formulas, while its semantics are characterized by the limitation of all quantifiers to a fixed domain of discourse. In Linguistics, syntax (from Ancient Greek grc συν- syn-, "together" and grc τάξις táxis, "arrangement" is the Semantics is the study of meaning in communication The word derives from Greek σημαντικός ( semantikos) "significant" from Quantification has two distinct meanings In Mathematics and Empirical science, it refers to human acts known as Counting and Measuring The domain of discourse, sometimes called the universe of discourse, logical discourse, or simply discourse, is an analytic tool used in Deductive

Early results about formal logic established limitations of first-order logic. The Löwenheim–Skolem theorem (1919) showed that if a set of sentences in a countable first-order language has an infinite model then it has at least one model of each infinite cardinality. In Mathematical logic, the Löwenheim–Skolem theorem states that if a countable first-order theory has an infinite model then for every infinite Cardinal number This shows that it is impossible for a set of first-order axioms to characterize the natural numbers, the real numbers, or any other infinite structure up to isomorphism. In Abstract algebra, an isomorphism ( Greek: ἴσος isos "equal" and μορφή morphe "shape" is a bijective As the goal of early foundational studies was to produce axiomatic theories for all parts of mathematics, this limitation was particularly stark.

Gödel's completeness theorem (Gödel 1929) established the equivalence between semantic and syntactic definitions of logical consequence in first-order logic. Gödel's completeness theorem is a fundamental theorem in Mathematical logic that establishes a correspondence between semantic truth and syntactic provability in "Therefore" redirects here For the symbol see Therefore sign. It shows that if a particular sentence is true in every model that satisfies a particular set of axioms, then there must be a finite deduction of the sentence from the axioms. The compactness theorem first appeared as a lemma in Gödel's proof of the completeness theorem, and it took many years before logicians grasped its significance and began to apply it routinely. In Mathematical logic, the compactness theorem states that a (possibly Infinite) set of first-order sentences has a model, Iff every It says that a set of sentences has a model if and only if every finite subset has a model, or in other words that an inconsistent set of formulas must have a finite inconsistent subset. ↔ The completeness and compactness theorems allow for sophisticated analysis of logical consequence in first-order logic and the development of model theory, and they are a key reason for the prominence of first-order logic in mathematics. In Mathematics, model theory is the study of (classes of mathematical structures such as groups, Fields graphs or even models

Gödel's incompleteness theorems (Gödel 1931) established additional limits on first-order axiomatization. In Mathematical logic, Gödel's incompleteness theorems, proved by Kurt Gödel in 1931 are two Theorems stating inherent limitations of all but the most The first incompleteness theorem states that no sufficiently strong, effectively given logical system can prove its own consistency (unless it actually is inconsistent). In formal logic, a formal system (also called a logical system, a logistic system, or simply a logic Formal systems in mathematics consist Here a logical system is effectively given if it is possible to decide, given any formula in the language of the system, whether the formula is an axiom. When applied to first-order logic, the first incompleteness theorem implies that any sufficiently strong, consistent, effective first-order theory has models that are not elementarily equivalent, a stronger limitation than the one established by the Löwenheim–Skolem theorem. In Mathematics, specifically Model theory, two structures for a given language are said to be elementarily equivalent if any sentence The second incompleteness theorem states that no sufficiently strong, consistent, effective axiom system for arithmetic can prove its own consistency, which has been interpreted to show that Hilbert's program cannot be completed.

Other classical logics

Many logics besides first-order logic are studied. These include infinitary logics, which allow for formulas to provide an infinite amount of information, and higher-order logics, which include a portion of set theory directly in their semantics. Those unfamiliar with Mathematical logic or the concept of Ordinals are advised to consult those articles first

The most well studied infinitary logic is L_{\omega_1,\omega}. In this logic, quantifiers may only be nested to finite depths, as in first order logic, but formulas may have finite or countably infinite conjunctions and disjunctions within them. Thus, for example, it is possible to say that an object is a natural number using a formula of L_{\omega_1,\omega} such as

(x = 0) \lor (x = 1) \lor (x = 2) \lor \cdots.

Higher-order logics allow for quantification not only of elements of the domain of discourse, but subsets of the domain of discourse, sets of such subsets, and other objects of higher type. The semantics are defined so that, rather than having a separate domain for each higher-type quantifier to range over, the quantifiers instead range over all objects of the appropriate type. The logics studied before the development of first-order logic, for example Frege's logic, had similar set-theoretic aspects. Although higher-order logics are more expressive, allowing complete axiomatizations of structures such as the natural numbers, they do not satisfy analogues of the completeness and compactness theorems from first-order logic, and are thus less amenable to proof-theoretic analysis.

Nonclassical and modal logic

Modal logics include additional modal operators, such as an operator which states that a particular formula is not only true, but necessarily true. A modal logic is any system of formal logic that attempts to deal with modalities. Although modal logic is not often used to axiomatize mathematics, it has been used to study the properties of first-order provability (Solovay 1976) and set-theoretic forcing (Hamkins and Löwe 2007).

Intuitionistic logic was originally developed by Heyting to study Brouwer's program of intuitionsim, in which Brouwer himself avoided formalization. Intuitionistic logic, or constructivist logic, is the Symbolic logic system originally developed by Arend Heyting to provide a formal basis for Brouwer Intuitionistic logic specifically does not include the law of the excluded middle, which states that each sentence is either true or its negation is true. This article uses forms of logical notation For a concise description of the symbols used in this notation see Table of logic symbols. Kleene's work with the proof theory of intuitionistic logic showed that constructive information can be recovered from intuitionistic proofs. For example, any provably total function in intuitionistic arithmetic is computable; this is not true in classical theories of arithmetic such as Peano arithmetic. In Mathematical logic, the Peano axioms, also known as the Dedekind-Peano axioms or the Peano postulates, are a set of Axioms for the Natural

Set theory

Main article: Set theory

Set theory is the study of sets, which are abstract collections of objects. Many of the basic notions, such as ordinal and cardinal numbers, were developed informally by Cantor before formal axiomatizations of set theory were developed. The first such axiomatization, due to Zermelo (1908), was extended slightly to become Zermelo–Fraenkel set theory (ZF), which is now the most widely-used foundational theory for mathematics. Zermelo–Fraenkel set theory with the axiom of choice, commonly abbreviated ZFC, is the standard form of Axiomatic set theory and as such is the most common

Other formalizations of set theory have been proposed, including von Neumann–Bernays–Gödel set theory (NBG), Morse–Kelley set theory (MK), and New Foundations (NF). In the Foundations of mathematics, Von Neumann–Bernays–Gödel set theory ( NBG) is an Axiomatic set theory that is a Conservative extension In the Foundation of mathematics, Kelley–Morse (KM or Morse–Kelley (MK set theory is a first order Axiomatic set theory that is closely In Mathematical logic, New Foundations ( NF) is an Axiomatic set theory, conceived by Willard Van Orman Quine as a simplification of Of these, ZF, NBG, and MK are similar in describing a cumulative hierarchy of sets. In Set theory and related branches of Mathematics, the von Neumann universe, or von Neumann hierarchy of sets, denoted V, is the class New Foundations takes a different tack; it allows objects such as the set of all sets at the cost of restrictions on its set-existence axioms. The system of Kripke-Platek set theory is closely related to generalized recursion theory. The Kripke–Platek axioms of set theory ( KP) (ˈkrɪpki ˈplɑːtɛk are a system of axioms of Axiomatic set theory, developed by Saul Kripke and

Two famous statements in set theory are the axiom of choice and the continuum hypothesis. In Mathematics, the axiom of choice, or AC, is an Axiom of Set theory. In Mathematics, the continuum hypothesis (abbreviated CH) is a Hypothesis, advanced by Georg Cantor, about the possible sizes of Infinite The axiom of choice, first stated by Zermelo (1904), was proved independent of ZF by Fraenkel (1922), but has come to be widely accepted by mathematicians. It states that given a collection of nonempty sets there is a single set C that contains exactly one element from each set in the collection. The set C is said to "choose" one element from each set in the collection. While the ability to make such a choice is considered obvious by some, since each set in the collection is nonempty, the lack of a general, concrete rule by which the choice can be made renders the axiom nonconstructive. Stefan Banach and Alfred Tarski (1924) showed that the axiom of choice can be used to decompose a solid ball into a finite number of pieces which can then be rearranged, with no scaling, to make two solid balls of the original size. Stefan Banach ( Ukrainian: Степан Степанович Банах 1892–1945 was a Polish Mathematician who worked in interwar Poland and in Alfred Tarski ( January 14, 1901, Warsaw, Russian ruled Poland – October 26, 1983, Berkeley California This theorem, known as the Banach-Tarski paradox, is one of many counterintuitive results of the axiom of choice. The Banach–Tarski paradox is a Theorem in set theoretic Geometry which states that a solid ball in 3-dimensional space can be split into several

The continuum hypothesis, first proposed as a conjecture by Cantor, was listed by David Hilbert as one of his 23 problems in 1900. In Mathematics, the continuum hypothesis (abbreviated CH) is a Hypothesis, advanced by Georg Cantor, about the possible sizes of Infinite Gödel showed that the continuum hypothesis cannot be disproven from the axioms of Zermelo-Frankel set theory (with or without the axiom of choice), by developing the constructible universe of set theory in which the continuum hypothesis must hold. Gödel universe redirects here For Kurt Gödel 's cosmological solution to the Einstein field equations, see Gödel metric. In 1963, Paul Cohen showed that the continuum hypothesis cannot be proven from the axioms of Zermelo-Frankel set theory (Cohen 1966). Paul Cohen may refer to Paul Cohen (mathematician (1934&ndash2007 American (middle initial J professor at Stanford University Paul Cohen This independence result did not completely settle Hilbert's question, however, as it is possible that new axioms for set theory could resolve the hypothesis. Recent work along these lines has been conducted by W. Hugh Woodin, although its importance is not yet clear (Woodin 2001). William Hugh Woodin (b April 23, 1955, Tucson, Arizona) is a set theorist at University of California Berkeley.

Contemporary research in set theory includes the study of large cardinals and determinacy. In the mathematical field of Set theory, a large cardinal property is a certain kind of property of Transfinite Cardinal numbers Cardinals with such properties Large cardinals are cardinal numbers with particular properties so strong that the existence of such cardinals cannot be proved in ZFC. This article describes cardinal numbers in mathematics For cardinals in linguistics see Names of numbers in English. The existence of the smallest large cardinal typically studied, an inaccessible cardinal, already implies the consistency of ZFC. In Set theory, an uncountable regular cardinal number is called weakly inaccessible if it is a Weak limit cardinal, and strongly inaccessible Despite the fact that large cardinals have extremely high cardinality, their existence has many ramifications for the structure of the real line. In Mathematics, the cardinality of a set is a measure of the "number of elements of the set" Determinacy refers to the possible existence of winning strategies for certain two-player games (the games are said to be determined). The existence of these strategies implies structural properties of the real line and other Polish spaces. In Mathematics, a Polish space is a separable completely metrizable Topological space; that is a space Homeomorphic to a complete

Model theory

Main article: Model theory

Model theory studies the models of various formal theories. In Mathematics, model theory is the study of (classes of mathematical structures such as groups, Fields graphs or even models In Mathematics, model theory is the study of (classes of mathematical structures such as groups, Fields graphs or even models Here a theory is a set of formulas in a particular formal logic and signature, while a model is a structure that gives a concrete interpretation of the theory. In Mathematical logic, a theory is a set of sentences in a Formal language. In Logic, especially Mathematical logic, a signature lists and describes the Non-logical symbols of a Formal language. In Universal algebra and in Model theory, a structure consists of an underlying set along with a collection of Finitary functions and relations Model theory is closely related to universal algebra and algebraic geometry, although the methods of model theory focus more on logical considerations than those fields. Universal algebra (sometimes called general algebra) is the field of Mathematics that studies Algebraic structures themselves not examples ("models" Algebraic geometry is a branch of Mathematics which as the name suggests combines techniques of Abstract algebra, especially Commutative algebra, with

The set of all models of a particular theory is called an elementary class; classical model theory seeks to determine the properties of models in a particular elementary class, or determine whether certain classes of structures form elementary classes. In the branch of Mathematical logic called Model theory, an elementary class (or axiomatizable class) is a class consisting of all

The method of quantifier elimination can be used to show that definable sets in particular theories cannot be too complicated. Quantifier elimination is a technique in Mathematical logic, Model theory, and Theoretical computer science. Tarski (1948) established quantifier elimination for real-closed fields, a result which also shows the theory of the field of real numbers is decidable. In Mathematics, a real closed field is a field F in which any of the following equivalent conditions are true There is a Total order In Computability theory, a set of Natural numbers is called recursive, computable or decidable if there is an Algorithm (He also noted that his methods were equally applicable to algebraically closed fields of arbitrary characteristic. ) A modern subfield developing from this is concerned with o-minimal structures. In Mathematical logic, and more specifically in Model theory, a totally ordered structure ( M,<

Morley's categoricity theorem, proved by Michael D. Morley (1965), states that if a first-order theory in a countable language is categorical in some uncountable cardinality, i. In Model theory, a branch of Mathematical logic, a theory is &kappa- categorical (or categorical in &kappa) if it has exactly one model of Michael Darwin Morley is an American Mathematician, currently professor emeritus at Cornell University. e. all models of this cardinality are isomorphic, then it is categorical in all uncountable cardinalities.

A trivial consequence of the continuum hypothesis is that a complete theory with less than continuum many nonisomorphic countable models can have only countably many. In Mathematics, the continuum hypothesis (abbreviated CH) is a Hypothesis, advanced by Georg Cantor, about the possible sizes of Infinite Vaught's conjecture, named after Robert Lawson Vaught, says that this is true even independently of the continuum hypothesis. The Vaught conjecture is a Conjecture in the mathematical field of Model theory originally proposed by Robert Lawson Vaught in 1961 Robert Lawson Vaught ( April 4 1926, Alhambra California – April 2 2002) was a Mathematical logician and one of the founders Many special cases of this conjecture have been established.

Recursion theory

Main article: Recursion theory

Recursion theory, also called computability theory, studies the properties of computable functions and the Turing degrees, which divide the uncomputable functions into sets which have the same level of uncomputability. Recursion theory, also called computability theory, is a branch of Mathematical logic that originated in the 1930s with the study of Computable functions Recursion theory, also called computability theory, is a branch of Mathematical logic that originated in the 1930s with the study of Computable functions Computable functions are the basic objects of study in computability theory. Recursion theory also includes the study of generalized computability and definability. Recursion theory grew from of the work of Alonzo Church and Alan Turing in the 1930s, which was greatly extended by Kleene and Post in the 1940s. Alonzo Church ( June 14, 1903 – August 11, 1995) was an American Mathematician and logician Alan Mathison Turing, OBE, FRS (ˈt(jʊ(ərɪŋ (23 June 1912 &ndash 7 June 1954 was an English Mathematician

Classical recursion theory focuses on the computability of functions from the natural numbers to the natural numbers. The fundamental results establish a robust, canonical class of computable functions with numerous independent, equivalent characterizations using Turing machines, λ calculus, and other systems. Computable functions are the basic objects of study in computability theory. Turing machines are basic abstract symbol-manipulating devices which despite their simplicity can be adapted to simulate the logic of any Computer Algorithm In Mathematical logic and Computer science, lambda calculus, also written as λ-calculus, is a Formal system designed to investigate function More advanced results concern the structure of the Turing degrees and the lattice of recursively enumerable sets. In Mathematics, a lattice is a Partially ordered set (also called a poset) in which every pair of elements has a unique Supremum (the elements' In Computability theory, traditionally called Recursion theory, a set S of Natural numbers is called recursively enumerable, computably

Generalized recursion theory extends the ideas of recursion theory to computations that are no longer necessarily finite. It includes the study of computability in higher types as well as areas such as hyperarithmetical theory and α-recursion theory. In Recursion theory, hyperarithmetic theory is a generalization of Turing computability In Recursion theory, the mathematical theory of computability alpha recursion (often written α recursion) is a generalisation of Recursion theory to subsets

Contemporary research in recursion theory includes the study of applications such as algorithmic randomness and computable model theory as well as new results in pure recursion theory. In Algorithmic information theory (a subfield of Computer science) the Kolmogorov complexity (also known as descriptive complexity, Kolmogorov-Chaitin Computable model theory is a branch of Model theory which deals with questions of Computability as they apply to model-theoretical structures

Algorithmically unsolvable problems

An important subfield of recursion theory studies algorithmic unsolvability; a problem is algorithmically unsolvable if there is no computable function which, given any (code for) an instance of the problem, returns the correct answer. In Computability theory and Computational complexity theory, a decision problem is a question in some Formal system with a yes-or-no answer depending on The first results about unsolvability, obtained independently by Church and Turing in 1936, showed that the Entscheidungsproblem is algorithmically unsolvable. In Mathematics, the Entscheidungsproblem ( German for ' Decision problem ' is a challenge posed by David Hilbert in 1928 Turing proved this by establishing the unsolvability of the halting problem, a result with far-ranging implications in both recursion theory and computer science. In computability theory, the halting problem is a Decision problem which can be stated as follows given a description of a program and a finite input

There are many known examples of undecidable problems from ordinary mathematics. The word problem for groups was proved algorithmically unsolvable by Pyotr Sergeyevich Novikov in 1955 and independently by W. In Mathematics, especially in the area of Abstract algebra known as Combinatorial group theory, the word problem for a recursively presented Pyotr Sergeyevich Novikov (Пётр Сергеевич Новиков ( August 15, 1901 – January 9, 1975) was a Russian Mathematician Boone in 1959. The busy beaver problem, developed by Tibor Radó in 1962, is another well-known example. In computability theory, a busy beaver (from the colloquial expression for "industrious person" is a Turing machine which when given an empty tape does Tibor Radó ( June 2 1895 &ndash December 29 1965) was a Hungarian mathematician who moved to the USA after World

Hilbert's tenth problem asked for an algorithm to determine whether a multivariate polynomial equation with integer coefficients has a solution in the integers. Hilbert's tenth problem is the tenth on the list of Hilbert's problems of 1900 Partial progress was made by Julia Robinson, Martin Davis, and Hilary Putnam. Julia Hall Bowman Robinson ( December 8, 1919 – July 30, 1985) was an American Mathematician, born in St This page is on the mathematician For the former tennis player see Martin Davis (tennis. Hilary Whitehall Putnam (born July 31 1926 is an American Philosopher who has been a central figure in Western philosophy since the 1960s especially in Philosophy The algorithmic unsolvability of the problem was proved by Yuri Matiyasevich in 1970 (Davis 1973). Yuri Vladimirovich Matiyasevich, (Юрий Владимирович Матиясевич born March 2, 1947 in Leningrad) is a Russian Mathematician

Proof theory and constructive mathematics

Main article: Proof theory

Proof theory is the study of formal proofs in various logical deduction systems. Proof theory is a branch of Mathematical logic that represents proofs as formal Mathematical objects facilitating their analysis by mathematical techniques Proof theory is a branch of Mathematical logic that represents proofs as formal Mathematical objects facilitating their analysis by mathematical techniques These proofs are represented as formal mathematical objects, facilitating their analysis by mathematical techniques. Several deduction systems are commonly considered, including Hilbert-style deduction systems, systems of natural deduction, and the sequent calculus developed by Gentzen. In Logic, especially Mathematical logic, a Hilbert-style deduction system is a type of system of formal deduction attributed In Philosophical logic, natural deduction is an approach to Proof theory that attempts to provide a Deductive system which is a formal model of logical In Proof theory and Mathematical logic, the sequent calculus is a widely known Proof calculus for First-order logic (and Propositional logic

The study of constructive mathematics, in the context of mathematical logic, includes the study of systems in non-classical logic such as intuitionistic logic, as well as the study of predicative systems. In Mathematics and Logic, impredicativity is the property of a self-referencing Definition. An early proponent of predicativism was Hermann Weyl, who showed it is possible to develop a large part of real analysis using only predicative methods (Weyl 1918). Hermann Klaus Hugo Weyl ( 9 November 1885 – 8 December 1955) was a German Mathematician.

Because proofs are entirely finitary, whereas truth in a structure is not, it is common for work in constructive mathematics to emphasize provability. The relationship between provability in classical (or nonconstructive) systems and provability in intuitionistic (or constructive, respectively) systems is of particular interest. Results such as the Gödel–Gentzen negative translation show that it is possible to embed (or translate) classical logic into intuitionistic logic, allowing some properties about intuitionistic proofs to be transferred back to classical proofs. In Proof theory, the Gödel–Gentzen negative translation is a method for embedding classical First-order logic into intuitionistic first-order logic

Recent developments in proof theory include the study of proof mining by Ulrich Kohlenbach and the study of proof-theoretic ordinals by Michael Rathjen. In Proof theory (a branch of Mathematical logic) proof mining is a research program that analyzes formalized proofs especially in analysis, to obtain In Proof theory, ordinal analysis assigns ordinals (often Large countable ordinals) to mathematical theories as a measure of their strength

Connections with computer science

The study of computability theory in computer science is closely related to the study of computability in mathematical logic. In Computer science, computability theory is the branch of the Theory of computation that studies which problems are computationally solvable using different There is a difference of emphasis, however. Computer scientists often focus on concrete programming languages and feasible computability, while researchers in mathematical logic often focus on computability as a theoretical concept and on noncomputability. Computational complexity theory, as a branch of the Theory of computation in Computer science, investigates the problems related to the amounts of resources

The study of programming language semantics is related to model theory, as is program verification (in particular, model checking). A programming language is an Artificial language that can be used to write programs which control the behavior of a machine particularly a Computer. In Theoretical computer science, formal semantics is the field concerned with the rigorous mathematical study of the meaning of Programming languages and models of In Mathematics, model theory is the study of (classes of mathematical structures such as groups, Fields graphs or even models In the context of hardware and software systems formal verification is the act of proving or disproving the Correctness of intended Algorithms underlying Model checking is the process of checking whether a given structure is a model of a given logical formula The Curry-Howard isomorphism between proofs and programs relates to proof theory, especially intuitionistic logic. The Curry-Howard correspondence is the direct relationship between computer programs and mathematical proofs Proof theory is a branch of Mathematical logic that represents proofs as formal Mathematical objects facilitating their analysis by mathematical techniques Intuitionistic logic, or constructivist logic, is the Symbolic logic system originally developed by Arend Heyting to provide a formal basis for Brouwer Formal calculi such as the lambda calculus and combinatory logic are now studied as idealized programming languages. In Mathematical logic and Computer science, lambda calculus, also written as λ-calculus, is a Formal system designed to investigate function Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for Variables in Mathematical logic A programming language is an Artificial language that can be used to write programs which control the behavior of a machine particularly a Computer.

Computer science also contributes to mathematics by developing techniques for the automatic checking or even finding of proofs, such as automated theorem proving and logic programming. Automated theorem proving ( ATP) or automated deduction, currently the most well-developed subfield of Automated reasoning (AR is the Logic programming is in its broadest sense the use of mathematical logic for computer programming

Foundations of mathematics

Main article: Foundations of mathematics

In the 19th century, mathematicians became aware of logical gaps and inconsistencies in the field. Foundations of mathematics is a term sometimes used for certain fields of Mathematics, such as Mathematical logic, Axiomatic set theory, Proof theory It was shown that Euclid's axioms for geometry, which had been taught for centuries as an example of the axiomatic method, were incomplete. Euclid ( Greek:.) fl 300 BC also known as Euclid of Alexandria, is often referred to as the Father of Geometry The use of infinitesimals, and the very definition of function, came into question in analysis, as pathological examples such as Weierstrass' nowhere-differentiable function were discovered. Infinitesimals (from a 17th century Modern Latin coinage infinitesimus, originally referring to the " Infinite[[ th]]" member of a series have The Mathematical concept of a function expresses dependence between two quantities one of which is given (the independent variable, argument of the function In Calculus, a branch of mathematics the derivative is a measurement of how a function changes when the values of its inputs change

Mathematicians began to search for axiom systems that could be used to formalize large parts of mathematics. In addition to removing ambiguity from previously-naive terms such as function, it was hoped that this axiomatization would allow for consistency proofs. In the 19th century, the main method of proving the consistency of a set of axioms was to provide a model for it. Thus, for example, non-Euclidean geometry can be proved consistent by defining point to mean a point on a fixed sphere and line to mean a great circle on the sphere. In mathematics non-Euclidean geometry describes how this all works--> hyperbolic and Elliptic geometry, which are contrasted with Euclidean geometry A great circle is a Circle on the surface of a Sphere that has the same circumference as the sphere dividing the sphere into two equal Hemispheres. The resulting structure, a model of elliptic geometry, satisfies the axioms of plane geometry except the parallel postulate. Elliptic geometry (sometimes known as Riemannian geometry) is a Non-Euclidean geometry, in which given a line L and a point

With the development of formal logic, David Hilbert asked whether it would be possible to prove that an axiom system is consistent by analyzing the structure of possible proofs in the system, and showing through this analysis that it is impossible to prove a contradiction. David Hilbert ( January 23, 1862 &ndash February 14, 1943) was a German Mathematician, recognized as one of the most This idea led to the study of proof theory. Proof theory is a branch of Mathematical logic that represents proofs as formal Mathematical objects facilitating their analysis by mathematical techniques Moreover, Hilbert proposed that the analysis should be entirely concrete, using the term finitary to refer to the methods he would allow but not precisely defining them. This project, known as Hilbert's program, was seriously affected by Gödel's incompleteness theorems, which show that the consistency of formal theories of arithmetic cannot be established using methods formalizable in those theories. Hilbert's program, formulated by German mathematician David Hilbert in the 1920s was to formalize all existing theories to a finite complete set of axioms and provide Gentzen showed that it is possible to produce a proof of the consistency of arithmetic in a finitary system augmented with axioms of transfinite induction, and the techniques he developed to so do were seminal in proof theory. Transfinite induction is an extension of Mathematical induction to well-ordered sets, for instance to sets of ordinals or cardinals.

A second thread in the history of foundations of mathematics involves nonclassical and constructive mathematics. In the late 19th century, not all mathematicians accepted Cantor's new methods of manipulating infinite sets. Famously, Leopold Kronecker stated "God made the integers; all else is the work of man," referring to Cantor's work with uncountable sets. Leopold Kronecker ( December 7, 1823 – December 29, 1891) was a German Mathematician and Logician who argued Objections were also raised to Zermelo's use of the axiom of choice, although this axiom quickly found broad acceptance among mathematicians. In Mathematics, the axiom of choice, or AC, is an Axiom of Set theory.

In the early 20th century, Luitzen Egbertus Jan Brouwer founded intuitionism as a philosophy of mathematics. Luitzen Egbertus Jan Brouwer ɛxˈbɛʁtəs jɑn ˈbʁʌuəʁ ( February 27 1881, Overschie – December 2 1966, Blaricum In the Philosophy of mathematics, intuitionism, or neointuitionism (opposed to Preintuitionism) is an approach to Mathematics as the constructive This philosophy, poorly understood at first, stated that in order for a mathematical statement to be true to a mathematician, that person must be able to intuit the statement, to not only believe its truth but understand the reason for it. A consequence of this definition of truth was the rejection of the law of the excluded middle, for there are statements that, according to Brouwer, could not be claimed to be true while their negations also could not be claimed true. This article uses forms of logical notation For a concise description of the symbols used in this notation see Table of logic symbols. Brouwer's philosophy was influential, and the cause of bitter disputes among prominent mathematicians. Later, Kleene and Kreisel would study formalized versions of intuitionistic logic (Brouwer rejected formalization, and presented his work in unformalized natural language). With the advent of the BHK interpretation and Kripke models, intuitionism became easier to reconcile with classical mathematics. In Mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of Intuitionistic logic was proposed by L Kripke semantics (also known as relational semantics or frame semantics, and often confused with Possible world semantics) is a formal Semantics

The study of constructive mathematics includes many different programs with various definitions of constructive. In the Philosophy of mathematics At the most accommodating end, proofs in ZF set theory that do not use the axiom of choice are called constructive by many mathematicians. More limited versions of constructivism limit themselves to natural numbers, number-theoretic functions, and sets of natural numbers (which can be used to represent real numbers, facilitating the study of mathematical analysis). In Mathematics, a natural number (also called counting number) can mean either an element of the set (the positive Integers or an In Number theory an arithmetic function or arithmetical function is a Function defined on the set of Natural numbers (i Analysis has its beginnings in the rigorous formulation of Calculus. A common idea is that in order to assert that a number-theoretic function exists, a concrete means of computing the values of the function must be known.

See also

External links

Notes

  1. ^ Undergraduate texts include Boolos, Burgess, and Jeffrey (2002), Enderton (2002), and Mendelson (1997). A classic graduate text by Shoenfield (2001) first appeared in 1967.
  2. ^ A detailed study of this terminology is given by Soare (1996).
  3. ^ Ferreirós (2001) surveys the rise of first-order logic over other formal logics in the early 20th century.

References

Undergraduate texts

Graduate texts

Research papers, monographs, texts, and surveys

Classical papers, texts, and collections

Dictionary

mathematical logic

-noun

  1. (logic) A subfield of logic and mathematics consisting of both of the mathematical study of logic and the application of this study to other areas of mathematics, exemplified by questions on the expressive power of formal logics and the deductive power of formal proof systems.
© 2009 citizendia.org; parts available under the terms of GNU Free Documentation License, from http://en.wikipedia.org
 Dapyx Software network: MP3 Explorer | Ebook Manager | Zenithic