现代数学的发端
2019-08-01 08:08:29
  • 0
  • 1
  • 0

现代数学的发端

  附件1代表现代数学发展观;附件2代表了传统数学发展观。

   希尔伯特计划就是现代数学的发端。希尔伯特是数学形式化的开山鼻祖。

袁萌 陈启 81

附件1

Hilbert's program

In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early part of the 20th century, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies. As a solution, Hilbert proposed to ground all existing theories to a finite, complete set of axioms, and provide a proof that these axioms were consistent. Hilbert proposed that the consistency of more complicated systems, such as real analysis, could be proven in terms of simpler systems. Ultimately, the consistency of all of mathematics could be reduced to basic arithmetic.

Gödel's incompleteness theorems, published in 1931, showed that Hilbert's program was unattainable for key areas of mathematics. In his first theorem, Gödel showed that any consistent system with a computable set of axioms which is capable of expressing arithmetic can never be complete: it is possible to construct a statement that can be shown to be true, but that cannot be derived from the formal rules of the system. In his second theorem, he showed that such a system could not prove its own consistency, so it certainly cannot be used to prove the consistency of anything stronger with certainty. This refuted Hilbert's assumption that a finitistic system could be used to prove the consistency of itself, and therefore anything else.

 

Contents

1 Statement of Hilbert's program

2 ödel's incompleteness theorems

3 ilbert's program after Gödel

4 ee also

5 eferences

6  ternal link

Statement of Hilbert's program

The main goal of Hilbert's program was to provide secure foundations for all mathematics. In particular this should include:

A formulation of all mathematics; in other words all mathematical statements should be written in a precise formal language, and manipulated according to well defined rules.

Completeness: a proof that all true mathematical statements can be proved in the formalism.

Consistency: a proof that no contradiction can be obtained in the formalism of mathematics. This consistency proof should preferably use only "finitistic" reasoning about finite mathematical objects.

Conservation: a proof that any result about "real objects" obtained using reasoning about "ideal objects" (such as uncountable sets) can be proved without using ideal objects.

Decidability: there should be an algorithm for deciding the truth or falsity of any mathematical statement.

Gödel's incompleteness theorems[edit]

Main article: Gödel's incompleteness theorems

Kurt Gödel showed that most of the goals of Hilbert's program were impossible to achieve, at least if interpreted in the most obvious way. Gödel's second incompleteness theorem shows that any consistent theory powerful enough to encode addition and multiplication of integers cannot prove its own consistency. This presents a challenge to Hilbert's program:

It is not possible to formalize all mathematical true statements within a formal system, as any attempt at such a formalism will omit some true mathematical statements. There is no complete, consistent extension of even Peano arithmetic based on a recursively enumerable set of axioms.

A theory such as Peano arithmetic cannot even prove its own consistency, so a restricted "finitistic" subset of it certainly cannot prove the consistency of more powerful theories such as set theory.

There is no algorithm to decide the truth (or provability) of statements in any consistent extension of Peano arithmetic. Strictly speaking, this negative solution to the Entscheidungsproblem appeared a few years after Gödel's theorem, because at the time the notion of an algorithm had not been precisely defined.

Hilbert's program after Gödel[edit]

Many current lines of research in mathematical logic, such as proof theory and reverse mathematics, can be viewed as natural continuations of Hilbert's original program. Much of it can be salvaged by changing its goals slightly (Zach 2005), and with the following modifications some of it was successfully completed:

Although it is not possible to formalize all mathematics, it is possible to formalize essentially all the mathematics that anyone uses. In particular Zermelo–Fraenkel set theory, combined with first-order logic, gives a satisfactory and generally accepted formalism for almost all current mathematics.

Although it is not possible to prove completeness for systems at least as powerful as Peano arithmetic (at least if they have a computable set of axioms), it is possible to prove forms of completeness for many other interesting systems. The first big success was by Gödel himself (before he proved the incompleteness theorems) who proved the completeness theorem for first-order logic, showing that any logical consequence of a series of axioms is provable. An example of a non-trivial theory for which completeness has been proved is the theory of algebraically closed fields of given characteristic.

