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.

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.

example 1

Show: P\/-P Show: --(P\/-P) -(P\/-P):AS Show: -P P:AS P\/-P:ADD 5 :ID 6 3 P\/-P:ADD 4 :ID 3 8 P\/-P:DNE 2 :DD 10

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.

example 2

Show: P\/-P Show: --(P\/-P) -(P\/-P):AS Show: -P P:AS P\/-P:ADD 5 :ID 6 3 P\/-P:ADD 4 :ID 3 8 P\/-P:DNE 2 :DD 10

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

example 3

Show P->(Q->R):CD P:AS Show Q->R:CD Q:AS P/\Q->R:PR P/\Q:&I 2 4 R:->O 5 6

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

example 4

(P->Q)->P :A/CI -P :A/~E P :A/CI Q :A/~E P :3 R -P :2 R Q :4-6 -E P->Q :3-7 CI P :8 1 CE -P :2 R P :2-10 -E ((P->Q)->P)->P :1-11 CI

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

example 5

Show -ExAy(-F(y,y) <-> F(x,y)) ExAy(-F(y,y)<->F(x,y)) :AS Show: -ExAy(-F(y,y) <-> F(x,y)) Ay(-F(y,y)<->F(c_1,y)) :AS -F(c_1,c_1)<->F(c_1,c_1) :UI 4 Show:-F(c_1,c_1) F(c_1,c_1) :AS F(c_1,c_1)->-F(c_1,c_1) :BC 5 -F(c_1,c_1) :MP 8 7 :ID 7 9 -F(c_1,c_1) -> F(c_1,c_1) :BC 5 F(c_1,c_1) :MP 11 6 Show: -ExAy(-F(y,y) <-> F(x,y)) :ID 6 12 :ED 13 2 4 :ID 2 3

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

example 6

[1] ExAy(Kxy -> Fxy) P [2] AxEy(Kxy) P [1,3] Ay(Kay -> Fay) (1)a EII [2] Ey(Kay) (2) UI [2,5] Kab (4)b EII [1,3] Kab -> Fab (3) UI [1,2,3,5] Fab (5) (6) TF [1,2,3,5] EyFay (7) EG [1,2,3,5] ExEyFxy (8) EG [1,2,3] ExEyFxy [5](9) EIE [1,2] ExEyFxy [3](10) EIE

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

example 7

AxAyAz(F(x,g(y,z)) ↔ h(x,y) = h(x,z)) :PR Show AwAxAyAz(F(w,g(x,y))∧F(w,g(x,z)) → F(w,g(y,z))) Show AxAyAz(F(a,g(x,y))∧F(a,g(x,z)) → F(a,g(y,z))) Show AyAz(F(a,g(b,y))∧F(a,g(b,z)) → F(a,g(y,z))) Show Az(F(a,g(b,c))∧F(a,g(b,z)) → F(a,g(c,z))) Show F(a,g(b,c))∧F(a,g(b,d)) → F(a,g(c,d)) F(a,g(b,c))∧F(a,g(b,d)) :AS F(a,g(b,c)) :S 7 F(a,g(b,d)) :S 7 AyAz(F(a,g(y,z)) ↔ h(a,y) = h(a,z)) :UI 1 Az(F(a,g(b,z)) ↔ h(a,b) = h(a,z)) :UI 10 F(a,g(b,c)) ↔ h(a,b) = h(a,c) :UI 11 F(a,g(b,d)) ↔ h(a,b) = h(a,d) :UI 11 F(a,g(b,c)) → h(a,b) = h(a,c) :BC 12 F(a,g(b,d)) → h(a,b) = h(a,d) :BC 13 h(a,b) = h(a,c) :MP 8 14 h(a,b) = h(a,d) :MP 9 15 h(a,c) = h(a,d) :LL 16 17 Az(F(a,g(c,z)) ↔ h(a,c) = h(a,z)) :UI 10 F(a,g(c,d)) ↔ h(a,c) = h(a,d) :UI 19 h(a,c) = h(a,d) → F(a,g(c,d)) :BC 20 F(a,g(c,d)) :MP 18 21 :CD 22 :UD 6 :UD 5 :UD 4 :UD 3

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.

example 8

