Prefix-free codes and ordinals

Very nice. I like that the ordinal based construction allows for quite some freedom, while still ensuring that every number can be represented uniquely, and that lexicographically greater codewords map to bigger numbers.

Allowing non-binary digits would provide even more freedom. I guess the only thing which would change in the ordinal based construction is that (2n-1+b) would be replaced by (rn-r+1+d), where d is an r-ary digit. And the encoding of would have to be adapted too.

I wonder what motivated you to write this post. Was it just the obvious motivation to construct a connection between ordinals and natural number representations?

What Immanuel Kant teach you

Consider the problem of representing a number in computer memory, which is idealized as a sequence of zeros and ones. The binary number system is a well-known solution to this problem — for example, the sequence “01101” represents $latex 0 cdot 2^4 + 1 cdot 2^3 + 1 cdot 2^2 + 0 cdot 2^1 + 1 cdot 2^0 = 11$. But there’s a problem: You don’t expect the entire computer to just be used to represent one number; you expect it to have other things stored afterwards. So how do you tell where the number ends? If the sequence begins $latex 01101001dots$ does this represent the number $latex 011_2$ or $latex 01101_2$ or $latex 0110100_2$?

The solution to this problem most commonly used in practice is to declare in advance a fixed number of bits that will be used to represent the number, usually 32 bits or 64 bits. For…

View original post 1,814 more words

Isomorphism of labeled uniqueness trees

The paper Deep Weisfeiler Leman by Martin Grohe, Pascal Schweitzer, Daniel Wiebking introduces a framework that allows the design of purely combinatorial graph isomorphism tests that are more powerful than the well-known Weisfeiler-Leman algorithm. This is a major achievement, see for example the beginning of an email I wrote to Jonathan Gorard (author of the paper Uniqueness Trees: A Possible Polynomial Approach to the Graph Isomorphism Problem) on June 25, 2016:

Dear author,

you recently proposed a purely combinatorial method towards determining isomorphism of graphs, which you called uniqueness trees. For purely combinatorial methods, the most interesting question is how they compare to Weisfeiler-Lehman, and “not being subsumed” by Weisfeiler-Lehman would be considered to be a major achievement, even if the method would not yield a polynomial time algorithm for checking graph isomorphism.

I never received an answer. This is not uncommon, as I wrote in another place:

I sometimes write the authors of such papers my thoughts, but the typical reaction is to totally ignore my email such that I don’t even know whether a spam filter eliminated it before reaching the author, the best reaction is an “thanks for your kind words, I’m used to much more insulting feedback”. Being totally ignored feels bad, but maybe it is an appropriate reaction to “proof refutation”?

But in this post, I want to elaborate another point which I mentioned in that email:

Rooted (colored) trees can be canonically labeled, which allows to use your method for iterative color refinement just like Weisfeiler Lehman. Your uniqueness trees on the other hand are also labeled with the original vertices, but isomorphism of rooted labeled trees is GI-complete, so the labels probably can’t be exploited/included for canonical labeling.

(For completeness, I will also give a small counterexample to the algorithm proposed in that paper.)

Definitions and known results for labeled tree isomorphism

For unlabeled rooted trees, the AHU algorithm (by Aho, Hopcroft and Ullman, Example 3.2 on page 84 in their book “The Design and Analysis of Computer Algorithms”) allows to efficiently decide whether two rooted trees are isomorphic. We may regard the AHU algorithm as an efficient implementation of color refinement (also known as naive vertex classification) for rooted trees. Therefore, color refinement decides (rooted) tree isomorphism. Does it also decide labeled tree isomorphism? That depends on what we mean by isomorphism of labeled graphs:

For labeled graphs, two definitions of isomorphism are in use.

Under one definition, an isomorphism is a vertex bijection which is both edge-preserving and label-preserving.[1][2]

Under another definition, an isomorphism is an edge-preserving vertex bijection which preserves equivalence classes of labels, i.e., vertices with equivalent (e.g., the same) labels are mapped onto the vertices with equivalent labels and vice versa; same with edge labels.[3]

For the first definition, where the isomorphism is required to be label-preserving, color refinement decides isomorphism. It won’t for the second definition, since we know

Theorem: Marked tree isomorphism is isomorphism complete

from section 6.4 Marked Graphs and Marked Trees in Booth, Kellogg S.; Colbourn, C. J. (1977), Problems polynomially equivalent to graph isomorphism, Technical Report CS-77-04, Computer Science Department, University of Waterloo. They used the definition that “A marked graph is a graph together with a partition of its vertices. An isomorphism of marked graphs is an isomorphism of the underlying graphs which preserves the partitioning.”

Isomorphism of labeled uniqueness trees is GI complete

I don’t remember how I figured out that isomorphism of rooted labeled trees is GI-complete when I wrote that email back in 2016. I guess I just looked it up in section 6.4 Marked Graphs and Marked Trees cited above. This time I didn’t look it up, and just came up with a rather obvious construction on the fly:

From a graph G, construct a rooted labeled tree T by putting a node below the root of the tree for every vertex of G. For every edge of G, put two nodes with the same label on the next lower level. An edge has two endpoints, connect the corresponding vertices (or rather the tree nodes corresponding to them) each with one of the tree nodes corresponding to the edge.

This construction does not yet rule out that the rooted labeled trees arising in the uniqueness trees algorithm could be efficiently tested for isomorphism. In those trees, no label is repeated on a given level of the tree. I initially believed that I had an efficient algorithm for this task. Then I realized that my algorithm was just an efficient implementation of color refinement for rooted labeled trees. So the question whether the algorithm worked boiled to whether color refinement decides isomorphism in this case. In the end it wasn’t that difficult to modify the above construction such that it also worked for this case:

A counterexample to the uniqueness trees algorithm

An easy way to break the uniqueness trees algorithm is to ensure that the trees don’t grow beyond depth 3 by replacing each edge by two nodes connected to the original end points of the edge, but not to each other. This ensures that only duplicate nodes are present at depth 2 or 3 of the uniqueness trees. Below we apply this construction to two non-isomorphis trees to construct two non-isomorphic graphs which cannot be distringuished by the uniqueness trees algorithm:

However, this counterexample does not answer the question whether the uniqueness trees algorithm is subsumed by Weisfeiler-Leman. Somebody told me that he remembers that the uniqueness trees algorithm was indeed subsumed by Weisfeiler-Leman. I still don’t see it, but I admit that it is quite plausible. It is probably subsumed by the algorithm where each vertex is individualized separately followed by color refinement to generate a label for that individualized vertex. And that algorithm in turn is probably subsumed by 2-WL. Or more generally, if each k-tuple is individualized separately followed by k-WL to generate a label for that k-tuple, then that algorithm is probably subsumed by 2k-WL.

Conclusions?

This was not the post I had planed to write next. It is reasonably short, which is definitively a good thing. It may also be a good thing that it reminds us that marked tree isomorphism is known to be GI complete. In fact, this cs.stackexchange question about a polynomial time algorithm for marked tree isomorphism motivated me to reformulate my supposedly efficient algorithm for labeled uniqueness trees in simple terms (i.e. as an instance of color refinement). This in turn allowed me to step back and find a reduction to show that it cannot work.

Maybe this post would have been more interesting, if I had talked more about details of the new Deep Weisfeiler Leman paper. At least I explained why I consider it to be a major achievement.

Defining a natural number as a finite string of digits is circular

The length of a finite string is a natural number. If a given Turing machine halts on the empty input, then the number of steps it performs before halting is a natural number. (A Turing machine halts if it reaches a halt state in a finite number of steps.) The concept of natural number is implicitly contained in the word “finite”. Is this circularity trivial?

Suppose that you have a consistent (but maybe unsound/dishonest) axiom system that claims that some given Turing machine would halt. Then this Turing machine defines a natural number in any model of that axiom system. To expose the trivial circularity, we can now use this natural number to define the length of a finite string of digits.

This idea was part of yet another attempt to explain how defining a natural number as a finite string of digits is circular. This post will explore whether this idea can be elaborated to construct a concrete non-standard model of the natural numbers, or more precisely of elementary function arithmetic, also called EFA. (This formal system is weaker then Peano arithmetic, because its induction scheme is restricted to formulas all of whose quantifiers are bounded. It is well suited as base system for our purpose, because all our proofs still go through without modification, and it is much easier to grasp which statements are independent of this system. Basically, it can prove that a function is total iff its runtime can be bounded by a finitely iterated exponential function.)

An attempt to explain that the circularity also occurs in practice

This section can be skipped. It is not a part of the main text. It tries to further illuminate the motivation for this post by quoting from a previous attempt to explain that circularity:

