Example where distinct variable constraints are violated based on automatic expansion of a definition

From Wikiproofs
Jump to: navigation, search

Here's an example of an expanding definition causing a distinct variable constraint to be violated.

The easiest way to get some kinds, terms, and statements with distinct variable constraints to work with is going to be to import one of our existing interfaces; here we pick Interface:First-order logic.

import (PROPOSITIONAL Interface:Classical_propositional_calculus () () Unable to import parameter PROPOSITIONAL(Interface:Classical_propositional_calculus)[]+: Unable to load module Interface:Classical_propositional_calculus

Here's a definition with a dummy variable (because p is found on the right hand side, but not the left hand side, of the definition).

Unknown command

Here is an example of a valid theorem with a distinct variable constraint.

Unknown command

Now suppose we want to prove (truth) → ∀ x (truth), which looks similar but which has a definition. What happens is that the definition gets expanded, and then JHilbert complains about the lack of a distinct variable constraint between x and the unnamed variable. The following should produce an error, specifically Required distinct variable constraints are not a subset of actual distinct variable constraints.

Unknown command

Zeichen 123.svg This page or section needs cleanup. You can help wikiproofs by replacing the above example with one which would be valid except for the automatic expansion. This often comes up in real life in removeThereExistsInConsequent for example. See Help:Contents if you haven't yet figured out how to edit and write proofs, or ask at WP:TEA if you have any questions.

This combination of the automatic expansion of definitions and the way that distinct variables work is a significant inconvenience in using definitions as they currently exist in JHilbert. One workaround is to expand the definitions manually (which allows the distinct variable constraints to be expressed explicitly), and another is to export to an interface in which the definition is not a def but a term.

An example of expanding the definitions manually is LessEqual in Basic arithmetic. An example of moving the proof into a separate module in which the term is declared with term rather than def is the way that Basic operations of Zermelo–Fraenkel set theory is separate from First steps in set theory.

Once JHilbert definitions are redesigned (see Wikiproofs:JHilbert definition soundness), it is likely that whatever kind of definitions allow dummy variables won't be automatically expanded.