**Instructions**. Write a formula in the textbox, click Decide, and

*tzimtsum*will tell you if that formula is true or false.

Click the example links in the Introduction to try them out! Syntax and semantics are described below.

This form will send your formula to the server.

To use tzimtsum locally, you can download the x86-64 Linux binary or compile the source code.

### Introduction

**Have you ever wanted to know if there's a largest natural number?**

`Ex.Ay.(>= x y)`

*There exists an x such that for all y, x is greater than
or equal to y.*

**Or if a natural plus a positive natural could ever equal itself?**

`Ex.Ey.La=0.(and (> y a) (+ x y x))`

*Let a = 0. There exist x, y for which y is greater than a and x plus y
equals x.*

**Or if there are infinite even numbers?**

`Ax.Ey.Ez.(and (> y x) (+ z z y))`

*For all x, there exists y that is larger than x and
is two times some z.*

**Or if there exist x, y, z with n greater than 2 for which
x ^{n} + y^{n} = z^{n} is satisfiable?**

Well, *tzimtsum* can't help you with that last one. But it will let
you decide the truth of *any* proposition involving quantifiers,
addition, and comparisons (but not variable multiplication).

That's because Presburger arithmetic is a decidable theory, although the runtime is lower bounded by a double exponential in the number of nested quantifiers!

*tzimtsum* uses the automata-based solution given in Michael
Sipser's Introduction to the Theory of Computation (6.2).

### tzimtsum Syntax and Semantics

The*tzimtsum*syntax is strict.

First, a series of quantifiers, either existential (E) or universal (A) and the variables they bind, separated by periods.

Then a series of literals (L), the variable it binds, an equals sign, and the natural number it binds to, separated by periods.

Then a formula using those variables and literals.

Be careful! Too many universals or too large of a formula will quickly grow too expensive to compute.

If a variable is not quantified over or bound to a literal, it defaults to zero.

*tzimtsum*accepts the following relations, which take in variables or literals and return a boolean.

- (<= a b) [true iff a is less than or equal to b]
- (< a b)
- (>= a b)
- (> a b)
- (= a b)
- (+ a b c) [true iff a plus b equals c]
- (+ a b c d)

*tzimtsum*accepts the following logical connectives, which take in booleans and return a boolean.

- (not x)
- (and x y)
- (or x y)
- (if x y) [equivalent to (or (not x) y)]

*tzimtsum*is written in Haskell, and uses Parsec for parsing input. Interested readers can check out the source code, contributors welcome!

Comments and suggestions can be mailed to surya at [this domain name].

> *In the magical art of Steganography, there is nothing frivolous, nor
contrary to the Gospels and the Catholic faith; nor have we taught
superstitious beliefs. Everything is based on natural, lawful and honest
principles; the mystery which veils the precepts of this art and the names
of the spirits, requires a cultivated reader; to hide the secrets of this
art, which could be harmful if made known to wicked men, we avail ourselves
of the services of the spirits.*

*tzimtsum is dedicated to my Friend, my Maybe Monad of Indiscriminate
Embrace. Uniform Whiskey!*