Logiweb sequent calculus, Appendix

Klaus Grue

GRD-2006-06-16.UTC:15:22:33.470061

Contents

1 Introduction 1

2 Notation 2 2.1 Hiding construct . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Metaquantification . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.3 The ‘Arbitrary’ proof constructor . . . . . . . . . . . . . . . . . . 4 2.4 Macro indentation . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.5 Protected macro expansion . . . . . . . . . . . . . . . . . . . . . 4 2.6 Object quantification . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.7 Proof constructs . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.8 Modus ponens at the object level . . . . . . . . . . . . . . . . . . 5

3 Side conditions 5 3.1 Logiweb terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Deduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.3 Avoidance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.4 Substition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

4 Proofs 9 4.1 Proofs of FOL axioms using the inference of deduction . . . . . . 9 4.2 A proof of x + y = y + x . . . . . . . . . . . . . . . . . . . . . . . 10

1 Introduction

The present appendix is part of the Logiweb page available at

http://www.diku.dk/cgi-bin/cginetd/grue/relay/go/
01313803F348EB08B2ABC13AA47B393A4999076AF4ADED86FC81F6A20806/2/
body/tex/page.pdf.

The hex number which contains a RIPEMD-160 [DBP96] hash key and a time stamp identifies the present paper uniquely on Logiweb. The part before the hex number is the address of a Logiweb relay which redirects the users browser to the paper. That part can be replaced by the address of any Logiweb relay. The part after the hex number indicates the address of the body of the paper relative to the official, binary representation (2/ is shorthand for ../../).

Actually, the present page is rendered as three pdf files present at 2/body/ tex/page.pdf, 2/body/tex/appendix.pdf, and 2/body/tex/chores.pdf where appendix.pdf is the present appendix. Many proofs and definitions are deferred to the present appendix to spare the reader of the main paper in the page.pdf file. The chores.pdf file defines how to render each construct in TEX. A good place to start browsing is 2/index.html.

Each Logiweb page has a Logiweb bibliography which lists previously published pages which the present page relies on. The present Logiweb page references the base page at

http://www.diku.dk/cgi-bin/cginetd/grue/relay/go/
01F4E7B0BEECE7657F45769B92BEE076DAE3035BDFF9BEC08A83DCA20806/2/
body/tex/page.pdf.

which defines the proof system used to verify the present page (c.f. 2/bibliography /tex/page.pdf).

As mentioned in the main paper, the user friendliness of the Logiweb sequent calculus is achieved by using the Turing complete macro expansion facility of Logiweb. To see the proofs present in the main paper after macro expansion, consult 2/expansion/tex/page.pdf. To see the proofs of the present appendix after macro expansion, consult 2/expansion/tex/appendix.pdf.

2 Notation

2.1 Hiding construct

[x^{hide} ▷◁ “hide”] proclaims x^{hide} to denote hiding. We introduce it here to have a visible hiding construct instead of the invisible ‘unicode start of text’ operator normally used for hiding, c.f. the base page. The use of hiding in [x ¨= y]^{hide} later in this appendix is play for the gallery since the x is introduced on the base page and since macro definitions only have effect when they occur on the home page of the construct being macro defined.

2.2 Metaquantification

The following macro definition makes e.g. ΠA, B, C: D expand into ∀A: ∀B: ∀C: D. Note that ∀x: y is meta quantification as defined on the base page which, unfortunately, is rendered exactly like object quantification in the present document. Such notational clashes are unavoidable in mathematics in general but becomes extremely visible in a system like Logiweb where referenced papers are only a click away. To avoid confusion between the two, identically looking quantifiers, we only use the meta quantifier from the base page in the macro definition below and otherwise use ∀x: y to denote object quantification. The (x)^{p} operator used in the definition protects against macro expansion. The left hand side of the macro definition is protected against macro expansion as is the ‘recursive’ call of the macro that occurs in the right hand side.

[(Πx: y)^{p} →^{macro} λt.λs.λc.M̃( if ¬t^{1} =^{r} ⌈x, y⌉ then Q̃(t, ⌈∀x: y⌉, ⟨⌈x⌉ : : t^{1}, ⌈y⌉ : : t^{2}⟩) else Q̃(t, ⌈∀x: (Πy: z)^{p}⌉, ⟨⌈x⌉ : : t^{1}^{1}, ⌈y⌉ : : t^{1}^{2}, ⌈z⌉ : : t^{2}⟩), s, c)]

