The tag has no wiki summary.

learn more… | top users | synonyms

6
votes
0answers
104 views

What is the most transparent, rigorous definition of the Univalence Axiom?

I've been studying homotopy type theory and trying to grasp the Univalence Axiom. I have yet to find a concise, accessible, rigorous definition of Univalence. I have several excellent survey papers ...
18
votes
3answers
2k views

Who needs Replacement anyway?

The set theory ETCS famously comes without the Replacement axiom schema (or an equivalent) that is part of ZFC. One (to me, not apparently useful) set that one cannot build in ETCS is $\coprod_{n\in ...
29
votes
0answers
727 views

Bidi: A new cardinal characteristic of the continuum?

This question assumes familiarity with combinatorial cardinal characteristics of the continuum. Identify an infinite set $a\subseteq\mathbb{N}$ with its increasing enumeration. Thus, for each natural ...
4
votes
0answers
278 views

Order theory as a foundation of mathematics?

I know the followings kinds of formalization of mathematics: based on set theory (e.g. ZFC) based on type theory (e.g. the formalism of Coq proof assistant, as an advanced example) based on category ...
3
votes
0answers
91 views

Hilb as a Colimit in the Category of Scott Complete Categories (foundations)

Here is a paper I found by Adamek that generalizes Domain theory into categories of categories called Scott Complete Categories. The category of Scott Complete categories is denoted SCC. For years, ...
8
votes
0answers
206 views

Is there a notion analogous to separability but requiring definable rather than countable sets?

Among models of $\lambda$-calculus, some like the Bohm tree model have the property that every element is a directed sup of definable elements, whereas others like the $D_\infty$ and $P(\omega)$ ...
4
votes
2answers
295 views

Can one make a category concrete by “enlarging the universe”?

This is more or less a followup of this question. There, it was established that (it is well known that) the homotopy category of topological spaces is not concrete, in other words, there is no ...
-5
votes
1answer
191 views

An axiomatic system with a set of constants that form a complete ordered field [closed]

I am developing a ZFC axiomatic system where together with the empty set, there is a singular (and huge) set of constants that are themselves sets and form a complete ordered field (cof) these ...
6
votes
1answer
641 views

Does Nelson try to prove PA inconsistent directly?

Edward Nelson is known for his serious attempts to show that Peano axioms, and sometimes even weaker theories, are inconsistent. I wasn't able to find Nelson's papers anywhere, so I wanted to ask a ...
12
votes
3answers
1k views

Proof correctness problem

I was watching this talk by Vladimir Voevodsky which was given at the Institute of Advanced Study in 2006. In his talk the first slide he shows has the following written on it: ...
5
votes
2answers
862 views

Why can't mathematics be formalised in terms of classes rather than sets? [closed]

I've always been curious about the seeming compulsion to found mathematics upon sets, be it ZF(C) or some other system. Of course, there are other approaches these days like category theory and type ...
4
votes
1answer
128 views

Class theory with support for self-application of class functions?

To every natural number $n$, we can assign its Church numeral $\underline{n}.$ A formal definition would be: $\underline{0}(f)=\mathrm{id}_{\mathrm{dom}(f)}$ $\underline{n+1}(f) = ...
1
vote
1answer
221 views

Would a non-constructible set become constructible if we had oracles of arbitrarily high cardinality for the halting problems of ordinal computers?

I still have trouble to grasp the concept of a non-constructible set, my intuition is that we could "avoid" the non-constructibility of many of them if we assume we have "ordinal computers" extended ...
8
votes
3answers
731 views

What set theoretical questions could never be answered by Turing machines of arbitrary cardinality?

Let us assume that there are Turing machines of arbitrary cardinality, by that I mean they can have input tapes of any arbitrarily high cardinality and compute for a number of steps also of ...
8
votes
3answers
733 views

Consistency of Analysis (second order arithmetic)

Is there a proof of the consistency of Analysis (second order arithmetic), which is similar to Gentzen's proof of the consistency of arithmetic? Update: Which (different) methods can be used to ...
-1
votes
1answer
264 views

What is an example of a non-axiomatic mathematical system? [closed]

In this wikipedia article on the foundations of mathematics, it says: In practice, most mathematicians ... do not work from axiomatic systems Is this correct? If so, what is an example of this?
4
votes
1answer
443 views

Why is adopting Russell's Axiom of Reducibility as strong as eliminating the Ramified Hierarchy?

In order to respond to concerns of impredicativity, Bertrand Russell developed a system of ramified second-order logic, which is like regular second-order logic except the comprehension schema is ...
1
vote
0answers
470 views

What is the role of the (formalized) omega rule in Ramified Analysis?

In the 1960's, Feferman and Schutte did groundbreaking proof-theoretic work to find out the strength of predicative systems of second-order arithmetic. They used the ramified theory of types, a ...
3
votes
2answers
270 views

What is the proof-theoretic ordinal of Hyperarithmetical Comprehension?

As I discuss in my answer here, it seems to me that Solomon Feferman shows, on pages 10-11 of his seminal 1964 paper "Systems of Predicative Analysis", that if you consider predicative second-order ...
1
vote
0answers
168 views

Has the Ramified Theory of Types been applied to Predicative Set Theories?

Questions of predicativity are well-studied in the context of arithmetic. We have a base theory, first-order Peano arithmetic. Some people, like Edward Nelson (in chapter 1 of his book) and Charles ...
4
votes
2answers
399 views

Did Gödel prove that the Ramified Theory of Types collapses at $\omega_1$?

Second-Order Arithmetic is considered impredicative, because the comprehension scheme allows formulas with bound second-order variables that range over all sets of natural numbers, including the set ...
4
votes
1answer
285 views

Can the Burgess-Hazen analysis of Predicative Arithmetic be extended to Transfinite Types?

Around page 300 of his book "Mathematical Thought and its Objects", Charles Parsons discusses the work of Edward Nelson, who believes that mathematical induction is impredicative, because it can be ...
6
votes
1answer
589 views

Original proof of Gödel's completeness theorem compared to Henkin's proof

May I have some clarification about original proof of Gödel's Completeness Theorem compared to "standard" Henkin's proof based on Model Existence Lemma ? My understanding of Gödel's original proof is ...
10
votes
2answers
446 views

Ways to define “definability”

The notion of a definable set is not expressible in the language of set theory: there is no formula $\delta(x)$ that is equivalent with there being a formula $\phi(y)$ such that $x = \lbrace y : ...
2
votes
0answers
118 views

Hosting Category Theory in a “universe” that is non-LFP

WHen I did my MSc, I was trained by a very talented topologist. I had a passion for the subject before and since. Now I am interested in category theory, but I seem to be very interested in the ...
4
votes
2answers
346 views

Functor category's objects fail to be a class?

Given two categories, we can form the functor category whose objects are functors. Functors by definition consist of two mappings from in general classes to classes, which makes it fail to be a set. ...
4
votes
2answers
272 views

On wild behavior of $\omega_{1}$ in the absence of some essential axioms of $ZFC$

The regularity of $\omega_{1}$ is one of the most well known facts of set theory. But it seems that in order to prove this simple fact we need the "full power" of mathematics! For example by an ...
1
vote
0answers
166 views

Is there a non-trivial consistency preserving transformation?

In ‎set ‎theory ‎"equiconsistency" (and not "consistency") ‎of ‎the ‎theories ‎is the‎ ‎main ‎part ‎of ‎researches. ‎So ‎we ‎usually ‎try ‎to ‎construct a‎ ‎new model ‎using a‎ ‎given ‎one. ‎In ‎the ...
11
votes
1answer
537 views

Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?

Let the proof theoretic ordinal $\alpha$ of a theory $T$ be the least recursive ordinal such that $T$ does not prove that $\alpha$ is well-founded. This ordinal is intended to quantify in some sense ...
12
votes
3answers
805 views

Where is the end of universe?

In some sense the empty set ($\emptyset$) and the global set of all sets ($G$) are the ends of the universe of mathematical objects. The world which $ZFC$ describes has an end from the bottom and is ...
2
votes
0answers
391 views

Is there a notion of “predicative given the real numbers”?

A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...
6
votes
3answers
367 views

Does the Feferman-Schutte analysis give a precise characterization of Predicative Second-Order Arithmetic?

A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...
24
votes
4answers
1k views

Illustrating Edward Nelson's Worldview with Nonstandard Models of Arithmetic

Mathematician Edward Nelson is known for his extreme views on the foundations of mathematics, variously described as "ultrafintism" or "strict finitism" (Nelson's preferred term), which came into the ...
8
votes
0answers
516 views

Has anyone pursued Frege's idea of numbers as second-order concepts?

Gottlob Frege was a pivotal figure in the history of mathematical logic. He gave an analysis of numbers that proceeded along roughly the following lines, in his books "The Foundations of Arithmetic" ...
14
votes
4answers
626 views

Does the existence of the von Neumann hierarchy in models of Zermelo set theory with foundation imply that every set has ordinal rank?

Let $T$ be the theory consisting of Zermelo's original set theoretic axioms (extensionality, empty set, pairing, union, powerset, infinity, separation, choice) together with foundation. Put more ...
-3
votes
3answers
512 views

Can different extensions of ZF have contradictory consequences for first-order arithmetic?

My question is basically, does there exist a statement X independent of ZF such that ZF + X implies a statement P of first-order arithmetic, but ZF + not X implies not P? Now X cannot be the axiom ...
10
votes
2answers
540 views

Are simplicial sets the intended model of HoTT?

While thinking about Jason Rute's question, I wondered if there was an intended model for HoTT. The main candidate for the intended model are simplicial sets, where Vladimir Voevodsky first observed ...
14
votes
1answer
582 views

On Joyal's completeness theorem for first order logic

In 1978, in a series of unpublished conferences in Montréal, A. Joyal announced a remarkable theorem that unified several completeness theorems for fragments of first order logic, as well as first ...
14
votes
3answers
1k views

Who introduced the terms “equivalence relation” and “equivalence class”?

Consider that the question does not concern the origin of the ideas of equivalence relation and equivalence class. It exactly concerns the origin of the terms "equivalence relation" and "equivalence ...
9
votes
2answers
826 views

Equivalent form of the Univalence Axiom

I'm reading the new HoTT book and I'm wondering about a potential equivalent form of the Univalence Axiom: $(A \simeq B) \simeq (A = B)$. For simplicity, I'm tacitly working in a fixed universe. It ...
11
votes
3answers
1k views

Is there a categorical proof of Gödel's incompleteness theorem?

A significant result in set theory was shown by Cohen when he showed that the continuum hypothesis was independent of ZFC using a new technique called forcing. In Topos theory, this result has a new ...
5
votes
1answer
493 views

What can be done with computability logic that previous logic systems can't?

I've been reading a lot about computability logic lately and I'm superficially aware that it unifies classical, intuitionistic and linear logics. What I'm seeking to know is: Can computability logic ...
7
votes
1answer
454 views

Normality of Chaitin's constant

Can anyone provide an overview of the proof that Chaitin's constant is normal, or better yet, the guiding intuition? Even if we replace the existential quantifiers in the assertion of non-normality ...
5
votes
1answer
704 views

Why do mathematicians prefer one definition over the other when they both define the same concept?

Here is a basic, though very important, example: Hilbert takes as primary the notion of “congruence” (or “equal”) between segments. His first axiom of congruence “requires the possibility of ...
17
votes
2answers
882 views

Age of Stochasticity?

One user on MSE made an interesting question, which was unanswered so I suggested him to post it here but he refused for personal reasons and said I could ask it here. The question is this: Today ...
2
votes
1answer
519 views

Surreal numbers and large cardinals

This is a question in two parts about the interaction of surreal numbers and large cardinals, in both cases just a request for references on the subject. Part 1 is about foundations. Much of the ...
18
votes
6answers
1k views

Where in ordinary math do we need unbounded separation and replacement?

[I have updated the question after initial comments in the hope of clarifying it.] I do quite a bit of reasoning, typically about topology and metric spaces, in "non-standard" foundations, such as ...
2
votes
3answers
488 views

Are integers real? [closed]

Do you think that $\mathbb Z \subset \mathbb R$? On one hand this inclusion is quite handy. We like to write things like: $$ \sqrt{n} \quad \text{for $n\in \mathbb Z$} $$ which requires the number $n$ ...
16
votes
1answer
555 views

Monte Carlo integration

As probably many other people here, I learned integration, as an undergrad, from Rudin's books. I recently realized, however, that I don't quite use Lebesgue integration in my work, or at least I use ...
1
vote
1answer
384 views

Cardinal Arithmetic, foundations and constructive math

This is not my area but a question occurred to me that I can not find the answer to. There is a very strong axiom of constructibility which ironically gives us highly non-constructive math (GCH is one ...