Next: Proof semantics
Up: Natural Deduction Language
Previous: Formulas
  Contents
Proof syntax
The following grammar describes the syntax of NDL proofs:
where the syntax of inference rule applications is as follows:
Proofs of the form
;
are called composite.
Proofs of the form assume
are called conditional
(or hypothetical) proofs. The formula
is called the hypothesis
and the subproof
is called the body of the conditional proof.
We say that the body
represents the scope of the hypothesis
.
Proofs of the form suppose-absurd
are called proofs
by contradiction. As with conditional proofs,
is called
the hypothesis and
--the scope of
--is called
the body.
Proofs of the form
are called universal generalizations. We refer to the variable
as an eigenvariable.
Proofs of the form
are called existential specializations. We refer to the variable
as the witness variable; we also say that
is an eigenvariable.
Proofs of the form
are called universal specializations, while proofs of the form
are called existential generalizations.
Proofs of the form
are called conclusion-annotated proofs.
assume, suppose-absurd, pick-any, pick-witness, and BY
all bind tighter than the composition operator ;. For example,
is parsed as the composition of assume A claim A and claim true,
not as the hypothetical proof with A as the hypothesis and
the composition claim A; claim true as the body.
The composition operator ; associates to the right, meaning
that
is parsed as
 |
(+1.1) |
and not as
 |
(+1.2) |
This is an important convention, because proof composition in NDL
is not associative--proofs (1.1) and (1.2)
do not have the same semantics. This will become more clear in the sequel.
These conventions can be overriden by using begin-end pairs.
Finally, we note that pick-any and pick-witness are variable-binding
constructs; they introduce variable scope. In particular, in a deduction
of the form
we say that the scope of the eigenvariable
is the deduction
.
And in a deduction of the form
we say that the scope of the witness variable
is
. Two deductions that
only differ in the names of their bound eigenvariables
are condidered identical. For instance, the two deductions
pick-any x
pick-any y
assume x = y
swap x = y
and
pick-any foo1
pick-any foo2
assume foo1 = foo2
swap foo1 = foo2
are considered identical.
We can define a notion of substitution (free variable occurrence replacement) for deductions
much as we do for formulas. Specifically, for any deduction
, variable
and term
, we define
as the deduction obtained from
by replacing every free occurrence of
inside
by
, possibly renaming
bound eigenvariables to avoid variable capture. A rigorous definition can be
found in the appendix.
Next: Proof semantics
Up: Natural Deduction Language
Previous: Formulas
  Contents
2004-08-04