866: Structural Mapping Theory/4
Christoph Benzmueller
c.benzmueller at fu-berlin.de
Sun Feb 14 03:19:19 EST 2021
Dear Harvey,
regarding your discussion under "3. CATEGORIES AS MANY SORTED STRUCTURES" I
want to point you to a related study (jww Dana Scott) titled "Automating
Free Logic in HOL, with an Experimental Application in Category Theory";
see [1] below (further studies with this framework are reported in [2]).
These works are employing an embedding of FREE LOGIC in HOL (Isabelle/HOL),
and then the introduced "free logic layer" is exploited for formal studies
with the computer.
In [1] we start from a generalization of the standard axioms for a monoid
and *we then present a stepwise development of various, mutually equivalent
foundational axiom systems for category theory (arriving at the axiom
system proposed by Dana Scott in the 1970's; see [3]).* We also study in
detail the relation of this axiom system to the axiom system presented by
Peter Freyd and Andre Scedrov in their 1990 textbook [4]. One interesting
aspect is (as we also discuss in [1]) how strictness of functions is
handled in both works (explicit, elegant handling in Scott's axioms system
versus implicit background assumptions in the work by Freyd and Scedrov).
Maybe our contributions are of some use for your project.
Best regards,
Christoph
[1] Automating Free Logic in HOL, with an Experimental Application in
Category Theory (Christoph Benzmüller, Dana S. Scott), In Journal of
Automated Reasoning, Springer Netherlands, volume 64, number 1, pp. 53--72,
2020. (Preprint: http://doi.org/10.13140/RG.2.2.11432.83202)
[2] Computer-supported Exploration of a Categorical Axiomatization of
Modeloids (Lucca Tiemens, Dana S. Scott, Christoph Benzmüller, Miroslav
Benda), In Relational and Algebraic Methods in Computer Science -- 18th
International Conference, RAMiCS 2020, Palaiseau, France, April 8--11,
2020, Proceedings, Springer, Lecture Notes in Computer Science, volume
12062, pp. 302--317, 2020. (Preprint (with proofs):
https://www.researchgate.net/publication/336838722)
[3] Scott D. (1979) Identity and existence in intuitionistic logic. In:
Fourman M., Mulvey C., Scott D. (eds) Applications of Sheaves. Lecture
Notes in Mathematics, vol 753. Springer, Berlin, Heidelberg.
https://doi.org/10.1007/BFb0061839
[4] Peter Freyd and Andre Scedrov (1990) Categories, Allegories,
Mathematical Library Vol 39, North-Holland. ISBN 978-0-444-70368-2.
*--*
*Christoph Benzmüller *(http://christoph-benzmueller.de)
On Sat, 13 Feb 2021 at 06:50, Harvey Friedman <hmflogic at gmail.com> wrote:
> SMAT (structural mapping theory) continues to clarify and evolve. The
> starting point that generates the excitement is
> [1]
> https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
> #113
> especially section 3.
>
> 1. Special Role of Set Theoretic Foundations - Ultimate Foundations
> https://cs.nyu.edu/pipermail/fom/2021-February/022480.html
> 2. Many sorted structures.
> https://cs.nyu.edu/pipermail/fom/2021-February/022480.html
> 3. Categories as many sorted structures - here
> 4. Semigroups of Functions - here
>
> 3. CATEGORIES AS MANY SORTED STRUCTURES
>
> NOBODY IS SUGGESTING HERE THAT ANYBODY CHANGE THEIR MATHEMATICAL
> NOTATION. I AM ONLY TALKING ABOUT ULTIMATE FOUNDATIONS WHICH YOU DO
> NOT HAVE TO TAKE INTO CONSIDERATION WHEN YOU DO YOUR MATHEMATICS. YOU
> CAN LET FOUNDATIONALISTS LIKE ME WORRY ABOUT ALL THIS.
>
> Putting categories under the rigid sweeping *unusually rigorous and
> specific* umbrella of many sorted structures is rather typical of how
> this is routinely done throughout mathematics, and does involve our
> use of FREE LOGIC that we explained in SMAT/3.
>
> A category is a many sorted structure of the form (OBJ,MORPH; ; ; dom,
> cdm, id, comp). The items before the semicolon are the list of sorts.
> After the semicolon, there is listed the constants, followed by a
> semicolon, then the relations, followed by a semicolon, and finally
> the functions, followed by ). There are only FINITELY many things
> overall that are listed. There must be at least one sort listed.
>
> In the case here, there are no constants, no relations, and four
> functions. Constants always denote. Functions are always partial
> functions (they may or may not be everywhere defined). The constants,
> relations, and functions have to come with the relevant sorts. HERE WE
> have omitted them in order to not shock the reader. Here is the full
> presentation.
>
> (OBJ,MORPH; ; ; dom(MORPH into OBJ), cdm(MORPH into OBJ), id(OBJ into
> MORPH), comp(MORPH x MORPH into MORPH)
>
> To be a category, this many sorted structure must obey a few
> fundamental sentences.
>
> a. For all morphisms x, dom(x) defined, and cdm(x) defined.
> b. For all objects x, id(x) defined.
> c. For all objects x, dom(id(x)) = cdm(id(x)) = x.
> d. For all morphisms x,y, comp(x,y) defined if and only if cdm(x) = dom(y).
> e. For all morphisms x,y,z, if cdm(x) = dom(y) then comp(x,y) is
> defined and dom(comp(x,y)) = dom(x) and cdm(comp(xy)) = cdm(y).
> f. For all morphisms x,y,z, comp(comp(x,y),z) =* comp(x,comp(y,z)).
> g. For all objects x and morphisms y, if dom(y) = x then comp(id(x),y) = y.
> h. For all objects x and morphisms y, if cdm(y) = x then comp(y,id(x)) = y.
>
> Notice we have used "defined" and = and =* as explained in SMAT/3 with
> FREE LOGIC.
>
> There are some redundancies here. b logically follows from g.
>
> NOTE: Unless stated otherwise, we demand that the sorts of a many
> sorted structure be SETS. The class theoretic version is of course
> allowing the sorts to be CLASSES. The above is therefore the
> definition of a SMALL CATEGORY. Under this terminology, a CATEGORY is
> a many sorted CLASS structure, which is the same as a many sorted
> structure, but where we allow the sorts to be PROPER CLASSES, and also
> allow the relations and functions to be PROPER CLASSES. Since the
> functions in a many sorted structure are only PARTIAL functions, even
> if the sorts are PROPER CLASSES, the relations and functions may all
> be SETS. Constants are always sets because they are elements of sorts,
> and any ELEMENT of a CLASS is a set.
>
> NOTE: My attitude towards classes is fluid.
>
> 4, STRUCTURES OF FUNCTIONS
>
> We now come to fitting the initial result that started all this
> commotion, into this framework. I am referring of course to
> [1]
> https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
> #113
> especially section 3.
>
> We could simply define SMAT in the following FAR TOO GENERAL WAY:
>
> *) SMAT is the investigation of which many sorted structures (set or
> classlike) have a non surjective mapping preserving certain basic
> relationships.
>
> Aside from not being even remotely specific concerning what
> preservation is being sought after, there is no indication of what
> kinds of many sorted structures should be looked at for this to be
> interesting.
>
> Now it may well be that *) is actually quite interesting and fruitful
> in many contexts far more broad than anything that I have in mind
> presently, or anything even remotely suggested by [1]. But at this
> stage, of course we need to do a hell of a lot better than *).
>
> We will start very close to home. Home is the semigroup of all f:D
> into D under composition. This is the symmetric semigroup on D.
>
> DEFINITION. Let phi be a first order theory of a single unary function
> f:D into D. Let SG(phi,D) be the semigroup generated by taking all f:D
> into D obeying phi.
>
> QUESTION: Is there a D such that there is a non surjective solvable
> equation preserving mapping of SG(phi,D)?
>
> Clearly yes from [1] using large cardinal hypothesis I2. And for this
> to always be the case for any phi, that is equivalent to I2 according
> to [1]. But for particular phi, it is far from clear what the status
> of this question is.
>
> ##########################################
>
> My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
> https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
> This is the 866th in a series of self contained numbered
> postings to FOM covering a wide range of topics in f.o.m. The list of
> previous numbered postings #1-799 can be found at
> http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
>
> 800: Beyond Perfectly Natural/6 4/3/18 8:37PM
> 801: Big Foundational Issues/1 4/4/18 12:15AM
> 802: Systematic f.o.m./1 4/4/18 1:06AM
> 803: Perfectly Natural/7 4/11/18 1:02AM
> 804: Beyond Perfectly Natural/8 4/12/18 11:23PM
> 805: Beyond Perfectly Natural/9 4/20/18 10:47PM
> 806: Beyond Perfectly Natural/10 4/22/18 9:06PM
> 807: Beyond Perfectly Natural/11 4/29/18 9:19PM
> 808: Big Foundational Issues/2 5/1/18 12:24AM
> 809: Goedel's Second Reworked/1 5/20/18 3:47PM
> 810: Goedel's Second Reworked/2 5/23/18 10:59AM
> 811: Big Foundational Issues/3 5/23/18 10:06PM
> 812: Goedel's Second Reworked/3 5/24/18 9:57AM
> 813: Beyond Perfectly Natural/12 05/29/18 6:22AM
> 814: Beyond Perfectly Natural/13 6/3/18 2:05PM
> 815: Beyond Perfectly Natural/14 6/5/18 9:41PM
> 816: Beyond Perfectly Natural/15 6/8/18 1:20AM
> 817: Beyond Perfectly Natural/16 Jun 13 01:08:40
> 818: Beyond Perfectly Natural/17 6/13/18 4:16PM
> 819: Sugared ZFC Formalization/1 6/13/18 6:42PM
> 820: Sugared ZFC Formalization/2 6/14/18 6:45PM
> 821: Beyond Perfectly Natural/18 6/17/18 1:11AM
> 822: Tangible Incompleteness/1 7/14/18 10:56PM
> 823: Tangible Incompleteness/2 7/17/18 10:54PM
> 824: Tangible Incompleteness/3 7/18/18 11:13PM
> 825: Tangible Incompleteness/4 7/20/18 12:37AM
> 826: Tangible Incompleteness/5 7/26/18 11:37PM
> 827: Tangible Incompleteness Restarted/1 9/23/19 11:19PM
> 828: Tangible Incompleteness Restarted/2 9/23/19 11:19PM
> 829: Tangible Incompleteness Restarted/3 9/23/19 11:20PM
> 830: Tangible Incompleteness Restarted/4 9/26/19 1:17 PM
> 831: Tangible Incompleteness Restarted/5 9/29/19 2:54AM
> 832: Tangible Incompleteness Restarted/6 10/2/19 1:15PM
> 833: Tangible Incompleteness Restarted/7 10/5/19 2:34PM
> 834: Tangible Incompleteness Restarted/8 10/10/19 5:02PM
> 835: Tangible Incompleteness Restarted/9 10/13/19 4:50AM
> 836: Tangible Incompleteness Restarted/10 10/14/19 12:34PM
> 837: Tangible Incompleteness Restarted/11 10/18/20 02:58AM
> 838: New Tangible Incompleteness/1 1/11/20 1:04PM
> 839: New Tangible Incompleteness/2 1/13/20 1:10 PM
> 840: New Tangible Incompleteness/3 1/14/20 4:50PM
> 841: New Tangible Incompleteness/4 1/15/20 1:58PM
> 842: Gromov's "most powerful language" and set theory 2/8/20 2:53AM
> 843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
> 844: Brand New Tangible Incompleteness/2 3/24/20 12:37AM
> 845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
> 846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
> 847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
> 848. Set Equation Theory/1 4/15 11:45PM
> 849. Set Equation Theory/2 4/16/20 4:50PM
> 850: Set Equation Theory/3 4/26/20 12:06AM
> 851: Product Inequality Theory/1 4/29/20 12:08AM
> 852: Order Theoretic Maximality/1 4/30/20 7:17PM
> 853: Embedded Maximality (revisited)/1 5/3/20 10:19PM
> 854: Lower R Invariant Maximal Sets/1: 5/14/20 11:32PM
> 855: Lower Equivalent and Stable Maximal Sets/1 5/17/20 4:25PM
> 856: Finite Increasing reducers/1 6/18/20 4 17PM :
> 857: Finite Increasing reducers/2 6/16/20 6:30PM
> 858: Mathematical Representations of Ordinals/1 6/18/20 3:30AM
> 859. Incompleteness by Effectivization/1 6/19/20 1132PM :
> 860: Unary Regressive Growth/1 8/120 9:50PM
> 861: Simplified Axioms for Class Theory 9/16/20 9:17PM
> 862: Symmetric Semigroups 2/2/21 9:11 PM
> 863: Structural Mapping Theory/1 2/4/21 11:36PM
> 864: Structural Mapping Theory/2 2/7/21 1:07AM
> 865: Structural Mapping Theory/3 2/10/21 11:57PM
>
> Harvey Friedman
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210214/74965cad/attachment-0001.html>
More information about the FOM
mailing list