Lambda the Ultimate

On Wolfram's blog. What is it? Will it be as revolutionary as claimed or will this just be another new kind of science? Reading the blog, it looks like they are banking on (a) a very rich library and (b) a cloud-based but built-in knowledge base akin to what you might get with F# type providers.

Mathematical foundations of Computer Science (CS) require great power as well as extreme rigor because of the requirement that computer systems be able to carry out all reasoning including reasoning about their own reasoning processes. The mathematical foundations of CS have important economic and security consequences.

Following a suggestion of [Scott 1967], mathematical foundations for Computer Science (CS) should be built on *both* types *and* sets:
* “there is only one satisfactory way of avoiding the paradoxes: namely, the use of some form of the theory of types... the best way to regard Zermelo's theory is as a simplification and extension of Russell's ...simple theory of types. Now Russell made his types explicit in his notation and Zermelo left them implicit. It is a mistake to leave something so important invisible...”
* “As long as an idealistic manner of speaking about abstract objects is popular in mathematics, people will speak about collections of objects, and then collections of collections of ... of collections. In other words set theory is inevitable.” [emphasis in original]

A natural way to proceed is to construct sets from characteristic functions by composing function spaces on ℕ (as axiomatised by Dedekind/Peano). Proceeding in this way, every set has finite rank. (The foundations of CS don’t seem to need the higher cardinals.
However, theories of higher cardinals can be axiomatised in the foundations.) Sets in the foundations are categorical in the type Sets◅ℕ▻, which is not a set (meaning that sets have been automatized up to isomorphism with a unique isomorphism). Categoricity is important for computer systems that reason model theoretically in order to avoid security holes. See “Formalizing common sense for scalable inconsistency-robust information integration” at Formalizing Common Sense.

Computer Science needs strong foundations that go far beyond the capabilities of first-order logic. For example, that a computer server provides service(i.e. ∃[i∈ℕ]→ ResponseBefore[i]) in the Actor Model) cannot be proved in a first-order theory.
Proof: In order to obtain a contradiction,suppose that it is possible to prove the theorem that computer server provides service (∃[i∈ℕ]→ ResponseBefore[i]) in a first-order theory T. Therefore the following infinite set of sentences is inconsistent: {⌈¬ResponseBefore[i]⌉|i∈ℕ}. By the compactness theorem of first-order logic, it follows that there is finite subset of the set of sentences that is inconsistent. But this is a contradiction, because all the finite subsets are consistent since the amount of time before a server responds is unbounded
∄[i∈ℕ]→ ⊢_T ResponseBefore[i]).

For further discussion, see “What is Computation? Actor Model versus Turing’s Model”.

Let Peano be the Peano/Dedekind theory of the natural numbers with the following strong induction axiom:
∀[P:Boolean^ℕ]→ Inductive[P]⇨∀[i∈ℕ]→ P[i]
where Inductive[P]⇔P[0]∧∀[i∈ℕ]→ P[i]⇨P[i+1]

Of course, there are inferentially undecidable propositions Ψ such that
⊬_PeanoΨ, ⊬_Peano¬Ψ, and ⊨_ℕΨ. But this is not fundamental defect of the theory Peano (regardless that ℕ is the categorical model of Peano) because in practice, proving ⊨_ℕΦ requires proving ⊢_Peano Φ.

The exact nature of the inferentially undecidable propositions of Peano is currently a matter of great controversy. See “Mathematics Self Proves its own Consistency”.