. 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,
Ken Kubota
I. Corrections
1. The critique
LIBDIR=${exec_prefix}
6. Build HOL (see: http://hol-theorem-prover.org/#get ):
poly < tools/smart-configure.sml
bin/build
Kind regards,
Ken Kubota
n 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/isar-ref.pdf
[S2] Reference in t
imilarly, in Church's simple theory of types, lambda-conversion
(beta-conversion) is implemented as the second (beta-reduction, also called
beta-contraction) and third (beta-expansion) of altogether six rules of
inference [cf. Church, 1940, p. 60].
Kind regards,
Ken Kubota
References
Andrews,
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 different types for the three different language
how 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
Ken Kubota
http://doi.or
s-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://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00069.html
[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
tions 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
References
Andrews, Peter B. (1986), An Introduction to Ma
t."
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 proving environment for higher order logic, Cambridge:
t
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.
Best,
Ken
Ken Kubota
doi: 10./100
http://dx.doi.org/10./100
> Am 23.10.2016 um 05:13 schr
e-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
Ken Kubota
doi: 10./100
http://dx.doi.org/10.
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.doi.org/10./100
> Am 18.10.2016 um 15:34 schrieb Roger Bishop Jones <
ns 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, respectively.
As mentioned off-list, a PDF version of "HOL Done Right&quo
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.11.2016 um 18:0
ributing 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 regards,
Ken Kubota
____
Ke
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./100
-
es 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,
Ken Kubota
Ken Kubota
http://doi.org/10./
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
____
Ken Kub
atural 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
References
Kubota, Ken (2017), Mathematical Formulae. Available online at
h
re or less identical with mathematics in general.
(more below)
> On Sat, Apr 15, 2017 at 6:19 PM, Ken Kubota <m...@kenkubota.de> wrote:
> > Am 15.04.2017 um 22:53 schrieb vvs <vvs...@gmail.com>:
> >
> > Thanks for your answer.
> >
> > On Saturday, Apri
on.
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/2017-July/date.html
___
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.)
________
Ken Kubota
http://do
ml
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 <a.pope...@mdx.ac.uk
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 fa6b5843efba4f73c2c17206f5bab931
7f6edb31686b933147abd17af8114277 b833baf189f42c2b7587c409aecaed1f
Kind regards,
Ken Kubota
p://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-qoolnHAgAJ
> Am 18.05.2017 um 0
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./100 <http://doi.org/10./100&
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 <m...@proof-technologies.com>:
&g
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 <marioxcc...@yandex.com>:
>
> Hello.
>
> I kn
http://www.deutschestextarchiv.de/book/view/hegel_logik0102_1813?p=79
For philosophical references, please see: http://doi.org/10./100.110
For mathematical references, please see: http://doi.org/10./100.111
Kind regards,
Ken Kubota
Ke
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 brackets, type 'o(o\3)^':
## Command:A
# wff 2
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.
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
____
Ken K
icism.
For the references, please see: http://doi.org/10.4444/100.111
Best regards,
Ken
Ken Kubota
http://doi.org/10./100
Some Research Results on Logical Frameworks
Link collection:
- Twelf's wiki: http://twelf.org/wiki/Case_s
-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 schrieb L
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 <c...@perdues.com>:
>
> On Mon, Jan 22, 2018 at 4:40 PM
her 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
___
) are 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
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
__
e 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://www.owlofminerva.ne
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,
/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 expressiveness, i.e., naturally expressing all of
formal logic and mathematics with a sm
<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)
> :
>
&
ttps://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=347
<https://www.owlofminerva.net/files/formulae.pdf#page=347>
Kind regards,
Ken
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 the identity element of group
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"
> Kop
iom 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.01.2023 u
47 matches
Mail list logo
