Fuzzy Logic and Inuitionistic Logic

I recently got rid of a pop science book on fuzzy logic that I purchased about eight years ago. When I first read it, it seemed to me to be not all that interesting, since it didn't seem like it created any particularly new ways of thinking about things. After all, calling someone "tall" is just shorthand, and it's not exactly revolutionary to call someone "somewhat tall" or "48% tall", since we can do that already when we talk about any continuous domain.

I put the book aside and figured that I either didn't get it, I had picked a bad explanation, or it truly was not something I would be interested in.

It occurs to me now that the idea of indeterminate truth should be very interesting to me, since I'm interested in intuitionistic logic, especially where provability differs from truth. The Stanford Encyclopedia of Philosophy indicates that the fuzzy logic I was thinking of is the "broad sense" or "fuzzy control", and that there's a whole other sense of fuzzy logic that is more closely related to my interests.

Constructability, Uncountability, and ω-Haskell

My last post about the uncountable ordinals ended up on the programming subreddit, where someone who I think is Lennart Augustsson said:

Wow, I didn't realize you could do this. Now I have to wrap my brain around in what sense you can represent uncountable ordinals in Haskell since there are only a countable number of Haskell programs. It must be something like constructive reals...

I think he's exactly right, and I think it has something to do with V=L, models, and how many functions are definable in Haskell. I'm going out of my comfort zone on this, so please correct me if I make any incorrect or nonsensical statements. I'll use as my example the powerset of the natural numbers, which is certainly uncountable, and already definable in Haskell with

data Nat = Z | S Nat
type Powerset t = t -> Bool

From the viewpoint of ZFC, there are an uncountable number of ZFC functions from the natural numbers to the booleans. From the viewpoint of Haskell, there are an uncountable number of Haskell functions from the natural numbers to the booleans. But, from the world of ZFC, the number of Haskell functions from the natural numbers to the booleans is countable: we can simply order them by their definitions lexicographically. Since every function definable in Haskell has a finite definition and the cardinality of a countable union of finite sets is countable, the function definitions of type Nat -> Bool are countable.

|{f : f <- (N -> 2)_ZFC}| >_ZFC |N|
|{f : f <- (N -> 2)_Haskell}| >_Haskell |N|
|{f : f <- (N -> 2)_Haskell}| =_ZFC Σ_{n <- N} |all n-bit functions from N -> Bool| = |N|

From the viewpoint of Haskell, though, this can't be proven; functions are opaque, so we have no way to order or count them. This might not be true if we use some of the unsafe features of Haskell that would allow us to look at the actual assembly corresponding to a function.

We could, I suppose, imagine a programming language which was not limited to finite-length function definitions. ω-Haskell would not only have types with seemingly uncountable numbers of inhabitants, but each inhabitant would also be definable. Yuk!

Existentials and Zero-Knowledge Proofs

When I use "∃ x . P(x)" in typed programming (using intuitionistic logic), I must have in hand an x and a proof of P(x). This is not the case in the classical logic, in which I might have a proof of ∃ x . P(x) without knowing any details of x at all.

This idea that I know such an x exists though I have no knowledge of it reminds me of zero-knowledge proofs. Of course, the zero-knowledge proofs referenced in the Wikipedia article aren't so much proofs as they are assurances with high probability. I looked around for zero-knowledge proofs that were more proof-like, but I didn't find much. I wonder if there is any deeper connection between classical existentials and zero-knowledge proofs?

Countable Ordinals in Haskell

In Haskell: What happens when you divide infinity by 2?, Eric Kidd asks:

...
2. Is it possible to represent any other (more interesting and/or more correct) definitions of infinity in Haskell?
3. What’s the best way to think about the infinite ordinals?

The code below is my answer to those questions for countable ordinals only. I'm not sure if it makes sense to talk about representing uncoutable sets on the kind of computers we have now: We can talk about infinite countable sets as computable limits of finite objects, but what would an uncountable set look like? They can't be objects of Nat -> Bool, since every object of this type is represented in some finite number of bits. It seems like we are stuck in a universe where Goedel's V=L is true.

