README

FOL Idris

I'm definitely not the first person to do this, but I had an idea a while back for correct by construction FOL terms and formulas in a dependently typed language, and finally got around to playing with it, and it is very cool. The idea is I have a type Term representing a term in some first order language, and a type Formula representing a formula in that language. Then, through some careful applications of dependent types, it is only possible to construct well-formed formulas. For example, suppose the signature N contains a binary function symbol Plus, a nullary function symbol (i.e. constant symbol) Zero, and a unary function symbol S. Then you can construct the term Plus(Zero, S(Zero)), but Plus(S(Zero(Zero), Zero)) doesn't type check.

Where things start to get really cool is that you can do the same thing with a proof object. So Proof is a type representing a proof, but only correct proofs can even be constructed. Typically you'd have representations of terms, formulas, and proofs, but then would have to write code to verify them; verify that the proof is correct and that the terms and formulas are well formed. You can also very easily play with different logics by just tweaking the constructors of Proof. For example, by removing the constructor Contra from Proof, and adding some other constructors that become necessary, you'd have an intuitionist logic. As it stands, the rules and connectives are extremely minimal, with derived rules existing as proofs in the Logic module¹.

I don't really have a goal with this project, and have just been working on it for fun. There's tons more work that can be done. As it stands, this is far less capable/usable than my last proof assistant, but I think it's pretty cool. It's pretty similar to lisa, but with a more trusted kernel and far less usability.

---

¹

EqRefl and EqTrans are provable from EqE, but using EqE is quite difficult in general, at least without the theorem elimBinder (inc t) s = t stating that adding a variable you don't use to a term then substituting it doesn't do anything, but I was struggling to prove that, not being familiar with Idris's capabilities as a proof assistant.