11/22/2020
The Preferences are a Menu Item on the Help Menu
Preferences allows the running application to be configured.
[As preferences are changed, what Deriver presents can also change, sometimes considerably. Most obviously, systems with extra rules of inference (for example, modal logic, set theory, theories with identity, etc. will add the relevant extra rules) then, for example, were a true 'modal' to be reset to false the modal rules would be removed. There can also be some not so obvious changes. For example, the Wizard Menu often has Derive It and Next Line menu items, these depend on a theorem prover which does the proof for you then produces it (or parts of it) at your request. But, for example, no theorem prover is available for set theory (with its axiom of induction), and none is available for modal logics, nor for identity. So, if the system starts running set theory (or modal logics, or with identity, etc.) the Derive It and Next Line items will no longer appear under the Wizard Menu.]
The Preferences Dialog opens to display
You select which Preference you wish to set, that will load its 'Key'. You then enter the 'Value' you want, and Press 'Put Key= Value'. That will set that preference, and changes will take place on all new and subsequent Browsers. (In the displayed image the 'colorProof' preference has been chosen, but no new value set for it.)
Home [default not set] shows or chooses the Directory that Deriver opens in. In general, there is probably not a lot of reason to be changing this by hand. When you Open or Save a file the standard Open/Save dialog will allow you to navigate to wherever you wish to be and Deriver will automatically remember where your last Save was. If you never do any Saves, and you wish to Open from somewhere other than the default, use this Preference to set your choice.
[There is a slight oddity here that can occur on a Macintosh. The Deriver program uses the actual file system on the host machine to navigate around, and everything is in the right place, so to speak. But Apple have provided for their devices 'iCloud Drive' which is storage in the cloud which also can appear on the device. However, where this iCloud Drive is in the device's file system is a bit of a question. Apple use a programming technique (trick?) and hide it in the Users library e.g.
The full path here for a iClooud Drive example file is "/Users/martin/Library/Mobile Documents/com~apple~CloudDocs/Programming/Deriver Programs/Deriver20/ExercisesAndDocumentation/PredicateExercisesGentzenMay15/PredEx8.lgc". Basically, you'd do yourself a favor here by avoiding this. Just don't keep your Deriver logic files in iCloud Drive. Keeping them in Google Drive, or Dropbox, etc. works fine without these contortions.]
User [default=""] is typically for lab or classroom use, where there are many Users, setting this identifies which student or User did the work.
colorProof [default=true] shows the subproofs, or indents, in different colors (red, blue, green, etc.). To give an example of changing a preference, this would be changed by selecting colorProof and typing in 'false'
then pressing 'Put Key=Value' and the result will be
derive [default=true], enables the theorem prover which will do the derivations for you (off the Wizard menu).
endorseMenuItem [default=true], enables the Endorse-Deny items off the Semantics Menu. This allows the User to play the Endorse-Deny game which is an elementary form of game-theoretic semantics.
firstOrder [default=false], enables First Order theories, such as arithmetic. Such theories often have constants of their own e.g. 0 (zero) and 1 (one), functions such as + (plus) which can be written infix (e.g. 1+1 not Plus(1,1)), and equality =. So, with firstOrder set to true, Deriver will parse, say, 0+1=1 and F(0+1') as being well-formed formulas, and you can do proofs with such formulas (extra rules, such as Induction, will be available).
gamesMenu [default=false], displays a Games menu.
htmlEditor [default=false], this adds an extra menu item HTML editing menu. It produces a fuller featured HTML editor.
htmlMenu [default=true], displays an HTML editing menu.
identity [default=false], if this is set true then formulas like a=b will be parsed as being well-formed and there will be extra rules of inference to permit derivations like F(a), a=b ∴ F(b).
interpretations [default=true], enables the drawing window and 'interpretations' for semantics.
lambda [default=false], enables the lambda calculus and its rules.
modal [default=false], enables modal logics and their rules.
paletteText [default=thePaletteTextRelevantToTheParserThatIsRunning], allows you to set the Palette text. The Palette is the small collection of symbols at the top of the journal (for your use in Proofs etc.). The default is that the Palette displays symbols suitable for the system you are using, for example & (for and) in one system and ^ (for and) in a different system, and modal symbols for modal, lambda symbols for lambda, etc. But, actually, you can have whatever you like, either special symbols, reminders, mottos, whatever. Just set the paletteText to, say, "Now is the winter of our discontent" and that is what will be on your palette.
parser [default=default], allows you to set the Parser (i.e. the logic system that Deriver will run). The display will look something like
default [barwise bergmann copi gentzen hausmann herrick howson priest]
the first entry, in this case 'default', is the logic system that Deriver is running. [Another example, in the image above the system is running 'barwise']. The other labels within the square brackets are the choices available to you, in this case
[barwise bergmann copi gentzen hausmann herrick howson priest]
So, if you wanted to run a 'priest' system, you would just type in priest as the value and Press 'Put Key= Value'. Which parser is running matters, for example Fa is well-formed in some systems but not in others (other systems might use F(a) as the syntax for that formula). There is a small 'gotcha' here. If you create and save some files in one system, say Gentzen, then change parser to, say, Hausmann, then try to open your Gentzen files with a Hausmann system, your files might not open with full information (the system will skip any formulas that are not well formed and your Gentzen formulas might not be well-formed under a Hausmann system).
proofs [default=true] enables the Proofs windows (in some settings Users might want to do Trees only, in which case they would set this false).
readFromClipboard [default=false] enables direct reading from the Clipboard. You can, of course, copy something and paste it in to the Journal etc.. But this speeds that process up. If it is enabled, you can select some text from anywhere, copy it (which copies it to the Clipboard), then Start a Proof, Start a Tree etc. and Deriver will read its input directly from
the Clipboard.
rewrite [default=true] enables the rewrite rules.
rightMargin [default=340] sets the right margin.
setTheory [default=false] enables set theory, so for example x ∈ y is well formed, and there are additional rules of inference.
simpleFileMenu [default=false] disables many choices on the File Menu to make the presentation easier for beginning students.
trees [default=true] enables the tree panel for tree proofs.
typeLabels [default=false] enables type labels.
useAbsurd [default=false] enables the use of Absurd. When doing a Reductio ad Absurdum proof, the proof is trying to derive a contradiction, say two formulas A and ~A. Sometimes this is easier to understand by having a propositional constant 'Absurd' which is defined as being A&~A (for any formula A), then a reductio proof makes an assumption then tries to derive Absurd from it.