10 ms·

Proofs, Computability, Undecidability, Complexity, and the Lambda Calculus [pdf]

135 points by bmc7505 6y ago

throwaway81523 6y ago
I'm looking at this now. It's a bit idiosyncratic but looks good. It covers standard topics in proof and recursion theory but from a more contemporary approach using natural deduction instead of Hilbert-style proof systems, and it also does complexity theory with various computation models. There are a fair number of exercises and problems, always a good thing. But it covers specialized topics at the expense of some standard ones. For example, I didn't spot any mention of the compactness theorem. So it's hard to call the book a usable general introduction to logic, despite it starting at a relatively beginner level. It's a draft and it has some typos and some long-winded passages that could use editing, but I'm glad it is out there, and it looks to me like a good way for computer people to learn some logic and computability theory if that strikes their fancy. I've only looked at the first couple chapters but the TOC mentions that Girard's polymorphic lambda calculus makes an appearance, so there must be some type theory in there. But, my preference would be to increase the coverage of that even if it means trimming back some of the computability stuff. Another improvement might be to include some coverage and exercises in mechanized proof checking using Coq, in the spirit of Software Foundations (also by authors at Penn, https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ ). Thanks to whoever posted this link!
- harperlee 6y ago
  Could you provide a couple of alternative recommendations in contrast with this? That would be very useful!
  - throwaway81523 6y ago
    Well, it depends on what you are looking for, but the traditional-style book that I'm used to is H. B. Enderton, "A Mathematical Introduction to Logic", and Enderton also has an accompanying book on set theory. I guess I'd suggest those as a companion rather than an alternative to the Gallier and Quaintance book. The G&Q book is imho more modern and more interesting from a CS-oriented perspective. It just leaves out too many important fundamentals. Alternatively, since it is still a work in progress, maybe some of the missing stuff could be added. Boolos and Jeffrey "Logic and Computability", whatever the current edition is, is supposed to be good, but I haven't read it yet. The G&Q book is weird in that it is about interesting topics that I'd consider slightly advanced, but written in a way that assumes almost no background, so if it's the only thing you read, you'll still be missing important background. I'd like a book that uses the G&Q approach but that includes the background. If it kept all the current contents and was expanded, it would probably end up as 2 volumes, which is fine. Or it could leave out some of the specialized stuff, but I think that stuff is there because that was what the authors wanted to write about, so I won't judge ;-).
    - throwaway81523 6y ago
      Can't edit to add this, so will post additional reply of an MO thread with a bunch of other recommendations. I will look into some of them myself. https://mathoverflow.net/questions/44620/undergraduate-logic-textbook https://mathoverflow.net/questions/44620/undergraduate-logic...