The question of whether there are finitary consistency proofs of strong theories is difficult to answer, mainly because there is no generally accepted definition of a "finitary proof". Most mathematicians in proof theory seem to regard finitary mathematics as being contained in Peano arithmetic, and in this case it is not possible to give finitary proofs of reasonably strong theories. On the other hand, Gödel himself suggested the possibility of giving finitary consistency proofs using finitary methods that cannot be formalized in Peano arithmetic, so he seems to have had a more liberal view of what finitary methods might be allowed. A few years later, Gentzen gave a consistency proof for Peano arithmetic. The only part of this proof that was not clearly finitary was a certain transfinite induction up to the ordinal ε0. If this transfinite induction is accepted as a finitary method, then one can assert that there is a finitary proof of the consistency of Peano arithmetic. More powerful subsets of second order arithmetic have been given consistency proofs by Gaisi Takeuti and others, and one can again debate about exactly how finitary or constructive these proofs are. (The theories that have been proved consistent by these methods are quite strong, and include most "ordinary" mathematics.)

Although there is no algorithm for deciding the truth of statements in Peano arithmetic, there are many interesting and non-trivial theories for which such algorithms have been found. For example, Tarski found an algorithm that can decide the truth of any statement in analytic geometry (more precisely, he proved that the theory of real closed fields is decidable). Given the Cantor–Dedekind axiom, this algorithm can be regarded as an algorithm to decide the truth of any statement in Euclidean geometry. This is substantial as few people would consider Euclidean geometry a trivial theory.

See also[edit]

Grundlagen der Mathematik

Foundational crisis of mathematics

Atomism

References[edit]

G. Gentzen, 1936/1969. Die Widerspruchfreiheit der reinen Zahlentheorie. Mathematische Annalen 112:493–565. Translated as 'The consistency of arithmetic', in The collected papers of Gerhard Gentzen, M. E. Szabo (ed.), 1969.

D. Hilbert. 'Die Grundlagen Der Elementaren Zahlentheorie'. Mathematische Annalen 104:485–94. Translated by W. Ewald as 'The Grounding of Elementary Number Theory', pp. 266–273 in Mancosu (ed., 1998) From Brouwer to Hilbert: The debate on the foundations of mathematics in the 1920s, Oxford University Press. New York.

S.G. Simpson, 1988. Partial realizations of Hilbert's program. Journal of Symbolic Logic 53:349–363.

R. Zach, 2006. Hilbert's Program Then and Now. Philosophy of Logic 5:411–447, arXiv:math/0508572 [math.LO].

External links[edit]

Entry on Hilbert's program by Richard Zach at the Stanford Encyclopedia of Philosophy.

 

hide

vte

Computable knowledge

Topics and

concepts

Alphabet of human thoughtAuthority controlAutomated reasoningCommonsense knowledgeCommonsense reasoningComputabilityFormal systemInference engineKnowledge baseKnowledge-based systemsKnowledge engineeringKnowledge extractionKnowledge representationKnowledge retrievalLibrary classificationLogic programmingOntologyPersonal knowledge baseQuestion answeringSemantic reasoner

Proposals and

implementations

ZairjaArs Magna (1300)An Essay towards a Real Character, and a Philosophical Language (1688)Calculus ratiocinator and characteristica universalis (1700)Dewey Decimal Classification (1876)Begriffsschrift (1879)Mundaneum (1910)Logical atomism (1918)Tractatus Logico-Philosophicus (1921)Hilbert's program (1920s)Incompleteness theorem (1931)World Brain (1938)Memex (1945)General Problem Solver (1959)Prolog (1972)Cyc (1984)Semantic Web (2001)Evi (2007)Wolfram Alpha (2009)Watson (2011)Siri (2011)Knowledge Graph (2012)Wikidata (2012)Cortana (2014)Viv (2016)

In fiction

