Next: Rules dealing with equality
Up: Proof semantics
Previous: The assumption base
  Contents
Rule applications
Perhaps the simplest inference rule of NDL is claim,
a unary ``reiteration'' rule which takes one formula
as
its sole argument. If the argument
is in the current assumption base, then claim simply returns
(i.e., it reiterates
). Otherwise, if
is not in the
assumption base, then claim reports an error.
Suppose, for example,
that the current assumption base contains the formula male(joe)
but does not contain the formula female(ann). Then
the deduction claim male(joe) will succeed, eliciting the
reply
By contrast, the deduction
will fail, generating an error message
of the form:
Evaluation error at line 3, position 27:
the claim female(ann) is not in the assumption base.
So the first claim succeeds, but the second fails. Note that NDL reports
the precise position of the failed claim (say, line 3, column 27
for this hypothetical example).
Also note that NDL pronounces the successful claim a theorem.
In fact every time a proof is successfully evaluated at the top level,
NDL reports the resulting formula as a theorem. There is a reason
for this: It can be proved rigorously that if any NDL proof
successfully produces a formula
in the context of an assumption
base
, then
is a logical consequence of
. This is the main
soundness guarantee provided by NDL, and it is the sense in which
the result of a proof is understood to be a theorem.
One question about claim that comes up sometimes is this:
If a formula
is in the assumption base and we try to
claim
, where
is a variant of
that is logically
equivalent to
but is not itself in the assumption base,
will the claim succeed? The answer is no. An application claim
will succeed if and only if
itself, as a syntactic object, is in
the assumption base. For instance, suppose that
is
the formula male(joe) and
is
where
is in the assumption base but
is not. Then
claim
will succeed, but claim
will
fail, even though
is logically equivalent to
.
There is a reason for this too: The problem of deciding whether
two formulas are logically equivalent is very
difficult. If fact it is undecidable, meaning that there is
no algorithm that could solve every instance the problem.
However, claim, like all other NDL rules, determines
formula identity up to alphabetic equivalence. For instance,
if
is
and
is
then claim
will succeed if and only if claim
suceeds.
All of the remaining inference rules
can be can be classified either as introduction or
as elimination rules for one of the sentential connectives
or quantifiers. Consider, for instance, conjunctions of the form .
There are two elimination rules for conjunctions, left-and
and right-and. The former will produce
, the left part
of the conjunction, while the latter will produce
, the right
part. Specifically, if the conjunction
is in the current assumption base, then the application
will produce the formula
as a result.
If the conjunction is not in the assumption base,
then the application will fail.
The rule right-and works exactly like left-and, save
that it produces the right component of the given conjunction.
It is instructive to compare NDL's formulation of these inference
rules with a more conventional presentation. For instance,
the left conjunction elimination rule is usually depicted
graphically as follows:
This says that if the premise
above the horizontal line
has already shown to be a theorem (where theoremhood is signified by
the turnstile
), then we may also derive
as a theorem.
Or, more loosely, if we already know that
holds then
we may conclude
.
In the case of NDL, ``
holds'' boils down to no more
and no less than it being in the assumption base. Therefore, the
NDL semantics of left-and can be understood as saying that
if
is in the assumption base, then we may conclude
.
The semantics of a proof form
can often be expressed succinctly
with judgements of the form
, which can
be read as follows:
For instance, the semantics of left-and can be captured
by the following rule:
 |
(+1.3) |
which says that applying left-and to a conjunction of the form
in any assumption base that contains this conjunction
will produce the conclusion
. Rule (1.3) can be viewed
as a pattern that can give rise to different rule instances depending on
what particular values we choose to substitute for
,
, and
.
For instance, both of the following are instances of (1.3):
The first is obtained from (1.3) via the substitution
while the second is obtained through the substitution
The rule does not tell us what happens when the assumption base does not contain
the premise
. We could explicitly
introduce rules such as
error |
whenever
|
but we will instead tacitly understand that in all such cases
the result will be an error. We will follow that convention
in the sequel when we come to state other similar rules.
The semantics of rule applications are summarized below:
Next: Rules dealing with equality
Up: Proof semantics
Previous: The assumption base
  Contents
2004-08-06