benrbray 6y ago
This is but one of many comprehensive texts about mathematics written Jean Gallier and Jocelyn Quaintance! They are all a little unpolished, but still an invaluable resource to students! Here are some more book titles copied from his website: (https://www.cis.upenn.edu/~jean/home.html https://www.cis.upenn.edu/~jean/home.html) * Linear Algebra and Optimization with Applications to Machine Learning (html) * Differential Geometry and Lie Groups (html) * Homology, Cohomology, and Sheaf Cohomology (html) * Proofs, Computability, Undecidability, Complexity, and the Lambda Calculus. An Introduction (pdf) * Aspects of Harmonic Analysis and Representation Theory (html) * Algebra, Topology, Differential Calculus, and Optimization Theory for Computer Science and Machine Learning (html) * Aspects of Convex Geometry Polyhedra, Linear Programming, Shellings, Voronoi Diagrams, Delaunay Triangulations (html) * Notes on Primality Testing and Public Key Cryptography Part 1: Randomized Algorithms Miller-Rabin and Solovay-Strassen Tests (08/2017) (pdf) * Spectral Graph Theory of Unsigned and Signed Graphs Applications to Graph Clustering: A Survey (12/2014) Posted to arXiv as paper cs.CV arXiv:1311.2492 (pdf) * Introduction to discrete probability (12/2014) (pdf)
- throwaway81523 6y ago
  Wow! There is a lot there to read.
- voldacar 6y ago
  Such breadth, you could dedicate a lifetime to learning only one of those topics!
- amelius 6y ago
  I tried to access "Differential Geometry and Lie Groups" but it seems there is only the table of contents.
ProfHewitt 6y ago
Unfortunately, the text by Gallier and Quaintancis is somewhat obsolete because it misses the following developments: * The Church/Turing Thesis is false for reasons outlined here: https://professorhewitt.blogspot.com/2021/03/the-churchturing-thesis-is-false.html https://professorhewitt.blogspot.com/2021/03/the-churchturin... * Gödel failed to prove inferential undecidablity in foundations for reasons outlined here: https://professorhewitt.blogspot.com/2021/03/godel-failed-to-prove-inferential.html https://professorhewitt.blogspot.com/2021/03/godel-failed-to... * That "theorems of an order can be computationally enumerated" is true but unprovable for reasons outlined here: https://professorhewitt.blogspot.com/2021/03/churchs-dilemma-resolved.html https://professorhewitt.blogspot.com/2021/03/churchs-dilemma... However, the text by by Gallier and Quaintancis does provide historical perspective.
- bmc7505 6y ago
  Why is this comment being downvoted?
  - drdeca 6y ago
    Because it is wrong. The comment is claiming that the comment author has overturned well understood results, when they have not done so.
    - ProfHewitt 6y ago
      You are welcome to join the debate! Scientific development proceeds building on previous results as is the case here as shown by references in articles.
  - exdsq 6y ago
    I assume because these are huge claims however they support these claims with their own blog site rather than a peer reviewed journal etc
    - ProfHewitt 6y ago
      The articles are published here: https://papers.ssrn.com/sol3/cf_dev/AbsByAuth.cfm?per_id=2561841 https://papers.ssrn.com/sol3/cf_dev/AbsByAuth.cfm?per_id=256...

135 points by bmc7505 6y ago

I'm looking at this now. It's a bit idiosyncratic but looks good. It covers standard topics in proof and recursion theory but from a more contemporary approach using natural deduction instead of Hilbert-style proof systems, and it also does complexity theory with various computation models. There are a fair number of exercises and problems, always a good thing. But it covers specialized topics at the expense of some standard ones. For example, I didn't spot any mention of the compactness theorem. So it's hard to call the book a usable general introduction to logic, despite it starting at a relatively beginner level. It's a draft and it has some typos and some long-winded passages that could use editing, but I'm glad it is out there, and it looks to me like a good way for computer people to learn some logic and computability theory if that strikes their fancy. I've only looked at the first couple chapters but the TOC mentions that Girard's polymorphic lambda calculus makes an appearance, so there must be some type theory in there. But, my preference would be to increase the coverage of that even if it means trimming back some of the computability stuff. Another improvement might be to include some coverage and exercises in mechanized proof checking using Coq, in the spirit of Software Foundations (also by authors at Penn, https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ ). Thanks to whoever posted this link!

harperlee 6y ago
Could you provide a couple of alternative recommendations in contrast with this? That would be very useful!
- throwaway81523 6y ago
  Well, it depends on what you are looking for, but the traditional-style book that I'm used to is H. B. Enderton, "A Mathematical Introduction to Logic", and Enderton also has an accompanying book on set theory. I guess I'd suggest those as a companion rather than an alternative to the Gallier and Quaintance book. The G&Q book is imho more modern and more interesting from a CS-oriented perspective. It just leaves out too many important fundamentals. Alternatively, since it is still a work in progress, maybe some of the missing stuff could be added. Boolos and Jeffrey "Logic and Computability", whatever the current edition is, is supposed to be good, but I haven't read it yet. The G&Q book is weird in that it is about interesting topics that I'd consider slightly advanced, but written in a way that assumes almost no background, so if it's the only thing you read, you'll still be missing important background. I'd like a book that uses the G&Q approach but that includes the background. If it kept all the current contents and was expanded, it would probably end up as 2 volumes, which is fine. Or it could leave out some of the specialized stuff, but I think that stuff is there because that was what the authors wanted to write about, so I won't judge ;-).
  - throwaway81523 6y ago
    Can't edit to add this, so will post additional reply of an MO thread with a bunch of other recommendations. I will look into some of them myself. https://mathoverflow.net/questions/44620/undergraduate-logic-textbook https://mathoverflow.net/questions/44620/undergraduate-logic...

