Notes on getting started with Bertie3 or Twootie.

1. Typically users will start by loading one or another of the stored problem sets, so both programs will start by asking you which problem set to load. You can press ESCAPE at any time to cancel a command and move around the menus.

The bottom line of the screen always describes your current options or the current command. Each program has a very extensive help system, which can be entered at any time by pressing function key F1.

2. Probably the biggest barrier to overcome is to learn what keys to press for logic symbols. Bertie3 and Twootie both use the following conventions:

 For            Press       Key name                Displayed as

 disjunction      v         lowercase letter "v"    v
 conjunction      &         ampersand               &
 conditional      >         greater than sign       arrow
 biconditional    <         less than sign          triple bar
 negation         -, ~      hyphen or tilde         tilde
 atoms          A...Z       upper case letters      A...Z
                except V

Predicate logic:

 constants      a...u       lower case letters      a...u
 variables      w...z       lower case letters      w...z
 predicates     A...Z       upper case letters      A...Z
                except V
 universal q.     V         uppercase letter "V"    V
 existential      ]         right square bracket    ]
 identity         =         identity                =
 functors       a...u       lower case letters      a...u

Disjunction ("either...or") is symbolized with the lowercase letter "v" (as in "victory"), directly above the space bar. Negation is entered with the hyphen, usually found above and to the right of the P key. You can also use the tilde (~) key, if you can find it. The universal quantifier is the uppercase letter "V" (as in "Victor"). The existential quantifier is the right square bracket ("]"). We cannot use "=" for the biconditional, since it is needed for identity.

Atomic sentences must be capitalized. Quantifiers require parentheses, as in (Vx)Fx. The outermost parentheses around sentences are optional. The typing is very much "case sensitive" (because of the differences between "v" and "V", "]" and "}", and so on), and so "Caps Lock" must be OFF.

3. The user can always enter an input string of the form:

      <sentence> / <line numbers> <rule name>

You need the slash (/) to separate sentences from justifications. A justification is typically one or more line numbers, followed by a rule name.

The rule names are very simple in The Logic Book and in both programs. The natural deduction system uses the connective followed by "i" or "e" (or "I" or "E") for "introduction" or "elimination" respectively. So ">I" is Conditional Introduction, "vE" is Disjunction Elimination, "VE" is Universal Introduction, and so on. Premises in the proof are justified with a "P", and auxiliary assumptions in a conditional proof with "A".

The semantic tableaux rules are all "decomposition" rules, signified by a "d". There is one for each connective, and one for each negated connective. So "<d" is Biconditional Decomposition, "-]d" is Negated Existential Decomposition, and so on. The initial set members in the tree are justified with "SM". If the program does not find a legal rule name in your input, it will say "Rule name not found".

Often the user can enter much less than the full input string above. Often all you need to type is a slash and a rule name, or a slash, a line number or two, and a rule name. Both programs will try to generate from the line numbers you cite the sentence that would be produced by applying the rule that you cite. Bertie3 "templates" can be generated by typing in nothing more than a slash and a rule name, though if you see one or two sentences that would be useful in generating the target sentence using the rule you have in mind, it is a good idea to cite them. Those cited sentences will be incorporated into the template.