Settings

Settings

This page documents the settings available at Options -> Settings.

Settings are persistent and saved in a .config file in the same folder as the main JAR file. Current settings will be saved if, and only if, you close the Proof Assistant via File -> Close (rather than the X in the corner).

Set Arities for Terms

This allows you to set the arity of any character you wish to use. Any characters not on the arity list will be treated as propositions.

To specify that a letter should be interpreted as a function or term, simply add the letter and its arity to the arity list. Terms should be treated as zero-ary functions.

For example, to add a unary function j, add "j1" to the arity list. To add a term n, add "n0" to the list. To add a 15-ary function k, add "k15" to the list and prepare to suffer through the proof.

You cannot reassign the arity of a used term. Used terms appear in the greyed out textbox. If you want to reassign the arity of a used term, you must undo until it is unused.

Note: Remember that s is used as a unary function for Robinson and Peano Arithmetic.

Shortcut Settings

• Use Magic Mode with universal elimination shortcuts: When the previous setting is active, Magic Mode will be run on the results of any universal elimination shortcuts.

Other Settings

• Show brackets around terms: Every term (and function) will be surrounded by brackets. This is useful if identities aren't working properly.
• Choose Symbols: Choose the symbol set to use in the proof. This can be updated at any time.
• Show numbers in Robinson Arithmetic: Instances of ss..s0 will be parsed to the appropriate number.