“Providing a sound and complete semantics for NL is an open problem in connexive logic.” —Heinrich Wansing, SEP
This project is a vibe-specified, vibecoded attempt to solve this open problem. I only began this because, when I threw the problem at ChatGPT for kicks, it spat out something that looked correct even to my math-understanding friends. Now I’m trying to finish it so as to give humanity a working semantics for these axioms.
The project consists of a human-readable semantics in Markdown+Latex which is at ChatGPT_semantics.md, and a Lean attempt to formalize it. The current version of this semantics has been rewritten to match the Lean and is also available here.
As of now, the project seems basically correct, I’m just looking over it a bit more.