The foundations tag has no usage guidance.

**4**

votes

**0**answers

87 views

### What useful admissible rules does ZFC have beyond the deduction theorem?

I'm interested in formal proof verification, and one of the surprisingly difficult parts of this is dealing with proofs by contradiction. The issue is that the final step of such proofs is typically ...

**8**

votes

**1**answer

251 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 ...

**24**

votes

**5**answers

3k views

### Nonstandard analysis in probability theory

I am quite new at nonstandard analysis, and recently I became aware of its use in probability theory mainly through the following two books:
Nelson (1987). Radically Elementary Probability Theory
...

**0**

votes

**0**answers

310 views

### Set as a (strict) infinite-category?

First, let me say that I have no idea if such a post has its place here. However, I believe that the ideas I'm going to present are important. The goal of this thread is three fold:
1) trying to ...

**19**

votes

**3**answers

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 ...

**24**

votes

**6**answers

4k views

### How true are theorems proved by Coq?

Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one makes with respect to ...

**27**

votes

**0**answers

809 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 ...

**5**

votes

**0**answers

327 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

**0**answers

97 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, ...

**6**

votes

**3**answers

394 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 ...

**12**

votes

**3**answers

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:
...

**8**

votes

**0**answers

214 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

**2**answers

301 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 ...

**6**

votes

**1**answer

658 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 ...

**-5**

votes

**1**answer

198 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 ...

**9**

votes

**10**answers

4k views

### Is PA consistent? do we know it?

1) (By Goedel's) One can not prove, in PA, a formula that can be interpreted to express the consistency of PA. (Hopefully I said it right. Specialists correct me, please).
2) There are proofs ...

**4**

votes

**1**answer

468 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 ...

**7**

votes

**8**answers

2k views

### ULTRAINFINITISM, or a step beyond the transfinite

Cantor has, in the immortal words of D. Hilbert, given all of us a paradise (or perhaps, I would rather say, a great vacation spot), the TRANSFINITE.
$\aleph_0, \aleph_1,\aleph_2\dots$
the lists ...

**11**

votes

**3**answers

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 ...

**8**

votes

**3**answers

771 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 ...

**5**

votes

**2**answers

888 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

**1**answer

136 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) = ...

**15**

votes

**1**answer

1k views

### Martin's “Philosophical Issues about the Hierarchy of Sets”

Some months ago (October 2010), in the context of the Workshop on Set Theory and the Philosophy of Mathematics, Professor Donald A. Martin gave a talk entitled "Philosophical issues about the ...

**1**

vote

**1**answer

234 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

**3**answers

766 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

**1**answer

332 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?

**1**

vote

**0**answers

483 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 ...

**2**

votes

**0**answers

402 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 ...

**4**

votes

**1**answer

302 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 ...

**5**

votes

**2**answers

409 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 ...

**14**

votes

**3**answers

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 ...

**3**

votes

**2**answers

290 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

**0**answers

173 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 ...

**6**

votes

**1**answer

617 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

**2**answers

450 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 : ...

**25**

votes

**4**answers

2k 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 ...

**2**

votes

**0**answers

119 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

**2**answers

363 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

**2**answers

277 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

**0**answers

173 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

**1**answer

605 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

**3**answers

819 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 ...

**5**

votes

**1**answer

522 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 ...

**8**

votes

**0**answers

533 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

**4**answers

649 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 ...

**18**

votes

**6**answers

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 ...

**-3**

votes

**3**answers

524 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

**2**answers

570 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

**1**answer

610 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 ...

**10**

votes

**2**answers

856 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 ...