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:

Similarly,

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

generates

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:

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:

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 resize render indent"} 
1.8 P :|-: Q->P
|1.Show Q->P
|2.   Q:AS
|3.   P:PR
|4.:CD 3
~~~

The result of the above is:

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:

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:

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:

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

So,

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

produces

Systems

If you don't want to use a predefined class, you can set the system option manually. This will give you complete control over which options are set—only the ones you select will be active. So you would write something like:

~~~{.ProofChecker system="prop" submission="none" feedback="manual"} 
1.11 -Q :|-: Q->P
~~~

to produce

The available propositional systems are: prop montagueSC LogicBookSD LogicBookSDPlus hausmanSL howardSnyderSL ichikawaJenkinsSL hausmanSL magnusSL magnusSLPlus thomasBolducAndZachTFL thomasBolducAndZachTFL2019 gamutMPND gamutIPND, gamutPND gamutPNDPlus tomassiPL and hardegreeSL. The available first-order systems are: firstOrder montagueQC magnusQL thomasBolducAndZachFOL thomasBolducAndZachFOL2019 thomasBolducAndZachFOLPlus2019 LogicBookPD LogicBookPDPlus gamutND 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:

So,

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

Produces: