# 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,

- John Gruber's original markdown specification.
- 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:

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

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

## 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:

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

### 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:

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

## 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:

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

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

with the result:

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

## 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:

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
~~~
```

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

#### 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
~~~
```

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:

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