“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 stipluate 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.
Here are some quick examples of what Carnap can do.
This is a proofbox with a Kalish and Montegue 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 Montegue 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 Montegue 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 Montegue System for First-Order Logic, displaying a proof of Russell's Theorem.
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 Montegue 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.
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.
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.
Basically, 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 read the documentation.
How can I use Carnap?
Carnap also powers Kansas State University's Introduction to Formal Logic and Introduction to Symbolic Logic I, allowing instructors to write problem sets in pandoc, handling the grading, and allowing students to build up a repetoire of derived rules and lemmas that they can use in their work. If you're interested in teaching your own logic class using Carnap, please don't hesitate to get in touch.
Other applications (including a command-line tool and a standalone desktop application) are in the works.
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 if you'd like to use Carnap in a class you're teaching, just get in touch on gitter on irc 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!