Derivations

The ProofChecker class indicates that a code block will contain derivation exercises. The Playground class indicates that a code block will generate a "playground" in which instead of checking whether the proof establishes something set in advance, Carnap will figure out what the proof establishes and display it at the top of the proof-box. The formal systems used can be controlled using predefined classes, or by setting attributes on the code-block (see below).

Predefined classes

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

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

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

exercise 1.7

Similarly,

~~~{.Playground .Prop} 
~~~

generates

Playground

The class Prop specifies that we wish to use the propositional formal system of the Carnap book, and specifies a couple of UI-defaults for displaying proofs in that system. The currently available predefined classes are:

Class Strings Description
.Prop, .FirstOrder, .SecondOrder, .PolySecondOrder, .MontagueSC,.MontagueQC, ElementaryST, SeparativeST 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.
.IchikawaJenkinsSL, .IchikawaJenkinsQL Fitch-style systems based on the Ichikawa-Jenkins Remix of Forall x.
HowardSnyderSL,HowardSnyderPL Systems based on Howard-Snyder's The Power of Logic.
HausmanSL,HausmanPL Systems based on Hausman's Logic and Philosophy.
.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

Options

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:

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
tabindent Insert indent on tab press
resize Automatically resizes proof area
exam Allows for submission of work which is incomplete or incorrect

These can all be included in the "options" string supplied to the options attribute of the code block, 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
~~~

The result of the above is:

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

Partial Solutions

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 (for readability) 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
~~~

This gives us:

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, thus:

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

Feedback

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

Name Effect
manual require a button-press for feedback
syntaxonly warn about syntax errors, but do not check proof for correctness
none do not offer feedback

So,

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

produces

exercise 1.10

Systems

If you don't want to use a predefined class, you can set the system option manually.

The available propositional systems are: prop montagueSC LogicBookSD LogicBookSDPlus hausmanSL howardSnyderSL ichikawaJenkinsSL hausmanSL magnusSL magnusSLPlus thomasBolducAndZachTFL tomassiPL and hardegreeSL. The available first-order systems are: firstOrder montagueQC magnusQL thomasBolducAndZachFOL LogicBookPD LogicBookPDPlus hausmanPL howardSnyderPL ichikawaJenkinsQL hardegreePL goldfarbAltND goldfarbNDPlus and goldfarbAltNDPlus. The available set theory systems are: elementarySetTheory and separativeSetTheory. The available second-order systems are: secondOrder and PolySecondOrder. The available propositional modal logic systems are: hardegreeL hardegreeK hardegreeT hardegreeB hardegreeD hardegree4 and hardegree5. The available predicate modal logic system is hardegreeMPL, and the available "world theory" system is hardegreeWTL.

Initialization

The init attribute may be set to "now" in order to check the proof as soon as it is loaded, instead of waiting for a user interaction.

Indentation Guides

Besides just the indentation guide created by setting guides in the options string, there are several more refined overlays available for increasing the readability of a typed proof. These are configured by setting the guides attribute. The available options for guides are:

Name Effect
montague Simple indentation gudie
fitch A fitch style proof overlay
hausman A Hausman style proof overlay
howard-snyder A Howard-Snyder style proof overlay

So,

~~~{.Playground .ForallxSL guides="fitch"} 
 P       :AS
 P/\P    :&I 1 1
 P       :&E 2
P->P        :->I 1-3
~~~

Produces:

Playground
P :AS P/\P :&I 1 1 P :&E 2 P->P :->I 1-3