Recent content on James Oswald
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. In this post I give a brief definition of what this notation means and how it relates to standard asymptotic notation. Particulary, I’m only going to…
Recently I’ve been looking at implementing Higher Order Modal Logic in Lean4, particularly custom quantifiers. Isabelle/HOL makes this quite easy, with a built in binder notation mechanism for defining custom quantifiers. Lean4 does not have this feature, but it does have a powerful macro system that allows us to implement custom syntax and pretty printing to achieve the same effect.…
Note This post is about Set.iUnion and tsum , almost exclusively over infinite sequences. We will make use of Finset.sum and by proxy but not focus on it. Examples tested in Lean version 4.23.0. Recently I’ve started using Lean4 and Mathlib for formalizing things like countable additivity and variants, for probability measures and semimeasures. i.e $P$ has countable additivity iff for all…
Earlier this week Overleaf went down. Not that you would ever know, as their status page still, days later, says nothing at all happened. Crowd sourced status sites like downdetector and isitdownrightnow tell a different story, with 100s of comments complaining about the outage. So surely this must be a bug in Overleaf’s status checking software right? I asked myself this question curiously…
As of writing Lean does not seem to have a natural way in the language to extend inductive types. In this post I contextualize the issue with a simple example of formulae, discuss what I would like out of inductive extension, and discuss some approaches to mimicking the desired behavior. Lets begin with an example to demonstrate what we mean by extending inductive types. For this example we look…
Note This post presents a basic (and most likely naive) typeclass for logic formulae. If you want more serious formulae typeclasses with a proven track record of being used to prove big results, I suggest looking at the recent incredible logic formalization work going on in the Foundation project which aims to formalize core mathematical logic results in lean, and has already completed…
Warning As of publishing this post, Jai is in active development with regular breaking changes. Any information or code in this post may be outdated or deprecated! Note This Post was originally written February 2nd, 2025 but only published April 22nd, 2025. I held onto it and forgot about it in my drafts folder because it did not feel very original, particularly after borrowing so much from…
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 one of the “founding fathers” of artificial intelligence. While digging into him, I came across a very interesting letter sent to…
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. While looking though the Wikipedia article I found an elegant algorithm that finds Collatz sequences for odd numbers represented as binary strings. The part about repeatedly dividing by two caught my eye, and the whole thing looked like a…
Background Link to heading I’m currently in the process of writing a post about things I like and things I dislike about Rust . One of the major things I like about Rust is their implementation of sum types and Inductive types . I like Rust’s sum types so much infact, that the section talking about them in that future post became large enough to become its own post (this post).
Warning As of publishing this post, Jai is in active development with regular breaking changes. Any information or code in this post may be outdated or deprecated! Last post we looked at Jai’s powerful standard library and probably praised it too much for making what others would probably call a bad decision: including too much specific stuff in the standard. But you know what, it brought me…
Warning As of publishing this post, Jai is in active development with regular breaking changes. Any information or code in this post may be outdated or deprecated! On Performance Link to heading While not mentioned much on my blog, back in the day (circa 2018) I considered myself something of a programming languages junkie and C/C++ evangelist, who’s job was to purge the internet of unholy…
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. Iteration and Deiteration Link to heading This inference rule states we can introduce a copy of a subgraph $\phi$ at any nested level in relation to $\phi$. Recall that we say a subgraph $\psi$ is at a…
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. It is sometimes given as a required problem in the intermediate logic class. In these classes, students must use the HyperSlate graphical interactive theorem prover . Here, I take a look at a proof in Lean4 as well. The Problem Link to heading Given…
Diaconescu’s Theorem says that the Axiom of Choice (AOC) implies the Law of Excluded Middle (LEM), but what of the converse? Does the Law of Excluded Middle imply the Axiom of Choice? The answer is no. Background Link to heading I recently ran into a situation where I wanted to prove something was equivalent to the axiom of choice (Specifically the Law of Trichotomy ). Remembering…
Background Link to heading Today my colleague Brandon Rozek released a new Lean4 tutorial on his blog. Brandon really likes for people to be able to read his proofs (for some unknown reason). I decided to write this companion piece where I showcase what Lean4 looks like when you don’t care if people can read it. Towards this end I will be golfing Brandon’s tutorial, that is, going for…
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. Readers interested in a more modern survey of approaches to proving the correctness of insertion sort in Lean 4 should check out this excelent post by Anthony Wang . Background Link to heading When I first started learning Lean almost a year ago now, in…
Note Originally published under the title “Worldbuilding Formal and Aesthetic Magic Systems: A Logicist Mage’s Manifesto”, renamed in April 2025. A Logicist Mage’s Manifesto Link to heading Dungeons and Dragons and the consequences of its magic system has been a disaster for the human race. The notions of (1) tiered magic, and (2) distinct well-thought-out spells that can be…
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. Github offers two default options for you to pick from: The Contributor Covenant used by some of the worlds largest open source projects, such as Linux, git, Tensorflow. The Citizen Code of Conduct is a general…
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 all that interesting on its own. In order for existential graphs to be useful, they should provide us some means of reasoning over…
In my last AEG post , we looked at an informal definitions of subgraphs for Alpha Existential Graphs (EGs). In this post we look at a simple (and inefficient) potential recursive definition for the set of subgraphs of an AEG in the tree representation from the last post. Given a function $C(G)$ that returns the children of $G$, and $\mathcal{P}(s)$ is the powerset of $s$ (the set of all subsets of…
Subgraphs, Levels, and Nested Levels Link to heading Last post we looked at what Alpha Existential Graphs represent and how we may build them. In the next post we will look at how we may reason with them using rules of inference. However, before we discuss inference rules for existential graphs, we need to discuss three important “syntactic” (2d syntactic!) concepts in existential…
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. Not only due to their very real ability as a tool for helping students learn logic and the benefits they offer as a formal system in overcoming an inference rule count vs proof…
About Me Link to heading You can find my CV here (Current as of 7/3/2026). Hello, my name is James Oswald! I am PhD student at Rensselaer Polytechnic Institute and graduate researcher with the The Rensselaer Artificial Intelligence and Reasoning (RAIR) Laboratory , under Professor Selmer Bringsjord and the CATS Laboratory under Professor Thomas Macaulay Ferguson . My primary research interest is…
Contact Link to heading If you contact me on anything besides these, it is unlikely I will see it. Personal Email: jamesoswald111@gmail.com University Email: oswalj@rpi.edu Discord Username: tenebrislux Deprecated Link to heading At one time I was able to be reached through these, this is no longer the case. Currently this serves as a fun list of some of my past emails.
My Profiles Link to heading Check me out on the following platforms. Core Profiles Link to heading Google Scholar DBLP Github LinkedIn Research Profiles Link to heading Please note the following platforms may have incorrect information on my publications. The best way to see a fully correct and curated list is on my Google Scholar or DBLP .