Thanks for the huge feedback sent both publicly and privately! Please let me reply to Rob's email first.
This limitation of Mike Gordon's HOL is due to its restricted expressiveness, i.e., the inability to bind type variables, yielding a free variable in the hypothesis. In R0, however, it is possible to bind type variables with lambda, and therefore also to quantify over the type variable in the Axiom of Choice in order to obtain a formulation of the Axiom of Choice with no free (type) variable. I have tested both cases (bound and free type variable) with R0, and the R0 implementation shows the desired behavior. Files are available online: http://www.kenkubota.de/files/ac_instantiation.r0.out.pdf http://www.kenkubota.de/files/ac_instantiation.r0.txt http://www.kenkubota.de/files/ac_instantiation_wrong.r0.txt Peter's formulation of the Axiom of Choice is the following: ## Source: [Andrews 2002 (ISBN 1-4020-0763-9), p. 236] # wff 1386 : ((E_{t,{o,t}})_[\j.((A_{o,t})_[\p.((=>_((E_t)_[\x.(p_x)]))_(p_(j_p)))])]) # := AC Then I applied universal quantification with the type variable 't' (the symbol 'A' stands for the universal quantifier, and the symbol '^' stands for tau, the type of types): ## Quantified Axiom of Choice (without a free type variable) ## Source: [Kubota 2018 (new)] := QAC ((A{{{o,{o,\3{^}}},^}}_^{^}){{o,{o,^}}}_[\t{^}{^}.AC{o}]{{o,^}}) # wff 1388 : ((A_^)_[\t.AC]) := QAC Universal instantiation of the trivial theorem # ((=>_QAC)_QAC) yields the following result: # ((=>_QAC)_((E_{o,{o,o}})_[\j.((A_{o,o})_[\p.((=>_((E_o)_[\x.(p_x)]))_(p_(j_p)))])])) Note that the type variable 't' was replaced by type 'o' for Boolean values. On the other hand, trying to substitute the free type variable in # ((=>_AC)_AC) will cause an error: # error 1 [A5220H.r0t.txt]: scope violation in substitution -- bound variable '$X5221H' is free in hypothesis 'AC' and free in equation '((={{{o,o},o}}_T{o}){{o,o}}_AC{o})' (wffs 4, 1386, 1430) The proof source files are attached. The software is available at (license restrictions apply): http://doi.org/10.4444/100.10.3 After building the program (just enter 'make'), run ./R0 ac_instantiation.r0.txt ./R0 ac_instantiation_wrong.r0.txt For HTML output, run make ac_instantiation.r0.out.html and on a Mac, directly create and open the HTML output with make ac_instantiation.r0.out.html && open -a Finder $_ For PDF output, run (pandoc and LaTeX installed) make ac_instantiation.r0.out.pdf && open -a Finder $_ (Add the following line to file 'hyphenation.txt' to obtain a line break in the last formula of the PDF file:) \# $\qquad \;\;\;\;\;\;\;\;\;\;\qquad \qquad {{{\supset}}_{{{oo}o}}{QAC}_{o}}|{({{{\exists}}_{{{o{(o\backslash3)}}{\tau}}}{{(o{(oo)})}}_{{\tau}}}{[{\lambda}j_{{o{(oo)}}}.({{{\forall}}_{{{o{(o\backslash3)}}{\tau}}}{{(oo)}}_{{\tau}}}{[{\lambda}p_{{oo}}.({{{\supset}}_{{{oo}o}}{({{{\exists}}_{{{o{(o\backslash3)}}{\tau}}}{o}_{{\tau}}}{[{\lambda}x_{o}.({p}_{{oo}}{x}_{o})_{o}]})}}{({p}_{{oo}}{({j}_{{o{(oo)}}}{p}_{{oo}})})})_{o}]})_{o}]})}$ Regards, Ken ____________________ Ken Kubota http://doi.org/10.4444/100 > Am 12.03.2018 um 21:20 schrieb Rob Arthan <r...@lemma-one.com>: > > > >> On 12 Mar 2018, at 19:12, Ken Kubota <m...@kenkubota.de> wrote: >> >> Thanks, this is what I expected. >> >> Concerning the Axiom of Choice (answering Mario's email, too), its use >> should >> be expressed as a conditional of the form AC => THM (or as a hypothesis) and >> not as an axiom in order to make the appeal to it explicit. >> >> An example is the theorem in exercise X5308 in [Andrews, 2002, p. 237]: >> "X5308. Prove AC => […]" > > Due to its simple but elegant treatment of polymorphism, there is a very > significant > difference between axioms and hypotheses in Mike Gordon’s formulation of HOL. > An axiom containing a type variable can be instantiated ad lib, but in a > hypothesis, > no instantiation is allowed. So you can’t realistically say that uses of the > Axiom > of Choice should be expressed as AC => THM. Having to express a theorem > with a hypothesis comprising all the type instances of AC used in its proof > would > be unworkable. > > Regards, > > Rob. ____________________ ac_instantiation.r0.txt ____________________ ## ## Type Instantiation of the Axiom of Choice with Hypothesis ## ## ## Source: [Kubota 2018 (new)] ## ## Copyright (c) 2018 Owl of Minerva Press GmbH. All rights reserved. ## Written by Ken Kubota (<m...@kenkubota.de>). ## ## This file is part of the publication of the mathematical logic R0. ## For more information, visit: <http://doi.org/10.4444/100.10> ## << definitions1.r0.txt << K8005.r0.txt ## ## Axiom of Choice ## ## Source: [Andrews 2002 (ISBN 1-4020-0763-9), p. 236] ## := AC ((E{{{o,{o,\3{^}}},^}}_{t{^},{o,t{^}}}{^}){{o,{o,{t{^},{o,t{^}}}}}}_[\j{{t{^},{o,t{^}}}}{{t{^},{o,t{^}}}}.((A{{{o,{o,\3{^}}},^}}_{o,t{^}}{^}){{o,{o,{o,t{^}}}}}_[\p{{o,t{^}}}{{o,t{^}}}.((=>{{{o,o},o}}_((E{{{o,{o,\3{^}}},^}}_t{^}{^}){{o,{o,t{^}}}}_[\x{t{^}}{t{^}}.(p{{o,t{^}}}{{o,t{^}}}_x{t{^}}{t{^}}){o}]{{o,t{^}}}){o}){{o,o}}_(p{{o,t{^}}}{{o,t{^}}}_(j{{t{^},{o,t{^}}}}{{t{^},{o,t{^}}}}_p{{o,t{^}}}{{o,t{^}}}){t{^}}){o}){o}]{{o,{o,t{^}}}}){o}]{{o,{t{^},{o,t{^}}}}}) ## ## Quantified Axiom of Choice (without a free type variable) ## ## Source: [Kubota 2018 (new)] ## := QAC ((A{{{o,{o,\3{^}}},^}}_^{^}){{o,{o,^}}}_[\t{^}{^}.AC{o}]{{o,^}}) ## .1 %K8005 ## use Proof Template A5221 (Sub): B --> B [x/A] := $B5221 %0 := $T5221 o := $X5221 x{$T5221} := $A5221 QAC << A5221.r0t.txt := $B5221; := $T5221; := $X5221; := $A5221 %0 ## .2 ## use Proof Template A5215H (ALL I): H => ALL x: B --> H => B [x/a] := $T5215H ^ := $X5215H t{$T5215H} := $A5215H o := $H5215H %0 << A5215H.r0t.txt := $T5215H; := $X5215H; := $A5215H; := $H5215H %0 ____________________ ac_instantiation_wrong.r0.txt ____________________ ## ## Wrong Type Instantiation of the Axiom of Choice (Creating a Scope Violation) ## ## ## Source: [Kubota 2018 (new)] ## ## Copyright (c) 2018 Owl of Minerva Press GmbH. All rights reserved. ## Written by Ken Kubota (<m...@kenkubota.de>). ## ## This file is part of the publication of the mathematical logic R0. ## For more information, visit: <http://doi.org/10.4444/100.10> ## << definitions1.r0.txt << K8005.r0.txt ## ## Axiom of Choice ## ## Source: [Andrews 2002 (ISBN 1-4020-0763-9), p. 236] ## := AC ((E{{{o,{o,\3{^}}},^}}_{t{^},{o,t{^}}}{^}){{o,{o,{t{^},{o,t{^}}}}}}_[\j{{t{^},{o,t{^}}}}{{t{^},{o,t{^}}}}.((A{{{o,{o,\3{^}}},^}}_{o,t{^}}{^}){{o,{o,{o,t{^}}}}}_[\p{{o,t{^}}}{{o,t{^}}}.((=>{{{o,o},o}}_((E{{{o,{o,\3{^}}},^}}_t{^}{^}){{o,{o,t{^}}}}_[\x{t{^}}{t{^}}.(p{{o,t{^}}}{{o,t{^}}}_x{t{^}}{t{^}}){o}]{{o,t{^}}}){o}){{o,o}}_(p{{o,t{^}}}{{o,t{^}}}_(j{{t{^},{o,t{^}}}}{{t{^},{o,t{^}}}}_p{{o,t{^}}}{{o,t{^}}}){t{^}}){o}){o}]{{o,{o,t{^}}}}){o}]{{o,{t{^},{o,t{^}}}}}) ## .1 %K8005 ## use Proof Template A5221 (Sub): B --> B [x/A] := $B5221 %0 := $T5221 o := $X5221 x{$T5221} := $A5221 AC << A5221.r0t.txt := $B5221; := $T5221; := $X5221; := $A5221 %0 ## .2 ## use Proof Template A5221H (Sub): H => B --> H => B [x/A in B] := $B5221H %0 := $T5221H ^ := $X5221H t{$T5221H} := $A5221H o << A5221H.r0t.txt := $B5221H; := $T5221H; := $X5221H; := $A5221H %0 ____________________ ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