{-# OPTIONS_GHC -fglasgow-exts #-}

{- See:
  http://en.wikipedia.org/wiki/Ordinal_arithmetic
  http://en.wikipedia.org/wiki/Large_countable_ordinals

  To add later:
  http://citeseer.ist.psu.edu/487179.html
-}


module Countable where

data Finite = Z
           | S !Finite

{- A countable ordinal is 0, a successor, or a limit of a countable
  sequence. This definition is weak, as the countable sequence should
  be strictly increasing, but that's hard to express. One way to do so
  would be to interpret (Limit f) as the limit of
  (sum i = 0 to n) (1 + f i). Note: this addition is not commutative.
  This would complicate things, however, so I'll leave it for a later
  extension.
-}
data Ordinal = Zero
            | Succ !Ordinal
            | Limit (Finite -> Ordinal) deriving (Show)

{- I believe that there is no computable Eq or Ord instance for Ordinals.
  Comments?
 
  We make an approximation here by taking the nth value of the limit.
  This calculation is very slow, and, of course, will equate a lot of
  ordinals that are not actually equal.
-}

nth :: Ordinal -> Finite -> Integer
nth Zero _ = 0
nth (Succ x) n = 1+(nth x n)
nth (Limit f) n = nth (f n) n

instance Show (Finite -> Ordinal) where
   show f = show [f Z,
                  f (S Z),
                  f (S (S Z)),
                  f (S (S (S Z)))]

instance Eq Ordinal where
   x == y = (show x) == (show y)

{- The basic ordinal arithmetic. Addition and multiplication are not
  commutative.
-}
addOrdinal :: Ordinal -> Ordinal -> Ordinal
addOrdinal x Zero = x
addOrdinal x (Succ y) = Succ (addOrdinal x y)
addOrdinal x (Limit y) = Limit (\z -> addOrdinal x (y z))

multiplyOrdinal :: Ordinal -> Ordinal -> Ordinal
multiplyOrdinal x Zero = Zero
multiplyOrdinal x (Succ y) = addOrdinal (multiplyOrdinal x y) x
multiplyOrdinal x (Limit y) = Limit (\z -> multiplyOrdinal x (y z))

expOrdinal :: Ordinal -> Ordinal -> Ordinal
expOrdinal x Zero = Succ Zero
expOrdinal x (Succ y) = multiplyOrdinal (expOrdinal x y) x
expOrdinal x (Limit y) = Limit (\z -> expOrdinal x (y z))

-- The first infinite ordinal
finite :: Finite -> Ordinal
finite Z = Zero
finite (S x) = Succ (finite x)

omega = Limit finite

-- Apply a f some number of times, starting at z
apply Zero f z = z
apply (Succ n) f z = f (apply n f z)
apply (Limit g) f z = Limit (\x -> apply (g x) f z)

-- With apply, we have more succinct definitions of arithmetic
addOrdinal' x y = apply y Succ x
multiplyOrdinal' x y = apply y (flip addOrdinal x) Zero
expOrdinal' x y = apply y (flip multiplyOrdinal x) (Succ Zero)

-- Enumerates the fixed points of a function.
fix Zero f = apply omega f Zero
fix (Succ n) f = apply omega f (Succ (fix n f))
fix (Limit g) f = Limit (\x -> fix (g x) f)

-- Some larger ordinals:
epsilon n = fix n (expOrdinal omega)

-- The Veblen heirarchy:
veblen Zero b = expOrdinal omega b
veblen (Succ a) b = fix b (veblen a)
veblen (Limit a) b = Limit (\x -> veblen (a x) b)

-- Feferman-Schutte ordinals
gamma n = fix n (flip veblen Zero)

Non-constructive Proofs and Programming

Two excellent examples of programming with non-constructive proofs are given in Simplifying Programs Extracted from Classical Proofs by Yevgeniy Makarov. The examples they give are better than the immediate example I think of: the proof that there are some two irrational numbers x and y such that x^y is rational. This proof is simple to do, but requires some heavy background machinery for rational and irrational numbers. Perhaps I could code this proof by using _|_ for the theorems about rational numbers that I know to be true, but don't wish to prove.

The other two examples of simple non-constructive proofs that I think of are the irrationality of the square root of 2 and the infinitude of the primes. Of course, those are usually stated in non-constructive ways, but they are actually constructive with only a slight bit of tweaking. I haven't read enough of the Makarov paper to see if the simplifications proposed would turn these non-constructive proofs into constructive ones.

Non-constructive Proofs and Productivity

Languages in the Dependent ML family allow users to ensure termination by using a termination metric, a number that is strictly decreasing on recursive calls in the definition of the function.

There is a counterpart to termination for co-recursive structures, where we need to show that a function produces values indefinitely. So, for the Collatz conjecture, we want to show termination for:

collatz n = collatz' n []
collatz' 1 r = 1:r
collatz' n r =
    if n `mod` 2 == 0
    then collatz' (n `div` 2) (n:r)
    else collatz' (3*n + 1) (n:r)

But for the twin prime conjecture we want to show the productivity of:

data Stream a = Stream a (Stream a)
twins = twins' 3
twins' n =
    if (primep n) && (primep (n+2))
    then Stream (n,n+2) (twins' (n+2))
    else twins (n+2)

I don't know if any of the members of the DML family can check productivity. Imagine they could, and imagine we had a non-constructive proof of the twin primes conjecture. Could we use that proof to allow a definition of twins to be marked productive?

Most of the time, we talk about the Curry-Howard correspondence in reference to intuitionist logic and functional programming, but non-constructive proofs of productivity seem like a good way to be able to use more powerful logic in programming, since they don't have to change the implementation of the function they are attached to.