1. Some people like to imagine natural numbers encoded in binary (least significant bit first) as finite strings of 0s and 1s. Note that this encoding uses equivalence classes of finite strings, since for example 10 and 100 both encode the number 1, i.e. the number of trailing zeros is irrelevant.
2. But the word “finite” string already presupposes that we know how to distinguish between finite and infinite strings. So let us assume instead that we only have infinite strings of 0s and 1s, and that we want to encode natural numbers as equivalence classes of such strings.
3. … (taken from 7.2 INTEGERS in http://www.wrcad.com/oasis/oasis-3626-042303-draft.pdf): “An unsigned-integer is an N-byte (N > 0) integer value. … the remaining seven bits in each byte are concatenated to form the actual integer value itself.”
4. … Slightly generalising those schemes, we can say that the length is encoded as a prefix-free code, and the number is encoded in binary in a finite string of 0s and 1s of the given length.
5. The vagueness of “finite” comes in because of the prefix-free code part of the encoding. … And using a non-prefix-free encoding for the length will only create more vagueness, not less.

The idea quoted in the introduction suggests to use a Turing machine as encoding for the length. In a certain sense, this is indeed a non-prefix-free encoding. In another sense, the Turing machine itself must also be encoded (as a finite string), so this does not refute point 5. But we will ignore this further implicit occurrence of “finite” in this post.

Interactions between partial lies, absolute truth, and partial truths

Since we want to construct a concrete non-standard model, we will use EFA + “EFA is inconsistent” as our axiom system. Let us call this axiom system nsEFA, as an acronym for non-standard EFA. Let M be a Turing machine for which nsEFA claims that it halts.

Let us assume that M has a push-only output tape, on which it will successively push the digits describing some number N. In the simplest case, there is just a single digit available, and we get an unary representation of N. More succinct representations are also possible, but this unary representation corresponds more closely to the number of steps performed by M. This correspondence is not exact, which raises an interesting issue:

Can it happen that M only outputs a finite number of digits in an absolute sense, but that nsEFA is undecided about the number of digits output by M?

There is no reason why this should not happen. But this would be bad for our purpose, since it could happen that M would represent 3 in one model of nsEFA, and 4 in another. We can prevent this from happening, by allowing only those M for which EFA can prove that M will halt or output infinitely many digits.

Are there other ways to prevent this from happening, which don’t use the trusted axiom system EFA in addition to nsEFA? We could rely on absolute truth, and only allow those M which halt or output infinitely many digits. (This is equivalent to a sentence for given M, hence I don’t like it.) Or we could use EFA only via the class of functions which can be proved total in EFA, and require that nsEFA must prove for a concrete total function tf(n) from this class that M will not take more steps before halting or outputing the next digit than tf(“total number of steps of M when previous digit was output”). (This is fine for me, since nsEFA cannot lie about this without being inconsistent.)

Preventing the same issue for more succinct representations is a bit more tricky. For a positional numeral systems, it seems to make sense to only allow those M which halt or output infinitely many non-zero digits. But in this case, we could have a valid M which outputs 99999… (in decimal) or 11111… (in binary), but if we add 1, we get 00000… as output, which would be invalid. One way to fix this issue is to allow the digit 2 (in binary) or the digit A (in decimal), then we can use 02111… (in binary) or 0A999… (in decimal) as output. (We will call this additional digit the “overflow” digit, and the digit preceeding it the “maximal” digit.) It is also possible to weaken our requirements instead of having to invent new representation systems (see Appendix C: Weakening the requirements for succinct representations).

So we fixed this issue, but there is another even more serious problem.

Here is the problem: comparing numbers for equality

Let us call a Turing machine which satisfies the conditions described in the previous section an n-machine (because it defines a possibly non-standard natural number in any model of nsEFA). Let M and M’ be n-machines (using the unary representation as output, for simplicity). So both M and M’ define a number in any model of nsEFA. If nsEFA can prove that both M and M’ produce the same output, then the number defined by M and M’ is the same in any model. If nsEFA cannot prove this, then there will be a model where M and M’ define different numbers. Which is good, since this gives us an obvious way to define equality on the set of n-machines. So where is the problem?

Even so we know that M defines a number in any model of nsEFA, we don’t know whether it will define the same number in all models. But we just fixed this in the previous section, no? Well, we only fixed it for the case where M defines a standard natural number.

Comparing numbers from different models for equality is not always possible. For example, the imaginary unit i from one model of the complex number cannot be compared for equality with the negative imaginary unit -i from another model. But often it is possible to say that two numbers are different, even if they come from different models, just like i+1 and i-1 are definitively different.

It can happen that nsEFA can neither prove that M and M’ produce the same output, nor that they produce different output. So there will be a model where M and M’ define the same number, and a model where M and M’ define different numbers. It is unclear whether we should conclude from this that M defines different numbers in different models. An argument using standard natural numbers might be more convincing:

Can it happen that the remainder of the division of M with a standard natural number like 2 or 3 is different in different models of nsEFA?

Yes, it can happen, since nsEFA can be undecided about the exact result for the remainder. So we could have |M| = x+x in one model, and |M| = y+y + 1 in another model (where |M| is the number defined by M in the corresponding models). The trouble is that there is even an n-machine M’, which defines x in the first model and y in the other model. M’ gets constructed from M by outputting only every second digit output by M. One could argue that this means that M or M’ really defines different numbers in those two models.

(For example, let M be a machine which searches for a proof of a contradiction in EFA, which always outputs two digits for each step during the search. Finally, it outputs an additional digit iff the bit at a given finite position in the binary encoding of the found proof is set.)

Why not stop here? What should be achieved?

We must conclude that the idea to build a concrete non-standard model of EFA using only numbers which can be defined by some n-machine M will not work as intended. So why not end the post at this point?

First, it is important to understand what has already been achieved. The idea for this post (see Appendix A: Initial questions about circularity and the idea for this post) was just to use an axiom system like nsEFA and a Turing machine (satisfying suitable requirements based on nsEFA) to define a natural number in any model of nsEFA. This has been achieved. The idea had a more subtle part, which was to use the Turing machine mainly for defining the length of the string of digits, which forms the actual natural number. This part still needs more elaboration, which is one reason to go on with this post.

Another idea for the construction presented in this post has not yet been mentioned explicitly. There is an interesting definition on the top of page 5 of the nice, sweet, and short paper Compression Complexity by Stephen Fenner and Lance Fortnow:

Let (“Busy Beaver of ”) be the maximum time for to halt over all halting programs of length at most . Let be the lexicographically least program of length at most that achieves running time.

That encoding of by is nice: For fixed , it is just as efficient as the encoding by the first -bits of Chaitin’s constant, but much easier to explain (and decode, or rather it must not even be decoded). And for variable , the overhead over Chaitin’s encoding is just quadratic, so not too bad either. But the “time to halt” is slightly too sensitive to minor details of the program to allow arithmetic. Replacing “time to halt” by “length of unary output” is a natural modification of this encoding which allows computable arithmetic (addition, multiplication, exponentiation, minimum, maximum, and possibly more).

On the one hand, it is no surprise that the concrete definition of these arithmetic operations for the concrete encoding is possible. On the other hand, the section below which actually defined those operations (for unary output) got so long and convoluted that most of its content has been removed from this post. One reason why it got so convoluted is that an n-machine defines a natural number in any model of nsEFA, so we have to prove that our concrete definition of these arithmetic operations coincides (for numbers definable by n-machines) with the arithmetic operations already available in models of nsEFA. In addition, feedback by various people indicated that it should have been made clearer how the concrete definitions of the arithmetic operations are computable and independent of nsEFA, while equality depends on nsEFA and is only semi-decidable (i.e. computably enumerable instead of decidable/computable). And there is also the confusion why it should be relevant that the arithmetic operations are concrete and computable, if we are fine with much less for equality (see Appendix B: What are we allowed to assume?).

More relevant than that certain operation are computable and that some relations are semi-decidable is that some operations are not definable at all. We have seen this in the previous section for the remainder (of the division of M with a standard natural number like 2 or 3), if the definition of an n-machine uses unary output. One may wonder whether we showed this fact sufficiently rigorously, and how our definitions gave rise to this fact. The important part of our definitions is that we prevented that a non-standard number can be equal to a standard number. So if some operation has a standard number as result, and if this standard number is different in different models of nsEFA for two concrete n-machines, then that operation is not definable at all (with respect to the specific definition of n-machine).

What we will try to show when discussing numbers encoded as strings of digits is that the minimum and maximum operations are not definable, but that there are number representations for which the remainder (of the division of M with a standard natural number like 2 or 3) is definable (and computable). This is another reason why we want to explore more succinct representations, in addition to the unary representation. However, the corresponding section does not dig into the more basic details of doing arithmetic with these succinct representations (see Appendix E: More on the LCM numeral system), but only mentions the bare minimum of facts to indicate how its claims could be elaborated.

Finally, it should also be mentioned that this post failed to address certain questions (see Appendix D: Some questions this post failed to answer). The constructed structures seem to be models of Robinson arithmetic, which is not a big deal. The totality of the order relation fails. Therefore, the constructed structures cannot be models of any axiom system which would prove the totality of the order relation. But what about satisfying induction on open formulas? Probably not. Another question is how well the constructed structure can act as a substitute for the non-existent free model of nsEFA, or as a substitute for the non-existent standard model of nsEFA? Probably not very well.

Another point where this post failed is the very existence of this section. It has been added after this post was already published, because feedback indicated that this post failed to clearly communicate what it is trying to achieve. Together with introducing this section, many existing sections have been turned into appendices, and Appendix A has been newly added. Sorry for that, it is definitively bad style to alter a published post in such a way. But this post felt significantly more confusing than any other post in this blog, so not trying to improve it was also not a good option.

Translating the meaning of words into formulas

To add the numbers |M| and |M’| defined by M and M’ (using the unary representation as output), we construct a machine M” which first runs M and then runs M’. We claim that M” is an n-machine and that nsEFA proves |M|+|M’| = |M”|. So the number defined by M” is the sum of |M| and |M’| in any model of nsEFA. We denote M” by ADD(M,M’).

But what does it actually mean that nsEFA proves |M|+|M’| = |M”|? It can only prove (or even talk about) formulas in the first order language of arithmetic. The statement that M defines a number |M| means that we can mechanically translate M into a formula such that nsEFA proves and . To prove |M|+|M’| = |M”|, nsEFA must prove .

We use a formula which describes the behavior of M. It says that M transitions in steps from the state to the state . This allows us to define . Here the first component of the state is the line number of the program (or the internal state of the machine), and is the unique line of the program with a statement (or the unique internal halt state of the machine). We used the second component of the state as the push-only (unary) output tape.

We also define the sentence HALT(M). (A sentence is a formula with no free variables.) M halts if and only if HALT(M) is true for the standard model of the natural numbers. However, the standard model of the natural numbers is not a model of nsEFA. But HALT(M) is still meaningfull for nsEFA: If M halts and nsEFA would prove that HALT(M) is false, then nsEFA would be inconsistent.

Already the definition of nsEFA as EFA + “EFA is inconsistent” uses this translation. We take some machine C which searches for a proof in EFA of a contradiction, and add the formula HALT(C) to EFA as an additional axiom. The expectation is that nsEFA can then prove HALT(C’) for any other machine C’ searching for a contradiction in EFA. This will obviously fail if C’ does unnecessary work in a way that nsEFA cannot prove that it will still find a contradiction in EFA. For example, it could evaluate the Ackermann–Péter function A(m,n) at A(m,0) for increasing values of m between the steps of the search for a contradiction. Or C’ could use a less efficient search strategy than C, like looking for a cut-free proof, while C might accept proofs even if they use the cut rule.

(What if we use EFA + “ZFC in inconsistent” or EFA + “the Riemann hypothesis is false” as our axiom system? In the first case, the remarks on the efficiency loss of cut-free proofs are still relevant. In the second case, it would be hard to come up with different translations for which EFA cannot prove that they are equivalent. And if EFA could prove “the Riemann hypothesis is true”, then that axiom system would be inconsistent anyway.)

We also define the sentence LIVE(M):=HALT(M)∨ (M halts or if M reaches state , then it reaches a state ) which says that M will only take finitely many steps before it outputs another non-zero digit or halts.

M is an n-machine if nsEFA proves HALT(M) and EFA proves LIVE(M). (EFA proves , independent of whether M is an n-machine or not. Namely EFA proves , which expresses the fact that M is deterministic.) If nsEFA proves HALT(M), then nsEFA also proves . This is trivial, since our definition of HALT(M) turns out to be equivalent to .

Back to M”:=ADD(M,M’). How do we know that nsEFA proves HALT(M”) and EFA proves LIVE(M”)? It follows because EFA proves HALT(M) HALT(M’) HALT(M”) and LIVE(M) LIVE(M’) LIVE(M”). Details of are needed to say more. And nsEFA proves because EFA proves for any M which doesn’t query the register and only increases it.

Using register machines for discussing EFA proofs

We defined ADD(M,M’) in the previous section. The definitions of MUL(M,M’) and POW(M’,M) will be more complicated, because |M’| might be zero (or one), hence the requirement that an n-machine does not run forever without outputting additional digits requires some care. We will also define SUB(M,x), DIV(M,x) and LOG(x,M). Here x must effectively be a standard natural number, for example a number defined by an n-machine for which EFA (instead of nsEFA) can prove that it halts.

In any case, we better define some machine architecture with corresponding programming constructs to facilitate the definition of those operations and the discussion of EFA proofs. A concrete machine architecture also facilitates the discussion of details of . Instead of Turing machines, we use register machines, since most introductory logic books use them instead of Turing machines. Typically, they first define register machines over an arbitrary alphabet like

	If then remove the last letter of the word in . Otherwise append the letter to the word in .
	Read the word in . If the word is empty, go to . Otherwise if the word ends with the letter , go to .
	Halt the machine.

and then focus on the case of the single letter alphabet . For that case, we use a more explicit instruction set, which is easier to read:

	Increment .
	Decrement . If it is zero, then it stays zero.
	Go to the unique line where is prepended.
	If , then go to .
	Halt the machine.

To avoid , we define two simple control constructs:

We also define two simple initialization constructs:

__	__ __ __ __ __

Next we need constructs that allow us to express things like “a machine which runs M, and each time M would output a digit, it runs M’ instead”. To avoid that M’ messes up the registers of M, we allow symbolic upper indices on the registers like , or even . We use this to define the program transform construction …

… and this section went on and on and on like this. It was long, the constructions were not robust, the proofs were handwavy, there were no nice new ideas, and motivations were absent. Maybe I will manage to create another blog post from the removed material. Anyway, back to more interesting stuff …

Succinct representations of natural numbers

The proposal from the introduction was to use the number of steps which a given Turing machine performs before halting to define the length of a finite string of digits. The observation that the unary representation fits into this framework too is no good excuse for not looking at more interesting strings of digits. So we have to look at least at a positional base b numeral system (for example with b=10 for decimal, or b=2 for binary). We will also look at the LCM numeral system, which is closely related to the factorial number system and to the primorial number system (see Appendix E: More on the LCM numeral system).

It is possible to define MAX(M,M’) and MIN(M,M’) for the unary representation. We did not define it in the previous section, because at least MIN(M,M’) requires to alternate between running M and M’, which was not among the constructions defined there. Neither MAX(M,M’) nor MIN(M,M’) can be defined for any of our succinct representations. The reason is that already the first few digits of the result will determine whether M or M’ is bigger, but there are M and M’ where in one model of nsEFA it is M which is bigger, and in another model it is M’.

All our succinct representations allow conversion to the unary representation. Since MAX(M,M’) and MIN(M,M’) are defined for the unary representation, but not for our succinct representations, we conclude that conversion from the unary representation to any of our succinct representations is not possible. The fact that conversion to unary is possible also makes it easier to compare numbers defined by n-machines using different representations for equality: The numbers are equal if nsEFA can prove that the numbers which were converted to unary are equal.

Let REM(M,x) (or rather |REM(M,x)|) be the remainder from the division of |M| by x such that x. For the LCM numeral system and the factorial number system, we have that REM(M,x) can be defined for any standard natural number x. For the primorial number system, it can only be defined for any square-free standard natural number x. For binary, x must be a power of two, and for decimal, x must be a product of a power of two and a power of five. We conclude from this that binary cannot be converted to decimal, neither binary nor decimal can be converted to LCM, factorial, or primorial, and primorial cannot be converted into any other of our succinct representations.

What about the remaining conversions between our succinct representations that we have not ruled out yet? If we know the lowest i digits of the decimal representation, then we can compute the lowest i digits of the binary representation. Therefore, we conclude that decimal can be converted to binary. In theory, we would have to check that nsEFA can actually prove that directly converting a decimal nummber to unary gives the same number as first converting it to binary and then to unary. But who cares?

To compute the lowest i digits of the binary representation, it is sufficient to know the lowest 2i digits of the factorial representation, or the lowest 2ⁱ digits of the LCM representation. So factorial and LCM can be converted to binary. To compute the lowest i digits of the decimal representation, it is sufficient to know the lowest 5i digits of the factorial representation, or the lowest 5ⁱ digits of the LCM representation. So factorial and LCM can be converted to decimal. To compute the lowest π(i) digits of the primorial representation (where π(n) is the prime-counting function), it is sufficient to know the lowest i digits of the factorial or LCM representation. So factorial and LCM can be converted to primorial. To compute the lowest π(i) digits of the LCM representation, it is sufficient to know the lowest i digits of the factorial representation. To compute the lowest i digits of the factorial representation, it is sufficient to know the lowest iⁱ digits of the LCM representation. So it is possible to convert LCM to factorial and factorial to LCM.

In the previous section, we defined ADD(M,M’), MUL(M,M’), POW(M’,M), SUB(M,x), DIV(M,x) and LOG(x,M) using the unary representation. ADD(M,M’), MUL(M,M’), and SUB(M,x) can be defined for any of our succinct representations, LOG(x,M) for none. For the LCM numeral system and the factorial number system, we have that DIV(M,x) can be defined for any standard natural number x. For binary, x must be a power of two, and for decimal, x must be a product of a power of two and a power of five. This is the same as for REM(M,x). But for primorial, DIV(M,x) cannot be defined at all, not if x is square-free (even so this is sufficient for REM(M,x) to be defined), not even if x is a prime number.

What about POW(M’,M)? We have , where is Euler’s totient function. Therefore POW(M’,M) can be defined for the LCM numeral system and the factorial number system, but not for any other of our succinct representations, not even in case |M’|=2. What about other functions? There is a
list of functions in the wikipedia article on primitive recursive functions. All those functions actually seem to be from ELEMENTARY, but that does not necessarily mean that they can be defined for one of our representations (not even unary). Maybe 4. Factorial a!, 11. sg(a): signum(a): If a=0 then 0 else 1, and 18. (a)_i: exponent of p_i in a are still interesting. The signum function can be definitively be defined for any of our representations. It seems that the factorial function too can be defined for any of our representations. It is interesting, because it will just output an infinite stream of zero digits for any non-standard natural number, for any of our succinct representations. Actually, our requirements for n-machines currently (see next section) don’t allow us to output an infinite stream of zero digits. However, there is a workaround: we can output the “overflow” digit instead of the first zero digit, and the “maximal” digits instead of the consecutive zero digits. The exponent of p_i cannot be defined for unary. But we can define it as a function from the LCM or factorial representation to the unary representation.

So we have a nice collection of trivial facts about our succinct representations. But what are our succinct representations good for, compared to unary? After all, the representation is just an n-machine in both cases, and the n-machine for a succinct representation is not much shorter than the corresponding n-machine for the unary representation. Their runtime and output can be exponentially shorter, but EFA does not care about that either. There is at least one important advantage: The finite initial segments of output digits reveal more information than for unary, and that information is guaranteed to be present (which is not the case for unary). Turns out that for our succinct representation, this information is no more than the remainders of the division with all standard natural numbers (or a suitable infinite subset of the standard natural numbers).

But why is this advantage relevant? Why is our nice collection of trivial facts relevant? In terms of absolute truth, a given n-machine is on the one hand what nsEFA can prove about it, but on the other hand it is also a possibly infinite string of digits. The length of this string is bounded by the number of steps the n-machine performs before it stops. So we nearly succeeded in exposing the circularity of defining a natural number as a finite string of digits. The length of the string (in any of our succinct representations) is indeed a natural number, but only in unary representation. And it cannot (in general) be converted back to any of our succinct representations. Since we used EFA, it is nice that we found a succinct representations for which POW(M’,M) can be defined. Since Gödel’s β function uses the remainder, it is nice that it can be defined. Since the exponent of p_i is one way for encoding sequences into natural numbers, it is interesting that is can only be defined as a function from LCM or factorial to unary.

Conclusions?

One of the initial ideas was to construct a non-standard model of EFA, or more precisely a model of nsEFA. This was not achieved. What has been achieved is a very concrete description of some non-standard numbers by Turing machines which do not halt in terms of absolute truth, but for which nsEFA proves that they halt. Those non-standard numbers define unique numbers in any model of nsEFA, and we ensured that it cannot happen that those numbers define different standard natural numbers in different models. We settled on an obvious way to compare those non-standard numbers for equality, and explained why we won’t be able to achieve our initial goal. We decided to go on with the post nevertheless, and show that addition, multiplication, and exponentiation can be defined for those numbers. We then started to dive deeply into technical details, till the point were a section got so technical that most of its content got removed again, because this is supposed to be a more or less straightforward and readable blog post after all.

Anyway, the most important thing about the natural numbers is the ability to write recursions. That’s kind of the defining property, really. You have to be able to do predecessor and comparison to zero or it’s not a good encoding, IMO.

This was a reaction to a previous attempt to explain that the encoding of natural numbers can be important. It has a valid point. Focusing on addition, multiplication, and exponentiation seemed to make sense from the perspective suggested by EFA, but recursion and induction should not have been neglected. On the other hand, Robinson arithmetic completely neglects recursion and induction, our non-standard number seem to be a model of it, and people still treat it as closely related to the natural numbers.

The main idea of this post was to use the natural number implicitly defined by a Turing machine which halts (or for which some axiom system claims that it halts) as the length of a string of digits. This idea turned out to work surprisingly well. The purpose was to illustrate how defining a natural number as a finite string of digits is circular. This was achieved, in a certain sense: We were naturally lead to define operations like SUB(M,x), DIV(M,x), MIN(M,M’), REM(M,x), and the exponent of p_i in M. Those operations require three different kinds of natural number: standard natural numbers (those for which EFA can prove that the machine halts), numbers in succinct representation, and numbers in unary representation. SUB and DIV work for both unary and succinct, but the second argument must be standard. MIN only works for unary, and REM only works for succinct. The last one only works as a function from succinct to unary, where p_i must be standard.

Were we really naturally lead there, or did some of our previous decisions lead us there, like to only allow those M which halt or output infinitely many non-zero digits? Well, yes and no. The decision to forbid non-standard numbers which are undecided about whether they are equal to a given standard number probably had some impact. At least it would have been more difficult otherwise to argue why certain functions cannot be defined. The specific way how we enforced this decision had no impact on the definability of the functions we actually investigated, and it is unclear whether it could have had in impact.

It did have a minor impact on our succinct representations, but in the end the “overflow” digit is only a minimal modification. It does offer some parallel speedup for addition, but signed digits are necessary to get good parallel speedup for multiplication. Those can be signed digits can be interpreted as a (a-b) representation (of integer numbers), and lures one into trying to find something close to the (c/d) representation (of rational numbers) which might allow good parallel speedup for division or exponentiation. (Well, that hope actually comes from a paper on Division and Iterated Multiplication by W. Hesse, E. Allender, and D. Barrington which says in section 4: “The central idea of all the TC0 algorithms for Iterated Multiplication and related problems is that of Chinese remainder representation.”) This lead to including the factorial and primorial representation in the succinct representations, and in trying to “fix” the primorial representation by including the LCM representation.

Appendix A: Initial questions about circularity and the idea for this post

Of course Hume is right that justifying induction by its success in the past is circular. Of course Copenhagen is right that describing measurements in terms of unitary quantum mechanics is circular. Of course Poincaré is right that defining the natural numbers as finite strings of digits is circular. …

But this circularity is somehow trivial, it doesn’t really count. It does make sense to use induction, describing measurement in terms of unitary quantum mechanics does clarify things, and the natural numbers are really well defined. But why? Has anybody ever written a clear refutation explaining how to overcome those trivial circularities? …

So I wondered how to make this more concrete, in a similar spirit like one shows that equality testing for computational real numbers is undecidable. The idea here is to take some Turing machine for which we would like to decide whether it halts or not, and write out the real number 0.000…000… with an additional zero for every step of the machine, and output one final 1 when (and only if) the machine finally halts. Deciding whether this real number is equal to zero is equivalent to solving the halting problem for the given Turing machine. How can one do something similarly concrete for natural numbers? Suppose that you have a consistent (but maybe unsound/dishonest) axiom system that claim that some given Turing machine would halt. Then this Turing machine defines a natural number in any model of that axiom system. To expose the trivial circularity, we can now use this natural number to define the length of a finite string of digits. How do we get the digits themselves? We can just use any Turing machine which outputs digits for that, independent of whether it halts or not. Well, maybe if it doesn’t halt, it would still be interesting whether it will output a finite or an infinite number of digits, but in the worst case we can ask the axiom system again about its opinion on this matter. The requirement here is that the natural numbers defined in this way should define a natural number in any model of that axiom system.

Appendix B: What are we allowed to assume?

It might seem strange to cast doubt on whether the concept of a natural number is non-circular, but at the same time taking Turing machines and axiom systems for granted. An attempt at an explanation why natural numbers are a tricky subject (in logic) was made in a blog comment after the line Beyond will be dragons, formatting doesn’t work… The bottom line is that it is possible to accept valid natural numbers, but not possible to reject (every possible type of) invalid natural numbers. So what should we allow ourselves to assume and what not? Specific natural numbers, Turing machines, and axiom systems can be given, since we can accept them when they (or rather their descriptions) are valid. A Turing machine can halt, and an axiom system can prove a given statement. This also means that we can talk about an axiom system being inconsistent, since this just means that it proves a certain statement. Talking about an axiom system being consistent is more problematic. We have done it anyway, because this appendix was only added after the post was already finished (based on feedback from Timothy Chow). We did try to avoid assuming that arbitrary arithmetical sentences have definitive truth values, and especially tried to avoid using oracle Turing machines.

However, in the end we are trying to construct a concrete model of an unsound/dishonest axiom system. Such an axiom system can have an opinion about the truth values of many arbitrary arithmetical sentences. So if it would have helped, we would have had no problem to assume that arbitrary arithmetical sentences have definitive truth values. And assuming consistency definitively helps when you are trying to constuct a model, so we just assumed that it was unproblematic.

Appendix C: Weakening the requirements for succinct representations

We did not use the “overflow” digit much in discussing our succinct representations. But we simply did not go into details of addition and multiplication. The previous post on signed digit representations focused more on details. It explained for example why having signed digits is even better than having an “overflow” digit for the speed of multiplication. At the point were we introduced the requirement to output infinitely many non-zero digits (which made the “overflow” digit necessary), we postponed the discussion of alternatives.

Let us try to weaken our requirements instead of having to invent new representation systems. We could forbid trailing zeros (or only allow a finite number of trailing zeros). This is meaningless in terms of absolute truth, since it is meaningless to talk about the trailing zeros if the machine M outputs infinitely many digits. What we want to express is that “if M would halt, then there would be no trailing zeros (or no more trailing zeros than a given finite number)”. So we are fine if nsEFA can prove this, since our requirements only need to ensure that non-standard natural numbers cannot mix with standard natural numbers. A slight refinement is to require that nsEFA must prove for a concrete function tf(n) which can be proved total in EFA that if M outputs more than tf(“total number of steps of M when previous non-zero digit was output”) consecutive zeros, then it will output at least one further non-zero digit before it halts. This refinement tries to ensure that a machine M valid according to our initial requirements is also valid according to our weakened requirements.

Appendix D: Some questions this post failed to answer

The section on comparing numbers for equality showed that our plan for constructing a concrete non-standard model of EFA will not work as intended. But this leaves open some questions, since we did construct a concrete stucture:

• The totality of the order relation obviously fails. But our concrete structure still seems to be a model of Robinson arithmetic. Does it also satisfy induction on open formulas? It is not obvious why induction on open formulas should fail.
• Is there some non-concrete equivalence relation on our structure such that the resulting quotient structure would be a model of nsEFA? Can we just take any consistent negation complete extension of nsEFA, and identify those n-machines for which that extension proves that they produce the same output? At least we are not guaranteed to get a model of that extension, because it will (in general) prove that more Turing machines halt than we have included in our structure. (Even worse, the extension has an opinion about arbitrary arithmetical sentences, so we might even have to include oracle Turing machines in our structure, if we wanted to get a model of that extension.) So the resulting quotient structure might not satisfy the induction scheme of nsEFA. Still, the order relation would be total, and the remainder (for a standard natural number) would be defined.
• In a certain sense, the free algebra is a canonical model of an equational theory. The straight-line program encoding is natural for storing the elements of the free algebra. But nsEFA does not have a canonical model, and the straight-line program encoding of natural numbers might rather feel deliberately perverse. Some people really do not understand why you would want to ever consider this as an encoding of natural numbers. And with respect to the natural numbers, the straight-line program encoding may indeed be inappropriate. So our efforts might be interpreted as an attempt to find appropriate encodings which can take over the role of straight-line program encodings in case of nsEFA. But can we make it more precise in which way our n-machines provide appropriate substitutes for the elements of the non-existing free algebra? Who knows, maybe if we tried hard enough, we would find reason why we cannot do that.

Appendix E: More on the LCM numeral system

As said before, we did not actually talk much about arithmetic in the LCM or factorial representation. Let me copy a discussion about division for factorial and LCM, and relatively fast multiplication for LCM below, to talk at least a bit about those topics:

If an arbitrarily huge number is divided by a fixed number (assumed to be small), then the factorial number system only needs to know the lowest digits of the huge input number for being able to write out the lowest digits of the result. The LCM number system also only need to look ahead a finite number of digits for writing out the lowest digits of the result. The exact look ahead is harder to determine, it should be more or less the lowest lowest digits of the huge input number.

However, the LCM number system also has advantages over the factorial number system. Just like the primorial number system, it allows a simple and relatively fast multiplication algorithm. The numbers can be quickly converted into an optimal chinese remainder representation and back:

with .

So to multiply and , one determines an upper bound for the number of places of , then computes value of and modulo all those places, multiplies them separately for each place (modulo ), and then converts the result back to the LCM representation. The conversion back is easy, since one can first determine , then by subtracting from the known value before converting it to , then by subtracting from the known value before converting it to , and so on.

This chinese remainder representation is optimal in the sense that the individual moduli are as small as possible for being able to represent a number of a given magnitude. The LCM number system may be even more optimal than the primorial number system in this respect. (It should be possible to do the computations modulo only for the biggest , due to the structure of the LCM number system.)

Theory and practice of signed-digit representations

The integers are sometimes formally constructed as the equivalence classes of ordered pairs of natural numbers . The equivalence relation is defined via

iff

so that gets interpreted as . This motivates the signed-digit representation. To avoid storing two numbers instead of one, the subtraction gets performed on the level of digits. This leads to signed digits. The overhead can be kept small by using unsigned 7-bit or 31-bit digits as starting point (instead of decimal or binary digits).

The overhead may be small, but the signed-digit representation remains redundant and non-unique. Comparing two integers in this representation is a non-trivial operation. But addition (and subtraction) becomes easy from a hardware perspective, since carry-bits no longer propagate. Multiplication also gets easier, since a part of multiplication consists of adding together intermediary results.

This post started as a subsection of another yet to be finished post. That subsection tried to use the trivial redundancy of representations of the computable real numbers as motivation to use similar redundant representations also for natural numbers. However, the constant references to simpler precursor ideas, to the well known practical applications, and to further complications and generalizations required in practical applications made that subsection grow totally out of proportion. It is still awfully long, even as a standalone post. The subsections try to cut it into more digestible pieces, but all the references to external material remain. The reader is not expected to read much of the linked material. It only serves as proof that this material has practical applications and is well known. This post may be seen as describing one specific alternative number format in detail, for which I dreamt about sufficient hardware support in a previous post.

Fast parallel arithmetic

In the 6502 Assembly language (C64, Apple II, …), addition is performed by the ADC instruction, which is the mnemonic for Add Memory to Accumulator with Carry. It adds the value in memory plus the carry-bit to the value in the accumulator, stores the result in the accumulator, and sets the carry-bit according to whether the addition overflowed or not. This operation could be represented as A + M + C -> A, or more precisely as
(A + M + C) % 256 -> A
(A + M + C) / 256 -> C
Since A and M can be at most 255 and C at most 1, the resulting C will again be either 0 or 1. This allows to add two arbitrarily long numbers. First one sets the carry bit to zero, then adds the lowest bytes, and then successively the higher bytes. Nice, but not very parallel.

Since the 6502 Assembly language has no instruction for multiplication, calling it fast would be an exaggeration. Let us instead imagine a machine which can perform 8 add with carry additions in parallel, where the carry-bits are stored in an additional byte. Since the meaning of the carry-bits before and after the parallel addition are different, we probably want to left-shift the carry-bits after the addition. Let us imagine that this machine can also perform 4 multiply with carry multiplications in parallel. How should it handle the carry-bits? Since (255+1)*(255+1)-1 can be represented in two bytes, it seems reasonable to treat them as a simple addition of 1 or 0 on input. The carry-bit on output might be interpreted as addition of 256 or 0, which would be consistent with the interpretation on output after addition.

Outputting a second carry-bit to be interpreted as addition of 256^2 or 0 would also be consistent, even so it is not required here. (Since (255+16+1)*(255+16+1)-16^3-256-16-1 = 16^4+16^3-16-1 cannot be represented in two bytes, allowing a second carry-bit may be useful to simplify recursive implementation of multiplication.) It is slightly inconsistent that the add with carry instruction only consumes one carry-bit per addition. After all, the idea is to represent intermediate results as M+C, in order to enable fast parallel addition of intermediate results. But consuming two carry-bits would be problematic since the result of (255+1)+(255+1) is not nicely representable.

What we just described is not new (of course). It is basically just the Carry Save Adder technique used to parallelize multiplication. However, since arithmetic with very long numbers is often used for modular arithmetic, this is not yet the end of the story. The Drawbacks section on wikipedia say that it has to be combined with the Montgomery modular multiplication technique, to be useful for public-key cryptography.

It is cool that our imagined computer can multiply 4 bytes and add 8 bytes in parallel, but how would we actually multiply two 4-bytes long numbers? Each byte of the first number must be multiplied by each byte of the second number, those results must be arranged appropriately and added together. The required 16 multiplication can be done by 4 subsequent parallel multiply with carry instructions, where the second 4-bytes (and the corresponding carry bits) are rotated in between. We have to add 1, 3, 5, 7, 7, 5, 3, 1 bytes in the different places of the result, which requires at least 24 additions. There are at most 6 additions in the last round, so we need at least 4 rounds of (8 bytes) parallel additions. And we might need even more rounds, since we get slightly too many carry-bits.

Faster multiplication and signed integers

Subtraction and signed integers are useful even for multiplication of positive integers, since subtraction is a basic operation required by fast multiplication algorithms like Karatsuba multiplication or its generalization, Toom-Cook multiplication. So what we describe next is not new either. See for example section “3.2 Multiplication” of The Complexity of Boolean Functions by Ingo Wegener, 1987, where the signed-digit representation is used for fast parallel multiplication algorithms.

The 6502 Assembly language also has an SBC instruction, which is the mnemonic for Subtract Memory from Accumulator with Borrow. This operation could be represented as A – M – ~C -> A, apparently the 6502 performs an ADC instruction with the bitwise-not of M. It makes sense, as this is the cheapest way to reduce subtraction to addition. For us, a SBB instruction where ~C got replaced by B fits better into our interpretation scheme
(A – M – B) % 256 -> A
(A – M – B) / 256 -> -B
The integer division here truncates towards , we could also write
(A – M – B + 256) % 256 -> A
(A – M – B + 256) / 256 -> 1-B
We can read A – M – B both as A – (M+B) and as (A-B) – M. The second reading is preferable, if we imagine a machine which can perform 8 SBB instructions in parallel, where the borrow-bits are stored in an additional byte. Again, we should left-shift the borrow-bits after the subtraction, since their meaning before and after the parallel subtraction is different. The parallel SBB instruction (+ left-shift) returned a signed integer in the a-b signed-digit representation, which we mentioned in the introduction.

Even so bit-twiddling may be nice, it somehow makes the trivial idea behind representing signed integers as a-b using signed-digits feel unnecessarily complicated. For D >= 3, we may just assume that we have a digit between -D+1 and D-1, after addition or subtraction we will have a result between -2*D+2 and 2*D-2, and if we stay in the range -D+2 and D-2, then we can just emit an overflow of -D, 0, or D, and the next digit can consume that overflow without overflowing itself.

More bit-twiddling with borrow-bits

Can we define a straightforward (parallel) ADB (add with borrow) instruction, which adds an unsigned integer to a signed integer, and returns a signed integer? We get
(A-B + M + 1) % 256 -> A
(A-B + M + 1) / 256 -> 1-B
if we just use ADC and replace C by (1-B). This represents the result as -1 + A + (1-B)*256. But how is this compatible with our signed-digit representation? When we left-shift the borrow-bits after the addition, we fill the rightmost place with 1 (instead of 0). In the other places, the -1 cancels with the 1 from (1-B)*256 of the previous byte. The leftmost place is also interesting: If B is set, then we can ignore it. But if it is not set, then A needs an additional byte set to 1. So signed-digit representation works with nearly no overhead.

We basically just replaced C by (1-B). But how could this trivial change enable us to represent signed integers? A-B = A – (1-C) = A+C – 1, so A and C now describe a digit in -1..255, while before it was a digit in 0..256. Even so we prefer the borrow-bits variant here, this way of looking at it (offset binary) can sometimes be helpful, for example when trying to interpret the SBC instruction of the 6502 Assembly language.

In my previous thoughts about (big) integers, there was the question whether the two’s complement representation is well suited for a variable width integer data type. One argument against it was that the addition or subtraction of a small number from a big number would take an unnecessarily long time. In the borrow-bits variant, for addition all bytes where the borrow-bit is not set must be touched, and for subtraction all bytes where the borrow-bit is set must be touched.

Before we come to parallel multiplication, what about multiplication by -1 and by a power of two? -1*(A-B)=B-A, so SBB of B (as bytes without borrow) and A gives the correct result. It is the sum of the bitwise-not of A, the byte-wise B and a carry-bit set to 1. The resulting (to be left-shifted) borrow-bit B is given by (1-C). The result of multiplication by a power of two is given by a left-shift followed by SBB. The same holds for multiplication by minus a power of two. In general, two successive multiplications by -1 will not yield the identity on the binary level, and identities about multiplication by powers of two (like associativity) will not hold on the binary level.

How to perform 4 multiply with borrow multiplications in parallel? If the borrow-bits are interpreted as simple addition of -1 or 0 on input, then the smallest result is -255, and the biggest 255*255, so the borrow-bit on output might be interpreted as addition of -256 or 0. However, what about the problem that addition cannot consume two borrow-bits? ADC outputs a digit in 0..2*255+1, SBB outputs a digit in -256..255, and ADB outputs a digit in -1..2*255. If we let ADB instead output a digit in 0..2*255-1 and an overflow of -256, 0, or 256, then the next digit can consume that overflow without overflowing itself. This extends the output range of ADB to -256…3*255, so we can now consume two borrows-bits of -1 and three bytes. (Basically the same as if we had just performed two subsequent ADB instructions, but the borrow propagation behaves nicer.)

The output range can also be extended one-sided (by 255). Extending ADB to the negative side or extending SBB to the positive side both yield a range -256..2*255, which can consume two borrow-bits of -1 and two bytes (or more precisely two positive bytes, one negative byte, and one borrow-bit of -1). ADC can be extended to the positive side to a range 0..3*255+1, so that it can consume two bytes and two carry-bits of +1.

Redundant representations of the computable real numbers

The idea of using a redundant representation for computable real numbers somehow feels trivial. There is no way to get a completely non-redundant representation anyway. The non-trivial idea is to exploit the redundancy to improve the computational properties of the computable real numbers. This idea is not new (of course, I keep repeating myself), and I tried my luck with it in an email 17 Dec 2018 TK: A signed-digit representation solves some issues to Norman Wildberger in response to the issues he raised in “Difficulties with real numbers as infinite decimals (II) | Real numbers + limits Math Foundations 92” on slide 8 at 31:24 before claiming: No such theory exists (2012)!! There are redundant representations of the computable real numbers, for which the operations of addition, subtraction and multiplication are computable. At the beginning of Problems with limits and Cauchy sequences | Real numbers and limits Math Foundations 94 on slide 1, we read

Attempts at ‘defining real numbers’:
– as infinite decimals
– as Cauchy sequences of rationals
– as Dedekind cuts
– as continued fractions
– others (Axiomatics, …)
None of these work!

In subsection “2.2. Non-termination” of Luther Tychonievich’s post on Continued Fractions, it is explained why computability (of addition and multiplication) fails for a representation by classical continued fractions. But they would be computable, if signed integers (instead of natural numbers) were allowed in the continued fraction expansion. One still needs to keep some restrictions on the numbers in the expansion, but it can be done, see section “3.3 Redundant Euclidean continued fractions” of Exact Real Com­puter Arithmetic with Con­tin­ued Frac­tions by Jean Vuillem­in, 1987. The signed-digit representation is also described there, in section “3.1 Finite representations of infinite sequences of numbers” at the bottom of page 13.

An infinite signed-digit representation of the computable real numbers

Signed-digit representations are not limited to integers. We will use them as representation of computable real numbers. The apparent drawback that the signed-digit representation of a number is not unique becomes a feature when it is used to represent computable real numbers.

We could try to define a computable real number as a Turing machine outputting the digits of its infinite binary extension. An objection is that addition of two such computable real numbers would not be computable. But what if we define it instead as the difference of two non-negative series of digits. It turns out that addition, subtraction and multiplication then become computable. (The reason why a signed-digit representation helps there is because it can eliminate chains of dependent carries.) However, testing whether such a number is zero turns out to be undecidable. This is fine, since

… equality testing for computable real numbers is undecidable. The idea here is to take some Turing machine for which we would like to decide whether it halts or not, and write out the real number 0.000…000… with an additional zero for every step of the machine, and output one final 1 when (and only if) the machine finally halts. Deciding whether this real number is equal to zero is equivalent to solving the halting problem for the given Turing machine.

Even so equality testing is undecidable, it would still be nice to have a representation for which addition and multiplication (and many other operations) are computable. And the signed-digit representation achieves exactly this, more or less. Division is still not computable, since it has a discontinuity at zero, and the signed-digit representation cannot easily avoid that issue. Using a representation via (a-b)/(c-d) can work around that issue, at the cost of also allowing 1/0 and 0/0. Jean Vuillem­in tries to explain why this is important, but at least initially his definitions just confused me.

Conclusions?

Even so the above text is awfully long and trivial, at least it is a proper blog post again. Maybe I should have talked more about the less trivial stuff, but the trivial stuff already filled the post. And this bit-twiddling is a real part of my thinking and acting, at least in my distant past. And I hope that having finally finished this post will allow me to also finish the other to be finished post soon, the one whose subsection grew totally out of proportion and turned into this post.

A list of books for understanding the non-relativistic QM — Ajit R. Jadhav’s Weblog

I really like that this post points out that QM is vast, and that it takes a prolonged, sustained effort to learn it. I also like that it explicitly recommends chemistry books. My own first exposure to the photoelectric effect (before university and before my physics teacher at school had even mentioned quantum) was from an introductory chemistry book by Linus Pauling.

TL;DR: NFY (Not for you). In this post, I will list those books which have been actually helpful to me during my self-studies of QM. But before coming to the list, let me first note down a few points which would be important for engineers who wish to study QM on their own. After all, […]

via A list of books for understanding the non-relativistic QM — Ajit R. Jadhav’s Weblog

I’m not a physicist

Background

At the end of 2016, I decided to focus on working through an introductory textbook in quantum mechanics, instead of trying to make progress on my paper(s) to be published. I finished that textbook, which taught me things like Clebsch-Gordan coefficients, the Aharanov-Bohm effect, perturbation theory, Fermi’s golden rule, path integrals, and the Dirac equation. Another physics book that I worked through in 2017 taught me about thermodynamics and its importance for chemistry and solid state physics.

I spend much time with other physics textbooks in 2017, but didn’t read them cover to cover. In general, I spent much time in 2017 on physics, and I was happy about that. My day job (in semiconductor manufacturing) is concerned with physics to a large part. I previously had a bad conscience, because I was spending so little time on physics, or at least I was making so little progress.

But spending so much time on physics meant that little time was left for this blog. And I submitted (with coauthors) an abstract for a conference, which got accepted as oral presentation. The conference was end of February 2018, and I spend the last two months before working day and night to still finish the paper (and presentation) in time. But even after the conference, I continued to spend most of my time on physics. So a post about physics seems like the only reasonable way to get any blog post done at all.

My love-hate relationship with physics

When I had the choice for my first job between one closely related to my thesis and one closely related to physics, I took the one related to physics. In my experience, establishing friendly relationships with physicists was easy. It did work out as expected, but I was surprised how much physics ended up on my plate. But it was fine for me, those were things like electrodynamics and optics, which were easy for me. When quantum mechanical tasks started to land on my plate, I protested that I didn’t manage to finish that course at university. But after switching jobs (Feb 2013), I sort of had to accept that the quantum mechanical tasks were part of my responsibilities.

On the one hand, this was a nice excuse for me to try to understand that part of physics which I was once unable to understand. On the other hand, the question “Why me? There are real physicists that already understood this stuff while at university!” hit me with all its practical implications. I had to spend time to read books and articles about practical and theoretical aspects of my specific tasks. And in parallel, I also had to fill-in the gaps in my understanding of the basics. But I never fully devoted my time to physics, at least not before 2017.

Given that it is my job, am I even allowed to admit that I still fill-in the basics? Or am I too hard trying to pretend being a physicist, for whatever reasons? I did wonder whether I should do a master in physics, given that it is my job. But what for, just to prove that I am able to fulfil some formal criteria for being a physicist? And I doubt that I would become a physicist in my heart, so it could turn out to be very hard to finish a master degree. But I still like to discuss physics, and I would like to be able to judge certain physical fashions.

The code of silence

What could I have said about the Lightwave Research Laboratory at Columbia University in New York? Nothing, it would have just been name dropping. What could I have said about Information ist Energie by Lienhard Pagel? Something, it might have given the impression of name dropping, and it is the reason for this silent section:

This book uses QM in normal handwaving mode. By information, the author means his definition of dynamic information, which is something like information(flow) per time. Higher energy is normally associated with shorter times. What is good about this book is that it really discusses the time dynamics, which is otherwise often neglected.

What could I have said about quantum field theory? I could have talked about my motivations to learn more about it. But most of those were pointless, because I expect silence, no matter how much I have learned. But Sean Carroll gave me a good reason to learn more about QFT with his lecture Extracting the Universe from the Wave Function. I started with Quantum Field Theory for the Gifted Amateur and the many comments in Quantum Field Theory I, Lecture Notes (HS14+) and Quantum Field Theory II, Lecture Notes (FS17). However, then I read An Interpretive Introduction to Quantum Field Theory cover to cover. It was easy to read, with a good mix of technical details, explanations, interpretations, and philosophical clarification.

… much of the interpretive work Teller undertakes is to understand the relationship and possible differences between quantum field-theory — i.e., QFT as quantization of classical fields — and quantum-field theory — i.e., a field theory of ‘quanta’ which lack radical individuation, or as Teller says, “primitive thisness.”

Not sure when I will continue to work through the more technical material. At the moment, I read How is Quantum Field Theory Possible?, just to see how far I will come, before it gets too boring or too difficult.

A conversation about the Copenhagen interpretation

I had an email conversation with BT in March 2017, where he praised Deutsch’s version of MWI, and I defended Heisenberg’s version of Copenhagen:
28 Feb 2017 BT: purpose of science is explanation
9 Mar 2017 TK: what is Copenhagen
13 Mar 2017 BT: Copenhagen is Bohr
20 Mar 2017 TK: historical defence of Copenhagen
28 Mar 2017 TK: QM as general probability

During that conversation, I did some historical investigations:

When David Bohm proposed his new interpretation in 1952, the term “Copenhagen interpretation” didn’t exist yet, he had to talk of the “usual physical interpretation of quantum theory” instead. The idea that the “Copenhagen interpretation” should be the common core of the beliefs by Bohr and Heisenberg probably goes back to Henry P. Stapp in 1972. Before, it was just another way to refer to the orthodox interpretation(s) taught by (good) text books. Heisenberg is the unfortunate soul who coined the term Copenhagen interpretation (in the 50s).

Here is how I see Heisenberg’s position, independent of whether Bohr agrees:

Max Born and Werner Heisenberg claimed in 1927 that quantum mechanics is a closed theory (abgeschlossene Theorie), just like Newton’s mechanics is a closed theory. And by this they meant that its description of reality is complete and accurate, whenever it is applicable. The limits of applicability are not part of the closed theories themselves, according to Heisenberg.

The conversation started, when I quoted Heisenberg’s own explanation:

… what one may call metaphysical realism. The world, i.e., the extended things, ‘exist’. This is to be distinguished from practical realism, and the different forms of realism may be described as follows: We ‘objectivate’ a statement if we claim that its content does not depend on the conditions under which it can be verified. Practical realism assumes that there are statements that can be objectivated and that in fact the largest part of our experience in daily life consists of such statements. Dogmatic realism claims that there are no statements concerning the material world that cannot be objectivated. Practical realism has always been and will always be an essential part of natural science. Dogmatic realism, however, …

and BT replied:

That’s all a bit technical for me! I can’t tell whether he is in favour of “explanations” in the simple(-minded?) Deutsch sense or not.

After setting the passage in context, I got very concrete:

But I disagree that the quoted passage is technical. If he adheres to this passage, then Heisenberg cannot claim that Schrödinger’s cat would be both alive and dead, or that the moon would not be there if nobody watches.

Others, like Christopher A. Fuchs and Asher Peres in Quantum Theory Needs No Interpretation”, are apparently less sure whether (neo-Copenhagen) quantum theory is so clear about that fact. Hence they try to weasel out by claiming: “If Erwin has performed no observation, then there is no reason he cannot reverse Cathy’s digestion and memories. Of course, for that he would need complete control of all the microscopic degrees of freedom of Cathy and her laboratory, but that is a practical problem, not a fundamental one.”

This is non-sense, because the description of the experiment given previously was complete enough to rule out any possibility for Erwin to reverse the situation. Note the relevance of “… a consistent interpretation of QM as applied to what we do in a physical laboratory and how practitioners experience QM in that context.” If Erwin had access to a time machine enabling him to realistically reverse the situation, then it might turn out that Cathy and Erwin indeed lived multiple times through both situations (and experienced real macroscopic superpositions), as depicted in movies like “Back to the Future”.

According to Jan Faye in the SEP article on the Copenhagen Interpretation, even Bohr does not disagree with that conclusion: “Thus, Schrödinger’s Cat did not pose any riddle to Bohr. The cat would be dead or alive long before we open the box to find out.” However, I doubt that Bohr really said this, or replied to the content of Schrödinger’s article in any other direct way. (I read that he complained to Schrödinger about that article for indirectly supporting Einstein in his crusade against QM.)

Questions about Schrödinger’s famous article

At the end of this article on Erwin Schrödinger there are links to interesting papers by Schrödinger. After reading “Die gegenwärtige Situation in der Quantenmechanik” (“The Present Status of Quantum Mechanics (“Cat” Paper)”), I had several questions:

1. Did Schrödinger know the density matrix formalism? He could have formulated some points he was making more explicit by using it.
2. Did Bohr ever admit that the example of the cat was spot on, and that of course the cat was either dead or alive, even if nobody cared to check?
3. Did Schrödinger know about Fermions and Bosons? The last paragraph talks about how the relativistic theory would make the foregoing discussion invalid.

When I first read Schrödinger’s article in September 2014, I didn’t knew much about quantum mechanics or it history. But I had the hope that my instrumentalist ideas related to the density matrix were not too far off from the orthodox interpretation. Today, I know that Carl Friedrich von Weizsäcker denied that the Copenhagen interpretation asserted: “What cannot be observed does not exist.” Instead, it follows the principle:

What is observed certainly exists; about what is not observed we are still free to make suitable assumptions. We use that freedom to avoid paradoxes.

The interesting thing is that Schrödinger’s article is not really about the cat, and not really about attacking quantum mechanics. Instead, Schrödinger tries to explain his own understanding of it. But Bohr interpreted the article as an attack on his interpretation.

1. Schrödinger at least knew the consequences that follow from the density matrix formalism, so I guess he knew it. Not sure why he does not use it, maybe it was not yet popular among physicists back then.
2. I doubt Bohr ever admitted that Schrödinger was right.
3. Schrödinger knew about Fermions and Bosons. The basic connection between Fermi–Dirac statistics, Bose–Einstein statistics and the spin was already known since 1926. But the first derivations of the spin-statistics theorem from relativistic quantum field theory by Markus Fierz and later by Wolfgang Pauli are from 1939.

However, I guess Schrödinger wrote that last paragraph not just because Fermions and Bosons were challenging to fit into his scheme of explanation. He also wanted to stress that relativistic quantum mechanics was not yet fully worked out, so that he could conclude: “Perhaps, the simple procedure of the nonrelativistic theory is only a convenient calculational trick, but it has at the moment attained a tremendous influence over our basic view of Nature.”

While talking about famous articles by Schrödinger, I want to quote a passage from the beginning of “Are There Quantum Jumps? Part I”:

Along with this disregard for historical linkage there is a tendency to forget that all science is bound up with human culture in general, and that scientific findings, even those which at the moment appear the most advanced and esoteric and difficult to grasp, are meaningless outside their cultural context. A theoretical science, unaware that those of its constructs considered relevant and momentous are destined eventually to be framed in concepts and words that have a grip on the educated community and become part and parcel of the general world picture – a theoretical science, I say, where this is forgotten, and where the initiated continue musing to each other in terms that are, at best, understood by a small group of close fellow travellers, will necessarily be cut off from the rest of cultural mankind; in the long run it is bound to atrophy and ossify, however virulently esoteric chat may continue within its joyfully isolated groups of experts.

I want to quote a passage from the beginning of “Are There Quantum Jumps? Part II”:

Even if this shorthand were admissible for the microevent, we have to keep in mind that physicists are not the only people interested in physics and in the outcome of theoretical research in physics. Those results that are tenable and will survive are destined, eventually, to be absorbed into our world picture and to become part and parcel thereof. A great many of our educated contemporaries, not equipped with the mathematical apparatus to follow our more technical deliveries, are yet deeply concerned with many general questions; one of the most stirring among them certainly is whether actually natura facit saltus or no. Whatever abbreviated language we physicists may find convenient to use among ourselves, we ought to be aware of the dilemmas that justly and duly interest others; we must be careful not to veil or distort them by indulging in loose speech

Conclusions

Why did I wrote this post? Probably because I wanted to share my email conversation about the Copenhagen interpretation. And because I finally managed to read a technical book about quantum field theory cover to cover. However, that part already touches the code of silence, and I really wrote two of the emails (the ones were silence would not hurt me too bad) for which I expected silence (and really got silence as expected). But it was a start, and I am confident that I will finish more of the small stuff in the near future, even if the silence will hurt me more. Writing about Schrödinger was just bonus, or maybe I wanted to avoid having to write about physics again in the near future. But I could do a post about my thoughts on probability, at least that would be related to logic.

ALogTime, LogCFL, and threshold circuits: dreams of fast solutions

Our protagonists are the following (DLogTime-) uniform circuit classes

• NC¹ (ALogTime)
• SAC¹ (LogCFL)
• TC⁰ (threshold circuits)

Interesting things can be said about those classes. Things like Barrington’s theorem (NC¹), closure under complementation by inductive counting (SAC¹), or circuits for division and iterated multiplication (TC⁰). Things like TC⁰ recognises the Dyck language with two types of parentheses, NC¹ recognises visibly pushdown languages, or SAC¹ recognises context free languages. (and also the languages recognisable in nondeterministic logarithmic-space).

But how are those classes related to dreams about speed? There are sometimes situations where both fixed width integers and floating point numbers are problematic, but much faster than better alternatives because of explicit hardware support. The dream is to allow arbitrary alternative number formats getting sufficient hardware support to remain reasonable alternatives to the number formats supported explicitly by current hardware.

ALogTime – fast solutions for predictable stack height

Considering how parameter passing to subroutines and a huge part of memory management in mainstream computer languages is stack based, an obvious and natural variation is to restrict the unbounded memory of a Turing machine to be a stack. With those words, I justified copying a part of my answer to my own question yet another time. During my research for that answer, I also learned about Nested Words and Visibly Pushdown Languages and that they can be recognized in LOGSPACE. Recently, I read

The Boolean formula value problem is in ALOGTIME (25 pages)
https://www.math.ucsd.edu/~sbuss/ResearchWeb/Boolean/paper.pdf
by S Buss – Jan 1987

I immediately suspected that Visibly Pushdown Languages can also be recognized in ALogTime, and that recognition in LOGSPACE is just a simple corollary. Indeed it is:

Complexity of Input-Driven Pushdown Automata (21 pages)
http://research.cs.queensu.ca/~ksalomaa/julk/p47-okhotin.pdf
by A Okhotin, K Salomaa – 2014

The remarks following the proof of theorem 8 (with the beautiful Figure 3 shown above) say: “Finally, Dymond [12] applied the method of Buss [7] to implement the Mehlhorn–Rytter algorithm [36] in NC¹“. Dymond’s paper is short and sweet:

Input-driven languages are in log n depth (4 pages)
https://www.sciencedirect.com/science/article/pii/0020019088901482?via%3Dihub
by P Dymond – 1988

Polynomial size log depth circuits: Between NC¹ and AC¹ by Meena Mahajan gives a different summary of Dymond’s paper:

Dymond gave a nice construction [14] showing that they are in fact in NC¹. His approach is generic and works not just for VPAs but for any PDA satisfying the following:

1. no ϵ moves,
2. an accepting run should end with an empty stack
3. the height of the pushdown, after processing i letters of the input, should be computable in NC¹. If there is more than one run (nondeterministic PDA), and if the height profiles across different runs are different, then the heights computed should be consistent with a single run. Furthermore, if there is an accepting run, then the heights computed should be consistent with some accepting run.

For such PDA, Dymond transforms the problem of recognition to an instance of formula value problem, and then invokes Buss’s ALogTime algorithm [8] for it.

This post links extensively to external material. It is clear that the reader of this post will not read most of it. The more interesting question is whether I have read that material, or at least plan to read it. The initial plan of this post was to indicate which material I have already read and understood, and which material I still plan to read. But this is unpractical and boring for the reader. What I want to say is that I have read Buss’ paper in principle, but didn’t yet work thoroughly enough through section 7, and I don’t understand yet why Buss says (page 10): “However, we shall use the yet stronger property (c) of deterministic log time reducibility. Although it is not transitive, it is perhaps the strongest possible reasonable notion of reducibility.” Why is DLogTime not transitive? In some of the other papers quoted above, I only read the parts which interested me. And here is another paper by Buss et al which I still plan to read:

An optimal parallel algorithm for formula evaluation (42 pages)
https://www.math.ucsd.edu/~sbuss/ResearchWeb/Boolean2/finalversion.pdf
by S Buss, S Cook, A Gupta, V Ramachandran – Nov 20, 1990

Parallel and distributed computing

The main conclusion of the last section is that ALogTime is quite powerful, because it can recognize languages accepted by input driven stack automata. I wondered whether this result is taught in typical introductions to parallel computing. Here is my sample:

Thinking in Parallel: Some Basic Data-Parallel Algorithms and Techniques (104 pages)
http://www.umiacs.umd.edu/users/vishkin/PUBLICATIONS/classnotes.pdf
by Uzi Vishkin – October 12, 2010

Parallel Algorithms (64 pages)
https://www.cs.cmu.edu/~guyb/papers/BM04.pdf
by Guy E. Blelloch and Bruce M. Maggs – 1996

Limits to Parallel Computation: P-Completeness theory (327 pages)
https://homes.cs.washington.edu/~ruzzo/papers/limits.pdf
by R Greenlaw, H Hoover, W Ruzzo – 1995

Parallel Algorithms (347 pages)
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.466.8142&rep=rep1&type=pdf
by H Casanova, A Legrand, Y Robert – 2008

My conclusion is that it is not taught, at least not explicitly. And I already took care that they would talk about ALogTime by saying (uniform) NC¹. Chapter 10 where Uzi Vishkin talks about tree contraction is related, and NC¹ is discussed in some of the texts. (It should be clear that I didn’t really try to read those texts, and just browsed through them.)

Some words on LogCFL and threshold circuits

I looked for hardware support for LogCFL, as seems possible for NC¹

A more promising approach could be to look for problems complete under appropriate many-one reductions for these classes. The word problem for (or ) would be such a problem for NC¹. The solution of that word problem is nicely scalable, since one can subdivide the word into smaller parts, and thereby generate a smaller word on which the same procedure can be applied again.

That many-one reduction to that word problem is Barrington’s theorem proved in

Bounded-width polynomial-size branching programs recognize exactly those languages in NC¹ (15 pages)
https://people.cs.umass.edu/~barring/publications/bwbp.pdf
https://www.sciencedirect.com/science/article/pii/0022000089900378
by David A.Barrington – 1987

One thing which could still go wrong when trying to use TC¹, NC¹, and SAC¹ for actual efficient computer architectures is that those fast and nice many-one reductions are studied to decision problems, but in the end we are much more interested in computing solutions to function problems. This came up when I described my plans to a friend. But I am not the first to dream about hardware support for those theoretical fast solutions:

Explicit Multi-Threading (XMT): A PRAM-On-Chip Vision
A Desktop Supercomputer (4 pages)
http://www.umiacs.umd.edu/users/vishkin/XMT/index.shtml
http://www.umiacs.umd.edu/users/vishkin/XMT/ICCD09proc-version.pdf
by Uzi Vishkin – 2009

Back to LogCFL: for “closure under complementation by inductive counting,” see:

Two applications of inductive counting for complementation problems (20 pages)
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.394.1662&rep=rep1&type=pdf
by A Borodin, S Cook, P Dymond, W Ruzzo, M Tompa – 1989

and for: “SAC¹ recognises context free languages. (and also the languages recognisable in nondeterministic logarithmic-space),” note that LogCFL = AuxPDA(log n, n^O(1)) = SAC¹ see here. This means the class of log n auxiliary pushdown automaton which run in non-deterministic polynomial time. (Probably “non-deterministic” can also be replaced by “deterministic”. The direct meaning of LogCFL is the class of problems which can be many-one reduced to CFL in deterministic logspace.) I also guess that LogCFL can be solved by a dynamic programming algorithm, since both NL and CFL allow such a solution. (Probably an easy exercise. I just wanted to have LogCFL in this post, since it is part of my dream, and allows to solve interesting problems. And it seems close to ALogTime from a hardware perspective.)

Now to threshold circuits: “TC⁰ recognises the Dyck language with two types of parentheses”. I don’t have a good primary reference at the moment. But this shows that threshold circuits are surprisingly close to ALogTime with respect to their capabilities. And “circuits for division and iterated multiplication,” has some references in the wikipedia article, but I liked the following lecture notes:

Lecture 8: Multiplication ∈ TC⁰ (4 pages)
https://users-cs.au.dk/arnsfelt/CT08/scribenotes/lecture8.pdf
by Kristoffer Arnsfelt Hansen – 2008

The paper by P Dymond – 1988 ends with the following speculation:

This result shows that a large class of cfl’s is in log depths, and it is natural to inquire about the possibility that all deterministic cfl’s, which are known to be in log space, might also be in log depth. One dcfl in log space which is not currently known to be recognizable in log depth is the two-sided Dyck language on four letters [5].

Word Problems Solvable in Logspace
https://rjlipton.wordpress.com/2009/04/16/the-word-problem-for-free-groups/
http://cpsc.yale.edu/sites/default/files/files/tr60.pdf
by RJ Lipton, Y Zalcstein – 1977

It is an interesting question whether ALogTime and LOGSPACE are different for naturally occurring problems. Including LogCFL in the hardware acceleration tries to evade this question. But there are programming approaches specifically focusing on LOGSPACE, since it may model an important aspect of practical algorithms for really big data:

Computation-by-Interaction for Structuring Low-Level Computation
http://www2.tcs.ifi.lmu.de/~schoepp/habil.pdf
by U Schöpp – 2014

Understanding whether ALogTime != PH is hard to prove

I was wondering about how to define function classes for ALogTime: How to transform words over an input alphabet to words over an output alphabet. I wondered whether I should write a mail to Emil Jeřábek. Maybe I only wanted to have a reason to write him, but I didn’t. Instead, I googled my way until I understood even much weaker function classes. Then a naive idea for proving ALogTime != PH crossed my mind: Prove some problem complete for ALogTime under some extremely weak many-one reduction. If that would work, it would be sort of a “fool’s mate”, since no genuinely new idea is needed, just a careful application of well known techniques. So when Scott Aaronson said

On reflection, though, Mubos has a point: all of us, including me, should keep an open mind. Maybe P≠NP (or P=NP!) is vastly easier to prove than most experts think, and is susceptible to a “fool’s mate.”

in HTTPS / Kurtz / eclipse / Charlottesville / Blum / P vs. NP, I couldn’t help but ask him about whether my naive idea has any chance of proving ALogTime != PH, even if just for testing whether he really keeps such an open mind. His answer was: “I don’t know enough to give you detailed feedback about your specific approach”. So he keeps an open mind, even if Stephen A. Cook is slightly more open with respect to the possibility that separating P from weaker classes like NL or ALogTime could be within reach of current techniques:

The Tree Evaluation Problem: Towards Separating P from NL (8 pages)
https://www.cs.toronto.edu/~toni/Courses/PvsNP/CS2429.html
https://www.cs.toronto.edu/~toni/Courses/PvsNP/Lectures/lecture6.pdf
by Stephen A. Cook – 2014

This post has many links to papers like the one above. As if I could justify myself for believing that ALogTime can be separated from P by current techniques. But the links show at least that investing time into this topic is an interesting learning experience. The following sections Weak reductions and isomorphism theorems, and DAG automata link to material which I read (or still plan to read) in order to make progress on ALogTime != P.

Weak reductions and isomorphism theorems

DLogTime many-one reduction already look quite weak. (I don’t understand yet why Buss says (page 10): “However, we shall use the yet stronger property (c) of deterministic log time reducibility. Although it is not transitive, it is perhaps the strongest possible reasonable notion of reducibility.” Why is DLogTime not transitive?) One could go weaker by looking at DLogTime-uniform NC⁰ reduction or even DLogTime-uniform projections (each output symbol/bit depends at most on a single input symbol/bit). But recently, people proposed even weaker uniformity notions than DLogTime:

A circuit uniformity sharper than DLogTime (19 pages)
https://hal.archives-ouvertes.fr/hal-00701420/document
by G Bonfante, V Mogbil – May 25, 2012

This proposed rational-uniformity can be summarized as as writing in binary and applying a finite state transducer to that input for computing the circuit description. I haven’t read the full paper yet. Another recently proposed approach uses descriptive complexity for defining very weak uniformity notions:

The lower reaches of circuit uniformity (16 pages)
https://eccc.weizmann.ac.il/report/2011/095/
by C Behle, A Krebs, K-J Lange, P McKenzie – May 12, 2012

I didn’t understand too much of that paper yet. I tried reading revision 0 (didn’t notice that it wasn’t the latest revision), but revision 1 might turn out to be easier to read: “Results are stated in more clear way, and overall readability was improved.”

Another line of attack for making the many-one reductions weaker is to only allow isomorphisms. It may seem counter-intuitive first that this should be possible, but the Schröder-Bernstein theorem can sometimes be adapted. This is described in two classic papers:

Reductions in Circuit Complexity: An Isomorphism Theorem and a Gap Theorem (17 pages)
https://www.sciencedirect.com/science/article/pii/S0022000098915835
http://ftp.cs.rutgers.edu/pub/allender/switch3.pdf
www.cs.cmu.edu/~rudich/papers/ac0reductions.ps
by M Agrawala, E Allender, S Rudich – 1998

Reducing the Complexity of Reductions (9 pages or 22 pages)
https://cseweb.ucsd.edu/~russell/reductions.ps
http://ftp.cs.rutgers.edu/pub/allender/stoc97.pdf
by M Agrawala, E Allender, R Impagliazzo, T Pitassi, S Rudich – 2001

I didn’t read those papers yet, but Algebra, Logic and Complexity in Celebration of Eric Allender and Mike Saks by Neil Immerman gives a nice survey of those results, which I read for a start.

DAG automata

One important property of input driven stack automata is that the dependency graphs will be planar DAGs. For general polynomial time algorithms, the dependency graphs will be general non-planar DAGs (due to variable binding with an unbounded number of variables). In order to learn what is already known about this, I googled “DAG automata”. The first three hits are awesome:

DAG Automata – Variants, Languages and Properties (48 pages)
http://www8.cs.umu.se/education/examina/Rapporter/JohannesBlum_submitted.pdf
by J Blum – May 25, 2015

How Useful are Dag Automata? (26 pages)
https://hal.archives-ouvertes.fr/hal-00077510/document
by S Anantharaman, P Narendran, M Rusinowitch – ‎2004

DAG Automata for Meaning Representation (12 pages)
http://aclweb.org/anthology/W17-3409
by F Drewes – London, UK, July 13–14, 2017

The first and third hit are related, Frank Drewes was the adviser of Johannes Blum. I read both, and they were really worth it. (I only browsed the paper from 2004, just to see that the newer papers really achieved a breakthrough.) They reduce determining which rules are useless to a question about Petri nets, and then provide a solution for that problem: “A Petri net is structurally cyclic if every configuration is reachable from itself in one or more steps. We show that structural cyclicity is decidable in deterministic polynomial time.”

Structurally Cyclic Petri Nets (9 pages)
https://arxiv.org/abs/1510.08331
by F Drewes, J Leroux – ‎2015

On understanding a problem, without solving it

One can understand a problem without solving it. So one can understand why something is a problem and why a solution would be challenging, without being able to come up with a solution. I don’t know whether the best experts in computer science understand P != NP in this sense. I don’t understand it yet, but I have the deeply rooted belief that it can be understood.

And understanding for me also means to be able to read work that others have done, and to see and feel the connection to the questions which interest me.

Conclusions?

This post is too long, but I didn’t really care this time. Since the reader is expected to read at least some of the linked material, it is implicitly even much longer than its nominal length (which is too long) indicates. The initial goal was to write it in order to be able to focus again on more urgent topics. But of course, this didn’t really worked out that way. Still, this post was always intended to be mainly a collection of links to papers I already read or still plan to read in order make progress on understanding ALogTime, LogCFL, and threshold circuits. And I also knew that I would try to justify myself for believing that this topic is worth studying.

Do I believe that the dreams of fast solutions can come true? I don’t know. Uzi Vishkin seems to have made a much more serious effort than I ever will, and even argued his case from an economic perspective:

Alas, the software spiral is now broken: (a) nobody is building hardware that provides improved performance on the old serial software base; (b) there is no broad parallel computing application software base for which hardware vendors are committed to improve performance; and (c) no agreed-upon architecture currently allows application programmers to build such software base for the future

Could proof of work problems for crytocurrency mining provide the incentive to make dreams come true? Who knows, money is important, after all. But personally, I am rather a believer in “constant dripping wears away the stone,” so I think in the long run, it is quite possible that things progress. Probably in ways I cannot even imagine today.

A subset interpretation (with context morphisms) of the sequent calculus for predicate logic

The previous two posts used the sequent calculus with a subset interpretation:

We work with sequents , and interpret the propositions (and ) as subsets of some universe set . We interpret the sequent itself as .

While writing the previous post, there was the temptation to introduce the sequent calculus rules for existential and universal quantification. But the subset interpretation with a fixed universe set didn’t seem helpful for free variables and quantification. But what if we allow different universe sets for different sequents? One way would be to augment the sequent rules to change the universe sets in a well defined way. However, the cut rule and two of the four quantification rules (those that replace an arbitrary term by a quantified variable) are a bit problematic. For them, the universe can sometimes be shrunk down, since a formula or a term was eliminated. Therefore, we just add two separate rules for changing the universe, and apply the sequent rules themselves only with respect to a fixed universe set.

This is the last planed post on the sequent calculus for the moment. (There might be an additional post in this series, extending the subset interpretation to natural deduction.) Since this post will remain vague and unsatisfactory in many ways, a list of related online materials on the sequent calculus seems appropriate: I often consulted the wikipedia article while writing these posts. (I never consulted Sequent Calculus Primer, but it looks nice and has exercises.) This MathOverflow question on introductions to sequent calculus suggests the chapter on Sequent Calculus from Frank Pfenning’s manuscript on Automated Theorem Proving, which I really liked. It also suggests Proofs and Types by Jean-Yves Girard, which was my first introduction to the sequent calculus. It left me unsatisfied, and I agree with Charles Stewart:

A warning: Girard’s style is a little slippery, and it is common for students to say they have read it, who turn out to have absorbed the opinions but little of the results.

I am still slightly ashamed that one of my first questions – when I met a group of academic logicians (with a focus on proof assistants) – was whether they found Girard easy to understand. Girard claims that the sequent calculus is generally ignored by computer scientists, an exception being Logic For Computer Science Foundations of Automatic Theorem Proving by Jean H. Gallier. A nice text, but who has time to read those 500+ pages? This is one reason why I like An Introduction to Proof Theory by Samuel R. Buss.

The sequent calculus rules for predicate logic

We are interested in normal first order predicate logic with predicates and functions. Here a signature with a finite number of predicate and function symbols is given, which include the arity for each of the symbols. The sequent calculus rules for quantification are:

Left quantification rules	Right quantification rules

Those rules look simple, but what do they mean? What is the difference between and ? And how to interpret a sequent with formulas containing free variables? First, is a free variable not occurring in , , or . And means that each free occurrence of in is replaced by . Next, is an arbitrary term, with no restrictions at all on the variables occurring in it. A term is just any reasonable combination of function symbols (from the signature) and variables, like where both and are binary function symbols.

There are many possible interpretations of predicate logic, but that answer just avoids answering the question. The interpretation of a formula or sequent with free variables can be controversial. My previous effort at a subset based interpretations of predicate logic compatible with non-classical logic left out equality, functions and constants. Even so we are talking only about classical logic here, the goal of the following interpretation is to be also applicable more generally. That interpretation will follow naturally once we clarify which models we want to allow.

Models and interpretations of predicate calculus

For the typical interpretations, a model consists of a set (which is the universe where the variables live), a subset of for each -ary predicate symbol, and a function for each -ary function symbol. A straightforward interpretation in that context is that a formula with free variables is a subset of , and a formula without free variables (i.e. a sentence) is either true or false. And for any set of variables, we can interpret any formula whose free variables are included in that set as a subset of . A sequent in this interpretation is true, iff for the subsets formed by the formulas interpreted relative to the set of all free variables in the sequent, the intersection of the subsets on the left side is contained in the union of the subsets on the right side.

This straightforward interpretation above is already a subset interpretation, but we want a slightly more general subset interpretation. For propositional logic, the possible models were given by a set and a subset of for each propositional variable . In predicate logic, the 0-ary predicates take the role of the propositional variables, so we want them to be subsets of . For our generalised interpretation, a model consists of a set (whose subsets are the truth values) and a set (which is the universe where the variables live), a subset of for each -ary predicate symbol, and a function for each -ary function symbol.

The way will enter into the model is to have some implicit context such that formulas like in the formal syntax become in the model. So for any set of free variables, we can interpret any formula whose free variables are included in that set as a subset of . For a given set of variables and a sequent for which the free variables of the formulas are contained in that subset, the a sequent is true, iff for the subsets formed by the formulas interpreted relative that set of variables, the intersection of the subsets on the left side is contained in the union of the subsets on the right side.

(If we have a formula like , we would like to interpret it as a subset of , so we normally use and then just omit it. Here the element is called unit, the set represents truth, and the empty set represents falsehood.)

Context morphisms give life to the subset interpretation

If we have (a sequent of) subsets over , then a (partial) function from to gives us (a sequent of) subsets over by taking inverse images of the subsets. We have

• 
• 
• 

and hence

The direct translation into the language of sequences reads

This just tells us that global substitution is unproblematic. (But is required in case is a partial function, which is easily missed.) However, the more typical function for our purpose is similar to , i.e. a function from to . It is typical, since the expressions grow in complexity for most rules of sequent calculus. Here is an example:

This example also shows, how we can separately change the universe set, and apply the sequent rules only with respect to a fixed universe set. After applying the or rule, we can shrink the universe set. To illustrate, let us first apply the and rule, where we cannot always shrink the universe set:

Here we cannot shrink the universe set.

Now we can shrink the universe set, but only after checking that the sequent no longer depends on . But when we apply , we can always shrink the universe set:

How can we justify this shrinking in terms of images or inverse images? The inverse image under for an arbitrary function (constant) could be a justification. But we don’t really write , and is arbitrary and irrelevant. So the image under might be a nicer justification. But we only have

• 
• 
• 

However, if we assume , then and hence

Doubts about context morphisms and substitutions

Let us apply the above to propositional logic. Surely, from we can deduce . But we cannot justify it from in terms of inverse images. Can we justify it from ? Yes, take the map with . Here and can be arbitrary and . Note that we only need .

How justified are those substitutions into the expressions? Here, we used

Can we justify this? Can such substitutions go wrong? Yes, if is a partial function:

Here fails, but it would work if were a total function. We could have omitted , but then it would fail because of . That was actually the point were I noticed that the restriction is required for partial functions.

The substitutions are justified, because they work for each operation individually:

• 
• 
• 
• 
• 
• 
• 
• 

Treating equality without special rules

Equality can be given by a binary predicate which is a congruence relation for the functions, and compatible with the other predicates. There are different ways to treat equality, and it is important for most interesting applications of predicate logic. A canonical approach is to write the axioms on the left side of the sequent, and use normal deductions. Concrete examples for the required axioms were already given in the last post in the section “Axiomatic theories in predicate logic without falsehood” for the theory of groups and in the section “Axiomatic theories in predicate logic without falsehood” for Robinson arithmetic.

Part of the reason for presenting a subset interpretation for predicate logic was to better understand how predicate logic could work in case of non-classical logics. There are theories like Heyting arithmetic (and Gentzen’s own work), which seem to fit nicely with the interpretation above. But there are also intuitionistic dependent type theories with special rules and equality types, whose possible interpretations remain unclear to me, despite the nice subset interpretation explained above. Maybe Per Martin Löf is right: In the end, everybody must understand for himself (p.166)

Conclusions?

This post was hard for me to write. This is the classical problem when explaining something obvious (predicate calculus). You have to make a lot of words for something which seems obvious, but where the language is missing to properly write down what is going on behind the scenes. I didn’t solve that language problem, but I came up with a natural example of how the obvious thing can fail to be true. That might help the reader to understand for himself.

The content above already became clear to me while writing the previous post. But only after this current post was nearly finished did I notice the restriction in case is a partial function. Which is funny, after I clarified the notion of context morphism which makes sense of that logic without truth from the first post (in this series), I find out that there is an additional restriction that the antecedent should never be empty. My first reaction was that I don’t like this. Maybe I should look for a transformation which turns this logic about partial functions into the logic without negation or falsehood. But my second reaction was that it could make sense, perhaps any logical deduction needs assumptions.

Still the question remains whether there is a reasonable transformation from the logic without truth (and partial functions) to the logic without negation and falsehood. Probably that question will be easy to answer. Somehow one has to take complements, and hope that the structure of the predicate calculus remains intact. It seems to work, but I still have trouble to intuitively understand it. And I want to finish this post now.

Logic without negation and falsehood

In the last post, consideration related to partial functions lead us to present a logic without truth and implication, using the binary minus operation as a dual of implication and substitute for unary negation. But logic without implication and equivalence is strange. So in this post we want to omit negation and falsehood instead.

(This post got surprisingly long. Sometimes I got slightly sidetracked, for example the discussion of the parity function and its sequent rules could have been omitted. But I already tried to remove most of those sidetracks. The real reason for the size explosion are the examples of axiomatic theories in predicate logic. But those had to be discussed, since they make it clear that one can really omit falsehood without loosing anything essential.)

The classical sequent calculus

Before starting to omit logical operations, let us first recall the classical sequent calculus including as many logical operations as barely reasonable. If we limit ourself to constants, unary operations, and binary operations, then we get:

• Constants for truth () and falsehood ()
• An unary operation for negation ()
• Binary operations for: or (), and (), implication (), minus (), nand (), nor (), equivalence (), and xor (). The remaining binary operations add nothing new: reverse implication, reverse minus, first, second, not first, not second, true, and false

We work with sequents , and interpret the propositions (and ) as subsets of some universe set . We interpret the sequent itself as . Let stand for arbitrary finite sequences of propositions.

Left structural rules	Right structural rules

Axiom	Cut

Left logical rules	Right logical rules

The rules for equivalence were taken from here, where they are also proved. Observe that . Clearly is the parity function, which is famous for its computational complexity. It is easy to derive the rules for it (from the rules given above), but those rules have sequents above the line.

The rules for and are obvious. The rules for and are also obvious, if we agree that this should be read as and . Then and , so there is no need for multi-argument versions of nand and nor.

Omitting falsehood from classical logic

If we want to omit falsehood, it is not sufficient to just omit falsehood (). The operations minus () and xor () must be omitted too, since . Also nand () and nor () must be omitted, since and . (They are functionally complete, so the only surprise is the length of the formulas). And if we want to keep truth () or any of the remaining binary operations (or (), and (), implication (), or equivalence ()), then also negation () must be omitted.

But without negation, how can we express the law of excluded middle or double negation? Both and use negation. If we look at proof by cases, then or rather its generalization suggests itself, which is called Peirce’s law. And the sequent calculus suggests , which expresses a nice algebraic property of classical logic. But how do we prove that we get classical logic, and what does that mean?

At least classical tautologies like not using any of the omitted operations should still be tautologies. If “still be tautologies” is interpreted as being provable in the classical sequent calculus, then this follows from cut elimination. The cut elimination theorem says that the rule (Cut) can be avoided or removed from proofs in the sequent calculus. Since for all other rules, the formulas above the line are subformulas of the formulas below the line, only operations occurring in the sequent to be proved can occur in a cut-free proof.

However, my intended interpretation of “still be tautologies” is being provable in the natural deduction calculus. But let us not dive into the natural deduction calculus here, since this post will get long anyway. We still need to clarify what it means that we get classical logic. The basic idea is that logical expressions involving falsehood can be translated into expressions avoiding falsehood, which still mean essentially the same thing. But what exactly can be achieved by such a translation? Time for a step back.

Boolean functions of arbitrary arity

A Boolean function is a function of the form , where is a Boolean domain and is a non-negative integer called the arity of the function. Any Boolean function can be represented by a formula in classical logic. If we omit falsehood, a Boolean function with certainly cannot be represented, for otherwise our goal to remove falsehood would have failed. The question is whether we can represent all Boolean functions with , and whether the complexity of this representation is still comparable to the complexity of the representation where falsehood is available.

A two step approach allows to convert a given representation to one where falsehood is avoided. The first step is to replace by , by , by , by , and by . This step increases the size of the representation only by a small constant factor. The second step is to replace by the conjunction of all input variables. This step increases the size of the representation by a factor in the worst case. It works, since at least one of the input variables is , if is evaluated at an argument different from .

If one can define a new variable, then the factor can be avoided by defining . However, the underlying idea is have a logical constant together with axioms . This is equivalent to the single axiom which simplifies to .

Interpretation of logic without falsehood

When I initially wondered about omitting negation and falsehood from classical logic, I didn’t worry too much about “what it means that we get classical logic” and said

For a specific formula, falsehood gets replaced by the conjunction of all relevant logical expressions.

Noah Schweber disagreed with my opinion that “you can omit negation and falsehood, and still get essentially the same classical logic” and said

First, I would like to strongly disagree with the third sentence of your recent comment – just because (basically) the same proof system is complete for a restricted logical language when restricted appropriately, doesn’t mean that that restricted logic is in any way similar to what you started with.

So I replaced my harmless initial words by

One approach might be to translate as , where is a free propositional variable. It should be possible to show that this works, but if not then we just keep falsehood in the language.

However, these new words are problematic, since is a classical tautology, but is not. My initial words were not ideal too, since the meaning of “the conjunction of all relevant logical expressions” remained unclear.

The intuition behind my initial words was that falsehood is just the bottom element of the partial order from the Boolean algebra. Removing the explicit symbol (name) for the bottom element from the language should be harmless, since the bottom element can still be described as the greatest lower bound of “some relevant elements”. (However, removing the symbol does affect the allowed homomorphisms, since the bottom element is no longer forced to be mapped to another bottom element.)

The intuition behind my new words was an unlucky mix up of ideas from Curry’s paradox and the idea to use a free variable as a substitute for an arbitrary symbol acting as a potentially context dependent replacement for falsehood. We will come back to those ideas in the section on axiomatic theories in predicate logic without falsehood.

What are the “relevant logical expressions” for the conjunction mentioned above? Are , , or relevant logical expressions? The first two are not, since , i.e. the propositional variable itself is already sufficient. The third one is relevant, at least for predicate logic with equality. For propositional logic, it is sufficient to replace falsehood by the conjunction of all proposition variables occurring in the formula (and the assumptions of its proof). For predicate logic, it is sufficient to replace falsehood by the conjunction of the universally quantified predicate symbols, including the equality predicate as seen above (if present).

Axiomatic theories not using negation or falsehood

If the axioms or axiom schemes of an axiomatic theory (in classical first order predicate logic) don’t use negation or falsehood or any of the other operations we had to remove together with falsehood, then we don’t need to explicitly remove falsehood.

Let us look at the theory of groups as one example. If we denote the group multiplication by and the unit by , then the axioms are

• 
• 
• 

We see that neither falsehood nor negation occurs in those axioms. This is actually a bit cheated, since it would seem that implication also doesn’t occur. It actually does occurs in the axioms governing equality. Here are some axioms for equality:

• 
• 
• 

They only use implication, but something like the axiom schema

• 

is still missing. Here is any formula, and may contain more free variables in addition to and . This doesn’t work for us, since this could also include formulas which use negation or falsehood! But at least for the theory of groups, the following two axioms (derived from instances of the axiom scheme) should be sufficient.

• 
• 

Here is a typical theorem of the theory of groups that should now be provable.

Here is an informal proof: Since and , we have . Since and , we have . Since and , we have . If we could show (this was omitted in axioms given above), then the proof would be complete.

Axiomatic theories in predicate logic without falsehood

Let us next look at Robinson arithmetic, which is essentially Peano arithmetic without the induction axiom schema.

1. 
2. 
3. 
4. 
5. 
6. 
7. 

Here are the additional axioms for equality.

• 
• 
• 
• 
• 

Universal quantification has been omitted, but that should not worry us here. We see that the first axiom is the only one using falsehood. We could replace it by

1. 

Or we could also introduce a constant and replace by the axioms

0. 
1. 

The second approach has the advantage that if we add the induction axiom schema to get Peano arithmetic, we can just replace falsehood by the constant . The first approach has the advantage that is shows that falsehood was never really required for the induction axiom schema.

The second approach comes closer to my motivations to remove falsehood from the language. I wanted to avoid negation and falsehood, because if there is no (bottom) element connecting everything together, then the damage caused by the principle of explosion can be restricted to specific domains of discourse. I also had the idea to use more specific propositional constants instead of falsehood. For ZFC set theory, one could use one propositional constant for the axiom asserting the existence of the empty set, and another propositional constant for the axiom asserting regularity. However, as soon as one adds the axioms and , both constants will probably turn out to be equivalent.

Conclusions

Such a long post, for such a trivial thing as removing falsehood from the language. At least it should be clear now that one can really remove falsehood if desired, and what it means that one doesn’t loose anything essential. But is there anything to be gained by removing falsehood? The initial idea to remove falsehood came from the rule (suggested by the sequent calculus), which characterises classical logic by a nice algebraic property (not involving negation or falsehood). The motivation to finish this post came from the realisation that implication is the central part of logic. I just read this recent post by Peter Smith on the material conditional, and realised that one really gains something by removing falsehood: the counterintuitive material conditional goes away, and implication becomes the first class citizen it should have always been.

The counterintuitive part didn’t really disappear. The material conditional decomposes into the two sequents and . The proof sketch for those is and . The proof of the second doesn’t even use the special properties of classical logic, but this part is the counterintuitive one: Why should be true, if ? Well, the intuitive everyday logic is more a sort of modal logic than a propositional or predicate logic.

Logic without truth

Pi is wrong! But so what? It is neither new, nor complicated enough to count as real math! And suggestions that  or  might be even better show that it not clear-cut either.

I recently invested sufficient energy into some logical questions to make real progress. But while telling friends and fellow logicians about it, I realized how irrelevant all my results and conclusions will be. I will have to publish them in an appropriate journal nevertheless, since they continue David Ellerman’s work on partition logic. Not publishing them would be dismissive towards the value of David Ellerman’s work, and he really invested lots of effort into it, and believes in its value. I won’t talk about those results here, since I don’t know how it would impact my ability to publish them.

Let’s have some fun instead, stay extremely close to classical logic, and still demonstrate a logic without truth. And let’s get back to Gerhard Gentzen.

Partial truths

I am fond of partial functions. For a partial function , we have

• 
• 
• 
• where

But is only true if is a total function. Especially is only true (even for specific ) if is total, since otherwise

Let’s also prove one of the other claims:

Note that . So the preserved operations are “and”, “or”, and “xor” if interpreted from a logical perspective. It would be nice if implication were preserved too. This seems hopeless, since is always true, and truth is not preserved. But we do have , which means that the external implication given by the order is preserved. So we should be able to turn this into a logic, where internal truth is not preserved under context morphisms.

Gerhard Gentzen’s sequent calculus

The sequent calculus is a proof calculus with significant practical and theoretical advantages compared to more obvious proof calculus systems. It works with sequents . The propositions (and ) could be logical formulas like (the 4-th Peano axiom). They can also be interpreted as subsets of some universe set , which is sufficient for understanding the basics of the sequent calculus. Then the sequent itself is interpreted as .

Left structural rules	Right structural rules

Here stand for arbitrary finite sequences of propositions. The structural rules may be relatively boring. The following global rules are slightly more interesting

Axiom	Cut

None of the rules up to now has used any logical constant or connective. They can be verified directly for the subset interpretation. The following logical rules can only be verified after the (intended) interpretation of the logical connectives has been fixed.

Left logical rules	Right logical rules

One possible interpretation for these connectives in terms of subsets would be , , , , and .

But it may be more instructive to see an interpretation where one of the classical logical rules is violated. So let us use instead, where is the interior operator of some topological space. The propositions (and ) are interpreted as open subsets in this case. The rule is violated now, and has to be replaced by the rule . This gives us the intuitionistic sequent calculus, which exactly characterizes the valid conclusions of intuitionistic logic.

To see that  is violated, let , correspond to , , and . Above the line we have , which is true. Below the line we have , which is false.

An evil twin of sequent calculus

Note that implication satisfies or rather . Let us replace implication by minus. Note that minus satisfies with . Then we get the following two rules instead of and .

Of course, we also remove and from the language together with the rule . This sequent calculus is still as sound and complete as the original sequent calculus. But we no longer reason about implication, but only about minus. Some sort of implication is still present in , but it is no longer mirrored internal in the language of the logic itself. So this is our logic without truth.

I don’t really know (or understand) whether this sort of context morphism has any sort of relevance, and whether that logic without truth occurs anywhere in the real world. Is there any relation to the fact that it is easier to deny the relevance or truth of a given conclusion than to prove that it is important and true? What I like about that logic is the asymmetry between implication and falsehood, because I wanted to find naturally occurring asymmetries in mathematical hierarchies and logic. Even for the results that I do want to publish, I have the same problem that I don’t really understand the relevance of the corresponding context morphisms, whether there even should be context morphisms, and whether my proposed context morphisms are the correct ones.

Conclusions?

That post initially also contained a logic without falsehood, or rather a logic where falsehood is not used. But it started to get long, and this post is already long enough. Not sure whether this was really a good idea, since the explanation of the sequence calculus was also intended to better understand how such a logic with a reduced set of logical constants and connectives still maintains its main features. Maybe I will manage to create another blog post from the removed material. Or maybe nobody including myself cares anyway, as already indicated at the beginning. Or maybe I should better use my time to finish the paper about the results I wrote about at the beginning, and submit them to…