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: Vx 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, Vxy 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 Vxyz' exists, then all of its genera exist: Vx, Vy, Vz', Vxy, Vxz', Vyz' — 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 Vx exists and the species V'xy' does not, then the missing species Vxy 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 VxVx'VyVy'VzVz' … 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.

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:

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 VxVx' 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	Vxy
O x y	Some x is not y	Vxy'
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	Vx'y
O' x y	Some non-x is not y	Vx'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

$ 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:

$ 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.

$ 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.