James Oswald

Yesterday I looked at def∇, a macro for Dyalog APL like self-referencing functions in Lean.

I’ve been writing recursive functions over syntax trees a lot recently.

In fully-observable non-deterministic (FOND) planning, there are three primary types of policies, weak policies, strong policies, and strong cyclic policies.

Recently I came across asympotic inequalities of the form $f(x) \le g(x) + O(1)$ in Li and Vitanyi’s An Introduction to Kolmogorov Complexity and Its Applications, where this notion is used to discuss bounds on the complexity of strings.

Recently I’ve been looking at implementing Higher Order Modal Logic in Lean4, particularly custom quantifiers.

Note This post is about Set.iUnion and tsum, almost exclusively over infinite sequences.

Earlier this week Overleaf went down.

Note This post presents a basic (and most likely naive) typeclass for logic formulae.

As of writing Lean does not seem to have a natural way in the language to extend inductive types.

Warning As of publishing this post, Jai is in active development with regular breaking changes.

Background Link to heading Recently, I was going down the rabbit hole on John McCarthy, best known to me as the inventor of the Situation Calculus but more widely know for the creation the Lisp family of programming languages and his folk designation as o…

I’ve recently had the terrible idea to start looking at the Collatz Conjecture on a hunch there may be an interesting equivalent statement in proof theory.

Background Link to heading I’m currently in the process of writing a post about things I like and things I dislike about Rust.

Warning As of publishing this post, Jai is in active development with regular breaking changes.

Warning As of publishing this post, Jai is in active development with regular breaking changes.

In this post we continue looking at the inference rules of alpha existential graphs, in particular we look at the final two rules of inference, Iteration and Deiteration, and provide some examples.

Background Link to heading This fun second order logic problem is given as an extra credit problem in RPI’s intro to logic class that I TA for.

Diaconescu’s Theorem says that the Axiom of Choice (AOC) implies the Law of Excluded Middle (LEM), but what of the converse?

Background Link to heading Today my colleague Brandon Rozek released a new Lean4 tutorial on his blog.

Warning 3/20/2026 Update: This post was written in early 2024 before the release of the grind tactic, which greatly simplifies some of the proofs.

Note Originally published under the title “Worldbuilding Formal and Aesthetic Magic Systems: A Logicist Mage’s Manifesto”, renamed in April 2025.

Recently while trying to get one of my Github repositories to meet Github’s recommended open source project guidelines, I found myself in need of a code of conduct for my project.

Reasoning over Alpha Existential Graphs Link to heading In the previous post, we have seen how to represent propositional logic statements as existential graphs (EGs) and vice versa, but merely representing logical statements in an alternative format isn’t

In my last AEG post, we looked at an informal definitions of subgraphs for Alpha Existential Graphs (EGs).

Subgraphs, Levels, and Nested Levels Link to heading Last post we looked at what Alpha Existential Graphs represent and how we may build them.

Preamble Link to heading Ever since learning about Existential Graphs (EGs) from a talk given by Bram Van Heuveln [1] at the New York Capital Region Logic Reading Group; I’ve had Existential Graphs on my mind a lot.