Hacker News

a day ago by benrbray

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)

* 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)

19 hours ago by voldacar

Such breadth, you could dedicate a lifetime to learning only one of those topics!

14 hours ago by amelius

I tried to access "Differential Geometry and Lie Groups" but it seems there is only the table of contents.

a day ago by throwaway81523

Wow! There is a lot there to read.

a day ago by throwaway81523

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/ ).

Thanks to whoever posted this link!

8 hours ago by harperlee

Could you provide a couple of alternative recommendations in contrast with this? That would be very useful!

21 hours ago by ProfHewitt

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:


* Gödel failed to prove inferential undecidablity in foundations for reasons outlined here:


* That "theorems of an order can be computationally enumerated" is true but unprovable for reasons outlined here:


However, the text by by Gallier and Quaintancis does provide historical perspective.

19 hours ago by drdeca

Let ◻ be the modal operator "It is provable that", so ◻P means that P is provable.

The first part of your argument in the second link says:[

Suppose that there is a proposition UNP such that UNP ⇔ ¬◻UNP .

Then, suppose that ¬UNP . It then follows that ¬¬◻UNP , i.e. that ◻UNP.

Therefore, ◻◻UNP .

Then, as UNP ⇔ ¬◻UNP, therefore ¬UNP ⇔ ◻UNP.

Then, replace the ◻UNP in ◻◻UNP with ¬UNP, and therefore conclude ◻¬UNP .

So, at this point, we have concluded that ◻¬UNP and also that ◻UNP. So, you can conclude that, __under these assumptions__, that ◻⊥ .

So, under the assumption that there is a statement UNP such that UNP ⇔ ¬◻UNP , and the additional assumption that ¬UNP, you can conclude that ◻⊥.



If a system admits a statement UNP, (and the system is strong enough to do the appropriate reasoning) (and peano arithmetic and such does admit such a statement UNP), then within the system, you can show that ¬UNP implies ◻⊥. I.e. "if the statement that claims it cannot be proven, can be proven, then the system proves a contradiction". This is entirely normal, and does not overturn anything.

However! While the assumption that ¬UNP allows us to derive ◻⊥, it does not allow us to derive ⊥. We have __not__ shown that ¬UNP → ⊥, we have only shown that ¬UNP → ◻⊥. Therefore, this is not justification in appealing to proof by contradiction, and concluding UNP (nor ◻UNP).

7 hours ago by ProfHewitt

Prove I’mUnprovable using proof by contradictions as follows:

    In order to obtain a contradiction, hypothesize   
    ¬I’mUnprovable. Therefore ⊢I’mUnprovable
    (using I’mUnprovable⇔⊬I’mUnprovable).  Consequently, 
    ⊢⊢I’mUnprovable using ByProvabilityOfProofs 
    {⊢∀[Ψ:Proposition<i>] (⊢Ψ)⇒⊢⊢Ψ}. However,
    ⊢¬I’mUnprovable (using I’mUnprovable ⇔⊬I’mUnprovable), 
    which is the desired contradiction in foundations.
Consequently, I’mUnprovable has been proved to be

a theorem using proof by contradiction in which

¬I’mUnprovable is hypothesized and a contradiction derived.

In your notation, the proof shows that following holds:

    ¬I’mUnprovable ⇒ ⊥
Why do you think that the proof is for the following?

    ¬I’mUnprovable ⇒ ⊢⊥

6 hours ago by drdeca

Because ◻P and ◻¬P together imply ◻⊥, not ⊥.

Edit: if you had as an axiom, or could otherwise prove within the system, that ¬◻⊥, I.e. that the system is consistent, then you could conclude from ◻P and ◻¬P that ⊥, by first concluding ◻⊥, and then combining this with ¬◻⊥ .

And in this case, you could indeed say that this is a contradiction, and therefore reject the assumption of ¬UNK, and then conclude UNK without assumptions.

So, if one could show ¬◻⊥ (or if the system had it as an axiom), the reasoning would go through. (This is the thing that is missing.)

Therefore, you could then prove ◻UNK, and therefore ¬UNK, and therefore (having already shown UNK) would have a contradiction, ⊥.

So, this is a way of showing that, if you can show ¬◻⊥ (and if there is a statement UNK), then the system is inconsistent. Which is just one of Gödel’s theorems: a strong system can’t prove its own consistency without being inconsistent.

16 hours ago by bloak

I've not read ProfHewitt's argument, so I'm just looking at your summary.

If ◻P means "P is a proposition that is formally provable within some implicit formal system" (perhaps there should be a subscripted letter to show which formal system because there are an infinite number of them), then I don't understand what ◻◻UNP means, because ◻UNP is not a proposition of the implicit formal system.

6 hours ago by drdeca

If we were doing this in Peano Arithmetic using Gödel numberings, then ◻P would be expression by taking the Gödel number encoding P and applying a predicate that expresses provability to that number. This might be written as like, Provable«P» with the quotes indicating taking the Gödel number of the proposition P, in order to encode it in a way that Peano arithmetic can talk about. (Usually one uses the right angle brackets on the upper corners for the quoting, but my phone doesn’t have that on the keyboard, which is why I’m using “«“ and “»”). Statements like this are statements in the same formal system as P.

The modal logic known as “provability logic” is a nice abstracted system which captures how these things work, and allows for dealing with them in a general case.

◻◻P is perfectly sensible, and if the system is able to describe itself sufficiently well (which is not a high bar; Peano arithmetic satisfies this requirement.) then if you can derive P within the system (without additional assumptions), then, simply by including a proof that the proof of P is a proof of P, one can produce a proof in the system of ◻P, And so, if one can derive ◻P, so too can one derive ◻◻P .

(ProfHewitt’s post also uses basically the same thing as ◻◻P , though he writes it using the turnstile symbol rather than the square symbol, and I prefer the square symbol for it, and the turnstile for something slightly different. Not saying the use of the turnstile for it is wrong though.)

12 hours ago by chriswarbo

> If ◻P means "P is a proposition that is formally provable within some implicit formal system" (perhaps there should be a subscripted letter to show which formal system because there are an infinite number of them)

It doesn't mean that. The formal system is explicit: it's the system we're using to write statements like `◻P` (it's a form of modal logic https://en.wikipedia.org/wiki/Modal_logic ).

7 hours ago by ProfHewitt

Excellent question Bloak!

The proof is for a foundation that can formalize its own

provability. Consequently, ⊢⊢I’mUnprovable means that

⊢I’mUnprovable is provable in the foundation.

17 hours ago by ganafagol

I'm having trouble understanding whether you are

(1) a troll hiding behind Carl Hewitts name using a veil of CS lingo that's just complex enough to appear legit but is actually nonsense, or

(2) actually Carl Hewitt losing his mind with a bunch of nonsense, or

(3) actually Carl Hewitt who is on to something big and the world has just not caught up with you.

To convince us of (3), have your theories been discussed at related conferences and what does the community make of them?

13 hours ago by wildmanx

Carl has a long history of twisting truth and sources.

For example https://www.theguardian.com/technology/2007/dec/09/wikipedia...

Or the discussion page of the wikipedia page about him: https://en.wikipedia.org/wiki/Talk:Carl_Hewitt

Constantly using "Prof" to prefix his name speaks for itself too.

(In other words, it's (2), but that's not a recent development.)

6 hours ago by ProfHewitt

Unfortunately, Wikipedia has a long history of libeling people :-(

It would be great if HN could stick to substantive discussions

and not degrade into personal attacks.

15 hours ago by ivanbakel

Having skimmed through the paper accessible at the end of the first link, I am leaning towards (1). It contains a barrage of eye-assaulting notation, lots of digressions and repetition, and basically no formal substance (which, for a logic/computation paper, is bizarre).

13 hours ago by emmelaich

His WP talk page is a shit-show. I'm leaning towards 2.



(to disclose, I am not qualified to actually judge the arguments)

6 hours ago by ProfHewitt

Sorry that mathematical notation is causing you problems.

How do you see the article lacking in formal substance?

18 hours ago by dandanua

That book doesn't touch any nondeterministic behavior at all. So, the nondeterministic extension of the Church-Turing Thesis is absolutely irrelevant here. Your other cited "developments" seem senseful only in your personal universe.

6 hours ago by ProfHewitt

Nondeterministic Turing Machines are the standard for the Church/Turing Thesis.

Do you have anything substantive to contribute to the discussion?

14 hours ago by arethuza

Yeah - its a long time since I studied this kind of stuff but I'm pretty sure the Church–Turing thesis doesn't say anything about non-determinism or not - being more relevant to complexity than computability?

14 hours ago by dandanua

The original thesis concerns only computable functions, which are deterministic by definition. It doesn't even consider their complexity. There are extended variations of the thesis, though. The complexity variation means that any computable function in one model of computation can have only a polynomial slowdown factor in comparison with another model of computation. It's believed to be false since the raise of quantum computations.

7 hours ago by ProfHewitt

The Church/Turing Thesis is that all computation can be

performed by a nondeterministic Turing Machine.

The Thesis is false because there are digital computations

that cannot be performed by a nondeterministic Turing Machine.

See the following article on how to formalize all of digital


"Physical Indeterminacy in Digital Computation"


3 hours ago by undefined


9 hours ago by jkhdigital

Ignore the downvotes: there is value in reading and attempting to understand some of this material, despite the inflammatory way the claims are made. Carl Hewitt is presumably in his 70s, so I'll forgive him for being an old man who probably doesn't give a shit what people think.

In particular, I find the discussion of "paradox" attacks to be quite illuminating. Bertrand Russell attempted to remove self-referential and self-applicable paradoxes through the embellishments of types and orders. Hewitt argues that Gödel basically "cheated" in his proofs because the Diagonalization Lemma violated restrictions on orders.

I'm not qualified to evaluate that argument on the basis of mathematical reasoning, but I do believe it points to a mismatch between the way computation is modeled in the abstract and the way it happens in reality. In the purely abstract world of natural numbers, there's really only one kind of thing: the natural number. Statements about natural numbers can be represented by natural numbers, statements about statements about natural numbers can also be represented by natural numbers, etc. While a given natural number can be parsed to compute if it is a valid encoding of a proposition of a certain order, it is always and forever a natural number and nothing else.

However, I'm not entirely convinced that this captures the nature of computation in reality. When computation is embodied in a physical system, is it possible that the output of some computation can itself manifest computational properties that are not mere compositions of the lower level computational model? Where the interactions between the "higher level" objects simply follow a different set of rules and thus form the foundation of a new formalism?

The notion of types seems to be a way to capture this, by introducing the possibility of distinguishing a "thing" from its abstract representation or description. If everything exists only within the world of the abstract representation, then a thing is indeed no different from its description, as any manipulation of the thing is equivalent to some manipulation of its description. But when the thing is, in fact, a physical object, it is clear that construction of the thing can fundamentally alter the model of computation. Why is this?

I suspect that it is because there are no "pure" or "inert" abstractions in the real world; everything is in fact performing computation all the time. So physical constructions are not just compositions of objects, but also compositions of the computational capabilities of those objects. I realize this probably sounds like navel-gazing at this point, but sometimes that can be a useful activity.

7 hours ago by ProfHewitt

Thanks for your interesting ideas!

My main purpose is to educate. So I am pleased that you got something out of the article :-)

Daily digest email

Get a daily email with the the top stories from Hacker News. No spam, unsubscribe at any time.