KRIPKE

Setup

To install dependencies:

bun install

To run:

bun run index.ts

This project was created using bun init in bun v1.1.33. Bun is a fast all-in-one JavaScript runtime.

Rules

• A Kripke frame with 4 worlds is generated.
• The game tells you how many accessibility relations are in the frame, but not the exact shape of it.
• You have a total of 10 moves. In each move you can do one of the following:
  • Enter a modal formula.
    • The game tells you in how many worlds the formula is valid (for every valuation).
  • Guess the Kripke frame.
    • If your frame is equal or isomorphic to the secret frame, you win.
• You lose when you run out of moves.

A typical gameplay looks like this:

Run !help for available commands.
A new Kripke frame is created! It has 4 worlds and 4 relations.
[10] Lp -> p
valid in 1 worlds, invalid in the rest.
[9] ~L0
valid in 3 worlds, invalid in the rest.
[8] ML0
valid in 1 worlds, invalid in the rest.
[7] (Lp -> p) & ML0
invalid.
[6] M(Lp -> p) & ML0
invalid.
[5] M(Lp -> p)
valid in 2 worlds, invalid in the rest.
[4] !guess aRa, bRc, bRd, dRa
incorrect.
[3] !guess aRa, bRc, dRa, dRb
incorrect.
[2] !guess aRa, bRc, dRa, dRc
incorrect.
[1] !guess aRa, bRc, dRa, aRd
correct! congratulations!!
id: 389
a ==> a
a ==> c
b ==> d
c ==> a

Syntax

See syntax.ts for details.

Formulae

You may use the following symbols:

• propositional variables, p, q, r, s (four are enough)
• verum: T, ⊤, 1, \top
• falsum: F, ⊥, 0, \bot
• negation: ~, ¬, \neg, \lnot
• box modality: [], □, L, \Box
• diamond modality: <>, ⋄, M, \Diamond
• conjunction: &, ^, ∧, \wedge, \land
• disjunction: |, v, ∨, \vee, \lor
• implication: ->, →, \rightarrow, \to, \implies
• equivalence: <->, ↔, \leftrightarrow, \iff
• parentheses: (, )

All operators are right associative.

Frames

You may use the following symbols:

• worlds: a, b, c, d
• accessibility relation: R, <, ≺, \prec
• comma: , (to separate relations)

License

MIT