This might be relevant to some other mailing lists as well.
> Anfang der weitergeleiteten Nachricht:
>
> Von: Ken Kubota
> Betreff: Aw: [isabelle] New in the AFP: Eudoxus Reals
> Datum: 4. November 2023 um 03:34:06 MEZ
> An: "Prof. Lawrence C. Paulson"
> Kopie:
ntified Axiom of Choice (without a free type variable)
∀τ[λt.AC]o
(wff 1388 = QAC)
is to be read as
∀ t . AC
where "t" is the type variable in question here.
Regards,
Ken
________
Ken Kubota
https://doi.org/10./100
> Am 16
e of Substitution / Proof Template A5221H (Sub):
https://www.owlofminerva.net/files/formulae.pdf#page=82
<https://www.owlofminerva.net/files/formulae.pdf#page=82>
Example for type substitution:
https://www.owlofminerva.net/files/formulae.pdf#page
available-for-download/
The well-formed formula
lggg
(or l: g -> g-> g) corresponds to the HOL4 expression of the binary operation
of group
op: 'a -> 'a -> 'a;
and the wff
eg
(or e: g) corresponds to the HOL4 expression of
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-July/msg00074.html>
Kind regards,
Ken Kubota
____
Ken Kubota
https://doi.org/10./100
> Am 03.02.2021 um 03:47 schrieb Norrish, Michael (Data61, Acton)
> :
>
>&
g00074.html
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00074.html>
But I am not aware of any current attempts to overcome the obvious
restrictions, which is not satisfying for a logician/mathematician.
Following Andrews' concept of expr
https://hol-theorem-prover.org/logic.pdf
<https://hol-theorem-prover.org/logic.pdf>
Kind regards,
Ken Kubota
____________
Ken Kubota
http://doi.org/10./100 <http://doi.org/10./100>
> Am 08.11.2019 um 16:48 schrieb Miranda,
.
Mike Gordon: "It must be admitted that the ε-operator looks rather suspicious."
[Gordon, 2001, p. 24] "The inclusion of ε-terms into HOL 'builds in' the Axiom
of Choice [...]." [Gordon, 2001, p. 24]
http:/
html#white-versus-brown-coats>
https://arxiv.org/pdf/1806.04002.pdf
<https://arxiv.org/pdf/1806.04002.pdf>, p. 2
Ken Kubota
________
Ken Kubota
http://doi.org/10./100 <http://doi.org/10./100>
> Am 07.07.2018 um 16:16 sc
veness", is discussed at
https://sympa.inria.fr/sympa/arc/coq-club/2017-02/msg00024.html
<https://sympa.inria.fr/sympa/arc/coq-club/2017-02/msg00024.html>
For references, please see: http://doi.org/10./100.111
Kind regards,
Ken Kubota
___
ontradiction [...], namely [...] negation as
self-reference." [Hegel, 1986 ff., vol. 6, p. 66, originally published in 1813;
translation by the author]
http://www.deutschestextarchiv.de/book/view/hegel_logik0102_1813?p=79
For philosophical references, please see: http://doi.org/10./
Dear Mario,
In order to preserve the font and layout information required to display
the formulae properly, let me copy to the Metamath list.
> Am 05.06.2018 um 01:22 schrieb Mario Xerxes Castelán Castro
> :
>
> On 02/06/18 09:33, Ken Kubota wrote:
>> Set theory (e.g., Z
r than Isabelle/HOL)
instead of
Metamath
Isabelle/ZF (but much less popular than Isabelle/HOL)
Ken
Ken Kubota
http://doi.org/10./100
## Internal type referencing
## Note that the universal quantifier has type '{{o,{o,\3{^}}},^}', or written
## without bracke
as
intended in Russell's philosophical program of logicism.
For the references, please see: http://doi.org/10./100.111
Best regards,
Ken
Ken Kubota
http://doi.org/10./100
Some Research Results on Logical Frameworks
Li
{{{\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}.
Isabelle and Metamath. These are also the only
two logical frameworks mentioned by Freek Wiedijk as of 2003, see p. 9 at
http://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf
Kinds regards,
Ken Kubota
Ken Kubota
http://doi.org/10./100
ether these are
axioms of pure logic or of mathematics" [Andrews, 2002, p. 204], and I also
clearly regard all of them as non-logical axioms. Note that they are not Axioms
for Q0 [cf. Andrews, 2002, p. 213].
For the references, please see: http://doi.org/10./100.111
Ken Kubota
__
We note that for this axiom it suffices to take the
simple formula [...]." [Andrews, 1963, p. 350]
http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52123.pdf
http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52124.pdf
The quote with the formulas is also available (p. 4) at
http://www.owlof
ced (which in HOL express the bijection for each new type).
Best regards,
Ken
________
Ken Kubota
http://doi.org/10./100
> Am 23.01.2018 um 03:21 schrieb Cris Perdue :
>
> On Mon, Jan 22, 2018 at 4:40 PM, wrote:
> HOL’s core princi
to publish a full description by the
end of the year.
Kind regards,
Ken Kubota
____________
Ken Kubota
http://doi.org/10./100
> Am 30.08.2017 um 17:36 schrieb Mario Castelán Castro :
>
> Hello.
>
> I know that HOL4 and HOL Ligh
Girards.html
http://dblp.org/rec/conf/lics/Coquand86
http://dblp.dagstuhl.de/db/conf/lics/lics86.html
Best regards,
Ken
________
Ken Kubota
http://doi.org/10./100
> Am 24.07.2017 um 14:07 schrieb Andrei Popescu :
>
> Hi C
not possible in standard mode, i.e., without explicitly passing the
flag "–allow-definition-removal" and
with the standard definitions in "basics.r0.txt" either as first command line
argument or included at the beginning of the file.)
art, as in the HOL/HOL4 documentation.
The Isabelle/HOL documentation currently doesn't conform to this clear standard
established by the original HOL system.
The emails quoted are attached below.
The full discussion is available at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users
ty of faithfulness is provided.
Concerning this question, I haven't studied HOL Zero and Metamath yet.
Best regards,
Ken
____
Ken Kubota
http://doi.org/10./100
> Am 25.06.2017 um 11:17 schrieb Mark Adams :
>
> Hi Ken,
>
> On 20/
o’s Solutions for Pollack-Inconsistency”
http://www.proof-technologies.com/papers/hzsyntax_itp2016.pdf
<http://www.proof-technologies.com/papers/hzsyntax_itp2016.pdf>
Kind regards,
Ken Kubota
Ken Kubota
http://doi.org/10
ls can be found at
http://www.owlofminerva.net/files/README.txt
Best regards,
Ken Kubota
________
Ken Kubota
http://doi.org/10./100
Link to mail and attachment:
https://groups.google.com/d/msg/metamath/I9obSTiuDl4/t-qoolnH
h, a mere proof checker (practically without any automation
at all).
A full treatment of R0 shall be announced at
http://doi.org/10./100.10.1
For references, please see: http://doi.org/10./100.111
The SHA-512 checksum for file 'R0-v1.0.0.tar.gz' is:
538e742c5d42258cf460e46d84c60ceb fa6
e or less identical with mathematics in general.
(more below)
> On Sat, Apr 15, 2017 at 6:19 PM, Ken Kubota wrote:
> > Am 15.04.2017 um 22:53 schrieb vvs :
> >
> > Thanks for your answer.
> >
> > On Saturday, April 15, 2017 at 11:00:55 PM UTC+3, Ken Kubota wrote:
>
e’s Prooftoys
( http://prooftoys.org , http://mathtoys.org ) - a natural deduction variant of
Andrews' Q0 - in R0, the turnstile symbol is replaced by the logical
implication [p. 12].
Kind regards,
Ken Kubota
Ken Kubota
http://doi.org/10./100
Re
seems as
if independently in same cases for this variant of Q0 exactly the same design
decisions were made as for R0, in particular, the replacement of the turnstile
by the logical implication, and the corresponding implementation of Rule R'.
Kind regards,
Ken Kubota
__
ke in
Goedel's proof) and show that they are isomorphic in terms of the theorems that
can be obtained in them. I would then argue that the other systems (natural
deduction) derive their legitimacy through this isomorphism to the original
more basic (Hilbert-style) logic.
Ken
_
//doi.org/10.1007/978-3-540-71067-7_6
The latter I found as reference no. 14 of Mark's 2016 paper.
Please let me know if you have other suggestions.
Kind regards,
Ken Kubota
Ken Kubota
http://doi.org/10./100
rovided by its syntactic
features.
Of course, Coq's way of expressing mathematics is perfectly legitimate and
produced impressive results. In particular, I like Russell O'Connor's proof of
what is called Goedel's First Incompleteness Theorem, as it quite elegantly
uses three
00.111
in order to clearly distinguish between approaches that rely on the
Curry-Howard isomorphism, and those that do not.
An adequate answer to the many arguments you gave will require some more time.
Thank you very much for your patience in advance.
Kind regards,
Ken Kubota
_________
ied with level 2 [2. Polymorphic Type Theory (PTT)
(type variables without quantification)].
However, R0 provides syntactic features which allow to replace the HOL
extensions with more natural means of expression:
https://sourceforge.net/p/hol/mailman/message/35448609/
Kind regards,
eemed to me insuperable
difficulties."
Quoted in: [Andrews, 2014b, p. 67]
Available online at: http://www.hist-analytic.com/Ramsey.htm
For the references, please see:
http://doi.org/10./100.111
Kind regards,
Ken Kubota
Ken Kubota
http://doi.org/10.
admits only a very restricted form of type
dependency are given, which Natarajan Shankar very kindly explained in an
e-mail:
http://pvs.csl.sri.com/mail-archive/pvs-help/msg01865.html
Ken
Ken Kubota
doi: 10./100
http://dx.doi.org/10./100
> Am 01.
, as the dependencies should be recorded
explicitly with the syntactic means of the formal language (as intended by
Russell), which is the typing (allowing only certain wffs) and the restriction
on (type) variables in Rule R' in Q0/R0 or the binding of (type) variables with
lambda,
ning de Bruijn terms in favour of a return to name-carrying
syntax."
https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf (p. 222)
Maybe it is best to continue discussion after the publication of R0, when
comparisons can be made easier.
Best,
Ken
y Andrews' definition of C, see Andrews' theorem 5313 and its
formal verification (here with type abstraction) at
http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf
(pp. 165 ff.)
Thank you very much for this interesting information, John.
icism
concerning the (current) HOL family quoted in the "Criticism" section.
Ken Kubota
____
Ken Kubota
doi: 10./100
http://dx.doi.org/10./100
> Anfang der weitergeleiteten Nachricht:
>
> Von: Ken Kubota
> Concerning Roger Jones' remarks, le
ttp://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf
(p. 12)
in the Historical Notes section. Note that Church mentions both, and Carnap, in
the first footnote
of his 1940 article.
Best regards,
Ken
Ken Kubota
doi: 10./100
http://dx.
which I found helpful.
Best regards,
Ken
____
Ken Kubota
doi: 10./100
http://dx.doi.org/10./100
> Am 17.10.2016 um 12:23 schrieb Rob Arthan :
>
> Ken,
>
> Thanks for sharing this interesting work.
>
> Two implemented systems that are alive
ited space, unfortunately not all people contributing to existing
projects could be mentioned.
For example, I am well aware that Michael Norrish maintains and contributes to
HOL4.
I apologize for having to restrict the presentation, mentioning only the
initiators or project leaders.
Kind r
[cf. Andrews, 2002, p. 235]
(which in turn requires the Axiom of Descriptions), not theorem 5312.
Kind regards,
Ken Kubota
References
Kubota, Ken (2015c), Proof of K8033. Available online at
http://www.kenkubota.de/files/R0_draft_excerpt_with_proof_of_K8033.pdf
(September 12, 2016). SHA-512
xiom of Choice,
but requiring the Axiom of Descriptions only. The Axiom of Descriptions allows
one to extract the single element from a singleton (unit set).
At the very first glance, your proposition might be derivable from theorem 5312
[cf. Andrews, 2002, p. 235].
Kind regards,
Ken Kubota
Refe
e
browser, e.g., via
https://hol-theorem-prover.org/documents/kananaskis-10-logic.pdf
since a download is a barrier for many people, for example, due to security
considerations, or at public terminals providing browsing, but not downloading.
For references, please see:
https:
Q0, and then to derive more
complex rules from it."
http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf
(p. 27)
Kind regards,
Ken Kubota
References
Gordon, Michael J. C., and Melham, Thomas F., eds. (1993), Introduction to HOL:
A theorem prov
makes use of a
function "SubFree" denoting the process of substitution (of all free
occurrences of a variable):
http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/#ForBasEqu
Similarly, in Church's simple theory of types, lambda-conversion
(bet
ml-5.6-1/x86-darwin
BINDIR=${exec_prefix}
LIBDIR=${exec_prefix}
6. Build HOL (see: http://hol-theorem-prover.org/#get ):
poly < tools/smart-configure.sml
bin/b
as properties in the definition of "Grp" (wff 266):
http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf
(p. 359)
Kind regards,
Ken Kubota
Sources
[S1] The Isabelle/Isar Reference Manual (February 17, 2016)
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isa
Russell O'Connor (in Coq) and Lawrence C. Paulson (in Isabelle) is undertaken
in order to foster the understanding of the proof. The type system implemented
by O'Connor is particularly well suited for demonstrating the three different
language levels in the proof.
Kind regards,
dence between the theorems/metatheorems of
the implementations of both automated deduction and proof verification, ideally
by a metamathematical proof arithmetizing both systems, or at least by
comparison of canonical definitions and proofs. My preference would be the
generation of R0 code by p
dence between the theorems/metatheorems of
the implementations of both automated deduction and proof verification, ideally
by a metamathematical proof arithmetizing both systems, or at least by
comparison of canonical definitions and proofs. My preference would be the
generation of R0 code by p
54 matches
Mail list logo