The Engine (Gulliver's Travels, 1726)Joe ("A Logic Named Joe", 1946)The Librarian (Snow Crash, 1992)Dr. Know (A.I. Artificial Intelligence, 2001)Waterhouse (The Baroque Cycle, 2003)

See also: Logic machines in fiction and List of fictional computers

Categories: Mathematical logicProof theoryHilbert's problems

 

Navigation menu

Not logged in

Talk

Contributions

Create account

Log in

Article

Talk

 

 

More

Search

 

 

Main page

Contents

Featured content

Current events

Random article

Donate to Wikipedia

Wikipedia store

Interaction

Help

About Wikipedia

Community portal

Recent changes

Contact page

Tools

What links here

Related changes

Upload file

Special pages

Permanent link

Page information

Wikidata item

Cite this page

Print/export

Create a book

Download as PDF

Printable version

 

Languages

Deutsch

Español

Français

Bahasa Indonesia

日本語

Português

Русский

中文

7 more

Edit links

This page was last edited on 3 May 2019, at 06:26 (UTC).

Text is available under the Creative Commons Attribution-ShareAlike License; additional terms may apply. By using this site, you agree to the Terms of Use and Privacy Policy. Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc., a non-profit organization.

Privacy policy

About Wikipedia

Disclaimers

Contact Wikipedia

Developers

Cookie statement

Mobile view

 附件2:“作业帮”的看法

《普通高中数学课程标准》指出:“形式化是数学的基本特征之一.在数学教学中,学习形式化的表达是一项基本要求,但是不能只限于形式化的表述,要强调对数学本质的认识,否则会将生动活泼的数学思维活动淹没在形式化的海洋里.数学的现代发展也表明,全盘形式化是不可能的.因此,高中数学课程应该返璞归真,努力揭示数学概念、法则、结论的发展过程的本质.

所谓“数学形式”,就是用特定的数学语言,包括数学的符号语言、图象语言和文字语言,表达自然现象和社会现象的空间结构和数量关系,即具有相对固定样式的数学概念、法则、结论,它具有如下特征:

1)稳定性.数学概念、法则、结论等内容一旦成为“形式”,就有相对稳定的特征,决不会因环境、条件的变更而发生变化.

2)概括性.数学形式是无数具体事物经抽象概括的结果,应该是研究数量关系或图形本质属性的反应.

3)简洁性.最简单的往往是最深刻的,越简洁的东西就越具有生命力,越具使用价值.数学形式就以其表述方式的简洁而称道.

4)广泛性.数学形式的概括性决定了它具有广泛性,可真正达到华罗庚教授所说的“数学是一个原则,无数内容,一个方法,到处有用.

5)可操作性.按照相关数学形式进行的程式化操作可称为行为模式.人的行为模式有两种,一种是需要智力投入、思维参与的行为模式;一种是较少需要智力投入、思维参与的行为模式.在数学学习和解决数学问题的所有活动中,创造性思维的含量只占少部分,运用更多的是程式化的操作.这种操作讲究的是熟练、准确、快速、高效.学生大多数解题是按既定法则进行模式化操作.即使是难度较大的需要一定的创造思维,但创造的“根”仍然扎在坚实的基本数学形式的土壤中.基本数学形式是创造的源泉与原型.当然,即便进行的是简单化、机械化、程序化的操作,也要在其中努力加大智力与思维的含量.

形式化有着不可否认的弊端:

1)形式化可能掩盖事物的本质,学生只会机械操作.

2)形式化会轻视过程,只知结论,不知来龙去脉.

3)形式化不利于学生对基础知识和基本能力的记忆及养成,教学中容易出现“开门见山,直达结论”的现象.

4)形式化会使学生产生思维惰性.

对概念、定理、法则和解题技法等若都能达到本质的理解固然很好,但毕竟有些内容要求学生在形式化的基础上形成机械记忆,并能投入操作应用即可.问题的关键是,哪些内容应保留形式,哪些内容需要否定形式,哪些内容需要形式和本质的和谐共处,这些不能靠主观臆断,而要靠我们老师在吃透新课程标准和新教材的基础上科学合理地来确定.一般来讲,数学教学之初,应该充分展示数学知识发生发展的过程,引导学生弄清本质,在熟练的基础上适度形式化,形成自己的技能,这样的知识学得牢固一些,对于大面积提高数学成绩也有帮助.再说行为模式,包括某些解题方法,必须引领学生在解题实践的过程中总结有典型意义的重要形式,且注意思维的参与,使这些行为模式的操作更有效.

 

作业帮用户 2016-12-07

 

 


 
最新文章
相关阅读