Atjaunināt sīkdatņu piekrišanu

Metamathematics, Machines and Gödel's Proof [Mīkstie vāki]

(SRI International, USA)
  • Formāts: Paperback / softback, 220 pages, height x width x depth: 248x175x17 mm, weight: 413 g, 4 Line drawings, unspecified
  • Sērija : Cambridge Tracts in Theoretical Computer Science
  • Izdošanas datums: 30-Jan-1997
  • Izdevniecība: Cambridge University Press
  • ISBN-10: 0521585333
  • ISBN-13: 9780521585330
Citas grāmatas par šo tēmu:
  • Mīkstie vāki
  • Cena: 61,22 €
  • Grāmatu piegādes laiks ir 3-4 nedēļas, ja grāmata ir uz vietas izdevniecības noliktavā. Ja izdevējam nepieciešams publicēt jaunu tirāžu, grāmatas piegāde var aizkavēties.
  • Daudzums:
  • Ielikt grozā
  • Piegādes laiks - 4-6 nedēļas
  • Pievienot vēlmju sarakstam
Metamathematics, Machines and Gödel's ProofPalielināt
  • Formāts: Paperback / softback, 220 pages, height x width x depth: 248x175x17 mm, weight: 413 g, 4 Line drawings, unspecified
  • Sērija : Cambridge Tracts in Theoretical Computer Science
  • Izdošanas datums: 30-Jan-1997
  • Izdevniecība: Cambridge University Press
  • ISBN-10: 0521585333
  • ISBN-13: 9780521585330
Citas grāmatas par šo tēmu:
Permanent link: https://www.kriso.lv/db/9780521585330.html
Keywords:
Mathematicians from Leibniz to Hilbert have sought to mechanise the verification of mathematical proofs. Developments arising out of Gödel's proof of his incompleteness theorem showed that no computer program could automatically prove true all the theorems of mathematics. In practice, however, there are a number of sophisticated automated reasoning programs that are quite effective at checking mathematical proofs. Now in paperback, this book describes the use of a computer program to check the proofs of several celebrated theorems in metamathematics including Gödel's incompleteness theorem and the ChurchRosser theorem. The computer verification using the BoyerMoore theorem prover yields precise and rigorous proofs of these difficult theorems. It also demonstrates the range and power of automated proof checking technology. The mechanisation of metamathematics itself has important implications for automated reasoning since metatheorems can be applied by labour-saving devices to simplify proof construction. The book should be accessible to scientists and philosophers with some knowledge of logic and computing.

Papildus informācija