The definition above is a general macro definition as opposed to more restricted macro definitions like [Arbitrary ≫ i; p ¨= Πi: p] which just define a left hand side to expand into a right hand side. The [x ¨= y]^{hide} construct itself is defined by a general macro definition and happens to expand into a general macro definition, so the [x ¨= y]^{hide} construct is just syntactic sugar.

A general macro definition assigns a ‘macro’ aspect to the principal operator of the right hand side. The definition ignores the parameters of the principal operator. Instead, the right hand side of the general macro definition must take three arguments, t, s, and c. When a macro aspect is invoked, it is applied to the term t to be expanded, a ‘macro state’ s, and a ‘Logiweb cache’ c.

The macro state should itself be a function of three parameters t, s, and c and it is the function to be invoked when continuing the macro expansion. A macro like the macro protection macro (x)^{p} protects its argument x against macro expansion by returning it instead of calling s on it. The construct above calls the general macro expansion invokation function M̃(t, s, c) which simply applies s to t, s, and c. So the definition above does something to t and then continues macro expansion.

The Logiweb cache c is the cache of the home page of t, i.e. the page on which t occurs. The cache contains, among other, all definitions present on the home page and all pages transitively referenced by the home page. It also contains other things like compiled versions of all value defined constructs. This is badly needed for efficiency reasons because macro expansion is done not by the Logiweb computing engine itself but by a self-interpretter which is run by the Logiweb engine and simulates the Logiweb engine. This self-interpretter, which resides inside the macro state s, fetches compiled versions of constructs from the cache c for efficiency reasons.

The term t has the structure described in Section 3.1. t^{2} is the second subtree of t and t^{1}^{2} is the second subtree of the first subtree of t. t =^{r} t′ is true when t and t′ have the same principal operator.

The Q̃(t, p, a) construct expands the pattern p according to the association list a. Some day, when the author has some spare time, a new version of Q̃(t, p, a) will be implemented in which the association list is replaced by a facility like the ‘comma’ in Lisp backquotes.

The construct Q̃(t, p, a) not only expands the pattern p according to the association list a, it also extracts the ‘debugging information’ of the principal operator of t and installs that debugging information in all operators that come from the pattern p. The debugging information indicates the exact location of the construct before macro expansion.

The ⌈t⌉ construct evaluates to the Logiweb representation of the term t.

2.3 The ‘Arbitrary’ proof constructor

The ‘Arbitrary’ proof constructor defined on the base page does not take advantage of the meta quantification macro above. For that reason we introduce a new construct for introducing arbitrary meta variables:

[Arbitrary ≫ i; p ¨= Πi: p]

Actually, the definition above was used as an example of a simple macro in Section 2.2. When the same aspect of the same construct is defined more than once (e.g. the macro aspect of Arbitrary ≫ i; p), only the first definition has effect. But the Logiweb compiler prints a warning if the same aspect of the same construct have definitions that contradict each other. The repeated definition of Arbitrary ≫ i; p above gives no warnings since the two definitions have identical right hand sides.

2.4 Macro indentation

The following construct increases the left margin. Should be used in inline math mode only. Should be replaced by automatic indentation inside blocks as soon as possible.

[MacroIndent(x) ¨= x]

2.5 Protected macro expansion

The following construct is a general macro definition construct which both protects its left hand side against macro expansion and renders its left hand side using the tex name aspect. To see the definitions of the tex and tex name aspects of [x =^{∘} y]^{hide} consult the chores part of the present Logiweb page.

[[x =^{∘} y] ¨= [(x)^{p} →^{macro} y]]

2.6 Object quantification

The following is a repetion of Section 2.2 but concerns object quantification. It allows to write ∀x, y, z: u for ∀x: ∀y: ∀z: u.

[(∀x: y)^{p} →^{macro} λt.λs.λc.M̃( if ¬t^{1} =^{r} ⌈x, y⌉ then Q̃(t, ⌈∀_{obj}x: y⌉, ⟨⌈x⌉ : : t^{1}, ⌈y⌉ : : t^{2}⟩) else Q̃(t, ⌈∀_{obj}x: (∀y: z)^{p}⌉, ⟨⌈x⌉ : : t^{1}^{1}, ⌈y⌉ : : t^{1}^{2}, ⌈z⌉ : : t^{2}⟩), s, c)]

