Carnap's Pandoc

Within Carnap, shared documents and problem sets are created using pandoc markdown, a simple formatting language (akin to LaTeX) developed by John McFarlane as part of the Pandoc project. Pandoc markdown extends John Gruber's original markdown syntax with some additional niceties.

It would be a little redundant to give the full specifications for pandoc markdown here, since there are many excellent resources already available. See, instead,

  1. John Gruber's original markdown specification.
  2. The Pandoc user's guide

If you learn best from example, it's also possible to download the source code for documents shared on Carnap.io from the shared document list, available at https://carnap.io/shared. The pandoc source for this document, should you wish to inspect it, is available here.

You can create pandoc documents in any text editing program. But there are some very good text-editor plugins and dedicated applications available for working with Pandoc. A list of these can be found here. An online pandoc editor, with live previews of what the rendered document will look like, can be found at http://markup.rocks.

What follows is an explanation of some special rules for inserting interactive exercises that Carnap adds to Pandoc's markdown.

Syntax Check

To add a formula-parsing exercise, of the type found in chapter 1 of the Carnap book, include something like the following text:

~~~{.SynChecker .Match} 
1.1 P /\ Q /\ R 
~~~

The marks ~~~ indicate that this is a code-block rather than just more text, and the subsequent {.SynChecker .Match} indicates that the code should be interpreted as a syntax-checker exercise, matching the main connective of a standard formula. 1.1 is a problem number that will be used to save the problem when the student submits it. Finally, P /\ Q /\ R is the formula to be parsed. So the result is:

exercise 1.1

For a formula parsing exercise more like the chapter 2 problems, just change .Match to .MatchClean, so that you write:

~~~{.SynChecker .MatchClean} 
1.2 P /\ Q /\ R 
~~~

The result will be

exercise 1.2

Advanced Usage

If you so desire, you can also set a custom point value (for example, 15 points) for the exercise by adding points=15 after .Match or .MatchClean. You can also disable the submission button by adding submission="none" after .Match or .MatchClean. Finally, you can require explicit "parsing of atoms" (pressing return with when an atom is highlighted to acknowledge that it contains no connectives) by adding options="parseAtoms". So for example,

~~~{.SynChecker .MatchClean submission="none" options="parseAtoms"} 
1.3 P->Q
~~~

Generates

exercise 1.3

Truth Tables

The construction of truth tables is similar:

~~~{.TruthTable .Simple}
2.1 ((P/\Q)\/R)<->((P\/R)/\(Q\/R))
~~~

Produces a truth table for checking whether a formula is a tautology:

exercise 2.1

and

~~~{.TruthTable .Validity}
2.2 P :|-: ((P/\Q)\/R)<->((P\/R)/\(Q\/R))
~~~

produces a truth-table for checking the validity of the argument P :|-: ((P/\Q)\/R)<->((P\/R)/\(Q\/R)) (where :|-: is just a stylized way of typing out the turnstile):

exercise 2.2

Advanced Usage

Truth Tables can be customized more extensively than Syntax checking exercises. In addition to setting a custom point value or turning off submission by adding points=VALUE and submission="none" after .Simple or .Validity, several other options are available:

Name Effect
nocheck Disables the "check" button
nocounterexample Disables the "counterexample" button
exam Allows for submission of work which is incomplete or incorrect
autoAtoms Prepopulates atomic sentence columns with truth values

All of these options are designed to make it possible to use an assignment as an "exam" by setting it to have a fairly brief period of visibility, and also allowing for incomplete submissions for partial credit.

They can be set by adding options="exam" somewhere after .Simple to allow for incomplete submissions, setting options="nocheck nocounterexamples" to allow for incomplete submissions and also disable checking, and so on, in general specifying the options you wish to use with a space-separated list. Note that truth tables need to be checked for correctness before submission unless exam is set. So if you set nocheck without exam, then it won't be possible to submit the problem.

So for example,

~~~{.TruthTable .Validity options="nocheck nocounterexample"}
2.3 P :|-: Q
~~~

Generates:

exercise 2.3

It is also possible to create a "partial truth table" problem, in which the truth table is partly filled in, and the student needs either to complete it or correct it. To do this, write the partial truth table you want, preceded by the bar character |, after the problem. So,

