I want to share this live playground for FOL, an old system from the late 70s. It has many precursor ideas about reasoning at the meta-level, including the now common proof by reflection which turns proving in the object theory into evaluation in the meta theory, and is common in Rocq, Lean, and other proof assistants.
No comments yet.