Describes the use of computer programs to check several proofs in the foundations of mathematics.
Preface xi
1 Introduction
1(34)
1.1 Background
3(18)
1.1.1 The Paradoxes
4(1)
1.1.2 Foundations of Mathematics
5(1)
1.1.3 Language and Metalanguage
6(1)
1.1.4 Logic
7(4)
1.1.5 Peano Arithmetic
11(1)
1.1.6 Set Theory
11(2)
1.1.7 Computability
13(1)
1.1.8 Lisp
14(2)
1.1.9 Metamathematics
16(1)
1.1.10 Automatic Proof Checking
17(3)
1.1.11 Why Check Proofs in Metamathematics?
20(1)
1.2 Overview
21(7)
1.2.1 The Rules of the Game
21(1)
1.2.2 Steps to the Incompleteness Theorem
22(1)
1.2.3 Formalizing Z2
22(1)
1.2.4 The Tautology Theorem
23(1)
1.2.5 The Representability Theorem
23(1)
1.2.6 Godel's Incompleteness Theorem
24(2)
1.2.7 The Church-Rosser Theorem
26(2)
1.3 The Boyer--Moore Theorem Prover and its Logic
28(5)
1.3.1 The Boyer-Moore Logic
28(1)
1.3.1.1 The Basic Axioms
29(1)
1.3.1.2 The Shell Principle
29(1)
1.3.1.3 Recursion and Induction
30(1)
1.3.2 The Theorem Prover
30(2)
1.3.2.1 A Sample Proof
32(1)
1.4 Summary
33(2)
2 The Statement of the Incompleteness Theorem
35(36)
2.1 The Metatheoretic Description of Z2
36(32)
2.1.1 The Symbols
36(4)
2.1.2 The Expressions
40(3)
2.1.3 Operations on Expressions
43(5)
2.1.4 The Logical Axioms
48(3)
2.1.5 The Rules of Inference
51(3)
2.1.6 The Set-Theoretic Axioms
54(4)
2.1.7 Admitting Definitions
58(3)
2.1.8 The Proof Checker
61(2)
2.1.9 An Example of a Formal Proof
63(2)
2.1.10 The Function and Predicate Definitions
65(3)
2.2 The Formal Statement of the Incompleteness Theorem
68(1)
2.3 Summary
69(2)
3 Derived Inference Rules
71(20)
3.1 Metamathematical Extensibility
72(1)
3.2 The Informal Proof of the Tautology Theorem
73(2)
3.2.1 A Tautology Checker
73(1)
3.2.2 The Tautology Theorem
74(1)
3.3 The Mechanical Proof of the Tautology Theorem
75(14)
3.3.1 Steps to the Proof of the Tautology Theorem
76(5)
3.3.2 Defining the Tautology Checker
81(2)
3.3.3 The Proof of the Tautology Theorem
83(3)
3.3.4 The Correctness of the Tautology Checker
86(2)
3.3.5 Using the Tautology Theorem
88(1)
3.4 Other Derived Inference Rules
89(1)
3.4.1 The Instantiation Rule
89(1)
3.4.2 The Equivalence Theorem
89(1)
3.4.3 The Equality Theorem
90(1)
3.5 Summary
90(1)
4 The Representability of the Metatheory
91(34)
4.1 A Brief Overview
91(2)
4.2 The Lisp Interpreter
93(5)
4.3 The Godel-Encoding
98(6)
4.3.1 Mapping Z-Expressions to N-Expressions
99(1)
4.3.2 Mapping N-Expressions to Sets
99(5)
4.4 The Representability Theorem
104(16)
4.4.1 Representing the Lisp Primitives
104(7)
4.4.2 Representing the Lisp Interpreter
111(1)
4.4.2.1 Defining the Formula Representing GET
111(1)
4.4.2.2 Constructing the Trace for GET
112(1)
4.4.2.3 The Representability of GET
113(5)
4.4.2.4 The Representability of EV
118(2)
4.5 Computability of the Metatheory
120(4)
4.6 Summary
124(1)
5 The Undecidable Sentence
125(18)
5.1 The Enumeration of Proofs
125(1)
5.2 The Theorem Checker
126(6)
5.3 Construction of the Undecidable Sentence
132(7)
5.4 Analysis
139(2)
5.5 Conclusions
141(2)
6 A Mechanical Proof of the Church-Rosser Theorem
143(40)
6.1 An Introduction to the Lambda Calculus
144(3)
6.1.1 Terms
144(2)
6.1.2 Substitution
146(1)
6.1.3 Alpha-steps and Beta-steps
146(1)
6.2 A Proof-Sketch of the Church-Rosser Theorem
147(5)
6.2.1 The Statement
147(2)
6.2.2 The Diamond Property over Transitive Closures
149(1)
6.2.3 The Definition of Walk
149(1)
6.2.4 The Diamond Property of Walks
150(2)
6.3 Formalizing the Lambda Calculus in Lisp
152(6)
6.4 Using the de Bruijn Notation
158(9)
6.4.1 The de Bruijn Notation
159(2)
6.4.2 Beta-Reduction
161(3)
6.4.3 Definition of a Walk
164(1)
6.4.4 The Statement of the Diamond Property for Walks
165(1)
6.4.5 The Statement of the Church-Rosser Theorem
166(1)
6.5 Highlights of the Mechanical Proof
167(4)
6.5.1 Some Properties of BUMP, SUBST, and WALK
167(1)
6.5.2 The Substitutivity of Walks
168(1)
6.5.3 The Church-Rosser Theorem
169(2)
6.6 A Sample Mechanical Proof
171(8)
6.7 Analysis
179(4)
7 Conclusions
183(13)
7.1 A Critique of the Boyer-Moore Theorem Prover
186(1)
7.2 Summary
187(9)
Bibliography 196