Mindblown: a blog about philosophy.

What more do we know about a theorem if we have a proof (by restricted means) than merely that it is true? That’s an old question of Kreisel’s that motivated his “unwinding program”: extract additional information from proofs of theorems in constructive theories, such as bounds on y in theorems of the form ∀x∃y A(x,…

From my colleague up north, Rob Wilson: The What Sorts of People blog is now up and running: check it out. This is the blog for the What Sorts of People Should There Be? network, a collaborative blog with regular contributions from around 10 team members. Short, recent posts are available on double-amputee Oscar Pistorius’s…

Rob Loftis has a roundup of open access introductory logic textbooks. And Hans von Ditmarsch has a list of logic course software.

It was only a matter of time.

You probably all know the result that Peano Arithmetic is not finitely axiomatizable (a result due to Ryll-Nardzewski), and a similar result for ZFC (due to Richard Montague, I believe). The standard axiom system for PA is not finite since the axiom scheme of induction stands for infinitely many sentences. Ryll-Nardzewski showed that there is…

So the colloquium honoring the recipients of the Gödel Research Fellowships is tomorrow. There should be a live feed. It starts at 9:00 CDT (that’s midnight tonight on the West Coast, and 3 am Eastern). I’ll try to find out if the lectures will be archived.

Erich Reck‘s entry on Richard Dedekind in the SEP is now online. I’m particularly happy about this one: It’s time Dedekind gets some of the attention for his philosophy of math that Frege’s been getting for his, and Erich’s entry as well as his other work, I hope, will help bring that about. While many…

Two more new entries in the Stanford Encyclopedia of interest to logicians: The Development of Proof Theory by Jan von Plato and Non-wellfounded Set Theory by Larry Moss. From Jan’s entry I see that his translation of the interesting third chapter of Genzen’s thesis–wherein Gentzen proved normalization of natural deduction derivations–is out in the next…

I am in favor of

There’s a very laudable enterprise: Blogging on Pseudoscience (at BPSDB.org) aggregates blog posts debunking or pointing out pseudo-scientific nonsense such as Intelligent Design. Lots of good stuff, PZ Meyers is part of it, etc. But, look at the logo they use: Yes, that’s a sequent calculus for linear logic. I know Girard has an idiosyncratic…