[isabelle] Binding the type variable in the Axiom of Choice – Re: Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic



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 <rda at lemma-one.com>:
> 
> 
> 
>> On 12 Mar 2018, at 19:12, Ken Kubota <mail at 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 (<mail at 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 (<mail at 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

____________________





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.