Help:JHilbert

From Wikiproofs

This page is designed to be (eventually) a full reference manual for JHilbert. If you don't have some familiarity with JHilbert, it is probably easier to start with the tutorial and then come back here.

The language in which the proofs and statements being proved are written is called JHilbert, which is also the name of the software that runs to verify the proof when you save or preview a page. On the wiki, JHilbert statements are enclosed between <jh> and </jh> tags.

JHilbert distinguishes between interfaces and modules and different commands are valid in interfaces or modules. Interfaces live in the Interface namespace (for example, Interface:Classical propositional calculus) and modules live in the main namespace (for example, Principia Mathematica propositional logic). Interfaces contain axioms and statements to be proved; modules prove those statements. A lemma which is proven in a module but which is not likely to be useful in contexts other than the given proof should not be listed in any interface.

Anything from # to the end of the line is a comment (that is, it is ignored by JHilbert).

Contents 1 Interfaces 2 Modules 3 Troubleshooting 4 External links

[edit] Interfaces

Interfaces contain:

• Parameters. This is a way to import kinds, terms and definitions from another interface. Except that it does not import statements, it has much the same meaning as the import statement in a module, and the same syntax except that it starts with param instead of import.

param (identifier page (parameter1 parameter2 …) prefix)

When interfaces with one or more param commands in them are imported or exported, the import or export command must be given a parameter list matching the parameters of the interface. This does not mean that parameters generated from exactly the same page with the correct prefix have to be used (in that case, parameter lists would be somewhat pointless). Instead, any parameters providing the kinds, terms and definitions as the specified page with prefix can be used.

• Kinds. Each variable will be of some kind, and the kinds are declared with the kind statement.

kind (new-kind)

For example, kind (formula) says there is a kind called formula.

• Variables. Variables are declared with a kind.

var (kind new-variable-1 new-variable-2...)

For example, var (formula p q r) declares variables p, q and r, all formulas.

• Terms.

term (kind (new-term argument-1-kind argument-2-kind...))

For example, term (formula (¬ formula)) defines a term called ¬ of kind formula which takes one argument, which is a formula. In the definition, the name of the term has to be on the left, but when invoked the name of the term can be in any position. This is generally done to make the notation look more like infix notation (for example, (p ∧ q) instead of (∧ p q)), but the term name is recognized by being a term name, not by position. In fact, even (p q ∧) would be legal and mean the same thing. Nevertheless, terms and variables have different namespaces and if an ambiguity arises, JHilbert will take the first valid term name and try to construct an expression, whether successfully or not.

• Definitions.

def (new-defined definition)

For example,

def ((¬ p) (p | p))

defines ¬ in terms of |. A variable which appears on the right hand side but not the left hand side is called a dummy (As of early 2010, the functioning of dummies is unsafe and subject to change; see discussion at User:GrafZahl/Definitions in JHilbert).

• Statements. Statements are either axioms (in which case there will be no modules which exports this interface, as axioms cannot be proved) or statements to be proved (in which case, some module will prove the statement and export the interface).

stmt (new-statement (distinct-variables) (hypothesis) (consequent))

For example, one version of the famous modus ponens states that from the hypotheses p and p → q, one can conclude q:

stmt (applyModusPonens () (p (p → q)) q)

• Distinct variables. The distinct variables are a list of pairs of variables, for example:

((φ x) (x y))

means that φ is distinct from x and x is distinct from y. The order of variables in each pair is not significant. The meaning of a distinct variable constraint is that anything substituted for the one variable must not contain any variables in common with the substitution for the other variable. For example, given the constraints above, if z = w is substituted for φ, and z is substituted for x, the first constraint would be violated. On the other hand, it is permissible to substitute some constant (const) for both x and y above, as constants do not contain variables at all. It is also possible to specify distinct variables in triples, quadruples, etc. JHilbert will then automatically generate the pairs as all mutually distinct combinations. For example, the constraint

((φ x y))

