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.”

Rudolf Carnap, Empiricism Semantics and Ontology

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.

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 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.

Documentation 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.

Who Uses Carnap?

Carnap was initially developed at Kansas State University, but is now used at dozens of colleges and universities around the world. Here's an (incomplete) list:

  • Arizona State University
  • Bard College at Simon's Rock
  • Boise State
  • Brigham Young University
  • California State University, Chico
  • California State University, Northridge
  • Institute of Philosophy, University of Zielona Gora, Poland
  • Kansas State University
  • McGill University
  • Mississippi State University
  • Northwestern University
  • Old Dominion University
  • Pacific University
  • Pepperdine University
  • Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio), Brazil
  • Tarleton State University
  • The American University in Cairo
  • The University of Alabama at Birmingham
  • University at Albany, State University of New York
  • University of Calgary
  • University of California, Davis
  • University of California, San Diego
  • University of California, Santa Cruz
  • University of Cincinnati
  • University of Illinois at Chicago
  • University of Illinois, Urbana Champaign
  • Université de Lorraine, Nancy France
  • University of Michigan, Ann Arbor
  • University of Puget Sound
  • University of Victoria
  • University of Wisconsin, Madison

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 Matrix which is bridged on IRC at ircs://irc.libera.chat:6697/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!