Frege to Russell to OCaml

russell.ml

(* Frege to Russell to OCaml

 * Gottlob Frege was a philosopher, logician, and mathematician who is
 * widely credited as the father of analytic philoshophy.  Around the
 * turn of the century he wanted to put mathematics on a rigorous
 * foundation.  To do so, he invented a programming language called
 * axiomatic predicate logic.  The basic idea is that you can express
 * set theory in this logic.  Since much of math can be described in
 * terms of set theory, it therefore could be expressed in axiomatic
 * predicate logic.  If this small core logic could be shown to
 * be "consistent", the basic correctness criteria of a logic, then
 * Frege would have succeeded.

 * Axiomatic predicate logic is actually just a subset of modern
 * programming languages, like OCaml.  The basic idea is that you
 * have predicates (Boolean valued functions) that you can compose and
 * apply and simple Boolean logic (and, or, not, etc.).  Within this
 * little programming language it's pretty easy (and cool) to see how
 * you code up set operations.

 * A Set is just a predicate that tells you whether a given element is
 * in the set.  Mathematicians might call this an "indicator function"
 * or "characteristic function".  From a programming perspective, it's
 * a neat way to deal with potentially infinite sets.

 * For example, we can define the set of all even integers as: *)

let even = fun x -> x mod 2 = 0

(* If you want to know if a given integer is in this set, you just 
 * apply the predicate: even 5 = false, even 18 = true.

 * Here's the empty set (there are no values that satisfy the
 * predicate): *)

let empty = fun x -> false

(* Here's the set that contains everything: *)

let all = fun x -> true

(* Using this idea, we can build up a library for set theory: *)

(* Given an element x, contsruct a singleton set {x}. *)
let singleton = fun x -> fun y -> x = y

(* Given sets s1 and s2, construct s1 ∪ s2. *)
let union = fun s1 -> fun s2 -> fun x -> s1 x || s2 x

(* Given sets s1 and s2, construct s1 ∩ s2. *)
let intersect = fun s1 -> fun s2 -> fun x -> s1 x && s2 x

(* Given set s1 and s2, construct s1 \ s2. *)
let diff = fun s1 -> fun s2 -> fun x -> s1 x && not (s2 x)

(* Now it's easy to compute different sets of things.  For example, the
 * set of all even integers between 3 and 19 could be define as: *)

let eg1 = intersect even (intersect (fun x -> x >= 3) (fun x -> x <= 19))

(* You can see that 5 is not in the set, nor is 2 or 28, but 4 and 8
 * are: *)

let eg1_5 = eg1 5
let eg1_2 = eg1 2
let eg1_28 = eg1 28
let eg1_4 = eg1 4
let eg1_8 = eg1 8

(* You could define the set of all tweets, short tweets, and bad tweets: *)

let tweet = fun x -> String.length x <= 280
let shorttweet = fun x -> String.length x <= 140
let badtweet = fun x -> diff tweet shorttweet

(* This is essentially what Frege set up as his axiomatic predicate
 * logic.  The only real difference between what Frege created and
 * this OCaml code is that Frege used something more like Scheme than
 * OCaml -- his language didn't have a type system.  But we didn't
 * write down any types here (we let OCaml infer them), so with a
 * superficial change in syntax, you could write this program in
 * Scheme.

 * Frege had published a book exploring these ideas and was getting
 * ready to publish another when, in 1902, his colleague Betrand
 * Russell sent a very kind note with the following curiosity he'd 
 * discovered:

   * There is just one point where I have encountered a
   * difficulty. You state (p. 17 [p. 23 above]) that a function too,
   * can act as the indeterminate element. This I formerly believed,
   * but now this view seems doubtful to me because of the following
   * contradiction. Let w be the predicate: to be a predicate that
   * cannot be predicated of itself. Can w be predicated of itself?
   * From each answer its opposite follows.

 * We can unpack this into modern set notation as the following:
 * Russell is defining a set---it's a weird set (that's why he choose
 * the name "w", "w" is for weird), so buckle up---that is the set of
 * all sets that don't contain themselves: Weird = { x | x ∉ x}.

 * Now the natural question is: does Weird contain itself?  To answer
 * yes implies you must answer no.  To answer no implies yes.  Either
 * way, you're screwed.  This is a logical paradox.

 * We can pose the question exactly as Russell did as an OCaml program: *)

let w = fun x -> not (x x)

(* And then ask the paradoxical question, does w contain itself: w w. *)

(* Now, were this a Scheme program, it would run, but never produce
 * an answer (because any answer would be wrong).  BUT, you'll notice
 * the OCaml compiler will reject this program as being nonsense:

 * File "./russell.ml", line 107, characters 24-25:
 * Error: This expression has type 'a -> 'b
 *        but an expression was expected of type 'a
 *        The type variable 'a occurs inside 'a -> 'b

 * It cannot figure out a type to infer for w.  In other words, there
 * is a type system that rules out these kinds of weird sets that lead
 * to paradoxes.

 * At the time, there were no computers, programming languages, or
 * type systems, but what Russell realized was that Frege made, what
 * today we'd call, a type error.  In fact, Russell invented type
 * theory in order to solve the problem he uncovered in Frege's
 * system. Fast forward a little more than a century and we program in
 * languages like OCaml that use exactly the theory he developed to
 * keep us from writing nonsense programs.

 * See also: https://plato.stanford.edu/entries/type-theory/ and
 * From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931

 * PS Russell showed the house of Frege was built on sand, then set
 * out to fix it.  Subsequently, a logician named Kurt Gödel came
 * along and showed that Russell's fix was an incomplete one.
 * Shockingly, he went further and proved that there can't possibly be
 * a complete solution to the problem Frege, Russell, and others had
 * set out to solve with the foundation of mathematics. *)

Neat! Reminds me of the development William Cook used for his essay about object encapsulation vs. abstract types. He presented this encoding of sets in the lambda calculus, and used it as evidence that lambda calculus was the first OO language. :)