Evolution of Computer Logic: From Axioms to Natural Deduction
Delve into the fascinating pre-history of computer logic, starting from David Hilbert's foundational problems in mathematics to the development of the Dedekind-Peano axioms for natural numbers. Explore Hilbert's finitist consistency program and the evolution of logic systems from Hilbert's axioms to Gerhard Gentzen's Natural Deduction. Witness the invention of proof theory that revolutionized the field of mathematics.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
CONSISTENCY AND AXIOMS Some pre-history of computer logic
HISTORY TIME! According to the course notes, Professor Reis has introduced you all to a bit of the historical context. I want to pick up that story and add some details that I think are interesting!
ONCE UPON A TIME Our story starts in 1900. David Hilbert sets out 23 problems for mathematics to solve. Riemann Hypothesis (still unsolved) 10thproblem: Find an algorithm to determine whether a given polynomial Diophantine equation with integer coefficients has an integer solution. (Solved 1970) 2ndproblem: Prove that the axioms of arithmetic are consistent.
AXIOMS OF ARITHMETIC The (Dedekind-Peano) axioms define the natural numbers {0,1,2,3, } 1. 0 is a natural number 2. If n is a natural number, so is n+1 3. n+1=m+1 implies n=m 4. 0 != n+1 for all natural numbers n 5. Mathematical induction works on natural numbers
HILBERTS FINITIST CONSISTENCY PROGRAM Consistency is a really basic requirement of axiom systems, so the methods of proving consistency should be as basic as possible. Using only finitist mathematics, prove the consistency of arithmetic, axiomatic set theory, axiomatic geometry, etc.
PRINCIPIA MATHEMATICA Hilbert learned logic in the 1910s with the help of Paul Bernays. They studied the giant book Principia Mathematica which was the first thorough formalization of mathematics. Hilbert loved axiomatizing, so he did it for logic!
HILBERT SYSTEMS (some)Axioms for logic Inference rule with restrictions on x
NATURAL DEDUCTION Gerhard Gentzen, a student of Bernays, invents Natural Deduction systems, including the sequent calculi. This logic is more rule-focused and not axiom focused. You can make assumptions (change contexts) in Natural Deduction!
INVENTION OF PROOF THEORY To conquer this field [concerning the foundations of mathematics] we must turn the concept of a specifically mathematical proof itself into an object of investigation, just as the astronomer considers the movement of his position, the physicist studies the theory of his apparatus, and the philosopher criticizes reason itself. David Hilbert, Axiomatische Denken [Axiomatic Thought], 1917
GDELS FIRST INCOMPLETENESS THEOREM! G del proves that the system of Principia Mathematica (PM) is incomplete: In particular, it can be shown that the notions "formula", "proof array", and "provable formula" can be defined in the system PM. [ ] We now construct an undecidable proposition of the system PM, that is, a proposition A for which neither A nor not-A is provable. (G del, 1931) If PM is consistent, then there are formulas it can t prove but also can t refute!
GDEL'S SECOND INCOMPLETENESS THEOREM! Theorem XI: [ ] in particular, the consistency of PM is not provable in PM, provided PM is consistent (in the opposite case, of course, every proposition is provable [in PM]). The entire proof of Theorem XI carries over word for word to the axiom system of set theory, M, and to that of classical mathematics, A, and here, too, it yields the result: There is no consistency proof for M, or for A, that could be formalized in M, or A, respectively, provided M, or A, is consistent.
DEATH OF HILBERTS PROGRAM Not every mathematical question can be answered by a single formal system Weak But proof theory thrives! mathematics can t prove consistency of stronger mathematics
PROOF THEORY We can still say interesting things about consistency! Arithmetic with classical logic is consistent if and only if arithmetic with intuitionistic logic is consistent! Intuitionistic arithmetic is called Heyting arithmetic. Arend Heyting was the original intuitionistic logician!
COMPLETE AXIOM SYSTEMS? Consider the following set Let T be the set of axioms. Then everything true in set theory is provable in a single step! T shows that set theory is complete! ......right?
IS THIS AN AXIOM? What is mathematically wrong with this axiomatization? You can t decide for sure whether something is an axiom or not! In order to say that something is an axiom, you have to know it s true, which would need proof!
HOW MANY AXIOMS? You might think that deciding which formulas are axioms is super easy since we only have finite axioms. But most systems have infinite axioms! They just have finite axiom schemas.
HOW MANY AXIOMS? Here is the formalization of the axioms for the set of natural numbers, where s(n) = n+1 The last axiom schema is a different axiom for each formula!
IS THIS AN AXIOM? How long would it take you to determine whether this was an axiom? You re just checking substitution! Easy peasy (but not always fun )
QUESTION OF THE 1930S What is a mathematically precise way to classify reasonable procedures (functions) of deciding whether a formula is an axiom or not? Church: ?-definability Turing: Turing Machine computable G del: general recursiveness
TRANSLATING EFFECTIVE INTO MATHEMATICS What counts as a reasonable procedure is not a mathematical question. It depends on your abilities and intuitions. Each author is giving a thesis and not a theorem because you can t prove anything about vague concepts like reasonable . Instead you try to replace the vague concept with a mathematical one. It turns out that all three notions include the exact same functions!
FUNCTIONS, IN MY LOGIC? Is the following function Recursive, Turing computable, or ?-definable?
COMPUTERS ON THE HORIZON Computers didn t exist when all this was happening! People did talk about computers, but they were talking about people. The people who did calculations. The original conceptions of computability were geared towards capturing what a person could do.
We may compare a man in the process of computing a real number to a machine which is only capable of a finite number of conditions q1, q2. .... qI. Computing is normally done by writing certain symbols on paper. "We may suppose this paper is divided into squares like a child's arithmetic book. TURING S MACHINE IS A PERSON The behaviour of the computer at any moment is determined by the symbols which he is observing, and his " state of mind " at that moment. (Turing 1937)
Theyre often portrayed as a tape with squares on it, where you write symbols. Turing did not consider 41693 a single symbol because of a human limitation: TURING MACHINES We cannot tell at a glance whether 9999999999999999 and 999999999999999 are the same. (Turing 1937)
EARLY COMPUTERS The first computer, the ABC, wasn t programmable or Turing complete in 1942 6 years after Turing/Godel/Church. The first full computer was the ENAIC in 1945 was Turing complete. We still have Turing s conception of computation even though our computers have gotten so much more powerful.
LOGIC, AT THE BEGINNING OF COMPUTATION G del in 1933: a perfectly precise language has been invented, by which it is possible to express any mathematical proposition by a formula. Some of these formulas are taken as axioms, and then certain rules of inference are laid down which allow one to pass from the axioms to new formulas and thus deduce more and more propositions, the outstanding feature of the rules of inference being that they are purely formal, i.e., refer only to the outward structure of the formulas, not to their meaning, so that they could be applied by someone who knew nothing about mathematics, or by a machine.
