To be fair, that's not it. I feel like you didn't address my specific question or expand on your remarks about fiber bundles, fibrations, and the n-tuples of real numbers taken as synonymous with propositions. Those are the kind of "bread and butter" things I'm trying to understand. But like I say I'm perfectly ok with that, because I got my money's worth from discovering Mac Lane. — fishfry
Minimal set of universal properties. That might be over my head. I know what universal properties are in terms of defining things like free groups, tensor products, and the like. I'm ignorant of what it would mean to select for certain universal properties. Or I'm not understanding you. — fishfry
Yes, but that correspondence is evident only in a dependent type theory, where you can make sense of the topology defined on your set of propositions (only open sets are propositions). In standard logic you cannot make sense of the topological structure of the space: no distinction between open and closed sets. All sets are both open and closed. That's the reason why taking the complement of the complement is an identity (boolean logic!). How can I show you the correspondence with dependent type theory without explaining dependent type theory? — Mephist
That's pretty standard old-fashioned model theory and first order logic (the topology is irrelevant: forget about open sets and take simply the set of all subsets of a given set R). I noticed that other people on this site were starting some kind of "introduction to first order logic" thing. Maybe they can help to make clear this part. — Mephist
Yes, well, the point is that you cannot "count" the objects of a category. You cannot distinguish between isomorphic objects. There is no "equality" relation defined on the set of all objects. How can you decide what's the cardinality of the set of all objects if you cannot associate them with another set? (no one-to-one correspondence possible between elements. Only equivalence makes sense, not equality!) — Mephist
Part one: C is a category ( like A is an abelian group )
Part two: for each pair of objects of A, B there is a "product object" P ( like for each pair of elements (a,b) of A there is a product element: A is a ring ) ( omitting other needed properties, of course... )
Adding properties to the category I add structure! For example, each pair of objects has a product, the set of objects has to be infinite (pairs made of other pairs recursively). In general, without this requirement, a category may even be made of 3 objects and 4 arrows... — Mephist
without this requirement, a category may even be made of 3 objects and 4 arrows... — Mephist
If we extended the topology to the product space ×JΩ×JΩ, I thiiiink this ends up being the discrete topology? But then it's also the set of all truth table rows of propositional logic formulae containing at most |J||J| propositions (well, so long as they don't contain duplicates...). — fdrake
Well, I know what a fiber bundle is so if you claim something is a fiber bundle you could just explain what it is that's the fiber bundle. What is the underlying set, what are the fibers above each point, etc. But maybe there's too much of an explanatory gap and we're at a point of diminishing returns. — fishfry
This is not about introduction to first order logic. This is about an explanatory gap. The topology is not irrelevant if you claim to have a sheaf. Perhaps we're done. — fishfry
We're talking past each other. And this is not about cardinalities at all since neither proper classes nor categories (in general) have cardinalities. But I think between what you know and what you're able to explain, and what I know and what I'm able to understand of what you're saying, we have a gap that's not getting bridged. — fishfry
And why would that be a problem? A group is a category with one element. — fishfry
and open sets are naturally represented as types in type theory — Mephist
In your model the topology of omega is not used, and there is no topology defined on the space of all propositions (how do you define the set of open sets of propositions?) — Mephist
So you get a discrete space of points split in two equivalence classes: true propositions and false propositions. — Mephist
I was hoping you'd be able to tell me, as it seems defining what a topology is in terms of the logic is precisely where the missing intuition is. I assumed there was some topology on the space of propositions, and tried to see if "pushing back" the open sets of the topology on ×KΩ×KΩ through the interpretation II made sense to you.
Something like, if we have a logical connective's truth function ff from ×KQ→Ω×KQ→Ω, and we glue together open sets on ×KΩ×KΩ 's discrete topology through the fibre {I(a)=1=f(c)|a∈×KQ,1∈Ω,c∈×KΩ}{I(a)=1=f(c)|a∈×KQ,1∈Ω,c∈×KΩ}. I guess inducing a topology by pulling back a topology through a continuous function and a connective (dunno if that works at all). — fdrake
It perhaps doesn't make much sense. Do you know the analogous construction for classical (or intuitionist) propositional logic? — fdrake
So we don't have to deal with the interpretation being a complicated set valued function. It should be in there somewhere and easier to talk about to exhibit a connection between a topology on the logic and a toplogy on the Omega product. — fdrake
The underlying set is the set of all propositions. The fibers are sets of elements of our model. — Mephist
The underlying set is the set of all propositions. The fibers are sets of elements of our model. — Mephist
would the pre-image of any open set of ΩΩ with the discrete topology be a type, and thus a proposition? Or a collection of propositions which co-satisfy/are equivalent? — fdrake
OK, I understand what you want to do. But in the case of fiber bundles you don't define the topology of the total space in terms of the topology of the base space. You assume a preexisting topological space E (the total space), and a preexisting topological space B (the base space), and a continuous function P from E to B, and then you define the fibers as inverse images of P. — Mephist
This starts looking suspiciously like a correspondence is in play between the algebra of sets on the product topology of ×KΩ×KΩ, and the production rules on the propositional symbols. The possible "propositional assignments" that satisfy an interpretation maybe float above an interpretation as an algebra (algebraic structure, anyway).
Maybe it doesn't help though, it's very scattered. — fdrake
Well, not only is useful, but if you find a relation between apparently completely different areas of mathematics, maybe those concepts have in some way a deeper meaning. — Mephist
I showed that convergence of complex limit periodic continued fractions useful as functional expansions could be accelerated by employing a feature of dynamical systems: attracting fixed points (Proceedings of the AMS). And could be analytically continued by using repelling fixed points (Mathematica Scandinavica and Proc. Royal Norwegian Soc. of Sci. & Letters). There are deeper meanings here by locating these concepts in theory of infinite compositions of complex functions. — jgill
analytical continuation of a complex function has something to do with chaotic systems? Did I understand correctly? — Mephist
The underlying set is the set of all propositions. The fibers are sets of elements of our model. — Mephist
Arghhh!!! :grimace: This is an example of intuitionistic dependently typed theory, corresponding to a non-trivial topological space. The previous one was an example of first order logic with set theory, since you didn't want type theory. And THERE IS NO NON-TRIVIAL TOPOLOGICAL SPACE CORRESPONDING TO FIRST ORDER LOGIC WITH SET THEORY. Than in that example, the topology was irrelevant! fdrake, did you understand?
If yes, can you please try to explain this in a better way? I don't even have much time for this, sorry. I have even to go to the hospital for a couple of days next week. — Mephist
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.