ExAy(-Fyy <-> Fxy):AS Ay(-Fyy<->Fry):AS -Frr<->Frr:AE 2 -Frr:AS Frr:<->E 3 4 -Frr:R 4 Frr:-E 4-6 -Frr:<->E 7 3 ExAy(-Fyy <-> Fxy):AS Frr:R 7 -Frr:R 8 -ExAy(-Fyy <-> Fxy):-I 9-11 -ExAy(-Fyy <-> Fxy):EE 1 2-12 ExAy(-Fyy <-> Fxy):R 1 -ExAy(-Fyy <-> Fxy):-I 1-14

example 9

ExAy(-Fyy <-> Fxy):AS Ay(-Fyy<->Fry):AS -Frr<->Frr:AE 2 -Frr:AS Frr:<->E 3 4 !?:~E 4 5 -- Frr:AS -Frr:<->E 3 8 !?:~E 8 9 !?:LEM 4-6 8-10 !?:EE 1 2-11 -ExAy(-Fyy <-> Fxy):-I 1-12

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.

example 10

Show EXAx(F(x)/\G(x)<->X(x)) Show Ax(F(x)/\G(x)<->\y[F(y)/\G(y)](x)) Show F(c)/\G(c)->\y[F(y)/\G(y)](c) F(c)/\G(c):AS \y[F(y)/\G(y)](c):ABS 4 :CD 5 Show \y[F(y)/\G(y)](c)->F(c)/\G(c) \y[F(y)/\G(y)](c):AS F(c)/\G(c):APP 8 :CD 9 F(c)/\G(c)<->\y[F(y)/\G(y)](c):CB 3 7 :UD 11 EXAx(F(x)/\G(x)<->X(x)):EG 2 :DD 13

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.

example 11

Show: AX2EY2∀x∀y(X2(x,y) ↔ Y2(y,x)) Show: ∀x∀y(X2(x,y) ↔ \w\v[X2(v,w)](y,x)) Show: ∀y(X2(a,y) ↔ \w\v[X2(v,w)](y,a)) Show: X2(a,b) -> \w\v[X2(v,w)](b,a) X2(a,b):AS \w\v[X2(v,w)](b,a):ABS2 5 :CD 6 Show: \w\v[X2(v,w)](b,a)-> X2(a,b) \w\v[X2(v,w)](b,a):AS X2(a,b):APP2 9 :CD 10 X2(a,b) <-> \x_1\x_2[X2(x_2,x_1)](b,a):CB 4 8 :UD 12 :UD 3 EY2∀x∀y(X2(x,y) ↔ Y2(y,x)):EG2 2 :UD2 15