2.7 Proof constructs

The Begin b; l : End; p construct puts a parenthesis around the block b and places a cut operator between b and p. The construct is complicated by the line number l which should be macro defined locally to denote the conclusion of the block b. This is non-trivial since the conclusion is the last line prefixed by all premises, side-conditions, and meta-quantifiers introduced in earlier lines.

[Begin b; l : End; p =^{∘} λt.λs.λc.Block_{1}(t, s, c)]

[Block_{1}(t, s, c) ˙= t!s!c! let b = M̃(t^{1}, s, c) in let x = Block_{2}(b) in let q = Q̃(t, ⌈(let l ¨= x in p)^{p}⌉, ⟨⌈l⌉ : : t^{2}, ⌈p⌉ : : t^{3}, ⌈x⌉ : : x⟩) in let q = M̃(q, s, c) in Q̃(t, ⌈b; q⌉, ⟨⌈b⌉ : : b, ⌈q⌉ : : q⟩)]

[Block_{2}(b) ˙= if b =^{r} ⌈x ⊢ y⌉ then Q̃(b, ⌈x ⊢ y⌉, ⟨⌈x⌉ : : b^{1}, ⌈y⌉ : : Block_{2}(b^{2})⟩) else if b =^{r} ⌈x ⊢⊢ y⌉ then Q̃(b, ⌈x ⊢⊢ y⌉, ⟨⌈x⌉ : : b^{1}, ⌈y⌉ : : Block_{2}(b^{2})⟩) else if b =^{r} ⌈Πx: y⌉ then Q̃(b, ⌈Πx: y⌉, ⟨⌈x⌉ : : b^{1}, ⌈y⌉ : : Block_{2}(b^{2})⟩) else if b =^{r} ⌈x; y⌉ then Block_{2}(b^{2}) else if b =^{r} ⌈x ≫ y⌉ then b^{2} else ⊥ ⊥]

[Last block line a ≫ i ; ¨= (a ≫ i)]

2.8 Modus ponens at the object level

We shall apply modus ponens to two arguments so often that this idiom deserves its own macro:

[x ⊵ y ¨= MP ⊳ x ⊳ y]

3 Side conditions

3.1 Logiweb terms

Metavariables, object terms, statements, and sequent terms are all implemented as Logiweb terms which essentially have the following syntax:

