Natural Deduction Style Proofs
allows proofs to be presented in natural deduction style. In
particular, Alfa provides library modules that defines connectives,
quantifiers and proof rules for propositional logic and predicate
logic. Using these, Alfa can be (and has been) used as tool for
teaching basic logic, since the user can construct proofs without first
learning all about the logical framework (type theory).
Below, we describe how to construct a proof
that logical conjunction is commutative, as illustrated by the
following animation. Apart from the first two steps, each step in the
animation corresponds to one mouse click or one key press.
Building a proof
Here are the necessary steps.
We are now ready to start working on the proof.
- Import the logic you want to use, in this case
(constructive) propositional logic. Use the
Import... command from the
File menu, click on the
Library button, then on the
Examples directory, then on
- Add a new definition (e.g., by using the command
New Declaration in the Edit
menu). Here you give the new proof a name,
and introduce the propositional variables that occur in the
After pressing the OK button (or the Return key), we
have the following skeleton definition:
- Fill in the type of the propositional variables, which should be
Prop, by clicking on Prop in the menu window.
- Enter the propsition. You can build it in a top-down order by
clicking on the appropriate connectives and propositional
variables in the menu window.
- The last thing to do before we can start working on the proof,
to make the proof appear in natural deduction style,
you have to use the command
ND Style Proof from the menu.
To simplify things for students, teachears can prepare exercise files
where these steps have already been performed.
Working on the proof
Once the preparations are done, you can concentrate on what proof
rules to use to construct the proof. The proof is built top-down,
i.e., you start from the final goal and work towards simpler
propositions that can be proved directly from assumptions or axioms
(i.e., proof rules without any premises). All you have to do is put
the cursor on a question mark (?) beside a proof rule and fill in what
rule to use by clicking on the name of a suitable rule in the menu window.
In our example, the proposition to be proved is an implication, so a
natural first step is an implication introduction, which we can click
on in the menu to obtain the following:
When the proof is complete, you might want to save it by using the
command Save or Save As... in the
Useful things to know
- If you in the
alternative Filter through type checker, only
applicable proof rules will be shown in the menu.
- Elimination rules are always applicable, since the allow you to
conclude anything. This doesn't meen that using them is always
- After using an elimination rule, the new subgoals usually
contains some metavariables (?). Most of the time, there is no
need to fill in these manually, just go ahead and fill in
the next proof rule to use intead.
- Assumptions are referred to by names that are shown with a
lambda to the left of the rule where the assumption is
discharged. To find out what is assumed click on the name of the
assumption next to the lambda.
- You can use Undo to go back one or more steps
if you used the wrong proof rules.
- You can mark and delete arbitrary parts of your proof, but, you
may then need to use the menu
command ND Style Proof again, to make the new
proof appear in natural deduction style.
- Proofs presented in Natural Deduction style easily become rather wide.
Top-Down Proof Tree is an alternative proof presentation style that
can be selected in the View menu.
Defining your own proof rules
You can easily define your own proof rules, since they are just
functions. When a function is used as a proof rule in a natural
deduction style proof, all visible arguments are assumed to be subproofs, so
arguments that aren't subproofs should probably be hidden. For
example, to use the commutativity of conjuction above as a proof rule,
we would first hide the two first arguments (the propositional variables).
See the section User defined layout
in the user's guide for how to do this.
A larger example
As a larger example, here is part of a proof of the correctness of
insertion sort. This example also illustrates that you can mix natural
deduction style with other constructions in the logical framework,
such as local definitions.
Proofs presented in Natural Deduction style can easily become rather wide,
particularly when propositions contain large terms. An alternative
proof style is Top-Down Proof Tree, which can be selected
from the View menu.
As an example of this proof style,
below is the above proof that conjunction is commutative: