# About Carnap

“The acceptance or rejection of abstract linguistic forms, just as the acceptance or rejection of any other linguistic forms in any branch of science, will finally be decided by their efficiency as instruments, the ratio of the results achieved to the amount and complexity of the efforts required. To decree dogmatic prohibitions of certain linguistic forms instead of testing them by their success or failure in practical use, is worse than futile; it is positively harmful because it may obstruct scientific progress.

Let us grant to those who work in any special field of investigation the freedom to use any form of expression which seems useful to them; the work in the field will sooner or later lead to the elimination of those forms which have no useful function. Let us be cautious in making assertions and critical in examining them, but tolerant in permitting linguistic forms.”

Carnap is a free and open-source Haskell framework for creating and exploring formal languages, logics, and semantics. It lets you quickly and straightforwardly define languages, construct logics for those languages, and stipulate their semantics. Carnap then uses your specifications to figure out how to check proofs in a variety of formal systems using your logic, how to find the meanings of compound expressions, and a whole lot more.

## Demos

Here are some quick examples of what Carnap can do.

This is a proofbox with a Kalish and Montague System for Propositional Logic. You can directly manipulate the proof by typing in the proofbox, and see the effects of your changes by mousing over the line-decorations on the right hand side.

This is a rendering proofbox with a Kalish and Montague System for Propositional Logic, which also visually displays the structure of the proof being developed.

This is a rendering proofbox with Hardegree's variation on a Montague system.

This is a proofbox with a Fitch system, using rules from *the Logic Book*
and visually rendering the proof structure in the Fitch style.

This is a proofbox with a Kalish and Montague System for First-Order Logic, displaying a proof of Russell's Theorem.

This is a proof with Goldfarb's Lemmon-style system of natural deduction, from the textbook *Deductive Logic*.

Here’s a proof of the fact that the bisectors of the sides of a triangle always meet at a point (from the assumption that a point is on the bisector of a segment if and only if it’s equidistant from the endpoints of that segment). ‟F(x,y)” abbreviates that ‟x is on y“, ‟g(y,z)” abbreviates ‟the bisector of the segment given by y and z”, and ‟h(x,z)” abbreviates ‟the distance from x to z”.

(Because of the number of variables, this one may take a moment to load initially. Once loaded, it should respond quickly to changes.)

Here are two more proofs of Russell's theorem, this time using a version of system QL,
from P.D. Magnus' free and open textbook Forall x,
and the system FOL from the Calgary remix
of *Forall x.*
Note that we've
changed how formulas are parsed (dropping the parentheses around
the arguments to predicates), to match the display
style of *Forall x.*

This is a proofbox with a Kalish and Montague System for Monadic Second-Order Logic, showing how to prove an instance of the comprehension scheme, using a predicate abstraction rule.

This is a proof that every relation has an inverse, in a system of arbitrarily (finitely) Polyadic Second-Order Logic, again making use of a predicate abstraction rule.

This is a proof that the powerset of a transitive set is transitive (exercise 3, chapter 3.3 from Velleman's
*How to Prove It*), in a system of elementary set theory.

Here are proofs of axioms 5 and B within natural deduction systems for propositional modal logics K5 and KTB, in the style of Hardegree's Modal Logic.

These use Fira Logic for nicer-looking logical symbols and use guards to help visually indicate the scope of each subproof.

Here's a proof of the Barcan Formula within a naïvely quantified system of modal logic, based on the system MPL of Hardegree's Modal Logic.

Carnap also includes a JSON API, making it possible to create pure JavaScript GUIs that use Carnap under
the hood for in-browser proof checking. Here's an example
of such a GUI, adapted from Kevin Klement's forallx proofchecker
using P.D. Magnus' *Forall x*
system SL.

## What's Carnap for?

Carnap is intended for use by educators, students, and researchers working on logic. Carnap makes it possible for educators to create interactive exercises and teaching materials, and for students to get quick and helpful feedback as they learn semantic and syntactic methods for determining what follows from what. Carnap also enables researchers interested in unorthodox formal systems to rapidly prototype proof-checking and semantic tools for computer-assisted logical investigation.

## How can I use Carnap right now?

You can use Carnap to teach your own logic class!

All you need to do is create an account, and then get in touch to register as an instructor.

Once you're an instructor, you can use this site—the one you're on right now, carnap.io—to run your class and automatically grade
homework. You can either assign problems from the free
textbook hosted here, or you can use your own
textbook and create automatically graded problem-sets for your own
preferred system. Carnap currently supports truth-tables and
translation and parsing exercises, as well as deductions
compatible with formal systems used in Kalish and Montague's
*Logic*, Bergmann and Moore's *Logic Book*,
Hardegree's *Modal Logic*, P.D. Magnus' *Forall x*,
and the Calgary Remix of *Forall x*. But the ambition of
the project is maximum coverage. So if your favorite system isn't
supported, let us know and we'll see about adding it.

Some tutorials for potential instructors can be found here.

## Why “Carnap”?

Carnap is named after Rudolf Carnap, the philosopher quoted above.

Carnap (the philosopher) famously advocated a tolerant and experimental approach to logic. Carnap (the program) is pluralistic by design. Inference rules are specified declaratively, making it easy to add new logics to those already provided for a given language. The algorithms for checking whether inferences are correct are applicable to a wide variety of languages, making it easy to introduce new languages.

Carnap (the philosopher) also had a lot to say about logical types, and how ignoring them can leave you with beliefs that don’t work very well. Carnap (the program) is written in Haskell, a statically-typed pure functional programming language that uses a theory of logical types to ensure code correctness.

## How does Carnap work?

Well, it's a little technical. There are a couple of different tricks involved.

Essentially, Haskell's type system makes it possible to represent different lexical categories as datatypes, to combine these lexical category datatypes into a larger datatype representing a lexicon (using something like the method described in this paper), and to define a language as the result of applying different elements of a lexicon to one another in a grammatical way.

The upshot is that, using Carnap, you can define a language as the result of snapping together predefined lexical categories. Thanks to Haskell's typeclasses, your languages will inherit various useful properties that their constituent lexical categories carry along with them (for example, languages that contain the lexical category for Boolean connectives will automatically know how to parse and display the symbol for “and”, or how to compute the semantic value of a conjunction from the semantic values of its conjuncts). And, because of Haskell's static typing and the trick of representing lexical categories as types, you're guaranteed that any programming mistake potentially resulting in an ungrammatical expression will be detected when you try to compile the program.

By representing a large class of languages uniformly (as the result of snapping together lexical categories), we also end up being able to manipulate them uniformly. In particular, we can use entirely generic algorithms for things like variable substitution, semantic evaluation, β-normalization, higher-order unification… all the good stuff that you need in order to, for example, check proofs for correctness using only a declaration of acceptable inference rules. As a result, we only need to write code for these algorithms once; we can then automatically use that code with any language that can be defined in the Carnap framework.

So that's the gist of it. If you'd like to learn more about the details, you can inspect the code, talk to a developer, or take a look at this paper.

## How can I get involved?

If you’d like to support Carnap, please consider starring us on Github. If you have suggestions, feature requests, or bug-reports, you can create an issue on Github. For general questions or discussion, you can also reach us on Gitter, on Matrix on IRC at irc://irc.freenode.net/carnap, or over email.

If you’d like to contribute some code to the project—anything from a new unification algorithm to a CSS tweak or pandoc template—just put in a pull request!