benrbray 6y ago

This is but one of many comprehensive texts about mathematics written Jean Gallier and Jocelyn Quaintance! They are all a little unpolished, but still an invaluable resource to students! Here are some more book titles copied from his website: (https://www.cis.upenn.edu/~jean/home.html https://www.cis.upenn.edu/~jean/home.html) * Linear Algebra and Optimization with Applications to Machine Learning (html) * Differential Geometry and Lie Groups (html) * Homology, Cohomology, and Sheaf Cohomology (html) * Proofs, Computability, Undecidability, Complexity, and the Lambda Calculus. An Introduction (pdf) * Aspects of Harmonic Analysis and Representation Theory (html) * Algebra, Topology, Differential Calculus, and Optimization Theory for Computer Science and Machine Learning (html) * Aspects of Convex Geometry Polyhedra, Linear Programming, Shellings, Voronoi Diagrams, Delaunay Triangulations (html) * Notes on Primality Testing and Public Key Cryptography Part 1: Randomized Algorithms Miller-Rabin and Solovay-Strassen Tests (08/2017) (pdf) * Spectral Graph Theory of Unsigned and Signed Graphs Applications to Graph Clustering: A Survey (12/2014) Posted to arXiv as paper cs.CV arXiv:1311.2492 (pdf) * Introduction to discrete probability (12/2014) (pdf)

throwaway81523 6y ago
Wow! There is a lot there to read.
voldacar 6y ago
Such breadth, you could dedicate a lifetime to learning only one of those topics!
amelius 6y ago
I tried to access "Differential Geometry and Lie Groups" but it seems there is only the table of contents.

ProfHewitt 6y ago

Unfortunately, the text by Gallier and Quaintancis is somewhat obsolete because it misses the following developments: * The Church/Turing Thesis is false for reasons outlined here: https://professorhewitt.blogspot.com/2021/03/the-churchturing-thesis-is-false.html https://professorhewitt.blogspot.com/2021/03/the-churchturin... * Gödel failed to prove inferential undecidablity in foundations for reasons outlined here: https://professorhewitt.blogspot.com/2021/03/godel-failed-to-prove-inferential.html https://professorhewitt.blogspot.com/2021/03/godel-failed-to... * That "theorems of an order can be computationally enumerated" is true but unprovable for reasons outlined here: https://professorhewitt.blogspot.com/2021/03/churchs-dilemma-resolved.html https://professorhewitt.blogspot.com/2021/03/churchs-dilemma... However, the text by by Gallier and Quaintancis does provide historical perspective.

bmc7505 6y ago
Why is this comment being downvoted?
- drdeca 6y ago
  Because it is wrong. The comment is claiming that the comment author has overturned well understood results, when they have not done so.
  - ProfHewitt 6y ago
    You are welcome to join the debate! Scientific development proceeds building on previous results as is the case here as shown by references in articles.
- exdsq 6y ago
  I assume because these are huge claims however they support these claims with their own blog site rather than a peer reviewed journal etc
  - ProfHewitt 6y ago
    The articles are published here: https://papers.ssrn.com/sol3/cf_dev/AbsByAuth.cfm?per_id=2561841 https://papers.ssrn.com/sol3/cf_dev/AbsByAuth.cfm?per_id=256...