New page small cardinality selection axiom.
]]>Hello,
I’m starting to learn about type theory (in HoTT or articles on the net) after having been “passively” using it for years in programming languages. My question may certainly be a bit simple but I couldn’t find a resource on the net, so better ask it!
Let’s say I take as granted usual set-theory (ZFC let’say), with its standard notion of set, function and real numbers. Then I would like to “inject” those objects in type theory formalism. My goal is to exploit the type theory expression system for constructive proofs without having “constructively-obtained objects”. In other words, I don’t really care about constructive sets, reals, measures, or anything. I’m more interested in expression theorems and structures in type theory, and using this language for object manipulation.
So I started an easy example or semi-ring of parts (from measure theory). So far, it goes at follows: (1) I use “set” to talk abut ZFC sets, “function” for function in the usual ZFC sense, and “program” for arrows from type theory (2) for any set E, I abuse notation by writing x:E when an object (set) x belongs to E, in the usual sense (judgment)
Fix two sets . For all , I define the set and So if I don’t mistake, this consists of programs from to that where constructed from programs with an additional specification that either it is proved that , or it is proved that the valued of the program are disjoint sets.
Next I define the type If I don’t mistake, this type consists of (dependent) programs that provide a proof that c (in E) may be written as a disjoint finite union of elements in A.
Next I define the type If I don’t mistake, this consists of programs that prove that for all x,y: A, there is a writing of the difference .
Now I assume the judgment is true (think of A as being a semi-ring in E, but that won’t be important for the remaining part), and I’m interested in constructing a program for , that is: as soon as there exists an element in A, the empty set belongs to A. First, is that indeed equivalent to ? For this, I’m going to use the element assumed to exist. I define the program as , that is: I evaluate the program at , yielding some . Now I project this to extract the proof as above.
To me, this formally defines a program . In my eyes, this is enough to conclude, because the type is the same as . But here I’m not sure how I should justify the argument. I’m ok to “inject” standard set-theoretic logic, so to me, it is sufficient to have a lemma proving this somewhere, which is kind of trivial. In the same spirit, is it ok to “assume” that and are equivalent programs?
Could someone, somehow validate my approach here?
I emphasize on the idea that I would like to exploit the formalism of type theory without committing to constructive analysis. I like my usual non-constructive analysis objects and I wouldn’t be happy in facing hard and touchy constructivist problems.
Regards,
Justin
]]>I am searching for all the possible features of reasoning (all of them can be expressed in logic), so far I have found the following features:
My question is this - are there any other features beside those 5, features that can improve the expresiveness of the logic.
I am trying to combine all those features in one logic and initially I would be happy to know that the set of those 5 features is exhaustive and so - when I come up with the language that can express all those 5 features then there is no more general language than that. Of course, I am thinking about templates, i.e., I will leave open the final set of modal operators and connectives (and the interactions among them), because different concrete logics can arise in each concrete choice of those. My aim is to create reasoner (forward chaining engine) that could be used for such templates and that works modulo concrete set of modal operators and connectives.
Of course, I will have to find common proofs for each of the logic but I plan to automate this task by formalizing each concrete logic in Coq or Isabelle/HOL as it has already be done by linear logics. Then (semi)automatic proof search can lead to the proofs of rejections of soundness and completeness theorems and other theorems for each logic. I am even thinking about combination of genetic search (for the operators/connectives/their sequence rules) with automatic theorem proving (for the theorems about concrete logic) (possibly - with deep learning inspired) for (semi)automatic discovery and development of logics. But to guide all this process, to predict the most general grammar for the possible logics, I should be sure that there is nothing beyond those 5 features. (Neural methods have stuck in deadlock, as can be seen from delayed introduction of autonomous vehicles, that is why strong boost of symbolic methods is necessary and automation of the discovery and research of the logics is the key process for the adoption of symbolic methods in industrial setting).
After that I will have to find semantics, but I am sure that set semantics (with probability distributions and set operations and relations (for modalities and substructural connectives)) is sufficient for all those 5 features, because everything in math can be expressed by (ZFC) set theory and that is why any other possible (sophisticated) semantics can be expressed via sets anyway.
Of course, I am aware of the efforts by Logica Universalis community, but the Florian Rabe, but the community of categorical logics and institution theory. But I am having hard time to find the logic that already encompass those 5 features and also I can not find definite answer that those 5 features are exhaustive or am I missing something?
I would like to add that it is very important that everyone at this time come up with some advice or suggestion, idea. Now the economic crisis is starting again and it is very important to finalize the achievement of artificial intelligence and streamline them into industry exactly now. Only the increase of the supply side productivity (by the artificial intelligence) can save the us from the coming crisis.
]]>Consider sets and functions. A relation between two sets can then be expressed as a subset of a Cartesian product, in other words, we can define it and describe it using functions.
Viceversa, can we describe functions using relations as the “fundamental” arrows? That is, can we define and describe functions without using other functions, only relations?
]]>Urs is doing a demo on the nlab. He is elaborating the axiom of determinacy. Set theorist, please elaborate.
]]>Hi,
If you haven’t looked at these yet, please have a look. They are calling it the biggest discovery in quantum mechanics for decades.
The reason I am posting this is that I would like to begin a discussion focusing on classical versus constructive (lack of excluded middle) mathematics as a means of dissecting the issue of realism in quantum mechanics. The articles listed are probing a very deep problem of realism in quantum mechanics. Does the wavefunction reflect our knowledge of a system or does it reflect reality itself. They use the language of ontic versus epistemic states and I will explain those.
Ontic states are variables which we think of as concerning an underlying reality and epistemic states are like probability distributions which reflect the information we have about a system. Were I to flip a coin and cover it and ask you to tell me about this coin, you would say it is 50 % heads and 50% tails. In my case, I peaked at the coin and the state that I would use to describe the coin is 100% heads, so the probability distribution just reflects the information we have been given and does not reflect reality. I could also have told you that the coin has landed on its side and is in the “Quails” state. You would then update your probability distribution to include a third state and this process begins again when I reflip the coin and ask you again what you think the state is.
The reason I am posting this here, is that this community seems familiar with the following research in the foundations of mathematics. In it I discovered the following interesting point:
Bifurcation of notions
On the other hand, differences in axiomatization or definition that make no difference classically can result in actual differences in behavior constructively. Therefore, classically equivalent notions often “bifurcate” (or “trifurcate” or worse) into multiple inequivalent constructive ones. This tends to happen whenever a concept involves negation and, to a lesser degree, disjunction and existential quantification.
I would like to offer for discussion the notion that the ontic states (bases and classical states, states of reality) and the epistemic states (quantum states, wavefunctions, states of knowledge) have been consistently treated to different axiomatizations in physics, perhaps even in the same paper/textbook without the author realizing it. Furthermore, I am offering that the multiple overlaping epistemic states which one can have for the same ontic state in quantum mechanics derives from the bifurcation between the classical mathematics one uses on the ontic states and the constructive mathematics on the epistemic states. It comes from the use of the existential quantification which one passes up from the ontic realm up to the epistemic realm when one talks about the elements of the Hilbert space or the space of quantum states. Further, we should find in the articles listed above that they represent an attempt to eliminate the constructive mathematics at the epistemic level. In particular, we see in Hardy’s paper the central axiom is of “Ontic Indifference” and here it is stated:
“Ontic indifference. Any quantum transformation on a system which leaves unchanged any given pure state, , can be performed in such a way that it does not affect the underlying ontic states, in the ontic support of that pure state.”
What we should note is the presence of the existential quantifier being passed up from the ontic states to the epistemic states. It is here where we can begin with dissecting this recent work in terms of foundations. Below, we the definition of “ontic support”:
“By the ontic support of a given state, , we mean the set, , of ontic states, which might be prepared when the given pure state is prepared (i.e. those ontic states that have a non-zero probability of being prepared when the given pure state is prepared)”
]]>Is the set of natural transformations between two simplicial (abelian) groups a simplicial group or a chain complex?
]]>Is there a well defined internal hom for cosimplicial objects? (sets, algebras, rings)
]]>Simple Question:
1.) How many morphisms are there in ?
( Or equivalent: What is $|\Delta [m]_n |$ ? )
2.) Is there a research field in combinatorics that is concerned with monotonic integer maps from to (Just in case I have another ’combinatorical’ question concerning )
]]>Suppose we have the sequence of sets , , , … Is there a Kan simplicial structure on this sequence of sets, that is not -coskeletal for some ?
To be more precise, is there a simplicial set (functor) with that is not -coskeletal for some ?
And very closely related: is there a simplicial set (functor) with (with ), that is not -coskeletal for some ?
]]>Suppose we have a simplicial set X and a m-truncated Kan simplicial set Y. Then how is it possible to construct as a subset ?
Since Severa used this in his work on the n-jet functor (for X the nerve of the pair groupoid over an arbitrary set), it should be possible. Nevertheless I can’t find an explicit construction including a proof that what he constructed is indeed .
By an explicit construction I mean something like: Let be given, then the appropriate simplicial morphism is given by as follows : ??? where the commutation with the face and degeneracy maps is seen as follows ??? … On the other side we that any simplicial morphism is given that way, because ???
….
So if someone could give me a proof (I think it will be an induction on something like or ) it would be great.
Likely this doesn’t work for arbitrary simplicial sets X, so another topic is to find the appropriate conditions on X .
Moreover this should be put into the nLab, too…
If nobody knows a proof it would be nice, if we could work it out together. At the end I will take the time to put in the nLab. Unfortunately my skills on simplicial sets are not good enough, to do it by myself.
]]>I have created a stub for constructible universe. I did not go through the version of the definition via definability. Now constructible sets are sets in the constructible universe. The notion of course, intentionally reminds the constructible sets in topology and algebaric geometry as exposed e.g. in the books on stratified spaces, on perverse sheaves (MacPherson e.g.) and in Lurie’s Higher Topos Theory. Now I wanted to create constructible set but I was hoping that there is a common definition for all these cases or at least logically defendable unique point of view, rather than partial similarity of definitions. I mean one always have some business of unions, complements etc. starting with some primitive family, say with open sets, or algebraic sets, or open sets relative strata etc. and inductively constructs more. Now, all the operations mentioned seem to have sense in some class of lattices. Maybe in Heyting lattices or at least in Boolean lattices. On the other hand, google spits out several references on constructible lattices *one of the authors is certain Janowitz), but the definition there is disappointing. I mean I would like that one has some sort of constructible completion of certain kind of a lattice and talk about the constructible elements as the elements of constructible completion. I am sure that the nLab community could nail the wanted common generalization down or to give a reference if the literature has it already.
]]>I plan to write few foundations/set theory stubs including Skolem paradox. It will wait for a bit as the Lab seems to be down at the moment.
The entry forcing has phrase downward Löwenheim-Skolem theorem. What does it mean downward in this phrase ? Is it a modifier at all ?
]]>Hello,
This is my first post here at nForum, and I’m a bit unsure whether my question is appropriate here, so please let me know if it should be moved or deleted. However, I’m just beginning to study Category Theory on my own, using Adamek, Herrlich and Strecker’s “Abstract and Concrete Categories”. I’m having a bit of a stumbling block with one of the exercises and would like to discuss it with someone.
The exercise just asks to show that where is the category of pointed sets and is equivalence of categories. Could somebody provide me with a little direction? I’d rather work from a hint than receive an answer, but I know that’s sometimes difficult for these elementary problems.
]]>