Difference between revisions of "Mathematical logic" - New World Encyclopedia

From New World Encyclopedia
(minor edit)
(re-import the newest edition)
Line 1: Line 1:
−
''Mathematical logic'' is a subfield of mathematics that is concerned with [[formal system]]s in relation to the way that they encode intuitive concepts of mathematical objects such as [[set]]s and [[number]]s, [[mathematical proof|proof]]s, and [[computation]].  
+
{{claimed}}
−
It is often divided into the subfields of  [[model theory]], [[proof theory]], [[set theory]] and [[recursion theory]].  Research in mathematical logic has played an important role in the study of [[foundations of mathematics]].
+
'''Mathematical logic''' is a subfield of [[mathematics]]. It is often divided into the subfields of  [[model theory]], [[proof theory]], [[set theory]] and [[recursion theory]].  Research in mathematical logic has contributed to, and been motivated by, the study of [[foundations of mathematics]], but mathematical logic also contains areas of pure mathematics not directly related to foundational questions.  
  
−
Earlier names for mathematical logic were [[symbolic logic]] (as opposed to [[philosophical logic]]) and [[metamathematics]]. The former term is still used (as in the [[Association for Symbolic Logic]]), but the latter term is now used for certain aspects of [[proof theory]].  
+
One unifying theme in mathematical logic is the study of the expressive power of formal [[logic]]s and formal [[proof (mathematics)|proof]] systems. This power is measured both in terms of what these formal systems are able to prove and in terms of what they are able to define.  
  
−
Mathematical logic is not so much the ''logic of mathematics'' as it is the ''mathematics of logic''. It includes those parts of [[logic]] that can be modeled and studied mathematically. It also includes areas of pure mathematics, such as [[model theory]] and [[recursion theory]], in which definability is central to the subject matter.
+
Earlier names for mathematical logic were '''symbolic logic''' (as opposed to [[philosophical logic]]) and '''[[metamathematics]]'''. The former term is still used (as in the [[Association for Symbolic Logic]]), but the latter term is now used for certain aspects of [[proof theory]].
  
 
==History==
 
==History==
  
−
''Mathematical logic'' was the name given by [[Giuseppe Peano]] to what is also known as symbolic logic. In essentials, it is still the logic of [[Aristotle]], but from the point of view of notation it is written as a branch of [[abstract algebra]].
+
''Mathematical logic'' was the name given by [[Giuseppe Peano]] to what is also known as symbolic logic. In its classical version, the basic aspects resemble the logic of [[Aristotle]], but written using symbolic notation rather than natural language. Attempts to treat the operations of formal logic in a symbolic or algebraic way were made by some of the more philosophical mathematicians, such as [[Leibniz]] and [[Johann Heinrich Lambert|Lambert]]; but their labors remained little known and isolated. It was [[George Boole]] and then [[Augustus De Morgan]], in the middle of the nineteenth century, who presented a systematic mathematical way of regarding logic. The traditional, Aristotelian doctrine of logic was reformed and completed; and out of it developed an adequate instrument for investigating the [[foundations of mathematics|fundamental concepts of mathematics]]. It would be misleading to say that the foundational controversies that were alive in the period 1900–1925 have all been settled; but [[philosophy of mathematics]] was greatly clarified by the "new" logic.
−
 
 
−
Attempts to treat the operations of formal logic in a symbolic or algebraic way were made by some of the more philosophical mathematicians, such as [[Leibniz]] and [[Johann Heinrich Lambert|Lambert]]; but their labors remained little known and isolated. It was [[George Boole]] and then [[Augustus De Morgan]], in the middle of the nineteenth century, who presented a systematic mathematical (of course non-[[quantitative]]) way of regarding logic. The traditional, Aristotelian doctrine of logic was reformed and completed; and out of it developed an adequate instrument for investigating the [[foundations of mathematics|fundamental concepts of mathematics]]. It would be misleading to say that the foundational controversies that were alive in the period 1900–1925 have all been settled; but [[philosophy of mathematics]] was greatly clarified by the "new" logic.
 
 
   
 
   
−
While the traditional development of logic (see [[list of topics in logic]]) put heavy emphasis on ''forms of arguments'', the attitude of current mathematical logic might be summed up as ''the combinatorial study of content''. This covers both the ''syntactic'' (for example, sending a string from a [[formal language]] to a [[compiler]] program to write it as sequence of machine instructions), and the ''semantic'' (constructing specific models or whole sets of them, in [[model theory]]).
+
While the Greek development of logic (see [[list of topics in logic]]) put heavy emphasis on ''forms of arguments'', the attitude of current mathematical logic might be summed up as ''the combinatorial study of content''. This covers both the ''syntactic'' (for example, sending a string from a [[formal language]] to a [[compiler]] program to write it as sequence of machine instructions), and the ''semantic'' (constructing specific models or whole sets of them, in [[model theory]]).  This study of mathematics from the outside is known as [[metamathematics]].
  
