FYI:Principia Logico-Metaphysica (Draft/Excerpt) Edward N. Zalta

[alex.shkotin]

Colleagues,

ENZ is well known for to be co-principal editor of https://plato.stanford.edu/info.html 

I just have got the URL to his axiomatic theory  https://mally.stanford.edu/principia.pdf may be interesting to compare with  TLOs. 

Just keep in mind that it is not only axiomatic but formalized one using Isabelle/HOL.

Alex

And two extractions to feel in.

(271) Remark: In Preparation for Kirchner’s Theorem. By deploying tools developed by, and in collaboration with, Christoph Benzmüller, Daniel Kirchner has been implementing object theory in Isabelle/HOL.188 This implementation consists of two parts: (a) a shallow semantic embedding of object theory in Isabelle/HOL, and (b) a reconstruction of PLM’s deductive system. (a) The shallow semantic embedding uses the infrastructure of Isabelle/HOL (which includes set theory in the framework of functional type theory) to (i) construct enhanced Aczel models of object theory, (ii) reconstruct (i.e., define) the syntax of object theory in terms of this model (by preserving and using as much of the syntax of Isabelle/HOL as possible),189 and (iii) prove that the axioms of object theory, thus reconstructed, are true in the model. (b) Using the shallow semantic embedding as a basis, Kirchner implements object theory computationally by rebuilding its deductive system, as developed here, on top of the reconstructed axioms. Thus, the automated/interactive reasoning system that results doesn’t imply any artifactual theorems, i.e., the resulting proof system doesn’t imply any set-theoretic consequences of the Aczel model that are not expressible in the language of object theory or any consequences that are expressible but not derivable in object theory.

[John F Sowa]

Alex,

Thanks for that info.   Zalta's Principia is a huge compendium (1501 pages with more to come) of formal definitions and proofs.  The Isabelle theorem prover is an excellent basis for automated reasoning with and about anything that uses those definitions.  And the supporting software can be downloaded for free.

As I said before, I was highly skeptical about any formal definitions developed in Ontolog Forum, because this is not a standards organization.  However, if the definitions are taken from or based on Zalta's Principia and supported by Isabelle, they can be posted in web pages shared by anybody and everybody.   I'm sure that Stanford would support or collaborate with anybody who develops such a repository.

Re Top-Level Ontologies:  The TLOs are specified in very restricted formats in a tiny subset of first-order logic.  Isabelle supports all of FOL plus much, much more.  As I have been pointing out, FOL is much simpler, more general, easier to use, and faster than OWL2.  The availability of Isabelle with all of the definitions in Zalta's tome would make a strong argument for OWL3 (the same notation for the hierarchy as OWL2, but full FOL as an upgrade).

There is a question about Common Logic, which is a different extension to FOL,  I believe that the HeTS tools could be extended to support mappings of CL to and from Isabelle. There are various issues about the mappings, and HeTS is sufficiently general that it could be extended to support them. 

Any TLO specified in OWL can be automatically mapped to FOL (the extension to OWL3) and used with anything specified in the Zalta's system.   Although Isabelle supports HOL, a large majority of the structures defined by Zalta use only the FOL subset.

Common Logic is a different extension to FOL.  The HeTS tools  and the OMG standard for DOL could be used to do the mappings. 

Since Isabelle also supports FOL as a subset, it would be a good tool for supporting OWL3.    That's another argument for getting rid of the limitations and exceptions of OWL2 and move to OWL3.  Existing applications that use OWL2 would not be affected.  But new applications could use the simpler OWL3 notation.

For more about Isabelle and links to resources, see the Wikipedia page:  https://en.wikipedia.org/wiki/Isabelle_(proof_assistant) .

John

_______________________________________

 

From: "alex.shkotin" <alex.s...@gmail.com>

Colleagues,

Edward N. Zalta is well known for to be co-principal editor of https://plato.stanford.edu/info.html .  I just got the URL to his axiomatic theory  https://mally.stanford.edu/principia.pdf may be interesting to compare with  TLOs. 

It is not only axiomatic but formalized one using Isabelle/HOL.

Alex

[Alex Shkotin]

John,

My position is utilitarian: there is a formalized axiomatic theory of Metaphysics [1]. Can we apply it when building our top-level formal ontologies? For example, BFO.

Have a look at p.502 I put after all.

Of course, another interesting issue is the use of Isabelle for writing and working with formal ontologies.

Isabelle is known in the hets.eu project, but nothing has been heard about ontologies on Isabelle.

If we talk about the formalization of physical theories on Isabelle, then I saw literally one recent work on the formalization of Lagrange Mechanics.

Physics is closely related to Geometry. And also somewhere at the beginning of the century there was work on the formalization in Isabelle of Hilbert's axiomatic theory of geometry.

It is interesting to see an example of a formal ontology made in Isabelle.

A lot of scientific and engineering knowledge should be formalized before to feed it to robots 🌩️

Alex

[1] https://mally.stanford.edu/principia.pdf

вт, 25 июн. 2024 г. в 21:01, John F Sowa <so...@bestweb.net>:

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info/
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/dc4823556f94495186d421d1d90bd334%40bestweb.net.