Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Binding the type variable in the Axiom of Choi...

Email Gateway (Aug 22 2022 at 16:57):

From: Ken Kubota <mail@kenkubota.de>
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

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@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)]

Written by Ken Kubota (<mail@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]

.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

Last updated: Apr 25 2024 at 20:15 UTC