is equivalent to

((φ x) (φ y) (x y))

This can save a lot of typing in some cases.

[edit] Modules

• Import statements. These represent kinds, terms, definitions and statements (either axioms, or statements proved elsewhere) to be assumed in proofs.

import (identifier page (parameter1 parameter2 …) prefix)

For example:

import (NICOD Interface:Nicod_axioms () ())

As you can see, interfaces with no parameters are imported with empty parameter lists. If the interface being imported has parameters, you need to first import the interfaces to be used as parameters, and then supply their identifiers as parameter1 and so on. For example:

import (CLASSICAL Interface:Classical_propositional_calculus () ())
import (PRINCIPIA Interface:Axioms_of_first-order_logic (CLASSICAL) ())

where the second interface expects Interface:Classical_propositional_calculus or a compatible interface as its only parameter.

The prefix allows the names in the interface to differ from the name in the module (which may be necessary to avoid naming conflicts with some of the imported interfaces, for example). For an example of avoiding naming conflicts, see Nicod's reduction of Principia Mathematica (which uses a prefix on the export). The prefix can be either a string or () for the empty string.

• Variables. Same syntax and meaning as in interfaces.

• Definitions. Same syntax as in interfaces.

• Proofs.

thm (new-theorem (distinct-variables) (hypotheses) (consequent) (proof))

This represents the proof of a theorem.

• new-theorem is the name of the theorem.
• hypotheses will need to be present to later apply the theorem, and can be empty. Each hypothesis consists of a label followed by the hypothesis (unlike in stmt, in which the labels can be omitted).
• consequent is what is being proved.
• proof is a sequence of atoms. Each atom can be the label of a hypothesis, a variable, or the name of a statement which is being applied. Hypotheses and variables are pushed onto the proof stack. Applying a statement proceeds by popping from the proof stack one element for each hypothesis and variable in the statement being applied. The variables should be pushed in the order in which they first appear in the statement. These elements must match what the statement expects. The statement then pushes its consequent onto the proof stack. At the end of the proof, the proof stack must contain one element, and it must be the consequent which is being proved.

• Kindbind. This allows a kind to have several names, which may be necessary in conjunction with the prefix feature of the export statement.

kindbind (existing-name new-name)

For example, if you have a kind called formula and you want .formula to refer to the same kind, specify

kindbind (formula .formula)

• Export statements. Once a module has proved everything it wants to, it can export those proofs to an interface.

export (identifier page (parameter1 parameter2 …) prefix)

See import for a description of identifier, page, parameters, and prefix.

[edit] Troubleshooting

Some of the contents of this section may be specific to the wiki, as opposed to JHilbert run in other ways

Some of the error messages you may encounter are:

Feed failure: I/O error

This can be a transient error (try just hitting "Preview" again, if you see it when previewing a page).

Not all bytes could be written.

This generally means there is another more informative error somewhere else on the page.

Attempt to prove result by illegal dummy assignment

This means that the statement left on the proof stack at the end of the proof has the same arrangement of terms as what you are trying to prove, but the variables don't line up. It can be something as mundane as proving x = y when what you need is y = x (see Illegal dummy assignment example).

No functor found in expression
Non-variable symbol in expression

If you do not see an obvious cause for this kind of syntax error, try seeing whether any parentheses are unbalanced.

[edit] External links

There's another partial JHilbert manual at:

• Quick rundown of the JHilbert syntax

Other related systems, which may help you understand JHilbert (especially until this manual is a bit more complete) are:

• Metamath. Metamath is in the same general family, in the sense of having fairly explicit proofs and a simple proof verifier. There is an automated converter to convert metamath to ghilbert.

• ghilbert. Ghilbert, compared with metamath, adds a number of features most notably definitions (in an attempt, not successful as of 2009, to make it impossible for a poorly constructed definition to render the system inconsistent) and the ability to separate proofs into interfaces and modules. In particular, the specification is rather close to what is described in this page.