# Logic in Reazon I: Generating Sentences of Modal Logic

Here’s a description of the language of modal logic from Boolos’s *The Logic of Provability*:

Modal sentences.Fix a countably infinite sequence of distinct objects, of which the first five are`⊥`

,`→`

,`□`

,`(`

,`)`

, and the others are the sentence letters… Modal sentences will be certain finite sequences of these objects. We shall use`A`

,`B`

, … as variables over modal sentences. Here is an inductive definition of:modal sentence(1)

`⊥`

is a modal sentence;(2) each sentence letter is a modal sentence;

(3) if

`A`

and`B`

are modal sentences, so is`(A → B)`

; and(4) if

`A`

is a modal sentence, so is`□(A)`

.[We shall very often write:

`(A → B)`

and:`□(A)`

as:`A → B`

and:`□A`

.]Sentences that do not contain sentence letters are

letterless. For example,`⊥`

,`□⊥`

, and`□⊥ → ⊥`

are letterless sentences.

It’s easy to translate this into a definition in Reazon miniKanren:

And given such a definition, it’s even easier to generate instances:

- ⊥
- _0
- (□ ⊥)
- (□ _0)
- (⊥ → ⊥)
- (⊥ → _0)
- (□ (□ ⊥))
- (□ (□ _0))
- (
_{0}→ ⊥) - (
_{0}→ _1)

All possible modal logic sentences would eventually be generated from that definition.

It’s also easy to add new syntax, like the negation operator `¬`

.

We can also tweak the definition to generate specific subsets of sentences. For example, the letterless sentences mentioned above contain some interesting cases, like `¬□⊥ → ¬□¬□⊥`

. Under the provability interpretation of modal logic, this sentence says that if there is no proof of a falsehood then there is no proof that there is no proof of a falsehood, i.e. Goedel’s second incompleteness theorem.

To get the letterless sentences, simply don’t include the sentence letters.

- ⊥
- (¬ ⊥)
- (¬ (¬ ⊥))
- (□ ⊥)
- (⊥ → ⊥)
- (¬ (¬ (¬ ⊥)))
- (□ (¬ ⊥))
- (¬ (□ ⊥))
- (¬ (⊥ → ⊥))
- (⊥ → (¬ ⊥))

We’re getting some interesting sentences, like `(¬ (□ ⊥))`

, but also a lot of junk, like `(⊥ → ⊥)`

and `(¬ (¬ (¬ ⊥)))`

. We can fix this by applying `¬`

only to sentences beginning with `□`

and by applying `→`

only to compound sentences.

- ⊥
- (¬ (□ ⊥))
- (□ ⊥)
- (¬ (□ (¬ (□ ⊥))))
- (¬ (□ (□ ⊥)))
- (□ (¬ (□ ⊥)))
- (¬ (□ (¬ (□ (¬ (□ ⊥))))))
- (□ (□ ⊥))
- (¬ (□ (¬ (□ (□ ⊥)))))
- (¬ (□ (□ (¬ (□ ⊥)))))
- (□ (¬ (□ (¬ (□ ⊥)))))
- (¬ (□ (¬ (□ (¬ (□ (¬ (□ ⊥))))))))
- ((¬ (□ ⊥)) → (¬ (□ ⊥)))
- (¬ (□ (□ (□ ⊥))))
- (□ (¬ (□ (□ ⊥))))
- (¬ (□ (¬ (□ (¬ (□ (□ ⊥)))))))
- ((¬ (□ ⊥)) → (□ ⊥))
- (□ (□ (¬ (□ ⊥))))
- (¬ (□ (¬ (□ (□ (¬ (□ ⊥)))))))
- (¬ (□ (□ (¬ (□ (¬ (□ ⊥)))))))
- (□ (¬ (□ (¬ (□ (¬ (□ ⊥)))))))
- (¬ (□ (¬ (□ (¬ (□ (¬ (□ (¬ (□ ⊥))))))))))
- ((¬ (□ ⊥)) → (¬ (□ (¬ (□ ⊥)))))

The twenty-third statement generated from this definition is `((¬ (□ ⊥)) → (¬ (□ (¬ (□ ⊥)))))`

, the modal logic statement of the second incompleteness theorem. Further on can be found its converse `((□ ⊥) → (□ (¬ (□ ⊥))))`

, and further still can be found `((□ ⊥) → (□ (□ ⊥)))`

, an instance of one of the Hilbert-Bernays derivability conditions.

We can also generate *substitution instances*. Take the *modal distribution axiom* `((□ (A → B)) → ((□ A) → (□ B)))`

.

- ((□ (⊥ → ⊥)) → ((□ ⊥) → (□ ⊥)))
- ((□ (⊥ → (¬ (□ ⊥)))) → ((□ ⊥) → (□ (¬ (□ ⊥)))))
- ((□ ((¬ (□ ⊥)) → ⊥)) → ((□ (¬ (□ ⊥))) → (□ ⊥)))
- ((□ (⊥ → (□ ⊥))) → ((□ ⊥) → (□ (□ ⊥))))
- ((□ (⊥ → (¬ (□ (¬ (□ ⊥)))))) → ((□ ⊥) → (□ (¬ (□ (¬ (□ ⊥)))))))
- ((□ ((¬ (□ ⊥)) → (¬ (□ ⊥)))) → ((□ (¬ (□ ⊥))) → (□ (¬ (□ ⊥)))))
- ((□ ((□ ⊥) → ⊥)) → ((□ (□ ⊥)) → (□ ⊥)))
- ((□ (⊥ → (¬ (□ (□ ⊥))))) → ((□ ⊥) → (□ (¬ (□ (□ ⊥))))))
- ((□ ((¬ (□ ⊥)) → (□ ⊥))) → ((□ (¬ (□ ⊥))) → (□ (□ ⊥))))
- ((□ (⊥ → (□ (¬ (□ ⊥))))) → ((□ ⊥) → (□ (□ (¬ (□ ⊥))))))

Notice that the third result, `((□ ((¬ (□ ⊥)) → ⊥)) → ((□ (¬ (□ ⊥))) → (□ ⊥)))`

, contains the contrapositive of the second incompleteness theorem as its consequent.