## ## Tutorial ## ## ## Source: [R0-v1.0.3 (doi: 10.4444/100.10.3)] ## ## Copyright (c) 2017 Owl of Minerva Press GmbH. All rights reserved. ## Written by Ken Kubota (). ## ## This file is part of the publication of the mathematical logic R0. ## For more information, visit: ## ## This file is subject to change and shall be extended continuously. ## Please check for a newer version at: http://doi.org/10.4444/100.10.3 ## To run the tutorial, enter ## ## make tutorial ## ## The file 'tutorial.r0i.out.txt' will contain both the tutorial and the ## results of the commands explained. ## For the references, please see: http://doi.org/10.4444/100.111 ## For questions and suggestions, send an email to mail@kenkubota.de after ## reading the material provided online via the link above. ## ## This tutorial explains the R0 proof language. ## ## ## For a proper understanding, please first read: ## ## 1. The syntactic part [Andrews, 2002, pp. 201–237] of chapter 5 of Andrews' ## 2002 textbook (ISBN 1-4020-0763-9) describing his logic Q0, ## ## 2. the introduction to R0 on pp. 11-12 of my book "Mathematical Formulae" ## available online at: http://doi.org/10.4444/100.10.2 ## (ISBN 978-3-943334-07-4), and ## ## 3. the file 'README.txt' as part of the R0 software package available for ## download at: http://doi.org/10.4444/100.10.3 ## ## 4. A full treatment of R0 shall be announced at ## http://doi.org/10.4444/100.10.1 ## ## ## Basic commands ## ## Comment lines start with a hash symbol (#). ## Comment lines beginning with two hash symbols (##) will be printed. ## Command: ## Visible comment line ## Visible comment line ## Comment lines beginning with only one hash symbol (#) will not be printed. ## Command: # Invisible comment line ## Let's print the help info (interactive mode only). ## Command: :h :help ## math commands: §= §\ §s §s' §r (§!) ## syntax commands: := << ## system commands: ? :h[elp] :p[rint] :s[tack] :q[uit] ## :w[ffs] :d[efinitions] :t[heorems] :[a]ll :i[d] ## Now, let's print the built-in definitions (interactive mode only). ## Command: :d # Definitions: # wff 0 : ^ # wff 1 : @ # wff 2 : o # wff 8 : = # wff 10 : i # ## You will see the identity/equality symbol (=) and its counterpart, ## the description or selection operator (i), plus the three basic types: ## the universal type: omega (@), which replaces Church's and Andrews' ## type of individuals, the type of truth values: omicron (o), ## and the type of types: tau (^). ## Furthermore, the logical implication (=>) is hard-wired in rule §s', ## meaning we have actually three primitive basic symbols (=,i,=>) and ## three primitive type symbols (^,@,o). From these primitive symbols, ## everything can be defined. ## The logical connectives are definable now. We shall use the definitions ## and axioms in file 'basics.r0.txt'. To include this file, we use the ## command '<<'. ## Command: << basics.r0.txt << basics.r0.txt ## Again, let's print the built-in definitions (interactive mode only). ## Command: :d # Definitions: # wff 0 : ^ # wff 1 : @ # wff 2 : o # wff 8 : = # wff 10 : i # wff 12 : ((=_=)_=) := T # wff 20 : ((=_[\x.T])_[\x.x]) := F # wff 29 : [\t.[\p.((=_[\x.T])_p)]] := A # wff 47 : [\x.[\y.((=_[\g.((g_T)_T)])_[\g.((g_x)_y)])]] # := & # wff 53 : [\x.[\y.((=_x)_((&_x)_y))]] := => # wff 57 : [\a.((=_F)_a)] := ! # wff 65 : [\a.[\b.(!_((&_(!_a))_(!_b)))]] := | # wff 72 : [\t.[\p.(!_((=_[\x.T])_[\x.(!_(p_x))]))]] := E # wff 79 : [\x.[\y.(!_((=_x)_y))]] := != # wff 92 : [\t.[\x.[\y.((A_t)_[\z.((=>_(x_z))_(y_z))])]]] # := SBSET # wff 103 : [\t.[\y.[\x.(((SBSET_t)_x)_y)]]] := PWSET # wff 112 : [\t.[\p.((E_t)_[\y.((=_p)_(=_y))])]] := E1 # wff 113 : [\x.T] := V # wff 114 : [\x.F] := O # wff 119 : [\t.[\x.[\y.((=_x)_y)]]] := == # wff 126 : [\t.[\x.[\y.(!_((=_x)_y))]]] := !== # wff 129 : [\t.[\x.(i_x)]] := I # wff 135 : [\x.[\y.(!_((=_x)_y))]] := XOR # wff 147 : [\t.[\f.((=_((f_x)_y))_((f_y)_x))]] := COMMT # wff 159 : [\t.[\f.((=_((f_((f_x)_y))_z))_((f_x)_((f_y)_z)))]] # := ASSOC # wff 170 : ((=_((&_(g_T))_(g_F)))_((A_o)_[\x.(g_x)])) # := A1 # wff 184 : ((=>_((=_x)_y))_((=_(h_x))_(h_y))) := A2 # wff 204 : ((=_((=_f)_g))_((A_b)_[\x.((=_(f_x))_(g_x))])) # := A3 # wff 207 : ((=_(i_(=_y)))_y) := A5 # ## You will see the definitions for truth (T), falsehood (F), the universal ## quantifier (A), conjunction (&), Axiom 1 (A1), any many others. ## To print a well-formed formula, simply enter it (interactive mode only). ## Command: & # wff 47 : [\x.[\y.((=_[\g.((g_T)_T)])_[\g.((g_x)_y)])]] # := & # w typd 47 : [\x{o}{o}.[\y{o}{o}.((={{{o,@},@}}_[\g{{{o,o},o}}{{{o,o},o}}.((g{{{o,o},o}}{{{o,o},o}}_T{o}){{o,o}}_T{o}){o}]{@}){{o,@}}_[\g{{{o,o},o}}{{{o,o},o}}.((g{{{o,o},o}}{{{o,o},o}}_x{o}{o}){{o,o}}_y{o}{o}){o}]{@}){o}]{{o,o}}] # { {{o,o},o} } # := & ## You will see the well-formed formula (wff) both in short form and with every ## part fully typed, and the type(s) of the wff itself ('{ {{o,o},o} }'). ## In the abstration '[\x{o}{o}. ... ]' with variable x of type o, ## 'x{o}' is the variable name, and the second '{o}' the type information ## stored in the lambda abstraction. ## Since a variable can only have a single type, variable x{o} is different ## from x{^} or x{@}, so the type of the variable is always part of its name. ## To print a well-formed formula, you also can use the wff number ## (interactive mode only). ## Command: 47 # wff 47 : [\x.[\y.((=_[\g.((g_T)_T)])_[\g.((g_x)_y)])]] # := & # w typd 47 : [\x{o}{o}.[\y{o}{o}.((={{{o,@},@}}_[\g{{{o,o},o}}{{{o,o},o}}.((g{{{o,o},o}}{{{o,o},o}}_T{o}){{o,o}}_T{o}){o}]{@}){{o,@}}_[\g{{{o,o},o}}{{{o,o},o}}.((g{{{o,o},o}}{{{o,o},o}}_x{o}{o}){{o,o}}_y{o}{o}){o}]{@}){o}]{{o,o}}] # { {{o,o},o} } # := & ## ## Carrying out a proof ## ## A simple proof that shall serve as an exercise is: ## Proof A5211: (T & T) = T ## Source: [Andrews 2002 (ISBN 1-4020-0763-9), p. 220 (Theorem 5211)] ## ## Step One (.1) ## ## Let's print the theorems we can use (interactive mode only). ## Command: :t # Theorems: # ((=_((&_(g_T))_(g_F)))_((A_o)_[\x.(g_x)])) # := A1 # ((=>_((=_x)_y))_((=_(h_x))_(h_y))) := A2 # ((=_((=_f)_g))_((A_b)_[\x.((=_(f_x))_(g_x))])) # := A3 # ((=_(i_(=_y)))_y) := A5 # ## Theorems are referenced as theorems using the percent symbol (%). ## Command: %A1 %A1 # ((=_((&_(g_T))_(g_F)))_((A_o)_[\x.(g_x)])) # := A1 # ((={{{o,o},o}}_((&{{{o,o},o}}_(g{{o,o}}{{o,o}}_T{o}){o}){{o,o}}_(g{{o,o}}{{o,o}}_F{o}){o}){o}){{o,o}}_((A{{{o,{o,\3{^}}},^}}_o{^}){{o,{o,o}}}_[\x{o}{o}.(g{{o,o}}{{o,o}}_x{o}{o}){o}]{{o,o}}){o}) # { o } := A1 ## Displaying a theorem makes it the last theorem on stack. ## The stack of the last theorems obtained is displayed with command ':stack'. ## Command: :s # thm %4 : ((=_((&_(g_T))_(g_F)))_((A_o)_[\x.(g_x)])) # := A1 # thm %3 : ((=>_((=_x)_y))_((=_(h_x))_(h_y))) := A2 # thm %2 : ((=_((=_f)_g))_((A_b)_[\x.((=_(f_x))_(g_x))])) # := A3 # thm %1 : ((=_(i_(=_y)))_y) := A5 # thm %0 : ((=_((&_(g_T))_(g_F)))_((A_o)_[\x.(g_x)])) # := A1 ## Note that Axiom 1 (A1) now occurs as theorem %0 (the last theorem obtained). ## To keep reasoning simple and proof scripts readable, one should only use ## the last eight theorems on stack (%0-%7), and recall older theorems by their ## name, as done above with '%A1'. ## In the first step (.1) of the proof, Andrews uses metatheorem 5209 for ## substituting a variable by an wff in an equation (in this case Axiom 1). ## Since R0 is a true Hilbert-style system, it has no syntactic variables, ## and metatheorems (of the meta-language) cannot be expressed directly in ## the (object) language for later instantiation of the syntactic variables. ## Instead, the metatheorem is implemented as a macro (called 'proof ## template'), and for each specific value (wff), the proof has to be carried ## out again. We pass over the values (wffs) by giving them definition labels, ## so the proof template can reference them by these definition labels. ## use Proof Template A5209 (incl. A5204): B = C --> (B = C) [x/A] := $M5209 o # wff 2 : o := $M5209 := $E5209 %0 # wff 170 : ((=_((&_(g_T))_(g_F)))_((A_o)_[\x.(g_x)])) # := $E5209 A1 := $T5209 {o,o} # wff 13 : {o,o} := $T5209 := $X5209 g{$T5209} # wff 160 : g := $X5209 := $A5209 [\y{o}{o}.T{o}] # wff 208 : [\y.T] := $A5209 << A5209.r0t.txt := $M5209 := $E5209 := $T5209 := $X5209 := $A5209 %0 # ((=_((&_([\y.T]_T))_([\y.T]_F)))_((A_o)_[\x.([\y.T]_x)])) # ((={{{o,o},o}}_((&{{{o,o},o}}_([\y{o}{o}.T{o}]{{o,o}}_T{o}){o}){{o,o}}_([\y{o}{o}.T{o}]{{o,o}}_F{o}){o}){o}){{o,o}}_((A{{{o,{o,\3{^}}},^}}_o{^}){{o,{o,o}}}_[\x{o}{o}.([\y{o}{o}.T{o}]{{o,o}}_x{o}{o}){o}]{{o,o}}){o}) # { o } ## Now 'g' in Axiom 1 is replaced by [\y.T], which finishes step one (.1). ## The command '$:= $A5209 [\y{o}{o}.T{o}]' defines '$A5209' as '[\y.T]'. ## Different commands within a line can be separated with the semicolon (;), ## e.g.: ':= $M5209; := $E5209; := $T5209; := $X5209; := $A5209'. ## The command ':= $A5209' removes this definition, which is allowed here, ## since the dollar sign ($) indicates that '$A5209' is a temporary definition. ## ## Step Two (.2) ## ## Now some lambda conversions of subparts of the theorem are performed. ## To print the full wff including a list of subparts, we use the print ## command, where ':p' abbreviates ':p %0' for printing the last theorem ## obtained. ## Command: :p # ((=_((&_([\y.T]_T))_([\y.T]_F)))_((A_o)_[\x.([\y.T]_x)])) # ((={{{o,o},o}}_((&{{{o,o},o}}_([\y{o}{o}.T{o}]{{o,o}}_T{o}){o}){{o,o}}_([\y{o}{o}.T{o}]{{o,o}}_F{o}){o}){o}){{o,o}}_((A{{{o,{o,\3{^}}},^}}_o{^}){{o,{o,o}}}_[\x{o}{o}.([\y{o}{o}.T{o}]{{o,o}}_x{o}{o}){o}]{{o,o}}){o}) # { o } /00000001 ( 1) ((=_((&_([\y.T]_T))_([\y.T]_F)))_((A_o)_[\x.([\y.T]_x)])) /00000010 ( 2) (=_((&_([\y.T]_T))_([\y.T]_F))) /00000100 ( 4) = /00000101 ( 5) ((&_([\y.T]_T))_([\y.T]_F)) /00001010 ( 10) (&_([\y.T]_T)) /00010100 ( 20) [\x.[\y.((=_[\g.((g_T)_T)])_[\g.((g_x)_y)])]] # := & /00101000 ( 40) x /00101001 ( 41) [\y.((=_[\g.((g_T)_T)])_[\g.((g_x)_y)])] /01010010 ( 82) y /01010011 ( 83) ((=_[\g.((g_T)_T)])_[\g.((g_x)_y)]) /10100110 (166) (=_[\g.((g_T)_T)]) /10100111 (167) [\g.((g_x)_y)] /00010101 ( 21) ([\y.T]_T) /00101010 ( 42) [\y.T] /01010100 ( 84) y /01010101 ( 85) ((=_=)_=) := T /10101010 (170) (=_=) /10101011 (171) = /00101011 ( 43) ((=_=)_=) := T /01010110 ( 86) (=_=) /10101100 (172) = /10101101 (173) = /01010111 ( 87) = /00001011 ( 11) ([\y.T]_F) /00010110 ( 22) [\y.T] /00101100 ( 44) y /00101101 ( 45) ((=_=)_=) := T /01011010 ( 90) (=_=) /10110100 (180) = /10110101 (181) = /01011011 ( 91) = /00010111 ( 23) ((=_[\x.T])_[\x.x]) := F /00101110 ( 46) (=_[\x.T]) /01011100 ( 92) = /01011101 ( 93) [\x.T] /10111010 (186) x /10111011 (187) ((=_=)_=) := T /00101111 ( 47) [\x.x] /01011110 ( 94) x /01011111 ( 95) x /00000011 ( 3) ((A_o)_[\x.([\y.T]_x)]) /00000110 ( 6) (A_o) /00001100 ( 12) [\t.[\p.((=_[\x.T])_p)]] := A /00011000 ( 24) t /00011001 ( 25) [\p.((=_[\x.T])_p)] /00110010 ( 50) p /00110011 ( 51) ((=_[\x.T])_p) /01100110 (102) (=_[\x.T]) /11001100 (204) = /11001101 (205) [\x.T] /01100111 (103) p /00001101 ( 13) o /00000111 ( 7) [\x.([\y.T]_x)] /00001110 ( 14) x /00001111 ( 15) ([\y.T]_x) /00011110 ( 30) [\y.T] /00111100 ( 60) y /00111101 ( 61) ((=_=)_=) := T /01111010 (122) (=_=) /11110100 (244) = /11110101 (245) = /01111011 (123) = /00011111 ( 31) x ## The first subpart of the wff chosen for lambda conversion is '([\y.T]_T)', ## which can be found as subpart number 21, which is the decimal representation ## of the binary number 00010101. Removing the leading zeros and the first one, ## the remaining part ('0101') reveals the location of the subpart within the ## wff tree: left (0) - right (1) - left (0) - right (1), where each node is ## either a lambda application or a lambda abstraction. ## We can print this subpart in short form by entering '%0/21' or simply '/21'. ## Command: /21 # wff 217 : ([\y.T]_T) # w typd 217 : ([\y{o}{o}.T{o}]{{o,o}}_T{o}) { o } ## We can print this subpart in full form by entering ':p %0/21' or simply ## ':p /21'. ## Command: :p /21 # wff 217 : ([\y.T]_T) # w typd 217 : ([\y{o}{o}.T{o}]{{o,o}}_T{o}) { o } type # 0: o = 2 /00000001 ( 1) ([\y.T]_T) /00000010 ( 2) [\y.T] /00000100 ( 4) y /00000101 ( 5) ((=_=)_=) := T /00001010 ( 10) (=_=) /00010100 ( 20) = /00010101 ( 21) = /00001011 ( 11) = /00000011 ( 3) ((=_=)_=) := T /00000110 ( 6) (=_=) /00001100 ( 12) = /00001101 ( 13) = /00000111 ( 7) = ## Now we do the first lambda conversion. ## Mathematical rules start with the paragraph symbol (§), and lambda ## conversion is denoted by §\ with the backslash (\) as lambda symbol. ## Command: §\ /21 §\ /21 # ((=_([\y.T]_T))_T) ## The result is: ([\y.T]_T) = T, written in prefix notation. ## We now use the rule of substitution (§s) to replace the subformula by the ## expanded expression in the original, second to last theorem (%1), using the ## last theorem (%0) as equation, and replacing the first occurrence (0) of ## this subformula. ## Command: §s %1 %0 0 §s %1 21 %0 # ((=_((&_T)_([\y.T]_F)))_((A_o)_[\x.([\y.T]_x)])) ## R0 will automatically figure out that the first occurrence (0) is subpart ## 21, here and display the non-interactive command ('§s %1 21 %0') instead of ## the used interactive command ('§s %1 %0 0') allowing some automation for ## easy use not available in the final (non-interactive) proof script. ## Performing a lambda conversion and then using the resulting equation for ## substitution is a very common pattern, so the combination of the rules §\ ## and §s is abbreviated as '§\s'. ## The other two subparts suitable for lambda conversion are number 11 and 15. ## Command: §\s /11 §\ ([\y{o}{o}.T{o}]{{o,o}}_F{o}) # ((=_([\y.T]_F))_T) §s %1 11 %0 # ((=_((&_T)_T))_((A_o)_[\x.([\y.T]_x)])) ## Command: §\s /15 §\ ([\y{o}{o}.T{o}]{{o,o}}_x{o}{o}) # ((=_([\y.T]_x))_T) §s %1 15 %0 # ((=_((&_T)_T))_((A_o)_[\x.T])) ## This completes step 2. For later use, we store the resulting theorem as ## temporary definition '$ATMP5211'. ## Command: := $ATMP5211 %0 := $ATMP5211 %0 # wff 244 : ((=_((&_T)_T))_((A_o)_[\x.T])) := $ATMP5211 ## ## Step Three (.3) ## ## The reflexion rule (§=) creates theorems of the form A = A for any wff A. ## Command: §= ((A{{{o,{o,\3{^}}},^}}_o{^}){{o,{o,o}}}_[\x{o}{o}.T{o}]{{o,o}}) §= ((A{{{o,{o,\3{^}}},^}}_o{^}){{o,{o,o}}}_[\x{o}{o}.T{o}]{{o,o}}) # ((=_((A_o)_[\x.T]))_((A_o)_[\x.T])) ## Lambda conversion of subpart 10... ## Command: §\s /10 §\ (A{{{o,{o,\3{^}}},^}}_o{^}) # ((=_(A_o))_[\p.((=_[\x.T])_p)]) §s %1 10 %0 # ((=_([\p.((=_[\x.T])_p)]_[\x.T]))_((A_o)_[\x.T])) ## Lambda conversion of subpart 5, but use the type for truth values (o) for ## the polymorphic identity relation in the resulting equation instead of the ## default universal type (@). ## Sometimes explicit type information is required to avoid later type ## mismatch. ## Command: §\ {o} /5 §\ {o} ([\p{{o,o}}{{o,o}}.((={{{o,{o,o}},{o,o}}}_[\x{o}{o}.T{o}]{{o,o}}){{o,{o,o}}}_p{{o,o}}{{o,o}}){o}]{{o,{o,o}}}_[\x{o}{o}.T{o}]{{o,o}}) # ((=_([\p.((=_[\x.T])_p)]_[\x.T]))_((=_[\x.T])_[\x.T])) ## Substitution... ## Command: §s %1 5 %0 §s %1 5 %0 # ((=_((=_[\x.T])_[\x.T]))_((A_o)_[\x.T])) ## Save result as temporary definition. ## Command: := $BTMP5211 %0 := $BTMP5211 %0 # wff 259 : ((=_((=_[\x.T])_[\x.T]))_((A_o)_[\x.T])) := $BTMP5211 ## The following steps are trivial and do not require further comments. ## See [Andrews 2002 (ISBN 1-4020-0763-9), p. 220 (Theorem 5211)] for details. ## use Proof Template A5210: T = (B = B) ## Command: := $T5210 {o,o} := $T5210 {o,o} # wff 13 : {o,o} := $T5210 ## Command: := $B5210 /21 := $B5210 [\x{o}{o}.T{o}] # wff 17 : [\x.T] := $B5210 ## Command: << A5210.r0t.txt << A5210.r0t.txt ## Command: := $T5210; := $B5210 := $T5210 := $B5210 ## Command: %0 %0 # ((=_T)_((=_[\x.T])_[\x.T])) # ((={{{o,o},o}}_T{o}){{o,o}}_((={{{o,{o,o}},{o,o}}}_[\x{o}{o}.T{o}]{{o,o}}){{o,{o,o}}}_[\x{o}{o}.T{o}]{{o,o}}){o}) # { o } ## Command: %$BTMP5211 %$BTMP5211 # ((=_((=_[\x.T])_[\x.T]))_((A_o)_[\x.T])) := $BTMP5211 # ((={{{o,@},@}}_((={{{o,{o,o}},{o,o}}}_[\x{o}{o}.T{o}]{{o,o}}){{o,{o,o}}}_[\x{o}{o}.T{o}]{{o,o}}){@}){{o,@}}_((A{{{o,{o,\3{^}}},^}}_o{^}){{o,{o,o}}}_[\x{o}{o}.T{o}]{{o,o}}){@}) # { o } := $BTMP5211 ## Command: §s %1 3 %0 §s %1 3 %0 # ((=_T)_((A_o)_[\x.T])) ## ## Step Four (.4) ## ## Command: %$ATMP5211 %$ATMP5211 # ((=_((&_T)_T))_((A_o)_[\x.T])) := $ATMP5211 # ((={{{o,o},o}}_((&{{{o,o},o}}_T{o}){{o,o}}_T{o}){o}){{o,o}}_((A{{{o,{o,\3{^}}},^}}_o{^}){{o,{o,o}}}_[\x{o}{o}.T{o}]{{o,o}}){o}) # { o } := $ATMP5211 ## Command: §= T §= T # ((=_T)_T) ## Command: §s %0 5 %2 §s %0 5 %2 # ((=_((A_o)_[\x.T]))_T) ## Command: §s %2 3 %0 §s %2 3 %0 # ((=_((&_T)_T))_T) ## Now save the result as theorem 'A5211'. ## Command: := A5211 %0 := A5211 %0 # wff 396 : ((=_((&_T)_T))_T) := A5211 ## Undefine local variables, with two commands separated by the semicolon (;) ## Command: := $ATMP5211; := $BTMP5211 := $ATMP5211 := $BTMP5211 ## Print the theorem. ## Q.E.D. %0 # ((=_((&_T)_T))_T) := A5211 # ((={{{o,o},o}}_((&{{{o,o},o}}_T{o}){{o,o}}_T{o}){o}){{o,o}}_T{o}) # { o } := A5211 ## ## Creating wffs ## ## Building complex formulae may require multiple steps. ## An example will follow. ## For obtaining a variable g{ooo} as in the definition of the conjunction, ## we first compose type 'oo'. ## Command: {o,o} # wff 13 : {o,o} # w typd 13 : {o,o} { ^ } ## Now append another 'o'. ## Command: {{o,o},o} # wff 35 : {{o,o},o} # w typd 35 : {{o,o},o} { ^ } ## Or use the wff number. ## Command: {13,o} # wff 35 : {{o,o},o} # w typd 35 : {{o,o},o} { ^ } ## Now we can obtain g{ooo}. ## Command: g{35} # wff 36 : g # w typd 36 : g{{{o,o},o}} { {{o,o},o} } ## Create a lambda application interactively with automatic type matching (__) ## from the last wff ($_) and variable x{o}. ## Command: __ $_ x{o} __ g{{{o,o},o}} x{o} # wff 42 : (g_x) # w typd 42 : (g{{{o,o},o}}{{{o,o},o}}_x{o}{o}) # { {o,o} } ## Create a lambda abstraction interactively with automatic type matching (\\) ## from g{ooo} (wff 36 and variable x{o}. ## Command: \\ x{o} g{35} \\ x{o} g{{{o,o},o}} # wff 397 : [\x.g] # w typd 397 : [\x{o}{o}.g{{{o,o},o}}{{{o,o},o}}] # { {{{o,o},o},o} } ## Create a lambda application interactively without type matching (_), but ## explicit type information (necessary if more than one match exists). ## Command: _ g{35} {35} x{o} {o} # wff 42 : (g_x) # w typd 42 : (g{{{o,o},o}}{{{o,o},o}}_x{o}{o}) # { {o,o} } ## Create a lambda abstraction interactively without type matching (\), but ## explicit type information. ## Command: \ x{o} {o} g{35} {35} # wff 397 : [\x.g] # w typd 397 : [\x{o}{o}.g{{{o,o},o}}{{{o,o},o}}] # { {{{o,o},o},o} } ## ## Miscellaneous ## ## Rename first bound variable 'x{o}' 'in lambda abstraction '[\x.x]' to 'z'. ## Command: §r [\x{o}{o}.x{o}{o}] z{o} §r [\x{o}{o}.x{o}{o}] z{o} # ((=_[\x.x])_[\z.z]) ## Introduce a new axiom (requires flag '--allow-additional-axioms' on program ## invocation). Use with caution! ## Command: §! x{o} §! x{o} # x ## Display the new axiom. ## Command: %0 %0 # x # x{o} { o } ## Quantification ## ## From Cambridge HOL by Mike Gordon, we are already familiar with the lambda ## notation style, e.g., the internal representation ALL [\x . f] (displayed as ## ALL x . f) is a lambda application of the definable symbol 'ALL' and the ## expression '[\x . f]'. [Gordon, 2001, pp. 11, 13] ## ## While in Mike Gordon's HOL, polymorphism (the type variable mechanism) is ## only implicit, in R0, with type abstraction, the type becomes explicit: ## ALL t [\x . f], with the type (or type variable) t. ## ## This corresponds to the common notation of the universal quantifier. ## The set-theoretic expression 'ALL n : NAT . n=n', where the set (type) of ## 'n' is specified, in the type theory R0 would be expressed as: ## ALL NAT [\n . n=n] ## ## As a simple example, we shall use the equivalent theorem for the type of ## truth values: ## ALL o [\x . x=x] ## Obtain x=x ## Command: §= x{o} §= x{o} # ((=_x)_x) ## use Proof Template A5220 (Gen): A --> ALL x: A := $T5220 o # wff 2 : o := $T5220 := $X5220 x{o} # wff 16 : x := $X5220 := $A5220 %0 # wff 404 : ((=_$X5220)_$X5220) := $A5220 << A5220.r0t.txt := $T5220 := $X5220 := $A5220 %0 # ((A_o)_[\x.((=_x)_x)]) # ((A{{{o,{o,\3{^}}},^}}_o{^}){{o,{o,o}}}_[\x{o}{o}.((={{{o,@},@}}_x{o}{@}){{o,@}}_x{o}{@}){o}]{{o,o}}) # { o ... } ## The theorem ((A_o)_[\x.((=_x)_x)]) or, using infix notation, ## ALL o [\x. x=x], says, that for all x of type o (truth values), ## x is identical with itself. ## Internal type referencing ## Note that the universal quantifier has type '{{o,{o,\3{^}}},^}', or written ## without brackets, type 'o(o\3)^': ## Command: A # wff 29 : [\t.[\p.((=_[\x.T])_p)]] := A # w typd 29 : [\t{^}{^}.[\p{{o,t{^}}}{{o,t{^}}}.((={{{o,{o,t{^}}},{o,t{^}}}}_[\x{t{^}}{t{^}}.T{o}]{{o,t{^}}}){{o,{o,t{^}}}}_p{{o,t{^}}}{{o,t{^}}}){o}]{{o,{o,t{^}}}}] # { {{o,{o,\3{^}}},^} } # := A ## The specification '\3' is a reference within the type, pointing to the type ## '^' of the first argument within 'o(o\3)^', thus handling dependencies of ## types within the formula structure similar to de Bruijn indices. For ## example, the application of 'ALL' of type 'o(o\3)^' to '@' of type '^' ## would result in the wff 'ALL @' of type 'o(o@)'. ## Similarly, 'ALL NAT' would have type 'o(o NAT)'. ## Use of rule §s' (Andrews' Rule R') ## (Instead of the turnstile, the logical implication is used.) ## ## §s' is the variant of §s with hypothesis. ## ## Its application differs, as the subpart index is starting from the right ## side of the implication in order to allow straight translations from proofs ## without hypothesis (§s) to those with hypothesis (§s'). ## H => C (for C we choose A = D) §! ((=>{{{o,o},o}}_h{o}{o}){{o,o}}_((={{{o,o},o}}_a{o}{o}){{o,o}}_d{o}{o}){o}) # ((=>_h)_((=_a)_d)) ## H => A = B §! ((=>{{{o,o},o}}_h{o}{o}){{o,o}}_((={{{o,o},o}}_a{o}{o}){{o,o}}_b{o}{o}){o}) # ((=>_h)_((=_a)_b)) ## Now print C (= %1/3) only, including its subparts ## Command: :p %1/3 # wff 825 : ((=_a)_d) # w typd 825 : ((={{{o,o},o}}_a{o}{o}){{o,o}}_d{o}{o}) # { o (=>{{{o,o},o}}_h{o}{o}) } type # 0: o = 2 type # 1: (=>{{{o,o},o}}_h{o}{o}) = 822 /00000001 ( 1) ((=_a)_d) /00000010 ( 2) (=_a) /00000100 ( 4) = /00000101 ( 5) a /00000011 ( 3) d ## The subpart to be substituted, 'a', has subpart number 5, as shown by the ## last line above. ## Now do the substitution. §s' %1 5 %0 # ((=>_h)_((=_b)_d)) ## The last line of a proof file should end with a line break in order to avoid ## an error message.