−
Some landmark publications were the ''[[Begriffsschrift]]'' by [[Gottlob Frege]], [[Studies in Logic]] by [[Charles Peirce]], ''[[Principia Mathematica]]'' by [[Bertrand Russell]] and [[Alfred North Whitehead]], and[[Godel's incompleteness theorem| On Formally Undecidable Propositions of Principia Mathematica and Related Systems]] by [[Kurt Gödel]].
+
Some landmark publications were the ''[[Begriffsschrift]]'' by [[Gottlob Frege]], [[Studies in Logic]] by [[Charles Peirce]], ''[[Principia Mathematica]]'' by [[Bertrand Russell]] and [[Alfred North Whitehead]], and ''[[On Formally Undecidable Propositions of Principia Mathematica and Related Systems]]'' by [[Kurt Gödel]].
  
−
===Fields of mathematical logic===
+
== Formal logic ==
  
−
According to the "Handbook of Mathematical Logic" (1977), Mathematical Logic is traditionally divided into four parts:
+
At its core, mathematical logic deals with mathematical concepts expressed using formal logical systems. The system of [[first-order logic]] is the most widely studied because of its applicability to [[foundations of mathematics]] and because of its desirable properties.  Stronger classical logics such as [[second-order logic]] or [[infinitary logic]] are also studied, along with nonclassical logics such as  
−
*[[model theory]]
+
[[intuitionistic logic]].
−
*[[set theory]] (usually interpreted as [[axiomatic set theory]])
 
−
*[[recursion theory]] (often now referred to as computability theory)
 
−
*[[proof theory]].  
 
−
The [[Mathematics Subject Classification|2000 Mathematics Subject Classification]] (which is used by the two major reviewing databases for mathematical articles, [[Mathematical Reviews]] and [[Zentralblatt MATH]]) divides mathematical logic into the following areas:
 
−
* Philosophical and critical (this area has a large overlap with philosophy)
 
−
* General logic (including such fields as [[modal logic]] and [[fuzzy logic]])
 
−
* Model theory
 
−
* Computability and recursion theory
 
−
* Set theory
 
−
* Proof theory and constructive mathematics
 
−
* Algebraic logic (which emphasizes connections to algebra, in particular [[lattice theory]])
 
−
* Nonstandard models (this area has a large overlap with other mathematical fields, such as analysis and measure theory)
 
−
The border lines between these fields, and also between mathematical logic and other fields of mathematics, are not always sharp; for example, [[Gödel's incompleteness theorem]] marks not only a milestone in recursion theory ''and'' proof theory, but has also led to [[Loeb's theorem]] which is important in modal logic.
 
  
−
==Connections with computer science==
+
==Fields of mathematical logic==
−
There are many overlaps with [[computer science]], since many early pioneers in computer science, such as [[Alan Turing]], were mathematicians and logicians.
 
  
−
The study of [[programming language]] [[semantics]]
+
The "Handbook of Mathematical Logic" (1977) divides mathematical logic into four parts: 
−
derives from [[model theory]], as does
 
−
[[program verification]], in particular [[model checking]].
 
  
−
The [[Curry-Howard isomorphism]] between proofs and programs
+
*'''[[Set theory]]''' is the study of [[sets]], which are abstract collections of objects.  The basic concepts of set theory such as [[subset]] and [[relative complement]] are often called '''[[naive set theory]]'''. Modern research is in the area of '''[[axiomatic set theory]]''', which uses logical methods to study which propositions are provable in various formal theories such as [[Zermelo-Frankel set theory|ZFC]] or [[New Foundations|NF]].  
−
relates to [[proof theory]]; [[intuitionistic logic]] and [[linear logic]] are significant here.
 
−
Calculi such as the [[lambda calculus]] and [[combinatory logic]] are nowadays studied mainly as idealized [[programming languages]].
 
  
−
Computer science also contributes to logic by developing techniques for the automatic checking or even finding of proofs, such as [[automated theorem proving]] and [[logic programming]].
+
*'''[[Proof theory]]''' is the study of formal proofs in various logical deduction systems. These proofs are represented as formal mathematical objects, facilitating their analysis by mathematical techniques.  Frege worked on mathematical proofs and formalized the notion of a proof.
  
−
==Some fundamental results==
+
*'''[[Model theory]]''' studies the models of various formal theories.  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.  The method of [[quantifier elimination]] is used to show that models of particular theories cannot be too complicated.
  
−
Some important results are:
+
*'''[[Recursion theory]]''', also called '''computability theory''', studies the properties of [[computable function]]s and the [[Turing degrees]], which divide the uncomputable functions into sets which have the same level of uncomputability.  Recursion theory also includes the study of generalized computability and definability.
  
−
*The set of valid [[first-order logic|first-order]] formulas is [[recursively enumerable]].  This follows from [[Gödel's completeness theorem]] (which establishes the equivalence of validity and provability), because the set of proofs for first-order logic formulas is recursively enumerable ("semi-decidable").  Therefore, there is a procedure that behaves as follows: Given a first-order formula as its input, the procedure eventually halts if the formula is valid, and runs forever otherwise.  Some [[first-order theorem provers]] have this completeness property.
+
The border lines between these fields, and also between mathematical logic and other fields of mathematics, are not always sharp; for example, [[Gödel's incompleteness theorem]] marks not only a milestone in recursion theory ''and'' proof theory, but has also led to [[Loeb's theorem]], which is important in modal logic.  The mathematical field of [[category theory]] uses many formal axiomatic methods resembling those used in mathematical logic, but category theory is not ordinarily considered a subfield of mathematical logic.
  
−
*The set of valid [[first-order logic|first-order]] formulas in a sufficiently rich language is ''not'' recursive, i.e., there is no algorithm for checking for universal validity.  This follows from [[Gödel's incompleteness theorem]].
+
==Connections with computer science==
 +
There are many connections between mathematical logic and [[computer science]]. Many early pioneers in computer science, such as [[Alan Turing]], were also mathematicians and logicians.
 +
 +
The study of [[computability theory (computer science)|computability theory in computer science]] is closely related to the study of computability in mathematical logic.  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.
  
−
*The set of all universally valid [[second-order logic|second-order]] formulas is not even recursively enumerable. This is also a consequence of [[Gödel's incompleteness theorem]].
+
The study of [[programming language]] [[Program semantics|semantics]] is related to [[model theory]], as is
 +
[[program verification]] (in particular, [[model checking]]). The [[Curry-Howard isomorphism]] between proofs and programs relates to [[proof theory]]; [[intuitionistic logic]] and [[linear logic]] are significant here. Calculi such as the [[lambda calculus]] and [[combinatory logic]] are nowadays studied mainly as idealized [[programming languages]].
  
−
*The [[Löwenheim-Skolem theorem]].  One form is: If a set of sentences in a countable language has an infinite model, then it has a model of any infinite cardinality.
+
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]].
  
−
*[[Cut-elimination]] in [[sequent calculus]].
+
==Groundbreaking results==
  
−
*The [[logical independence|independence]] of the [[continuum hypothesis]] with ZFC. The fact that the continuum  hypothesis is consistent with ZFC (if ZFC itself is consistent) was proved by [[Kurt Gödel|Gödel]] in 1940.  The fact that the negation of the continuum hypothesis is consistent with ZFC (if ZFC is consistent) was proved by [[Paul Cohen (mathematician)|Paul Cohen]] in 1963.
+
*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.
 +
*[[Gödel's completeness theorem]] (1929) established the equivalence between semantic and syntactic definitions of logical consequence in first-order logic.
 +
*[[Gödel's incompleteness theorems]] (1931) showed that no sufficiently strong formal system can prove its own consistency.
 +
*The algorithmic unsolvability of the [[Entscheidungsproblem]], established independently by [[Alan Turing]] and [[Alonzo Church]] in 1936, showed that no computer program can be used to correctly decide whether arbitrary mathematical statements are true.
 +
*The [[logical independence|independence]] of the [[continuum hypothesis]] from [[ZFC]] showed that an elementary proof or disproof of this hypothesis is impossible. The fact that the continuum  hypothesis is consistent with ZFC (if ZFC itself is consistent) was proved by [[Kurt Gödel|Gödel]] in 1940.  The fact that the negation of the continuum hypothesis is consistent with ZFC (if ZFC is consistent) was proved by [[Paul Cohen (mathematician)|Paul Cohen]] in 1963.
 +
*The algorithmic unsolvability of [[Hilbert's tenth problem]], established by [[Yuri Matiyasevich]] in 1970, showed that it is not possible for any computer program to correctly decide whether multivariate polynomials with integer coefficients have any integer roots.  
  
−
==Technical reference==
+
<!-- to do: add earlier results —>
−
{{main|First-order logic}}
 
−
<!--''This section is '''not''' intended as a crash course in mathematical logic. There is no doubt that the bare display of concise definitions is very far from an adequate encyclopedical presentation, but sections with more amenable paragraphs shall follow soon... Likewise, the several topics will be pertinently separated as soon as it makes sense, and when and where it is found a proper place.''—>
 
  
−
===First-order languages and structures===
+
<!--
 +
*Gentzen's [[Cut-elimination]] in [[sequent calculus]].
 +
—>
  
−
<div id="Definition:FirstOrderLanguage" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
+
== See also ==
−
'''Definition.''' A '''first-order language''' <math>\mathfrak{L}\,</math> is a collection of distinct typographical symbols classified as follows:
+
* [[Theorem]]
−
 
+
* [[List of mathematical logic topics]]
−
# The '''equality symbol''' <math>=\,</math>; the '''connectives''' <math>\lor\,</math>, <math>\lnot\,</math>; the '''universal quantifier''' <math>\forall\,</math> and the '''parentheses''' <math>(\,</math>, <math>)\,</math>.
+
* [[List of computability and complexity topics]]
−
# A countable set of '''variable symbols''' <math>\{v_i\}_{i = 0}^\infty\,</math>.
+
* [[List of set theory topics]]
−
# A set of '''constant symbols''' <math>\{c_\alpha\}_{\alpha \in \Alpha}\,</math>.
+
* [[List of first order theories]]
−
# A set of '''function symbols''' <math>\{f_\beta\}_{\beta \in \Beta}\,</math>.
 
−
# A set of '''relation symbols''' <math>\{R_\gamma\}_{\gamma \in \Gamma}\,</math>.
 
−
</div>
 
−
 
 
−
Thus, in order to specify a language, it is often sufficient to specify only the collection of constant symbols, function symbols and relation symbols, since the first set of symbols is standard. The parentheses serve the only purpose of forming groups of symbols, and are not to be formally used when writing down functions and relations in formulas.
 
−
 
 
−
These symbols are just that, ''symbols''. They don't stand for anything. They do not ''mean'' anything.  However, that deviates further into semantics and linguistic issues not useful to the formalization of mathematical language, yet.
 
−
 
 
−
''Yet'', because it will indeed be necessary to get some meaning out of this formalization. The concept of ''model'' over a language provides with such a semantics.
 
−
 
 
−
<div id="Definition:Structure" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' An <math>\mathfrak{L}\,</math>-'''structure''' over the language <math>\mathfrak{L}\,</math>, is a bundle consisting of a nonempty set <math>A\,</math>, the universe of the structure, together with:
 
−
 
 
−
# For each constant symbol <math>c\,</math> from <math>\mathfrak{L}\,</math>, an element <math>c^{\mathfrak{A}} \in A\,</math>.
 
−
# For each <math>n\,</math>-ary function symbol <math>f\,</math> from <math>\mathfrak{L}\,</math>, an <math>n\,</math>-ary function <math>f^{\mathfrak{A}} : A^n \longrightarrow A\,</math>.
 
−
# For each <math>n\,</math>-ary relation symbol <math>R\,</math> from <math>\mathfrak{L}\,</math>, an <math>n\,</math>-ary relation on <math>A\,</math>, that is, a subset <math>R^{\mathfrak{A}} \subseteq A^n\,</math>.
 
−
</div>
 
−
 
 
−
Often, the word ''model'' is used for that of ''structure'' in this context. However, it is important to understand perhaps its motivation, as follows.
 
−
 
 
−
===Terms, formulas and sentences===
 
−
 
 
−
<div id="Definition:Term" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' An <math>\mathfrak{L}\,</math>-'''term''' is a nonempty finite string <math>t\,</math> of symbols from <math>\mathfrak{L}\,</math> such that either
 
−
 
 
−
* <math>t\,</math> is a variable symbol.
 
−
* <math>t\,</math> is a constant symbol.
 
−
* <math>t\,</math> is a string of the form <math>f t_1 ... t_n\,</math> where <math>f\,</math> is an <math>n\,</math>-ary function symbol and <math>t_1\,</math>, ..., <math>t_n\,</math> are terms of <math>\mathfrak{L}\,</math>.
 
−
</div>
 
−
 
 
−
<div id="Definition:Formula" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' An <math>\mathfrak{L}\,</math>-'''formula''' is a nonempty finite string <math>\phi\,</math> of symbols from <math>\mathfrak{L}\,</math> such that either
 
−
 
 
−
* <math>\phi\,</math> is a string of the form <math>t_1 = t_2\,</math> where <math>t_1\,</math> and <math>t_2\,</math> are terms of <math>\mathfrak{L}\,</math>.
 
−
* <math>\phi\,</math> is a string of the form <math>R t_1 ... t_n\,</math> where <math>R\,</math> is an <math>n\,</math>-ary relation symbol and <math>t_1\,</math>, ..., <math>t_n\,</math> are terms of <math>\mathfrak{L}\,</math>.
 
−
* <math>\phi\,</math> is of the form <math>\lnot(\alpha)\,</math> where <math>\alpha\,</math> is an <math>\mathfrak{L}\,</math>-formula.
 
−
* <math>\phi\,</math> is of the form <math>(\alpha \lor \beta)\,</math> where both <math>\alpha\,</math> and <math>\beta\,</math> are <math>\mathfrak{L}\,</math>-formulas.
 
−
* <math>\phi\,</math> is of the form <math>(\forall y)(\alpha)\,</math> where <math>y\,</math> is a variable symbol from <math>\mathfrak{L}\,</math> and <math>\alpha\,</math> is an <math>\mathfrak{L}\,</math>-formula.
 
−
</div>
 
−
 
 
−
<div id="Definition:AtomicFormula" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' An <math>\mathfrak{L}\,</math>-formula that is characterized by either the first or the second clause is called an '''atomic'''.
 
−
</div>
 
−
 
 
−
<div id="Definition:FreeVariable" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>\phi\,</math> be an <math>\mathfrak{L}\,</math>-formula. A variable symbol <math>x\,</math> from <math>\mathfrak{L}\,</math> is said to be '''free''' in <math>\phi\,</math> if either
 
−
 
 
−
* <math>\phi\,</math> is atomic and <math>x\,</math> occurs in <math>\phi\,</math>.
 
−
* <math>\phi\,</math> is of the form <math>\lnot(\alpha)\,</math> and <math>x\,</math> is free in <math>\alpha\,</math>.
 
−
* <math>\phi\,</math> is of the form <math>(\alpha \lor \beta)\,</math> and <math>x\,</math> is free in <math>\alpha\,</math> or <math>\beta\,</math>.
 
−
* <math>\phi\,</math> is of the form <math>(\forall y)(\alpha)\,</math> where <math>x\,</math> and <math>y\,</math> are not the same variable symbols and <math>x\,</math> is free in <math>\alpha\,</math>.
 
−
</div>
 
−
 
 
−
<div id="Definition:Sentence" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' A '''sentence''' is a formula with no free variables.
 
−
</div>
 
−
 
 
−
===Assignment functions===
 
−
 
 
−
Hereafter, <math>\mathfrak{L}\,</math> will denote a first-order language, <math>\mathfrak{A}\,</math> will be an <math>\mathfrak{L}\,</math>-structure with underlying universe set denoted by <math>A\,</math>. Every formula will be understood to be an <math>\mathfrak{L}\,</math>-formula.
 
−
 
 
−
<div id="Definition:VariableAssignmentFunction" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' A '''variable assignment function''' (v.a.f.) into <math>\mathfrak{A}\,</math> is a function from the set of variables of <math>\mathfrak{L}\,</math> into <math>A\,</math>.
 
−
</div>
 
−
 
 
−
<div id="Definition:TermAssignmentFunction" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>s\,</math> be a v.a.f. into <math>\mathfrak{A}\,</math>. We define the '''term assignment function''' (t.a.f.) <math>\overline{s}\,</math>, from the set of <math>\mathfrak{L}\,</math>-terms into <math>A\,</math>, as follows:
 
−
 
 
−
* If <math>t\,</math> is the variable symbol <math>x\,</math>, then <math>\overline{s}(t) = s(x)\,</math>.
 
−
* If <math>t\,</math> is the constant symbol <math>c\,</math>, then <math>\overline{s}(t) = c^{\mathfrak{A}}\,</math>.
 
−
* If <math>t\,</math> is of the form <math>f t_1 ... t_n\,</math>, then <math>\overline{s}(t) = f^{\mathfrak{A}}(\overline{s}(t_1), ..., \overline{s}(t_n))\,</math>.
 
−
</div>
 
−
 
 
−
<div id="Definition:VariableAssignmentFunctionModification" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>s\,</math> be a v.a.f. into <math>\mathfrak{A}\,</math> and suppose that <math>x\,</math> is a variable and that <math>a \in A\,</math>. We define the v.a.f. <math>s[x|a]\,</math>, referred to as an <math>x\,</math>-'''modification of the assignment function''' <math>s\,</math>, by
 
−
 
 
−
<center>
 
−
<math>
 
−
s[x|a](v) = \begin{cases}
 
−
s(v) & \mbox{if } v \ne x \\
 
−
a & \mbox{if } v = x
 
−
\end{cases}
 
−
\,</math>
 
−
</center>
 
−
</div>
 
−
 
 
−
===Logical satisfaction===
 
−
 
 
−
<div id="Definition:Satisfaction" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>\phi\,</math> be formula and suppose <math>s\,</math> is a v.a.f. into <math>\mathfrak{A}\,</math>. We say that <math>\mathfrak{A}\,</math> '''satisfies''' <math>\phi\,</math> '''with assignment''' <math>s\,</math>, and write <math>\mathfrak{A} \models \phi[s]\,</math>, if either:
 
−
 
 
−
* <math>\phi\,</math> is of the form <math>t_1 = t_2\,</math> and <math>\overline{s}(t_1) = \overline{s}(t_2)\,</math>.
 
−
* <math>\phi\,</math> is of the form <math>R t_1 ... t_n\,</math> and <math>(\overline{s}(t_1), ..., \overline{s}(t_n)) \in R^{\mathfrak{A}}\,</math>.
 
−
* <math>\phi\,</math> is of the form <math>\lnot(\alpha)\,</math> and <math>\mathfrak{A}\mbox{ }\not\models\mbox{ }\alpha[s]\,</math>.
 
−
* <math>\phi\,</math> is of the form <math>(\alpha \lor \beta)\,</math> and <math>\mathfrak{A} \models \alpha[s]\,</math> or <math>\mathfrak{A} \models \beta[s]\,</math>.
 
−
* <math>\phi\,</math> is of the form <math>(\forall y)(\alpha)\,</math> and for each element <math>a \in A\,</math>, <math>\mathfrak{A} \models \alpha[s[y|a]]\,</math>.
 
−
</div>
 
−
 
 
−
<div id="Definition:ModelFormula" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>\phi\,</math> be formula and suppose that <math>\mathfrak{A} \models \phi[s]\,</math> for every v.a.f. <math>s\,</math> into <math>\mathfrak{A}\,</math>. Then we say that <math>\mathfrak{A}\,</math> '''models ''' <math>\phi\,</math>, and write <math>\mathfrak{A} \models \phi\,</math>.
 
−
</div>
 
−
 
 
−
<div id="Definition:ModelSetOfFormulas" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>\Phi\,</math> be a set of formulas and suppose that <math>\mathfrak{A} \models \phi\,</math> for every formula <math>\phi \in \Phi\,</math> then we say that <math>\mathfrak{A}\,</math> '''models''' <math>\Phi\,</math>, and write <math>\mathfrak{A} \models \Phi\,</math>.
 
−
</div>
 
−
 
 
−
In the case that <math>\phi\,</math> is a sentence, that is, a formula with no free variables, the existence of a single v.a.f. for which <math>\mathfrak{A} \models \phi[s]\,</math> immediately implies that <math>\mathfrak{A} \models \phi\,</math>.
 
−
 
 
−
<div id="Definition:TruthInStructure" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>\phi\,</math> be a sentence and suppose that <math>\mathfrak{A} \models \phi\,</math>. Then we say that <math>\phi\,</math> is '''true in''' <math>\mathfrak{A}\,</math>.
 
−
</div>
 
−
 
 
−
===Logical implication and truth===
 
−
 
 
−
<div id="Definition:LogicalImplication" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>\Psi\,</math> and <math>\Phi\,</math> be sets of formulas. We say that <math>\Psi\,</math> '''logically implies''' <math>\Phi\,</math>, and write <math>\Psi \models \Phi\,</math>, if for every structure <math>\mathfrak{A}\,</math>, <math>\mathfrak{A} \models \Psi\,</math> implies <math>\mathfrak{A} \models \Phi\,</math>.
 
−
</div>
 
−
 
 
−
As a shortcut, when dealing with singletons, we often write <math>\Psi \models \phi\,</math> instead of <math>\Psi \models \{\phi\}\,</math>.
 
−
 
 
−
<div id="Definition:ValidFormula" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>\phi\,</math> be a formula and suppose that <math>\varnothing \models \phi\,</math>. Then we say that <math>\phi\,</math> is '''universally valid''', or simply valid, and in this case we simply write <math>\models \phi\,</math>.
 
−
</div>
 
−
 
 
−
To say that a formula <math>\phi\,</math> is valid really means that every <math>\mathfrak{L}\,</math>-structure <math>\mathfrak{A}\,</math> models <math>\phi\,</math>.
 
−
 
 
−
<div id="Definition:Truth" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>\phi\,</math> be a sentence and suppose that <math>\models \phi\,</math>. Then we say that <math>\phi\,</math> is '''true'''.
 
−
</div>
 
−
 
 
−
===Variable substitution===
 
−
 
 
−
<div id="Definition:VariableSubstitutionInTerm" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>u\,</math> be a term and suppose <math>x\,</math> is a variable and <math>t\,</math> is another term. We define the term <math>u_t^x\,</math>, read <math>u\,</math> '''with''' <math>x\,</math> '''replaced by''' <math>t\,</math>, as follows:
 
−
 
 
−
* If <math>u\,</math> is the variable symbol <math>x\,</math>, then <math>u_t^x\,</math> is defined to be the term <math>t\,</math>.
 
−
* If <math>u\,</math> is a variable symbol other than <math>x\,</math>, then <math>u_t^x\,</math> is defined to be the term <math>u\,</math>.
 
−
* If <math>u\,</math> is a constant symbol, then <math>u_t^x\,</math> is defined to be the term <math>u\,</math>.
 
−
* If <math>u\,</math> is of the form <math>f t_1 ... t_n\,</math>, then <math>u_t^x\,</math> is defined to be the term <math>f {t_1}_t^x ... {t_n}_t^x\,</math>.
 
−
</div>
 
−
 
 
−
<div id="Definition:VariableSubstitutionInFormula" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>\phi\,</math> be a formula and suppose <math>x\,</math> is a variable and <math>t\,</math> is a term. We define the formula <math>\phi_t^x\,</math>, read <math>\phi\,</math> '''with''' <math>x\,</math> '''replaced by''' <math>t\,</math>, as follows:
 
−
 
 
−
* If <math>\phi\,</math> is of the form <math>t_1 = t_2\,</math>, then <math>\phi_t^x\,</math> is defined to be the formula <math>{t_1}_t^x = {t_2}_t^x\,</math>.
 
−
* If <math>\phi\,</math> is of the form <math>R t_1 ... t_n\,</math>, then <math>\phi_t^x\,</math> is defined to be the formula <math>R {t_1}_t^x, ..., {t_n}_t^x\,</math>.
 
−
* If <math>\phi\,</math> is of the form <math>\lnot(\alpha)\,</math>, then <math>\phi_t^x\,</math> is defined to be the formula <math>\lnot(\alpha_t^x)\,</math>.
 
−
* If <math>\phi\,</math> is of the form <math>(\alpha \lor \beta)\,</math>, then <math>\phi_t^x\,</math> is defined to be the formula <math>(\alpha_t^x \lor \beta_t^x)\,</math>.
 
−
* If <math>\phi\,</math> is of the form <math>(\forall y)(\alpha)\,</math>, then
 
−
** if <math>x\,</math> and <math>y\,</math> are the same variable symbol, <math>\phi_t^x\,</math> is defined to be the formula <math>\phi\,</math>.
 
−
** else, <math>\phi_t^x\,</math> is defined to be the formula <math>(\forall y)(\alpha_t^x)\,</math>.
 
−
</div>
 
−
 
 
−
===Substitutability===
 
−
 
 
−
<div id="Definition:Substitutability" style="border-left: 3px double #CCCCCC; padding-left: 5px; ">
 
−
'''Definition.''' Let <math>\phi\,</math> be a formula and suppose <math>x\,</math> is a variable and <math>t\,</math> is a term. We say that <math>t\,</math> '''is substitutable for''' <math>x\,</math> '''in''' <math>\phi\,</math>, if either:
 
−
 
 
−
* <math>\phi\,</math> is [[atomic formula|atomic.]]
 
−
* <math>\phi\,</math> is of the form <math>\lnot(\alpha)\,</math> and <math>t\,</math> is substitutable for <math>x\,</math> in <math>\alpha\,</math>.
 
−
* <math>\phi\,</math> is of the form <math>(\alpha \lor \beta)\,</math> and <math>t\,</math> is substitutable for <math>x\,</math> in both <math>\alpha\,</math> and <math>\beta\,</math>.
 
−
* <math>\phi\,</math> is of the form <math>(\forall y)(\alpha)\,</math> and either
 
−
** <math>x\,</math> is not a free variable in <math>\phi\,</math>.
 
−
** <math>y\,</math> does not occur in <math>t\,</math> and <math>t\,</math> is substitutable for <math>x\,</math> in <math>\alpha\,</math>.
 
−
</div>
 
  
−
The notion of substitutability of terms for variables corresponds to that of the preservation of truth after substitution is carried out in terms or formulas. Strictly speaking, substitution is always allowed, but substitutability will be imperative in order to yield a formula which meaning was not deformed by the substitution.
+
==Further Reading==
−
 
+
*The [http://www.ucl.ac.uk/philosophy/LPSG/ London Philosophy Study Guide] offers many suggestions on what to read, depending on the student's familiarity with the subject:
−
==References==
+
**[http://www.ucl.ac.uk/philosophy/LPSG/MathLogic.htm Mathematical Logic]
−
* [[George Boolos]], John Burgess, and [[Richard Jeffrey]] (2002) ''Computability and Logic'', 4th ed. Cambridge University Press. ISBN 0521007585.
+
**[http://www.ucl.ac.uk/philosophy/LPSG/SetTheory.htm Set Theory & Further Logic]
−
* Enderton, Herbert (2002) ''A mathematical introduction to logic'', 2nd ed. Academic Press.
+
**[http://www.ucl.ac.uk/philosophy/LPSG/PhilMath.htm Philosophy of Mathematics]
−
* Hamilton, A. G. (1988) ''Logic for Mathematicians'' Cambridge University Press.
 
−
* [[Wilfred Hodges]], 1997. ''A Shorter Model Theory''. Cambridge University Press.
 
−
* Mendelson, Elliott (1997) ''Introduction to Mathematical Logic'', 4th ed. Chapman & Hall.
 
−
* [[A. S. Troelstra]] & H. Schwichtenberg (2000) ''Basic Proof Theory'', 2nd. ed. (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press. ISBN 0521779111.
 
  
 
== External links ==
 
== External links ==
 
* [http://world.logic.at/ Mathematical Logic around the world]
 
* [http://world.logic.at/ Mathematical Logic around the world]
 
* [http://home.swipnet.se/~w-33552/logic/home/index.htm Polyvalued logic]
 
* [http://home.swipnet.se/~w-33552/logic/home/index.htm Polyvalued logic]
 +
* ''[http://www.fecundity.com/logic/ forall x: an introduction to formal logic]'', by P.D. Magnus, is a free textbook.
 
* Detlovs, Vilnis, and Podnieks, Karlis (University of Latvia) ''[http://www.ltn.lv/~podnieks/mlog/ml.htm Introduction to Mathematical Logic.]'' A hyper-textbook.
 
* Detlovs, Vilnis, and Podnieks, Karlis (University of Latvia) ''[http://www.ltn.lv/~podnieks/mlog/ml.htm Introduction to Mathematical Logic.]'' A hyper-textbook.
 
*[[Stanford Encyclopedia of Philosophy]]: [http://plato.stanford.edu/entries/logic-classical/  Classical Logic] — by [[Stewart Shapiro]].
 
*[[Stanford Encyclopedia of Philosophy]]: [http://plato.stanford.edu/entries/logic-classical/  Classical Logic] — by [[Stewart Shapiro]].
  
−
== See also ==
+
==References==
−
* [[List of mathematical logic topics]]  
+
* [[Barwise, Jon]], ed. (1977) ''Handbook of Mathematical Logic'', Amsterdam: North-Holland.
−
*[[Logic]]
+
* [[George Boolos]], John Burgess, and [[Richard Jeffrey]] (2002) ''Computability and Logic'', 4th ed. Cambridge University Press. ISBN 0-521-00758-5.
−
*[[Foundations of mathematics]]
+
* Enderton, Herbert (2002) ''A mathematical introduction to logic'', 2nd ed. Academic Press.
−
*[[Metamathematics]]
+
* Hamilton, A. G. (1988) ''Logic for Mathematicians'' Cambridge University Press.
−
*[[List of Boolean algebra topics ]]
+
* [[Wilfrid Hodges]], 1997. ''A Shorter Model Theory''. Cambridge University Press.
−
* [[List of computability and complexity topics]]
+
* Mendelson, Elliott (1997) ''Introduction to Mathematical Logic'', 4th ed. Chapman & Hall.
−
* [[List of large cardinal properties]]
+
* [[A. S. Troelstra]] & H. Schwichtenberg (2000) ''Basic Proof Theory'', 2nd. ed. (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press. ISBN 0-521-77911-1.
−
*[[consistency]]
 
−
*[[completeness]]
 
−
*[[decidable]]
 
−
*[[Set theory]]
 
−
*[[Axiomatic set theory]]
 
−
*[[List of set theory topics]]
 
−
*[[Category theory]]
 
−
*[[Model Theory]]
 
−
*[[Proof theory]]
 
−
*[[Recursion theory]]
 
−
*[[Algebraic logic]]
 
−
*[[Propositional logic]]
 
−
*[[Predicate logic]]
 
−
*[[First-order logic]]
 
−
*[[List of first order theories]]
 
−
*[[Intuitionistic logic]]
 
−
*[[Infinitary logic]]
 
−
*[[Provability logic]]
 
−
*[[Computability logic]]
 
−
*[[Institution (computer science)|Theory of institutions]]
 
−
*[[Table of mathematical symbols]]
 
−
 
 
−
{{Mathematics-footer}}
 
  
 
[[Category:Philosophy and religion]]
 
[[Category:Philosophy and religion]]
 
[[category:philosophy]]
 
[[category:philosophy]]
  
−
{{credit|64168864}}
+
{{credit|133382752}}

Revision as of 17:18, 28 May 2007

Mathematical logic is a subfield of mathematics. It is often divided into the subfields of model theory, proof theory, set theory and recursion theory. Research in mathematical logic has contributed to, and been motivated by, the study of foundations of mathematics, but mathematical logic also contains areas of pure mathematics not directly related to foundational questions.

One unifying theme in mathematical logic is the study of the expressive power of formal logics and formal proof systems. This power is measured both in terms of what these formal systems are able to prove and in terms of what they are able to define.

Earlier names for mathematical logic were symbolic logic (as opposed to philosophical logic) and metamathematics. The former term is still used (as in the Association for Symbolic Logic), but the latter term is now used for certain aspects of proof theory.

History

Mathematical logic was the name given by Giuseppe Peano to what is also known as symbolic logic. In its classical version, the basic aspects resemble the logic of Aristotle, but written using symbolic notation rather than natural language. Attempts to treat the operations of formal logic in a symbolic or algebraic way were made by some of the more philosophical mathematicians, such as Leibniz and Lambert; but their labors remained little known and isolated. It was George Boole and then Augustus De Morgan, in the middle of the nineteenth century, who presented a systematic mathematical way of regarding logic. The traditional, Aristotelian doctrine of logic was reformed and completed; and out of it developed an adequate instrument for investigating the fundamental concepts of mathematics. It would be misleading to say that the foundational controversies that were alive in the period 1900–1925 have all been settled; but philosophy of mathematics was greatly clarified by the "new" logic.

While the Greek development of logic (see list of topics in logic) put heavy emphasis on forms of arguments, the attitude of current mathematical logic might be summed up as the combinatorial study of content. This covers both the syntactic (for example, sending a string from a formal language to a compiler program to write it as sequence of machine instructions), and the semantic (constructing specific models or whole sets of them, in model theory). This study of mathematics from the outside is known as metamathematics.

Some landmark publications were the Begriffsschrift by Gottlob Frege, Studies in Logic by Charles Peirce, Principia Mathematica by Bertrand Russell and Alfred North Whitehead, and On Formally Undecidable Propositions of Principia Mathematica and Related Systems by Kurt Gödel.

Formal logic

At its core, mathematical logic deals with mathematical concepts expressed using formal logical systems. The system of first-order logic is the most widely studied because of its applicability to foundations of mathematics and because of its desirable properties. Stronger classical logics such as second-order logic or infinitary logic are also studied, along with nonclassical logics such as intuitionistic logic.

Fields of mathematical logic

The "Handbook of Mathematical Logic" (1977) divides mathematical logic into four parts:

  • Set theory is the study of sets, which are abstract collections of objects. The basic concepts of set theory such as subset and relative complement are often called naive set theory. Modern research is in the area of axiomatic set theory, which uses logical methods to study which propositions are provable in various formal theories such as ZFC or NF.
  • Proof theory is the study of formal proofs in various logical deduction systems. These proofs are represented as formal mathematical objects, facilitating their analysis by mathematical techniques. Frege worked on mathematical proofs and formalized the notion of a proof.
  • Model theory studies the models of various formal theories. 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. The method of quantifier elimination is used to show that models of particular theories cannot be too complicated.
  • 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 includes the study of generalized computability and definability.

The border lines between these fields, and also between mathematical logic and other fields of mathematics, are not always sharp; for example, Gödel's incompleteness theorem marks not only a milestone in recursion theory and proof theory, but has also led to Loeb's theorem, which is important in modal logic. The mathematical field of category theory uses many formal axiomatic methods resembling those used in mathematical logic, but category theory is not ordinarily considered a subfield of mathematical logic.

Connections with computer science

There are many connections between mathematical logic and computer science. Many early pioneers in computer science, such as Alan Turing, were also mathematicians and logicians.

The study of computability theory in computer science is closely related to the study of computability in mathematical logic. 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.

The study of programming language semantics is related to model theory, as is program verification (in particular, model checking). The Curry-Howard isomorphism between proofs and programs relates to proof theory; intuitionistic logic and linear logic are significant here. Calculi such as the lambda calculus and combinatory logic are nowadays studied mainly as idealized programming languages.

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.

Groundbreaking results

  • 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.
  • Gödel's completeness theorem (1929) established the equivalence between semantic and syntactic definitions of logical consequence in first-order logic.
  • Gödel's incompleteness theorems (1931) showed that no sufficiently strong formal system can prove its own consistency.
  • The algorithmic unsolvability of the Entscheidungsproblem, established independently by Alan Turing and Alonzo Church in 1936, showed that no computer program can be used to correctly decide whether arbitrary mathematical statements are true.
  • The independence of the continuum hypothesis from ZFC showed that an elementary proof or disproof of this hypothesis is impossible. The fact that the continuum hypothesis is consistent with ZFC (if ZFC itself is consistent) was proved by Gödel in 1940. The fact that the negation of the continuum hypothesis is consistent with ZFC (if ZFC is consistent) was proved by Paul Cohen in 1963.
  • The algorithmic unsolvability of Hilbert's tenth problem, established by Yuri Matiyasevich in 1970, showed that it is not possible for any computer program to correctly decide whether multivariate polynomials with integer coefficients have any integer roots.


See also

  • Theorem
  • List of mathematical logic topics
  • List of computability and complexity topics
  • List of set theory topics
  • List of first order theories

Further Reading

External links

References
ISBN links support NWE through referral fees

  • Barwise, Jon, ed. (1977) Handbook of Mathematical Logic, Amsterdam: North-Holland.
  • George Boolos, John Burgess, and Richard Jeffrey (2002) Computability and Logic, 4th ed. Cambridge University Press. ISBN 0-521-00758-5.
  • Enderton, Herbert (2002) A mathematical introduction to logic, 2nd ed. Academic Press.
  • Hamilton, A. G. (1988) Logic for Mathematicians Cambridge University Press.
  • Wilfrid Hodges, 1997. A Shorter Model Theory. Cambridge University Press.
  • Mendelson, Elliott (1997) Introduction to Mathematical Logic, 4th ed. Chapman & Hall.
  • A. S. Troelstra & H. Schwichtenberg (2000) Basic Proof Theory, 2nd. ed. (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press. ISBN 0-521-77911-1.

Credits

New World Encyclopedia writers and editors rewrote and completed the Wikipedia article in accordance with New World Encyclopedia standards. This article abides by terms of the Creative Commons CC-by-sa 3.0 License (CC-by-sa), which may be used and disseminated with proper attribution. Credit is due under the terms of this license that can reference both the New World Encyclopedia contributors and the selfless volunteer contributors of the Wikimedia Foundation. To cite this article click here for a list of acceptable citing formats.The history of earlier contributions by wikipedians is accessible to researchers here:

The history of this article since it was imported to New World Encyclopedia:

Note: Some restrictions may apply to use of individual images which are separately licensed.

Retrieved from https://www.newworldencyclopedia.org/p/index.php?title=Mathematical_logic&oldid=306097

Content is available under Creative Commons Attribution/Share-Alike License; additional terms may apply. See Terms of Use for details.
Copyright Logo
Powered by MediaWiki