This is a proof that the powerset of a transitive set is transitive (exercise 3, chapter 3.3 from Velleman's Deductive Logic), in a system of elementary set theory.

example 12

Show P(a) within P(P(a)) a within P(a):PR Ax(x in a -> x in P(a)):Def-S 2 Show Ax(x in P(a) -> x in P(P(a))) Show b in P(a) -> b in P(P(a)) b in P(a) :AS b within a:Def-P 6 Ax(x in b -> x in a):Def-S 7 Show b in P(P(a)) Show Ax(x in b -> x in P(a)) Show c in b -> c in P(a) c in b :AS c in b -> c in a:UI 8 c in a :MP 12 13 c in a -> c in P(a) :UI 3 c in P(a):MP 14 15 :CD 16 :UD11 b within P(a):Def-S 10 b in P(P(a)):Def-P 19 :DD 20 :CD 9 :UD 5 P(a) within P(P(a)):Def-S 4 :DD 24

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.

example 13

Show <>[]P->[]P /0 :CD <>[]P /0 :AS Show []P /0 :ND Show P /0-1 :DD []P /0-2 :<>O 2 P /0-1 :[]O(5) 5

example 14

Show <>[]P->P /0 :CD <>[]P /0 :AS []P /0-1 :<>O 2 P /0 :[]O(b) 3

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 .

example 15

Show Ax[]Fx->[]AxFx /0 :CD Ax[]Fx /0 :AS Show []AxFx /0 :ND Show AxFx /0-1 :UD Show Fa /0-1 :DD []Fa /0 :AO 2 Fa /0-1 :[]O 6

Carnap supports proofs written in the sequent calculus, via ProofJS . Among the systems supported are propositional and first order variants of Gentzen's original LK and LJ.

example 16

{"ident":0,"label":"AxEy(F(x)/\\G(y)):|-:EyAx(F(x)/\\G(y))","rule":"ER","forest":[{"ident":1,"label":"AxEy(F(x)/\\G(y)) :|-: EyAx(F(x)/\\G(y)), Ax(F(x)/\\G(b))","rule":"AL","forest":[{"ident":2,"label":"Ey(F(a)/\\G(y)), AxEy(F(x)/\\G(y)) :|-: Ax(F(x)/\\G(b)), EyAx(F(x)/\\G(y))","rule":"EL","forest":[{"ident":3,"label":"F(a)/\\G(c), AxEy(F(x)/\\G(y)) :|-: Ax(F(x)/\\G(b)), EyAx(F(x)/\\G(y))","rule":"&L","forest":[{"ident":4,"label":"G(c), AxEy(F(x)/\\G(y)) :|-: EyAx(F(x)/\\G(y)), Ax(F(x)/\\G(b))","rule":"AR","forest":[{"ident":5,"label":"G(c), AxEy(F(x)/\\G(y)) :|-: EyAx(F(x)/\\G(y)), F(d)/\\G(b)","rule":"&R","forest":[{"ident":6,"label":"AxEy(F(x)/\\G(y)), G(c) :|-: EyAx(F(x)/\\G(y)),F(d)","rule":"AL","forest":[{"ident":7,"label":"Ey(F(d)/\\G(y)), G(c) :|-: F(d), EyAx(F(x)/\\G(y))","rule":"EL","forest":[{"ident":8,"label":"F(d)/\\G(e), G(c) :|-: F(d), EyAx(F(x)/\\G(y))","rule":"&L","forest":[{"ident":9,"label":"F(d), G(c) :|-: EyAx(F(x)/\\G(y)), F(d)","rule":"WR","forest":[{"ident":10,"label":"F(d), G(c) :|-: F(d)","rule":"WL","forest":[{"ident":28,"label":"F(d) :|-: F(d)","rule":"Ax","forest":[{"ident":29,"label":"","rule":"","forest":[]}]}]}]}]}]}]},{"ident":11,"label":"AxEy(F(x)/\\G(y)), G(c):|-:EyAx(F(x)/\\G(y)),G(b)","rule":"XR","forest":[{"ident":11,"label":"AxEy(F(x)/\\G(y)), G(c):|-:G(b),EyAx(F(x)/\\G(y))","rule":"ER","forest":[{"ident":12,"label":"AxEy(F(x)/\\G(y)), G(c):|-:G(b),Ax(F(x)/\\G(c))","rule":"AR","forest":[{"ident":13,"label":"AxEy(F(x)/\\G(y)),G(c) :|-: G(b), F(a)/\\G(c)","rule":"AL","forest":[{"ident":14,"label":"Ey(F(a)/\\G(y)),G(c) :|-:G(b), F(a)/\\G(c)","rule":"EL","forest":[{"ident":15,"label":"F(a)/\\G(d),G(c) :|-:F(a)/\\G(c), G(b)","rule":"&L","forest":[{"ident":16,"label":"F(a), G(c) :|-:G(b), F(a)/\\G(c)","rule":"&R","forest":[{"ident":17,"label":"G(c),F(a) :|-: G(b), G(c)","rule":"WL","forest":[{"ident":18,"label":"G(c):|-:G(b),G(c)","rule":"WR","forest":[{"ident":26,"label":"G(c):|-:G(c)","rule":"Ax","forest":[{"ident":27,"label":"","rule":"","forest":[]}]}]}]},{"ident":19,"label":"F(a), G(c):|-: G(b), F(a)","rule":"WL","forest":[{"ident":20,"label":"F(a):|-:G(b), F(a)","rule":"WR","forest":[{"ident":22,"label":"F(a):|-:F(a)","rule":"Ax","forest":[{"ident":25,"label":"","rule":"","forest":[]}]}]}]}]}]}]}]}]}]}]}]}]}]}]}]}]}

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 Keven Klement's Forall x proof checker using P.D. Magnus' Forall x system SL.

example 17

(W ∨ X), (Y ∨ Z), X → Y, ¬Z ∴ W ∨ Y

〈 1 / n 〉

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