pdigit  ::= “1” | “2” | “3” | “4” | “5” | “6” | “7” | “8” | “9”
digit  ::= “0” | pdigit
positive ::= pdigit | positive digit
cardinal ::= “0” | positive
reference ::= cardinal
identifier ::= cardinal
symbol ::= “(” reference“␣” identifier “)”
arglist  ::= “)” | “␣” term arglist
term  ::= “(” symbol arglist

The only thing omitted from the syntax is a third element of symbols which contains debugging information. For details on debugging information, consult the base page.

Each Logiweb page introduces one or more new constructs. As an example, the present page introduces the binary operation x ⇒ y.

Each Logiweb page has a unique reference, and each construct introduced by a page has an identifier which is unique within the page. Hence, reference and identifier together determine a construct uniquely.

3.2 Deduction

[Ded(p, c) ¨= λx.Ded_{0}(⌈p⌉, ⌈c⌉)] True if the premise p implies the conclusion c according to the deduction rule. The construct quotes its arguments and pass them on to Ded_{0}(p, c). The quoting and the λx. · · · makes Ded(p, c) suited as a side condition. The present side condition ignores x. But when a side condition is invoked, it is applied to the cache of the home page of the side condition (the page on which the side condition occurs). That way the side condition gets access to all definitions present on the home page and all pages transitively referenced by the home page. As an example, that has allowed to define an ‘axiom of definition’ in another theory on another Logiweb page in which all value definitions automatically become axiom schemes.

[Ded_{0}(p, c) ˙= c!Ded_{8}(p, T) ¨∧ Ded_{1}(Ded_{7}(p), c, T)] True if the premise p implies the conclusion c according to the deduction rule. The function checks the premise for meta-closedness, strips meta-quantifiers from p and then calls Ded_{1}(p, c, s) with an empty list s of side conditions. The x!y construct evaluates and discards x and then returns y. It is included to ensure strictness of Ded_{0}(p, c) which in turn increases the efficiency. Some day the present author will define a ‘strict value definition’ operator so that users don’t have to add x!y operators manually. The x!y construct takes zero CPU-time when used in functions that are ‘fit’ for optimization. See the base page for details on ‘fitness’ analysis.

[Ded_{1}(p, c, s) ˙= if c =^{r} ⌈x ⊢⊢ y⌉ then Ded_{1}(p, c^{2}, c^{1} : : s) else Ded_{2}(p, c, s)] Move side conditions from the conclusion c to the list s. x =^{r} y is true if the terms x and y have the same root (i.e. the same principal operator) so c =^{r} ⌈x ⊢⊢ y⌉ is true if the principal operator of c is an endorsement. c^{1} and c^{2} are the first and second argument, respectively, of the endorsement.

[Ded_{2}(p, c, s) ˙= s!p =^{r} ⌈x ⊢ y⌉∧c =^{r} ⌈x ⇒ y⌉ \{ \begin{matrix}Ded_{3}(p^{1}, c^{1}, s, T) ∧ Ded_{2}(p^{2}, c^{2}, s) \\ Ded_{4}(p, c, s, Ded_{6}(p, c, T, T)) \end{matrix} ]

This function is true if the premise p is equal to the conclusion c except that inferences are replaced by implications. if x then y else z

and x \{ \begin{matrix}y \\ z \end{matrix} express the same conditional construct. Choosing be-

tween the two is a purely stylistic choice.

[Ded_{3}(p, c, s, b) ˙= if ¬c =^{r} ⌈∀x: y⌉ then Ded_{4}(p, c, s, b) else if p =^{r} ⌈∀x: y⌉ ∧ p^{1} =^{t} c^{1} then Ded_{4}(p, c, s, b) else Ded_{3}(p, c^{2}, s, (c^{1} : : c^{1}) : : b)] Ded_{3}(p, c, s, b) moves quantified variables from the premise p to the association list b of ‘bindings’. Each quantified variable x is added to b as the pair x : : x indicating the x should be replaced by x (which is a way of saying that the variable cannot be instantiated). Moving of bound variables stops when there are no more bound variables to move or when the premise and conclusion happen to quantify the same variable. In both cases we have reached a point where premise and conclusion should be identical except for instantaition of variables. x =^{t} y is true if the terms x and y are identical. Logiweb terms contain debugging information which indicates the precise location each operator before macro expansion. x =^{t} y ignores this debugging information when it tests two terms for identity.

[Ded_{4}(p, c, s, b) ˙= s!b!

if p =^{r} ⌈x⌉ then lookup(p, b, T) =^{t} c else if ¬p =^{r} c then F else if p =^{r} ⌈∀x: y⌉ then p^{1} =^{t} c^{1} ∧ Ded_{4}(p^{2}, c^{2}, s, (p^{1} : : p^{1}) : : b) else if ¬p =^{r} ⌈X ⌉ then Ded_{4}^{∗}(p^{t}, c^{t}, s, b) else p^{1} =^{t} c^{1} ∧ Ded_{5}(p, s, b)] Test that the premise p is identical to the conclusion c except for instantiation of object variables as specified by the association list b. A term is an object variable if the root of the term is the ‘object variable operator’. For that reason, one can test whether or not a variable is an object variable by comparing its root to the root of an arbitrary object variable. For each meta variable, check that there are side conditions which ensure that the meta variables denote terms whose free object variables do not get caught in the context. Meta variables are recognized the same way as object variables. The object variable x and the meta variable X macro expand into \overline{x} and \underline{x}, respectively, adding the object and meta variable operator, respectively, to the term x. The term x is neither an object nor a meta variable. x is a Logiweb programming language variable because no Logiweb definition assigns a value to it.

[Ded_{4}^{∗}(p, c, s, b) ˙= c!s!b!if p then T else Ded_{4}(p^{h}, c^{h}, s, b) ∧ Ded_{4}^{∗}(p^{t}, c^{t}, s, b)] Elementwise application of Ded_{4}(p, c, s, b). x^{h} and x^{t} denote the head and tail, respectively, of the pair x. Terms are represented as lists comprising the principal operator followed by arguments just like Lisp S-expressions. The principal operator in turn is a list whose first two elements are cardinals that identify the operator followed by debugging information.

[Ded_{5}(p, s, b) ˙= p!s!if b then T else ⟨⌈x#y⌉^{h}, ⟨⌈⌈∗⌉⌉^{h}, b^{h}^{h}⟩, ⟨⌈⌈x⌉⌉^{h}, p⟩⟩ ∈_{t} s ∧ Ded_{5}(p, s, b^{t})] For each variable that is bound in the context according to the association list b, check that the list s of side conditions ensures that the meta variables p denotes a term whose free variables do not get caught in the context. x ∈_{t} y is true if the term x belongs to the list y of terms.

[Ded_{6}(p, c, e, b) ˙= p!c!b!e!

if p =^{r} ⌈x⌉ then p ∈_{t} e \{ \begin{matrix}b \\ (p : : c) : : b \end{matrix} else

if ¬p =^{r} c then T else if p =^{r} ⌈A⌉ then b else if p =^{r} ⌈∀x: y⌉ then Ded_{6}(p^{2}, c^{2}, c^{1} : : e, b) else Ded_{6}^{∗}(p^{t}, c^{t}, e, b)]

[Ded_{6}^{∗}(p, c, e, b) ˙= p!c!b!e!if p then b else Ded_{6}^{∗}(p^{t}, c^{t}, e, Ded_{6}(p^{h}, c^{h}, e, b))] Elementwise application of Ded_{6}(p, c, e, b).

[Ded_{7}(p) ˙= p =^{r} ⌈Πx: y⌉ \{ \begin{matrix}Ded_{7}(p^{2}) \\ p \end{matrix} ]

Removal of all metaquantifiers.

[Ded_{8}(p, b) ˙= if p =^{r} ⌈Πx: y⌉ then Ded_{8}(p^{2}, p^{1} : : b) else if p =^{r} ⌈A⌉ then p ∈_{t} b else Ded_{8}^{∗}(p^{t}, b)] True if all free meta variables of p occur in the list b of meta variables.

[Ded_{8}^{∗}(p, b) ˙= b!if p then T else Ded_{8}(p^{h}, b) ¨∧ Ded_{8}^{∗}(p^{t}, b)] Elementwise application of Ded_{8}(p, b).

3.3 Avoidance

[x^{var} ˙= x =^{r} ⌈\overline{x}⌉]

[x#y ¨= ⌈x⌉#^{0}⌈y⌉]

[x#^{0}y ˙= λc.x^{var} ∧ y^{C} ∧ x#^{1}y]

[x#^{1}y ˙= if y^{var} then ¬x =^{t} y else if ¬y =^{r} ⌈∀x: y⌉ then (x#^{∗}y^{t}) else if x =^{t} y^{1} then T else (x#^{1}y^{2})]

[x#^{∗}y ˙= x!If(y, T, (x#^{1}y^{h}) ¨∧ (x#^{∗}y^{t}))]

3.4 Substition

[⟨a≡b|x:=t⟩ ¨= ⟨⌈a⌉≡^{0}⌈b⌉|⌈x⌉:=⌈t⌉⟩]

[⟨a≡^{0}b|x:=t⟩ ˙= λc.x^{var} ∧ ⟨a≡^{1}b|x:=t⟩] [⟨a≡^{1}b|x:=t⟩ ˙= a!x!t!

if b =^{r} ⌈∀u: v⌉ ¨∧ b^{1} =^{t} x then a =^{t} b else

if b^{var} ∧ b =^{t} x then a =^{t} t else
a =^{r} b ¨∧ ⟨a^{t}≡^{∗}b^{t}|x:=t⟩]

[⟨a≡^{∗}b|x:=t⟩ ˙= b!x!t!If(a, T, ⟨a^{h}≡^{1}b^{h}|x:=t⟩ ¨∧ ⟨a^{t}≡^{∗}b^{t}|x:=t⟩)]

4 Proofs

4.1 Proofs of FOL axioms using the inference of deduction

We now prove axiom schemes A1 and A2 from [Men87]. Furthermore, we prove two, particular instances of A4 and A5 in a way that generalizes to arbitrary instances of those axiom schemes.

Furthermore, we prove a Repetition lemma which says ΠA: A ⊢ A by a ‘hand made proof’, i.e. by giving a proof metatactic explicitly which generates the sequent proof.

A page is verified by a top level verifier. The top level verifier of the present page is defined on the base page. That verifier invokes, among other, a proof verifier. The proof verifier invokes each proof (where each proof is supposed to be a proof metatactic). When it does so, it applies the proof metatactic to a Logiweb cache c and a pair n : : l. The cache c is the Logiweb cache of the home page of the proof, i.e. a structure which contains all definitions present on the home page plus all transitively referenced Logiweb pages. n is the identifier of the lemma (a cardinal which identifies the lemma uniquely within the home page) plus the contents of the lemma. The proof metatactic given below for proving Repetition ignores both arguments and just constructs a sequent term that proves ΠA: A ⊢ A. All other proofs in the present paper macro expand into proofs that are proved by a metatactic which scans the proof for object tactics and invokes those object tactics. The only object tactic used is named ≫ and does unification.

[S lemma Repetition: ΠA: A ⊢ A]

[S lemma A1′: ΠA, B: A ⇒ B ⇒ A]

[S lemma A2′: ΠA, B, C: (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C]

[S lemma A4′: ∀x, y: x + y = y + x ⇒ 2 + 3 = 3 + 2]

[S lemma A5′: ∀x: (2+3 = 5 ⇒ 2+3+x = 5+x) ⇒ 2+3 = 5 ⇒ ∀x: 2+3+x = 5 + x]

[Proof of Repetition: λc.λx.⌈S ⊢ ΠA: A^{I}⌉]

S proof of A1′:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;

L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A  ;
L05: Premise ≫  B  ;
L06: Repetition ⊳ L04 ≫  A  ;
L07: Block ≫  End  ;
L08: Ded ⊳ L07 ≫  A ⇒ B ⇒ A  □

S proof of A2′:

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B, C  ;
L04: Premise ≫  A ⇒ B ⇒ C  ;
L05: Premise ≫  A ⇒ B  ;
L06: Premise ≫  A  ;
L07: L05 ⊵ L06 ≫  B  ;
L08: L04 ⊵ L06 ≫  B ⇒ C  ;
L09: L08 ⊵ L07 ≫  C  ;
L10: Block ≫  End  ;
L11: Ded ⊳ L10 ≫  {(A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ \atop A ⇒ C  □}

S proof of A4′:

L01: Block ≫  Begin  ;
L02: Premise ≫  x + y = y + x  ;
L03: Repetition ⊳ L02 ≫  x + y = y + x  ;
L04: Block ≫  End  ;
L05: Ded ⊳ L04 ≫  {∀x: ∀y: x + y = y + x ⇒ 2 + 3 = \atop 3 + 2  □}

S proof of A5′:

L01: Block ≫ Begin ;
L02: Premise ≫  2 + 3 = 5 ⇒ 2 + 3 + x = 5 + x ;
L03: Premise ≫  2 + 3 = 5  ;
L04: L02 ⊵ L03 ≫  2 + 3 + x = 5 + x  ;
L05: Gen ⊳ L04 ≫  ∀x: 2 + 3 + x = 5 + x  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  ∀x: (2 + 3 = 5 ⇒ 2 + 3 + x = ; 5 + x) ⇒ 2 + 3 = 5 ⇒ ∀x: 2 + ; 3 + x = 5 + x  □

4.2 A proof of x + y = y + x

[S lemma Prop 3.2a: ΠA: A = A] [S lemma Prop 3.2b: ΠA, B: A = B ⊢ B = A] [S lemma Prop 3.2c: ΠA, B, C: A = B ⊢ B = C ⊢ A = C] [S lemma Prop 3.2d: ΠA, B, C: A = C ⊢ B = C ⊢ A = B] [S lemma Prop 3.2e: ΠA, B, C: A = B ⊢ A + C = B + C] [S lemma Prop 3.2f: ΠA: A = 0 + A] [S lemma Prop 3.2g: ΠA, B: A′ + B = (A + B)′] [S lemma Prop 3.2h: ΠA, B: A + B = B + A] S proof of Prop 3.2a:

L01: Arbitrary ≫  A  ;
L02: S5 ≫  A + 0 = A  ;
L03: S1 ⊳ L02 ⊳ L02 ≫  A = A  □

S proof of Prop 3.2b:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A = B  ;
L03: Prop 3.2a ≫  A = A  ;
L04: S1 ⊳ L02 ⊳ L03 ≫  B = A  □

S proof of Prop 3.2c:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A = B  ;
L03: Premise ≫  B = C  ;
L04: Prop 3.2b ⊳ L02 ≫  B = A  ;
L05: S1 ⊳ L04 ⊳ L03 ≫  A = C  □

S proof of Prop 3.2d:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A = C  ;
L03: Premise ≫  B = C  ;
L04: Prop 3.2b ⊳ L03 ≫  C = B  ;
L05: Prop 3.2c ⊳ L02 ⊳ L04 ≫  A = B  □

[S lemma Prop 3.2e_{1}: ΠA, B: A = B ⇒ A + 0 = B + 0] S proof of Prop 3.2e_{1}:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A = B  ;
L05: S5 ≫  A + 0 = A  ;
L06: Prop 3.2c ⊳ L05 ⊳ L04 ≫  A + 0 = B  ;
L07: S5 ≫  B + 0 = B  ;
L08: Prop 3.2d ⊳ L06 ⊳ L07 ≫  A + 0 = B + 0  ;
L09: Block ≫  End  ;
L10: Ded ⊳ L09 ≫  A = B ⇒ A + 0 = B + 0  □

[S lemma Prop 3.2e_{2}: ΠA, B, C: (A = B ⇒ A + C = B + C) ⇒ (A = B ⇒ A + C′ = B + C′)] S proof of Prop 3.2e_{2}:

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B, C  ;
L04: Premise ≫  A = B ⇒ A + C = B + C  ;
L05: Premise ≫  A = B  ;
L06: L04 ⊵ L05 ≫  A + C = B + C  ;
L07: S2 ⊳ L06 ≫  (A + C)′ = (B + C)′  ;
L08: S6 ≫  A + C′ = (A + C)′  ;
L09: Prop 3.2c ⊳ L08 ⊳ L07 ≫  A + C′ = (B + C)′  ;
L10: S6 ≫  B + C′ = (B + C)′  ;
L11: Prop 3.2d ⊳ L09 ⊳ L10 ≫  A + C′ = B + C′  ;
L12: Block ≫  End  ;
L13: Ded ⊳ L12 ≫  {(A = B ⇒ A + C = B + C) ⇒ \atop A = B ⇒ A + C′ = B + C′  □}

S proof of Prop 3.2e:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A = B  ;
L03: Block ≫  Begin  ;
L04: Prop 3.2e_{1} ≫  x = y ⇒ x + 0 = y + 0  ;

L05: Prop 3.2e_{2} ≫

(x = y ⇒ x + z = y + z) ⇒
(x = y ⇒ x + z′ = y + z′) ;
L06: S9 @ z ⊳ L04 ⊳ L05 ≫  x = y ⇒ x + z = y + z  ;
L07: Block ≫  End  ;
L08: Ded ⊳ L07 ≫  A = B ⇒ A + C = B + C  ;
L09: L08 ⊵ L02 ≫  A + C = B + C  □

[S lemma Prop 3.2f_{1}: 0 = 0 + 0] S proof of Prop 3.2f_{1}:

L01: S5 ≫  0 + 0 = 0  ;
L02: Prop 3.2b ⊳ L01 ≫  0 = 0 + 0  □

[S lemma Prop 3.2f_{2}: ΠA: A = 0 + A ⇒ A′ = 0 + A′] S proof of Prop 3.2f_{2}:

L01: Arbitrary ≫  A  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A  ;
L04: Premise ≫  A = 0 + A  ;
L05: S2 ⊳ L04 ≫  A′ = (0 + A)′  ;
L06: S6 ≫  0 + A′ = (0 + A)′  ;
L07: Prop 3.2d ⊳ L05 ⊳ L06 ≫  A′ = 0 + A′  ;
L08: Block ≫  End  ;
L09: Ded ⊳ L08 ≫  A = 0 + A ⇒ A′ = 0 + A′  □

S proof of Prop 3.2f:

L01: Arbitrary ≫  A  ;
L02: Block ≫  Begin  ;
L03: Prop 3.2f_{1} ≫  0 = 0 + 0  ;
L04: Prop 3.2f_{2} ≫  x = 0 + x ⇒ x′ = 0 + x′  ;
L05: S9 @ x ⊳ L03 ⊳ L04 ≫  x = 0 + x  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  A = 0 + A  □

[S lemma Prop 3.2g_{1}: ΠA: A′ + 0 = (A + 0)′] S proof of Prop 3.2g_{1}:

L01: Arbitrary ≫  A  ;
L02: S5 ≫  A′ + 0 = A′  ;
L03: S5 ≫  A + 0 = A  ;
L04: S2 ⊳ L03 ≫  (A + 0)′ = A′  ;
L05: Prop 3.2d ⊳ L02 ⊳ L04 ≫  A′ + 0 = (A + 0)′  □

[S lemma Prop 3.2g_{2}: ΠA, B: A′ + B = (A + B)′ ⇒ A′ + B′ = (A + B′)′] S proof of Prop 3.2g_{2}:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A′ + B = (A + B)′  ;
L05: S2 ⊳ L04 ≫  (A′ + B)′ = (A + B)′′  ;
L06: S6 ≫  A′ + B′ = (A′ + B)′  ;
L07: Prop 3.2c ⊳ L06 ⊳ L05 ≫  A′ + B′ = (A + B)′′  ;
L08: S6 ≫  A + B′ = (A + B)′  ;
L09: S2 ⊳ L08 ≫  (A + B′)′ = (A + B)′′  ;
L10: Prop 3.2d ⊳ L07 ⊳ L09 ≫  A′ + B′ = (A + B′)′  ;
L11: Block ≫  End  ;
L12: Ded ⊳ L11 ≫  {A′ + B = (A + B)′ ⇒ A′ + B′ = \atop (A + B′)′  □}

S proof of Prop 3.2g:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Prop 3.2g_{1} ≫  x′ + 0 = (x + 0)′  ;

L04: Prop 3.2g_{2} ≫

x′ + y = (x + y)′ ⇒ x′ + y′ =
(x + y′)′ ;
L05: S9 @ y ⊳ L03 ⊳ L04 ≫  x′ + y = (x + y)′  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  A′ + B = (A + B)′  □

[S lemma Prop 3.2h_{1}: ΠA: A + 0 = 0 + A] S proof of Prop 3.2h_{1}:

L01: Arbitrary ≫  A  ;

L02: S5 ≫  A + 0 = A  ;
L03: Prop 3.2f ≫  A = 0 + A  ;
L04: Prop 3.2c ⊳ L02 ⊳ L03 ≫  A + 0 = 0 + A  □

[S lemma Prop 3.2h_{2}: ΠA, B: A + B = B + A ⇒ A + B′ = B′ + A]

S proof of Prop 3.2h_{2}:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A + B = B + A  ;
L05: S2 ⊳ L04 ≫  (A + B)′ = (B + A)′  ;
L06: S6 ≫  A + B′ = (A + B)′  ;
L07: Prop 3.2c ⊳ L06 ⊳ L05 ≫  A + B′ = (B + A)′  ;
L08: Prop 3.2g ≫  B′ + A = (B + A)′  ;
L09: Prop 3.2d ⊳ L07 ⊳ L08 ≫  A + B′ = B′ + A  ;
L10: Block ≫  End  ;
L11: Ded ⊳ L10 ≫  {A + B = B + A ⇒ A + B′ = \atop B′ + A  □}

S proof of Prop 3.2h:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Prop 3.2h_{1} ≫  x + 0 = 0 + x  ;
L04: Prop 3.2h_{2} ≫  x +y = y+x ⇒ x +y′ = y′+x ;
L05: S9 @ y ⊳ L03 ⊳ L04 ≫  x + y = y + x  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  A + B = B + A  □

References

[DBP96] Hans Dobbertin, Antoon Bosselaers, and Bart Preneel. RIPEMD-160: A strengthened version of RIPEMD. In Fast Software

        Encryption, pages 71–82, 1996. http://citeseer.nj.nec.com/
        dobbertin96ripemd.html.

[Men87] E. Mendelson. Introduction to Mathematical Logic. Wadsworth and Brooks, 3. edition, 1987.