rules
The following rules need special documentation
- (eg): W(e),(x=>e)|- for some x:T(W(x)) -- -- --(e is an expression of type T)
- (ei): for some x:T(W(x)), (x=>v)|- v:T, W(v) -- -- --(v is free variable)
- (ui): for one x:T(W(x), (v=>x)|- W(v) -- -- --(v is free variable)
- (ui): for all x:T(W(x)), (v=>x)|- W(e)-- -- --(e is an expression of type T)
. . . . . . . . . ( end of section rules) <<Contents | Index>>
Abc
So it is valid to derive
- 9 = 3*3
from
- (1): 3=sqrt(9)
by
- (Sqrt(x=>3, y=>9)) |- (2): if 3=sqrt(9) then 9=3*3,
- (2, mp) |- (3): 9=3*3.
Normally details are omitted:
- (Sqrt(x=>3, y=>9))|- 9=3*3.
Block Structure
Intro
In addition to deductive steps we can use nested pieces of documentation can explore the consequences of extra assumptions. Propositions of the form
- for x:S, if P then Q
- are often proved by documentation that
List
- * introduces a temporary declaration (x:S),
- * makes an assumption (P) and
- * derives a consequence Q.
The syntax using the symbols "Let{" and "}" like this:
Let{ (1): x:S, (2):P. |-..., |-Q, }..
Generic Syntax of a proof
The general syntax is
- proof::= (natural | analytical | reducto_ad_absurdum) &( po "{" analysis #( or analysis) "}",
- analysis::=hypothesis derivation closure,
- hypothesis::= #(axiom|comment|definition),
- derivation::=#(derived|comment|definition).
- closure::=derived.
- Consider{
(x'=x-y;y'=x+y;x'=y-x)
- = Net{x'=x-y, y'=y, y''=x'+y', x''=x'};x'=y-x
- = for some a,b(a=x-y and b=y and y''=a+b and x''=a);x'=y-x
- = ((y''=x-y+y and x''=x-y);x'=y-x)
- = ((y'=x and x'=x-y);x'=y-x)
- = (y'=x and x'=x-y and y''=y' and x''=y'-x')
- = (x'=y and y'=x)
}.
