6. First-Order Logic
We extend our propositions and our linear proof
format to include universal and existential quantification.
Here is an example demonstrating All-introduction and -elimination and
Exists-introduction:
| proof AllEx : !y:t. (!x:t. A(x)) => ?x:t. A(x) =
begin
[ c : t;
[ !x:t. A(x);
A(c);
?x:t. A(x) ];
(!x:t. A(x)) => ?x:t. A(x)];
!y:t. (!x:t. A(x)) => ?x:t. A(x)
end;
|
The scope of a quantification starts at the `.' and extends as far
to the right as syntactically possible. Thus the All-quantified variable
`y' is bound in the whole proposition, whereas the scope of
`!x:t.' is limited by parentheses to preserve the intended
meaning of the proposition.
Invoking the proof checker Tutch, it gives the following justifications
| Proving AllEx: !y:t. (!x:t. A x) => ?x:t. A x ...
1 [ c: t;
2 [ !x:t. A x;
3 A c; by ForallE 2 1
4 ?x:t. A x ]; by ExistsI 1 3
5 (!x:t. A x) => ?x:t. A x ]; by ImpI 4
6 !y:t. (!x:t. A x) => ?x:t. A x by ForallI 5
QED
|
Universal quantification !y:t. B(y) can be introduced by a frame
[c:t; ... B(c)] as we see in the last line: Here B(y) is
which does not contain any occurrence of y. Universal
quantification can be eliminated if we have a term of the type over
which the
quantification is ranging. An example can be seen in line 3: We have an
All-quantified assertion !x:t. A x in line 2 and a term c :
t, the parameter introduced in line 1. Thus we can deduce A x
where all occurrences of x are replaced by c, which is
A c.
To introduce an existential quantification ?x:t. A x (line 4)
we need a witness c : t (line 1) and a proof for the special
instance of the proposition A c (line 3). For existential
elimination we consider the following example:
| proof ExNotImpNotAll : (?x:t. ~A(x)) => ~!x:t. A(x) =
begin
[ ?x:t. ~A(x);
[ !x:t. A(x);
[ c: t, ~A(c);
A(c);
F ];
F ];
~!x:t. A(x) ];
(?x:t. ~A(x)) => ~!x:t. A(x);
end;
|
To prove falsehood F in proof line 6, we eliminate the
existential quantification in the first line. This gives us two new
hypotheses to show our goal: A witness c : t and a proof of
~A(c). In principle Exists-elimination is used in the same way as disjunction
elimination. Note that we extended our frame syntax to include the
introduction of several hypotheses, separated by commas.
For further information consult the reference.
This document was generated
by Andreas Abel on October, 24 2002
using texi2html