Help:JHilbert

From Wikiproofs
Revision as of 05:21, 1 May 2012 by Kingdon (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

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).

Interfaces[edit]

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. See Example of trying to supply a parameter with a non-matching definition.

  • 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 and is given unique variables (As of 2010, the functioning of dummies is unsafe and subject to change; see Wikiproofs:JHilbert definition soundness). By "given unique variables" we mean that the variables do not match any named variable, but are eligible for unifying with other variables. For example, if we are supposed to prove (p ∨ (¬ p)) ↔ (⊤) it suffices to prove (p ∨ (¬ p)) ↔ (q ∨ (¬ q)) (see Tautology) but it is not sufficient to prove (p ∨ (¬ p)) ↔ (p ∨ (¬ p)) (see Example of definition dummies which leads to illegal variable assignment). Definition dummies can also be subject to distinct variable constraints, see Example where distinct variable constraints are violated based on automatic expansion of a definition (distinct variable constraints are described in greater detail later in this page).

Related to definitions are abbreviations, the intention of which is to allow expressing something more concisely without the complexities of being able to introduce dummy variables. For now, JHilbert does not have distinct definition and abbreviation features, and def needs to serve for both. To see examples of how an abbreviation feature might be defined, see Interface:Example of abbreviation which tries to introduce a variable and Example of abbreviation in proof module which contains a variable. For two examples of how abbreviations are expanded in error cases, see Example of abbreviations and consequent of theorem does not match proof result and Example of abbreviations and illegal variable assignment.

  • 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) (hypotheses) (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.

Modules[edit]

  • 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. For the export to succeed, the proof module must have:

Troubleshooting[edit]

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). For an example which shows this error in the context of automatic abbreviation expansion, see Example of abbreviations and illegal variable assignment.

Consequent of theorem does not match proof result

The statement left on the proof stack does not have the same arrangement of terms as what you are trying to prove. For an example, see Example of consequent of theorem does not match proof result. For an example which shows this error in the context of automatic abbreviation expansion, see Example of abbreviations and consequent of theorem does not match proof result.

Unification error while popping hypotheses from proof stack: Invalid change of variable assignment 

This happens when you are invoking a proof step with hypotheses but the hypotheses don't match. Example: change the last occurrence of buildThereExistsInConsequent to buildForAllInConsequent in UnionAxiomObject at [1] or see Example of invalid change of variable assignment. (TODO: elaborate on this a bit more).

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.

Distinct variable constraint violation: Intersection of cartesian product factors is not empty 

This means that you are trying to invoke a theorem which has a distinct variable constraint but there is a variable which appears in the two terms which are supposed to be distinct. See Example of distinct variable constraint violation: Intersection of cartesian product factors is not empty.

Required distinct variable constraints are not a subset of actual distinct variable constraints 

This means that somewhere in the proof there is an invocation of a theorem which has a distinct variable constraint, but the theorem you are trying to prove does not have a distinct variable constraint which assures that the invocation is OK. See Example of required distinct variable constraints are not a subset of actual distinct variable constraint.

If you can't see where the variable which is causing the problem is, consider the possibility that it resulted from the automatic expansion of a definition. For example, see various applications of LessEqual in Basic arithmetic or Example where distinct variable constraints are violated based on automatic expansion of a definition. (TODO: also want an example(s) where similar issues, such as expanding multiple definitions in one theorem, lead to "Attempt to prove result by illegal dummy assignment" or other errors). The solution is using a theorem like LessEqual to expand the definition, and/or moving your proof into a separate module in which the term is declared with term rather than def (for example, the way that Basic operations of Zermelo–Fraenkel set theory is separate from First steps in set theory).

Kind mismatch

A theorem invocation has the wrong kind. For example, with just about anything built on Interface:First-order logic, saying x when (value x) is needed will produce this error. See Example of kind mismatch.

Proof step is neither a symbol nor a hypothesis

A proof contains an atom which is not a hypothesis, a variable, or the name of a previous theorem. This can happen by misspelling a theorem name, forgetting to list a previously proved theorem in an appropriate interface, or failing to declare a variable. See Example of proof step is neither a symbol nor a hypothesis.

External links[edit]

There's another partial JHilbert manual at:

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.