# Deductive Solver

A *definition* of *x* may be called a rule that divides every existing (and every conceivable) individual object in our world into two parts: those that match the definition *x*, and those that do not, *¬x*.

While the subject sciences build up a conceptual apparatus, logic studies how concepts relate to one another. Concepts live over the set of all objects under consideration.

As the Polish mathematical tradition on the one hand and N. P. Brusentsov on the other rightly point out, the symbol of "existence" of some object, written as ∃, is in fact closely related to disjunction, ∨. Specifically, it is an "integral" disjunction — a disjunction over a set: V*x* means that we run through every object checking it against *x*, and if at least one of them fits, then the set-wide disjunction holds over the whole set as well.

By extending sets to three-valued ones — in which an element may be definitely present, definitely absent, or free — we can examine logical concepts in all of their relations.

Modern mathematical logic normally combines the features of objects (or anti-features, i.e. failures to match a feature) using Boolean algebra, without three-valued sets. That approach is very successful at describing a single object within a conceptual system fixed in advance. At the same time, it is a poor fit for describing **systems**: more precisely, it forces systems to be described as single objects, which is usually deeply unnatural.

The solution is to consider the algebra of three-valued sets over *combinations* of concepts. For example, V*xy* means that somewhere in the set of objects there exists an object combining the features *x* and *y*, whereas V'*xy*' means the opposite: there is no *x* without *y* (which, under additional assumptions, is the relation of entailment).

This idea is discussed in the books of the team that built the "Setun" computer — above all in the books of N. P. Brusentsov. It is presented most fully in his *Foundations of Informatics* (Начала информатики) and *The Art of Reliable Reasoning* (Искусство достоверного рассуждения).

The deductive solver works with compound logical concepts (for example *xy'z* — an event or object combining *x*, not-*y*, and *z*) and with facts (set-wide disjunctions over such concepts, or negations of those disjunctions).

## The four rules (Lewis Carroll's diagram)

Charles Dodgson, better known as Lewis Carroll, studied questions of logic intensively. He devised a tabular diagram — somewhat reminiscent of a cellular automaton or a game — that allows logical computation to be carried out. Generalizing it, one can state four rules applied to concepts, two of which are "obvious" and two of which create "new" information:

1. **Upward truth (obvious).** "If the species V*xyz*' exists, then all of its genera exist: V*x*, V*y*, V*z*', V*xy*, V*xz*', V*yz*' — and moreover the indeterminate something V exists (the wholly unspecific concept)."

2. **Downward falsity (obvious).** "If the genus V'*xy*' does not exist, then none of its species exist either, for example V'*xy*'*z* and V'*xy*'*z*'."

3. **Downward truth (new).** "If the genus V*x* exists and the species V'*xy*' does not, then the missing species V*xy* that completes the genus is guaranteed to exist."

4. **Upward falsity (new).** "If both species fail to exist, V'*xy*' and V'*xy*, then the genus V'*x* does not exist either."

Applying these rules to the already known facts for as long as any information ("obvious" or "new") keeps being produced, we eventually obtain every logical relation that holds in the system of concepts.

## On Aristotle's categorical syllogisms

For Aristotle's traditional categorical syllogisms — and for entailment in the natural-language sense of the word — one must additionally require that every elementary concept is neither empty nor total, that is, that V*x*V*x*'V*y*V*y*'V*z*V*z*' … holds for all concepts *x*, *y*, *z*, …

This is what the `--aristotle` flag does (see below).

## Building

The project is plain GHC with no external dependencies; `shell.nix` provides a suitable environment.

```sh
nix-shell            # optional, if you use Nix
ghc -o solver Main.hs
```

To build the syllogism test runner, compile `Tests/Test.hs` from the project root (it imports the `Ternary.*` modules) and feed it `Tests/syllotest`:

```sh
ghc -i. -o syllotest Tests/Test.hs
./syllotest < Tests/syllotest
```

## Usage

```
solver [PARAMETERS]
```

Statements are read from **standard input**, one per line, and results are written to standard output.

| Parameter | Meaning |
| --- | --- |
| `-A`, `--aristotle` | Use the Aristotelian universe: assume V*x*V*x*' for every concept *x* mentioned in the input (no concept is empty or total). |
| `-n`, `--new` | Print only "new" facts, omitting those that were given in the input. |
| `--prove` | Proof mode: check whether the first input line follows from the remaining ones. |
| `-h`, `--help` | Show the built-in help. |
| `-v`, `--version` | Show the version. |

Parameters are checked in the order `--help`, `--version`, `--prove`, then normal solving. Note that `--prove` always runs with the Aristotelian universe and ignores `-A` and `-n`.

### Input format

Each line is a Haskell-readable value of type `Statement String`:

```
Statement KIND "subject" "predicate"
```

Both terms must be quoted. `KIND` is one of the eight traditional forms — `A`, `E`, `I`, `O` and their primed variants `A'`, `E'`, `I'`, `O'`, in which the *first* term is negated:

| Kind | Reads as | Equivalent fact |
| --- | --- | --- |
| `A x y` | Every *x* is *y* | V'*xy*' |
| `E x y` | No *x* is *y* | V'*xy* |
| `I x y` | Some *x* is *y* | V*xy* |
| `O x y` | Some *x* is not *y* | V*xy*' |
| `A' x y` | Every non-*x* is *y* | V'*x*'*y*' |
| `E' x y` | No non-*x* is *y* | V'*x*'*y* |
| `I' x y` | Some non-*x* is *y* | V*x*'*y* |
| `O' x y` | Some non-*x* is not *y* | V*x*'*y*' |

A statement that would place a term and its own negation under the same V — such as `Statement A "x" "x"` — is rejected with an error.

### Output format

Facts are printed in Brusentsov's notation, with a **backtick** standing for negation (the `'` used in the prose above):

- `Vxy` — there exists an object that is both *x* and *y*;
- `` V`xy` `` — there exists no object that is *x* but not *y* (i.e. every *x* is *y*);
- a backtick immediately after `V` negates the whole set-wide disjunction; a backtick after a term name negates that term.

### Example: solving

```sh
$ printf 'Statement A "man" "mortal"\nStatement A "Socrates" "man"\n' | ./solver
V`manmortal`
V`Socratesman`
V`mortal`Socrates
```

The third line is the conclusion of the syllogism *Barbara*: there is no non-mortal Socrates — that is, Socrates is mortal.

With the Aristotelian universe and only the newly derived facts:

```sh
$ printf 'Statement A "man" "mortal"\nStatement A "Socrates" "man"\n' | ./solver -A -n
V`mortal`Socrates
VmortalmanSocrates
VSocrates`man`mortal`
```

### Example: proving

In `--prove` mode the **first** line is the statement to be proved and the remaining lines are the premises. Three blocks are printed, separated by blank lines: the knowledge derived from the premises *together with* the statement, the knowledge derived from the premises alone, and the verdict.

```sh
$ printf 'Statement A "Socrates" "mortal"\nStatement A "man" "mortal"\nStatement A "Socrates" "man"\n' | ./solver --prove
[V`Socratesmortal`,V`manmortal`,V`Socratesman`,VmortalmanSocrates,VSocrates`man`mortal`]

[V`manmortal`,V`Socratesman`,V`mortal`Socrates,VmortalmanSocrates,VSocrates`man`mortal`]

Just True
```

The verdict is one of:

| Verdict | Meaning |
| --- | --- |
| `Just True` | The statement follows from the premises — adding it yields no new knowledge. |
| `Just False` | The statement contradicts the premises. |
| `Nothing` | Undetermined: the statement neither follows from nor contradicts the premises. |