Cammy/Consistency

Is Cammy consistent?

What is consistency?

A logic is consistent if it never proves a statement true and false simultaneously. Immediately, there are several problems with applying this concept directly to Cammy; Cammy does not have logical negation, and categorical logic is always constructive.

If we restrict ourselves to set theory, then a logic over a collection of sets is consistent if it never witnesses an inhabitant of an empty set. This is connected to the first definition by the idea that the only inhabitants of empty sets are falsehoods and contradictions; no valid proof tree will ever indicate that an empty set has any elements. However, this also does not apply to Cammy, because Cammy's types do not include an initial object, and so any set-theoretic model of Cammy will trivially fail to have inconsistencies.

There is a much weaker notion that we can use instead: a logic is consistent if it has a model. Therefore, if we can demonstrate a model for Cammy, then we will have shown that Cammy is -- in some weak sense -- consistent.

A computer-oriented set-theoretic model

Our model will assign a set to every Cammy object. Each set will only contain bitstrings: possibly-infinite sequences of 0 and 1. For sanity, the empty bitstring is also allowed. This collection has the wikipedia:shortlex order; every set is well-ordered. Cammy expressions, which each denote arrows, will be assigned functions. We will use the following sets:

• 0 cannot be denoted, but it would be the empty set
• 1 will be denoted by a singleton set; for levity, we choose the singleton 101010
• 2 will be denoted by the set {0, 1}
• N will be denoted by all finite bitstrings without leading 0s, including the empty bitstring
• F is wholly left as an exercise to the reader, following IEEE 754

We will also build some composite sets. First, pairs. Given sets S and T, their product S × T is the Morton encoding over each pair of elements. To allow for pairing of elements of differing lengths, we will length-prefix every element and zero-pad the shorter element on the right (possibly out to infinity); lengths are written in expanded binary, with 0 mapped to 01, 1 mapped to 11, and terminator mapped to 00. For example, suppose we wish to pair 0 and 01. First, we prefix the lengths 1 and 2 respectively, obtaining the coded lengths 0100 and 110100. Then, we append the elements themselves, obtaining 01000 and 11010001. Finally, we zero-pad and Morton-encode by interleaving the bits, obtaining 01110001000001. We may then project out either element of the pair.

Sums are somewhat easier. Given sets S and T, their sum S + T has elements from S prefixed with 0, and elements from T prefixed with 1. This prefix bit acts as a flag indicating to which side of the union each element belongs.

We'll include lists to make hom-sets easier. Given a set S, its set of finite lists [S] contains length-prefixed sequences of length-prefixed elements concatenated together. For example, the list with two elements, first 0 and then 1, is encoded as 1101001100011001, because 0 is encoded as 11000 and 1 is encoded as 11001. Note that the empty list is therefore encoded as 00.

Finally, given sets S and T, their hom-set [S, T] will rely on the well-ordering of S. A function from S to T merely is a list of elements of T, one for each element of S, but the existence of N means that this list may be infinite. To accommodate this, we extend our length encoding so that the infinite length is mapped to 10.

Now, we can imagine how the various combinators operate on these bitstrings:

• `id` and `comp` map to the identity function and composition of functions
• `ignore` maps to the constant function sending everything to 101010
• `pair` Morton-encodes as described; `fst` and `snd` select the even and odd bits respectively, decoding the length prefixes to strip trailing 0s
• `left` and `right` prefix 0 and 1 respectively; `case` strips the prefix and applies the corresponding function
• `curry` is not easily computable, but can be constructed using set comprehensions
• `uncurry` applies `fst` and `snd`, then applies its corresponding function twice

For Boolean algebra:

• `t` and `f` pick out 1 and 0 respectively
• `not` switches 1 and 0
• The rest are left as a standard exercise to the reader

For natural numbers:

• `zero` picks out the empty bitstring
• `succ` scrolls to the end of the bitstring and applies a binary increment operation, sending the empty bitstring to 1; this is total because every element of N is finite
• `(pr x f)` scrolls to the end of the bitstring, applies `x` to create the return value, then interprets the bitstring as a binary number and applies `f` to the return value that many times

For lists:

• `nil` picks out 00
• `cons` prefixes a list with the given element, incrementing the length and shifting the original contents of the list to the right
• `(fold x f)` scrolls to the end of the list by reading lengths, applies `x` to create the return value, then repeatedly applies `f` with each element, working right-to-left