This page contains a few exercises based on Basil Smith's Elementary Theory of Relations. To get familiar with the theory, you can try to prove the exercises using Jitpro in your browser. The higher order theorem prover LEO-II (working with the first order theorem prover E) can prove all the exercises in milliseconds (as of 2008).

Basil Smith's Elementary Theory of Relations

Basil Smith talked about an elementary theory of relations at CAMELEON 08. This theory has one sort U and a ternary relation Cog on U. Cog x y z is intended to mean "y relates x to z". In Jitpro, we specify this as follows.

It is also helpful to declare some names for variables ranging over U.

Next we give a number of definitions corresponding to those given in Basil Smith's talk.

Here are a few "easy to prove" claims from the talk:

LEO-II Versions

The definitions in thf syntax for Leo-II are here. Files with the claims in thf syntax for Leo-II are given below.

Jitpro/LEO-II Exercises

1. Sing implies Cls (thf file for Leo-II)

2. Op implies Jec (thf file for Leo-II)

3. Cls implies Trans, Sym, and Refl (thf file for Leo-II)

4. Prim implies Clas and Trans (thf file for Leo-II)

5. Jec and Cls implies Sing (thf file for Leo-II)