The integers are sometimes formally constructed as the equivalence classes of ordered pairs of natural numbers 
so that 
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 
(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 Computer Arithmetic with Continued Fractions by Jean Vuillemin, 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 Vuillemin 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.
(or 
) would be such a problem for NC1. 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.
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:
, and interpret the propositions 
(and 
) as subsets of some universe set 
. We interpret the sequent itself as ![[A_{1}]\cap\ldots\cap [A_{r}]\ \subseteq\ [B_{1}]\cup\ldots\cup [B_{s}]](https://s0.wp.com/latex.php?latex=%5BA_%7B1%7D%5D%5Ccap%5Cldots%5Ccap+%5BA_%7Br%7D%5D%5C+%5Csubseteq%5C+%5BB_%7B1%7D%5D%5Ccup%5Cldots%5Ccup+%5BB_%7Bs%7D%5D&bg=ffffff&fg=333333&s=0 "[A_{1}]\cap\ldots\cap [A_{r}]\ \subseteq\ [B_{1}]\cup\ldots\cup [B_{s}]")
.![\begin{array}{c} \Gamma,A[t/x]\vdash\Delta\\ \hline \Gamma,\forall xA\vdash \Delta \end{array}(\forall L)](https://s0.wp.com/latex.php?latex=%5Cbegin%7Barray%7D%7Bc%7D+%5CGamma%2CA%5Bt%2Fx%5D%5Cvdash%5CDelta%5C%5C+%5Chline+%5CGamma%2C%5Cforall+xA%5Cvdash+%5CDelta+%5Cend%7Barray%7D%28%5Cforall+L%29&bg=ffffff&fg=333333&s=0 "\begin{array}{c} \Gamma,A[t/x]\vdash\Delta\\ \hline \Gamma,\forall xA\vdash \Delta \end{array}(\forall L)")
![\begin{array}{c} \Gamma\vdash A[t/x],\Delta\\ \hline \Gamma\vdash \exists xA,\Delta \end{array}(\exists R)](https://s0.wp.com/latex.php?latex=%5Cbegin%7Barray%7D%7Bc%7D+%5CGamma%5Cvdash+A%5Bt%2Fx%5D%2C%5CDelta%5C%5C+%5Chline+%5CGamma%5Cvdash+%5Cexists+xA%2C%5CDelta+%5Cend%7Barray%7D%28%5Cexists+R%29&bg=ffffff&fg=333333&s=0 "\begin{array}{c} \Gamma\vdash A[t/x],\Delta\\ \hline \Gamma\vdash \exists xA,\Delta \end{array}(\exists R)")
![\begin{array}{c} \Gamma,A[y/x]\vdash\Delta\\ \hline \Gamma,\exists xA\vdash \Delta \end{array}(\exists L)](https://s0.wp.com/latex.php?latex=%5Cbegin%7Barray%7D%7Bc%7D+%5CGamma%2CA%5By%2Fx%5D%5Cvdash%5CDelta%5C%5C+%5Chline+%5CGamma%2C%5Cexists+xA%5Cvdash+%5CDelta+%5Cend%7Barray%7D%28%5Cexists+L%29&bg=ffffff&fg=333333&s=0 "\begin{array}{c} \Gamma,A[y/x]\vdash\Delta\\ \hline \Gamma,\exists xA\vdash \Delta \end{array}(\exists L)")
![\begin{array}{c} \Gamma\vdash A[y/x],\Delta\\ \hline \Gamma\vdash \forall xA,\Delta \end{array}(\forall R)](https://s0.wp.com/latex.php?latex=%5Cbegin%7Barray%7D%7Bc%7D+%5CGamma%5Cvdash+A%5By%2Fx%5D%2C%5CDelta%5C%5C+%5Chline+%5CGamma%5Cvdash+%5Cforall+xA%2C%5CDelta+%5Cend%7Barray%7D%28%5Cforall+R%29&bg=ffffff&fg=333333&s=0 "\begin{array}{c} \Gamma\vdash A[y/x],\Delta\\ \hline \Gamma\vdash \forall xA,\Delta \end{array}(\forall R)")
and 
? And how to interpret a sequent with formulas containing free variables? First, 
, 
, or 
. And ![A[y/x]](https://s0.wp.com/latex.php?latex=A%5By%2Fx%5D&bg=ffffff&fg=333333&s=0 "A[y/x]")
means that each free occurrence of 
in 
where both 
and 
are binary function symbols.
(which is the universe where the variables live), a subset of 
for each 
-ary predicate symbol, and a function 
for each 
for each 
for each 
such that formulas like 
in the formal syntax become 
in the model. So for any set 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.
, 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.)
from 
to 
of the subsets. We have
![p^{-1}([A_{1}])\cap\ldots\cap p^{-1}([A_{r}])\ \subseteq\ p^{-1}([B_{1}])\cup\ldots\cup p^{-1}([B_{s}])](https://s0.wp.com/latex.php?latex=p%5E%7B-1%7D%28%5BA_%7B1%7D%5D%29%5Ccap%5Cldots%5Ccap+p%5E%7B-1%7D%28%5BA_%7Br%7D%5D%29%5C+%5Csubseteq%5C+p%5E%7B-1%7D%28%5BB_%7B1%7D%5D%29%5Ccup%5Cldots%5Ccup+p%5E%7B-1%7D%28%5BB_%7Bs%7D%5D%29&bg=ffffff&fg=333333&s=0 "p^{-1}([A_{1}])\cap\ldots\cap p^{-1}([A_{r}])\ \subseteq\ p^{-1}([B_{1}])\cup\ldots\cup p^{-1}([B_{s}])")
is required in case 
is a partial function, which is 
, 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:
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:
for an arbitrary function (constant) 
could be a justification. But we don’t really write  \vdash [\forall x P(x)](c)](https://s0.wp.com/latex.php?latex=%5B%5Cforall+xP%28x%29%5D%28c%29+%5Cvdash+%5B%5Cforall+x+P%28x%29%5D%28c%29&bg=ffffff&fg=333333&s=0 "[\forall xP(x)](c) \vdash [\forall x P(x)](c)")
, and 
is arbitrary and irrelevant. So the image under 
might be a nicer justification. But we only have
![F^{-1}(F([A_i]))=[A_i]](https://s0.wp.com/latex.php?latex=F%5E%7B-1%7D%28F%28%5BA_i%5D%29%29%3D%5BA_i%5D&bg=ffffff&fg=333333&s=0 "F^{-1}(F([A_i]))=[A_i]")
, then ![F([A_i]\cap\dots\cap [A_r])=F([A_i])\cap\dots\cap F([A_r])](https://s0.wp.com/latex.php?latex=F%28%5BA_i%5D%5Ccap%5Cdots%5Ccap+%5BA_r%5D%29%3DF%28%5BA_i%5D%29%5Ccap%5Cdots%5Ccap+F%28%5BA_r%5D%29&bg=ffffff&fg=333333&s=0 "F([A_i]\cap\dots\cap [A_r])=F([A_i])\cap\dots\cap F([A_r])")
and hence![F([A_{1}])\cap\ldots\cap F([A_{r}])\ \subseteq\ F([B_{1}])\cup\ldots\cup F([B_{s}])](https://s0.wp.com/latex.php?latex=F%28%5BA_%7B1%7D%5D%29%5Ccap%5Cldots%5Ccap+F%28%5BA_%7Br%7D%5D%29%5C+%5Csubseteq%5C+F%28%5BB_%7B1%7D%5D%29%5Ccup%5Cldots%5Ccup+F%28%5BB_%7Bs%7D%5D%29&bg=ffffff&fg=333333&s=0 "F([A_{1}])\cap\ldots\cap F([A_{r}])\ \subseteq\ F([B_{1}])\cup\ldots\cup F([B_{s}])")
we can deduce 
. But we cannot justify it from 
in terms of inverse images. Can we justify it from 
? Yes, take the map 
with , [C\to D](c,d))](https://s0.wp.com/latex.php?latex=%28c%2Cd%29+%5Cto+%28%5BC%5Clor+D%5D%28c%2Cd%29%2C+%5BC%5Cto+D%5D%28c%2Cd%29%29&bg=ffffff&fg=333333&s=0 "(c,d) \to ([C\lor D](c,d), [C\to D](c,d))")
. Here 
and 
can be arbitrary and 
. Note that we only need 
., [C\to D](c,d))=[(C\lor D)\land (C\to D)](c,d)](https://s0.wp.com/latex.php?latex=%5BA%5Cland+B%5D%28%5BC%5Clor+D%5D%28c%2Cd%29%2C+%5BC%5Cto+D%5D%28c%2Cd%29%29%3D%5B%28C%5Clor+D%29%5Cland+%28C%5Cto+D%29%5D%28c%2Cd%29&bg=ffffff&fg=333333&s=0 "[A\land B]([C\lor D](c,d), [C\to D](c,d))=[(C\lor D)\land (C\to D)](c,d)")
)\vdash [B(\cdot)](p(y))\\ \hline [\top](y)\vdash [B(p(\cdot))](y)\\ \hline \top\vdash B(p(y)) \end{array}](https://s0.wp.com/latex.php?latex=%5Cbegin%7Barray%7D%7Bc%7D+%5Ctop%5Cvdash+B%28x%29%5C%5C+%5Chline+%5B%5Ctop%5D%28p%28y%29%29%5Cvdash+%5BB%28%5Ccdot%29%5D%28p%28y%29%29%5C%5C+%5Chline+%5B%5Ctop%5D%28y%29%5Cvdash+%5BB%28p%28%5Ccdot%29%29%5D%28y%29%5C%5C+%5Chline+%5Ctop%5Cvdash+B%28p%28y%29%29+%5Cend%7Barray%7D&bg=ffffff&fg=333333&s=0 "\begin{array}{c} \top\vdash B(x)\\ \hline [\top](p(y))\vdash [B(\cdot)](p(y))\\ \hline [\top](y)\vdash [B(p(\cdot))](y)\\ \hline \top\vdash B(p(y)) \end{array}")
) = [\top](y)](https://s0.wp.com/latex.php?latex=%5B%5Ctop%5D%28p%28y%29%29+%3D+%5B%5Ctop%5D%28y%29&bg=ffffff&fg=333333&s=0 "[\top](p(y)) = [\top](y)")
fails, but it would work if 
, but then it would fail because of 
. That was actually the point were I noticed that the restriction ) = [\bot](y)](https://s0.wp.com/latex.php?latex=%5B%5Cbot%5D%28p%28y%29%29+%3D+%5B%5Cbot%5D%28y%29&bg=ffffff&fg=333333&s=0 "[\bot](p(y)) = [\bot](y)")
) = [A](p(y))\land [B](p(y))](https://s0.wp.com/latex.php?latex=%5BA%5Cland+B%5D%28p%28y%29%29+%3D+%5BA%5D%28p%28y%29%29%5Cland+%5BB%5D%28p%28y%29%29&bg=ffffff&fg=333333&s=0 "[A\land B](p(y)) = [A](p(y))\land [B](p(y))")
) = [A](p(y))\lor [B](p(y))](https://s0.wp.com/latex.php?latex=%5BA%5Clor+B%5D%28p%28y%29%29+%3D+%5BA%5D%28p%28y%29%29%5Clor+%5BB%5D%28p%28y%29%29&bg=ffffff&fg=333333&s=0 "[A\lor B](p(y)) = [A](p(y))\lor [B](p(y))")
) = [A](p(y))-[B](p(y))](https://s0.wp.com/latex.php?latex=%5BA-B%5D%28p%28y%29%29+%3D+%5BA%5D%28p%28y%29%29-%5BB%5D%28p%28y%29%29&bg=ffffff&fg=333333&s=0 "[A-B](p(y)) = [A](p(y))-[B](p(y))")
) = [A](p(y))\oplus [B](p(y))](https://s0.wp.com/latex.php?latex=%5BA%5Coplus+B%5D%28p%28y%29%29+%3D+%5BA%5D%28p%28y%29%29%5Coplus+%5BB%5D%28p%28y%29%29&bg=ffffff&fg=333333&s=0 "[A\oplus B](p(y)) = [A](p(y))\oplus [B](p(y))")
) = \forall z [A](p(y))](https://s0.wp.com/latex.php?latex=%5B%5Cforall+z+A%5D%28p%28y%29%29+%3D+%5Cforall+z+%5BA%5D%28p%28y%29%29&bg=ffffff&fg=333333&s=0 "[\forall z A](p(y)) = \forall z [A](p(y))")
) = \exists z [A](p(y))](https://s0.wp.com/latex.php?latex=%5B%5Cexists+z+A%5D%28p%28y%29%29+%3D+%5Cexists+z+%5BA%5D%28p%28y%29%29&bg=ffffff&fg=333333&s=0 "[\exists z A](p(y)) = \exists z [A](p(y))")
) = [A(p(\cdot))](y)](https://s0.wp.com/latex.php?latex=%5BA%28%5Ccdot%29%5D%28p%28y%29%29+%3D+%5BA%28p%28%5Ccdot%29%29%5D%28y%29&bg=ffffff&fg=333333&s=0 "[A(\cdot)](p(y)) = [A(p(\cdot))](y)")
)
)
), 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
stand for arbitrary finite sequences of propositions.
. Clearly 
is the 
sequents above the line.
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.
. Also nand (
and 
. (They are functionally complete, so the only surprise is the length of the formulas). And if we want to keep truth (
and 
use negation. If we look at proof by cases, then 
or rather its generalization 
suggests itself, which is called 
, which expresses a nice algebraic property of classical logic. But how do we prove that we get classical logic, and what does that mean?
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.
, where 
is a Boolean domain and 
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.
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 
, if 
.
. However, the underlying idea is have a logical constant 
. This is equivalent to the single axiom 
which simplifies to 
.
, where 
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.
, 
, 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).
and the unit by 
, then the axioms are
is any formula, and may contain more free variables in addition to 
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.
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.
and replace by the axioms
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.
goes away, and implication becomes the first class citizen it should have always been.
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.
or 
might be even better show that it not clear-cut either.
, we have
where 
is only true if 
is only true (even for specific 
. 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 
(the 4-th Peano axiom). They can also be interpreted as subsets of some universe set ![[\bot]:=\emptyset](https://s0.wp.com/latex.php?latex=%5B%5Cbot%5D%3A%3D%5Cemptyset&bg=ffffff&fg=333333&s=0 "[\bot]:=\emptyset")
, ![[\top]:=X](https://s0.wp.com/latex.php?latex=%5B%5Ctop%5D%3A%3DX&bg=ffffff&fg=333333&s=0 "[\top]:=X")
, ![[A\land B]:=[A]\cap [B]](https://s0.wp.com/latex.php?latex=%5BA%5Cland+B%5D%3A%3D%5BA%5D%5Ccap+%5BB%5D&bg=ffffff&fg=333333&s=0 "[A\land B]:=[A]\cap [B]")
, ![[A\lor B]:=[A]\cup [B]](https://s0.wp.com/latex.php?latex=%5BA%5Clor+B%5D%3A%3D%5BA%5D%5Ccup+%5BB%5D&bg=ffffff&fg=333333&s=0 "[A\lor B]:=[A]\cup [B]")
, and ![[A\to B]:=[A]^c\cup [B]](https://s0.wp.com/latex.php?latex=%5BA%5Cto+B%5D%3A%3D%5BA%5D%5Ec%5Ccup+%5BB%5D&bg=ffffff&fg=333333&s=0 "[A\to B]:=[A]^c\cup [B]")
.![[A\to B]:=\mathrm{int}([A]^c\cup [B])](https://s0.wp.com/latex.php?latex=%5BA%5Cto+B%5D%3A%3D%5Cmathrm%7Bint%7D%28%5BA%5D%5Ec%5Ccup+%5BB%5D%29&bg=ffffff&fg=333333&s=0 "[A\to B]:=\mathrm{int}([A]^c\cup [B])")
instead, where 
is the interior operator of some topological space. The propositions 
. This gives us the intuitionistic sequent calculus, which exactly characterizes the valid conclusions of intuitionistic logic.
is violated, let 
, ![[A]=(0,\infty)](https://s0.wp.com/latex.php?latex=%5BA%5D%3D%280%2C%5Cinfty%29&bg=ffffff&fg=333333&s=0 "[A]=(0,\infty)")
, 
, and 
. Above the line we have 
, which is true. Below the line we have ![\mathbb R \subseteq \mathrm{int}((-\infty,0])\cup (0,\infty)](https://s0.wp.com/latex.php?latex=%5Cmathbb+R+%5Csubseteq+%5Cmathrm%7Bint%7D%28%28-%5Cinfty%2C0%5D%29%5Ccup+%280%2C%5Cinfty%29&bg=ffffff&fg=333333&s=0 "\mathbb R \subseteq \mathrm{int}((-\infty,0])\cup (0,\infty)")
, which is false.
or rather ![[C]\cap [A] \subseteq [B] \Leftrightarrow [C] \subseteq [A\to B]](https://s0.wp.com/latex.php?latex=%5BC%5D%5Ccap+%5BA%5D+%5Csubseteq+%5BB%5D+%5CLeftrightarrow+%5BC%5D+%5Csubseteq+%5BA%5Cto+B%5D&bg=ffffff&fg=333333&s=0 "[C]\cap [A] \subseteq [B] \Leftrightarrow [C] \subseteq [A\to B]")
. Let us replace implication by minus. Note that minus satisfies ![[A] \subseteq [B]\cup [C] \Leftrightarrow [A-B] \subseteq [C]](https://s0.wp.com/latex.php?latex=%5BA%5D+%5Csubseteq+%5BB%5D%5Ccup+%5BC%5D+%5CLeftrightarrow+%5BA-B%5D+%5Csubseteq+%5BC%5D&bg=ffffff&fg=333333&s=0 "[A] \subseteq [B]\cup [C] \Leftrightarrow [A-B] \subseteq [C]")
with ![[A-B]:=[A]{}\setminus{}[B]](https://s0.wp.com/latex.php?latex=%5BA-B%5D%3A%3D%5BA%5D%7B%7D%5Csetminus%7B%7D%5BB%5D&bg=ffffff&fg=333333&s=0 "[A-B]:=[A]{}\setminus{}[B]")
. Then we get the following two rules instead of 
and 
. 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.