~~~{.TruthTable .Simple"}
2.4 :|-: P\/~P
| T-FT
| F-TF
~~~

Generates

exercise 2.3
T-FT F-TF

Translations

You can also create a propositional logic translation problems, which are checked up to logical equivalence:

~~~{.Translate .Prop}
3.1 P/\Q : People want to know what's going on and questions are unavoidable
~~~

The colon separates the solution from the text that will be presented for translation. The result of the above is:

exercise 3.1
People want to know what's going on and questions are unavoidable

It is also possible to create first-order translation problems, thus

~~~{.Translate .FOL}
3.2 AxF(x) : Everything is fine
~~~

with the result:

exercise 3.2
Everything is fine

At the moment, these need to be correct verbatim (so a logically equivalent solution, like "¬∃x¬F(x)" will not be accepted), so it's best to keep them simple.

Advanced usage

In addition to allowing for custom point values with points=VALUE, and turning off submission with submission="none", translations also have the following options

Name Effect
nocheck Disables the "check" button
exam Allows for submission of work which is incomplete or incorrect

As with truth tables, this is done by including options= followed by a space-separated list of the desired options. As with truth tables, setting nocheck without setting exam makes it impossible to submit a problem.

It's possible to create a partial translation problem, by including the partial solution after a | following the problem. So for example,

~~~{.Translate .FOL options="nocheck"}
3.4 AxF(x) : Everything is fine
| For all x, x is fine
~~~

Generates

exercise 3.4
For all x, x is fine

Derivations

To get started, it's possible to create simple exercises, in the propositional system of the Carnap book, like this:

~~~{.ProofChecker .Prop} 
1.7 P :|-: Q->P
~~~

Where the :|-: again indicates a turnstile. The result is then:

exercise 1.7

The string .Prop specifies a formal system, together with a couple of UI-defaults for displaying proofs in that system. The system strings currently available are:

Strings Description
.Prop, .FirstOrder, .SecondOrder, .PolySecondOrder, .MontagueSC,.MontagueQC Montague-Style systems, the first two of which are used in the Carnap book.
.LogicBookSD, LogicBookSDPlus, LogicBookPD, .LogicBookPDPlus Fitch style systems based on Bergmann Moore and Nelson's Logic Book.
.ForallxSL, .ForallxSLPlus, .ForallxQL Fitch-style systems based on Magnus's Forall x.
.ZachTFL, .ZachFOL Fitch-style systems based on the Calgary Remix of Forall x.
.GoldfarbND, .GoldfarbAltND, .GoldfarbNDPlus, .GoldfarbAltNDPlus Lemmon-style systems based on Goldfarb's Deductive Logic.
.TomassiPL Lemmon-style system based on Tomassi's Logic
.HardegreeSL, .HardegreePL, .HardegreeWTL, .HardegreeL, .HardegreeK, .HardegreeT, .HardegreeB, .HardegreeD, .Hardegree4, .Hardegree5, .HardegreeMPL Hardegree-style systems based on Hardegree's Modal Logic

Advanced Usage

Like the other exercises, derivations allow for points=VALUE and submission="none".

Derivations, however, currently have a little more depth than the other types of exercises. There are, correspondingly, more options available.

Partial Solutions and Playgrounds

A partial solution to a problem can be included by following a problem with a derivation that is line-by-line prefixed with the | character, optionally followed by a line number followed by a period, like this:

~~~{.ProofChecker .Prop} 
1.7 P :|-: Q->P
|1.Show Q->P
|2.   Q:AS
|3.   P:PR
|4.:CD 3
~~~
exercise 1.7
Show Q->P Q:AS P:PR :CD 3

Everything after the line number (or the | if you don't use numbers) is included in the proof, so be careful about spaces!

You can also include a partial derivation without specific solution, by replacing .ProofChecker with .Playground, writing for example:

~~~{.Playground .Prop} 
|1.Show Q->P
|2.   Q:AS
|3.   P:PR
|4.:CD 3
~~~

which gives you a proof box that calculates what has been derived and displays it at the top, rather than calculating whether the derivation proves a given sequent

Playground
Show Q->P Q:AS ?:PR :CD 3

Options

The following extra options are available for proof-boxes:

Name Effect
guides Includes vertical indentation-level indicators
fonts Uses Fira Logic font, including ligatures for logical symbols
popout Makes it possible to open the problem in a new window
render Renders a picture of the proof as you type
indent Automatically indents newlines to the level of the previous line
resize Automatically resizes proof area
exam Allows for submission of work which is incomplete or incorrect

These can all be included by adding an "options" string to the problem specification, like this:

~~~{.ProofChecker .Prop options="indent fonts popout render autoIndent"} 
1.8 P :|-: Q->P
|1.Show Q->P
|2.   Q:AS
|3.   P:PR
|4.:CD 3
~~~
exercise 1.8
Show Q->P Q:AS P:PR :CD 3

An options string will override any options that are included by default in a given derivation type. For example, .Prop automatically turns on the resize option. However if we have just

~~~{.ProofChecker .Prop options="indent"} 
1.9 P :|-: Q->P 
~~~

We get a proofbox that resizes manually:

exercise 1.9

Feedback options

The defaults for feedback (check the proof with every keypress) can also be overridden. The override options for feedback are

Name Effect
manual require a button-press for feedback
none do not offer feedback

So,

~~~{.ProofChecker .Prop submission="none" feedback="manual"} 
1.10 P :|-: Q->P
~~~

produces

exercise 1.10