diff --git a/packages/kripke/syntax.ts b/packages/kripke/syntax.ts
index df01341..ac06634 100644
--- a/packages/kripke/syntax.ts
+++ b/packages/kripke/syntax.ts
@@ -51,3 +51,101 @@ export const or = (left: Formula, right: Formula) =>
   ({ type: "or", left, right }) as const satisfies Formula;
 export const iff = (left: Formula, right: Formula) =>
   ({ type: "iff", left, right }) as const satisfies Formula;
+
+export type Symbols = Record<Exclude<Formula["type"], "propvar">, string>;
+
+export const asciiSymbols: Symbols = {
+  top: "T",
+  bot: "F",
+  box: "[]",
+  diamond: "<>",
+  not: "~",
+  and: "^",
+  or: "v",
+  to: "->",
+  iff: "<->",
+};
+
+export const unicodeSymbols: Symbols = {
+  top: "⊤",
+  bot: "⊥",
+  box: "□",
+  diamond: "⋄",
+  not: "¬",
+  and: "∧",
+  or: "∨",
+  to: "→",
+  iff: "↔",
+};
+
+export const latexSymbols: Symbols = {
+  top: "\\top",
+  bot: "\\bot",
+  box: "\\Box",
+  diamond: "\\Diamond",
+  not: "\\neg",
+  and: "\\land",
+  or: "\\lor",
+  to: "\\to",
+  iff: "\\leftrightarrow",
+};
+
+export function prettyPrint(
+  fml: Formula,
+  config?: { paren?: boolean | ((fml: Formula) => boolean); symbols?: Symbols },
+): string {
+  const { paren = false, symbols = unicodeSymbols } = config ?? {};
+  const withParen = (s: string) =>
+    (typeof paren === "boolean" ? paren : paren(fml)) ? `(${s})` : s;
+
+  switch (fml.type) {
+    case "top":
+      return symbols.top;
+    case "bot":
+      return symbols.bot;
+    case "propvar":
+      return fml.name;
+    case "not":
+      return `${symbols.not}${prettyPrint(fml.fml, { paren: true, symbols })}`;
+    case "box":
+      return `${symbols.box}${prettyPrint(fml.fml, { paren: true, symbols })}`;
+    case "diamond":
+      return `${symbols.diamond}${prettyPrint(fml.fml, { paren: true, symbols })}`;
+    case "and": {
+      const newConfig: typeof config = {
+        symbols,
+        paren: (f) => f.type !== "and",
+      };
+      return withParen(
+        `${prettyPrint(fml.left, newConfig)} ${symbols.and} ${prettyPrint(fml.right, newConfig)}`,
+      );
+    }
+    case "or": {
+      const newConfig: typeof config = {
+        symbols,
+        paren: (f) => f.type !== "or",
+      };
+      return withParen(
+        `${prettyPrint(fml.left, newConfig)} ${symbols.or} ${prettyPrint(fml.right, newConfig)}`,
+      );
+    }
+    case "to": {
+      const newConfig: typeof config = {
+        symbols,
+        paren: (f) => f.type !== "to",
+      };
+      return withParen(
+        `${prettyPrint(fml.left, { symbols, paren: true })} ${symbols.to} ${prettyPrint(fml.right, newConfig)}`,
+      );
+    }
+    case "iff": {
+      const newConfig: typeof config = {
+        symbols,
+        paren: (f) => f.type !== "iff",
+      };
+      return withParen(
+        `${prettyPrint(fml.left, newConfig)} ${symbols.iff} ${prettyPrint(fml.right, newConfig)}`,
+      );
+    }
+  }
+}