The Gap Between How We Think and How We Prove

Natural language is imprecise by design. When we say "every student passed an exam," we might mean each student passed at least one exam (possibly different exams), or that there exists a single exam everyone passed. In conversation, context resolves these ambiguities. In formal reasoning, they become logical errors.

First-order logic (FOL) eliminates this ambiguity. Developed by Gottlob Frege in 1879 and independently by Charles Sanders Peirce in 1885, FOL provides a precise language for expressing statements about objects, their properties, and their relationships. It's the foundation of modern mathematics, database query languages, and automated theorem proving.

The problem: learning FOL notation is a barrier. LOGICAFFEINE removes that barrier.

What LOGICAFFEINE Does

LOGICAFFEINE is an English-to-FOL transpiler built on LOGOS. You write sentences in plain English:

"Every philosopher who teaches logic influences some student."

LOGICAFFEINE parses the sentence using Montague semantics — a framework developed by mathematician Richard Montague that treats natural language with the same rigor as formal languages — and outputs the corresponding logical formula:

∀x((Philosopher(x) ∧ TeachesLogic(x)) → ∃y(Student(y) ∧ Influences(x, y)))

The universal quantifier (∀) was introduced by Gerhard Gentzen in 1935, derived from a rotated "A" for "all." The existential quantifier (∃) was introduced by Giuseppe Peano in 1896, derived from a rotated "E" for "exists." LOGICAFFEINE outputs both Unicode symbols and LaTeX notation.

Why This Matters Now

The rise of AI systems that can engage in complex reasoning — like Anthropic's Claude, which uses Constitutional AI to reason about ethical constraints — has renewed interest in formal logic as a verification layer. If an AI system claims to have proven something, how do we verify the proof?

Formal verification tools like the Z3 theorem prover can check logical validity, but they require input in formal notation. LOGICAFFEINE bridges this gap: you express your reasoning in English, and we produce verifiable formal logic.

This matters for:

  • Critical thinking education — see exactly what your arguments claim, no symbolic notation required
  • AI alignment research — express constraints in natural language, verify them formally
  • Software specification — describe requirements in English, generate testable formal specifications
  • Legal and policy analysis — identify logical ambiguities in contract language or regulations

The Technology

LOGICAFFEINE uses a parsing architecture inspired by research in computational linguistics. The lexer classifies words using a curated vocabulary database. The parser builds abstract syntax trees using techniques from the Open Logic Project, a collaborative effort to create open-source logic education materials. The transpiler generates FOL following the notation conventions established in forall x, a free textbook used in university logic courses worldwide.

Get Started

Visit the Learn page for an interactive curriculum starting from first principles, or jump directly into the Studio to experiment with your own sentences.

Formal logic has been the foundation of rigorous reasoning since Aristotle. LOGICAFFEINE makes it accessible to anyone who can write a sentence.