Questions tagged [foundations]
Mathematical logic, Set theory, Peano arithmetic, Model theory, Proof theory, Recursion theory, Computability theory, Univalent foundations, Reverse mathematics, Frege foundation of arithmetic, Goedel's incompleteness and Mathematics, Structural set theory, Category theory, Type theory.
330 questions
11
votes
2
answers
1k
views
Meta-undecidability
Could there be an undecidable statement $S$ in ${\sf ZFC}$ of which one will never be able to prove its undecidability for principal reasons (ie we will never know that $S$ is undecidable)?
If this ...
- 48.8k
25
votes
5
answers
4k
views
What is some current research going on in foundations about?
What is some current research going on in the foundations of mathematics about?
Are the foundations of mathematics still a research area, or is everything solved? When I think about foundations I'm ...
21
votes
2
answers
3k
views
Do set theorists work in T?
In the thread Set theories without "junk" theorems?, Blass describes the theory T in which mathematicians generally reason as follows:
Mathematicians generally reason in a theory T which (...
- 221
3
votes
1
answer
625
views
Are the paradoxes of material or strict implication used anywhere to prove theorems in mathematics
In the Stanford Encyclopedia of Philosophy entry "Relevance Logic", the following inference is listed as classically valid:
The moon is made of green cheese. Therefore, it is raining in Ecuador ...
- 6,132
1
vote
1
answer
484
views
"Co-ordinate-free" mathematics for general structures? [closed]
Edit (15 November 2017): I've just stumbled across this question, which I think is asking essentially the same thing I tried to ask below, but probably worded it more clearly - and got far more ...
- 3,612
10
votes
3
answers
1k
views
Is a paraconsistent and provably non-trivial foundation for math possible?
Would it be possible to use a paraconsistent logic and axioms similar to ZFC to create a formal sytem, that can be proven to be non-trivial (so that there are some statements which can´t be proven in ...
- 139
0
votes
1
answer
678
views
Why do we try to encode every mathematical object as a set? [closed]
Probably everyone of us has seen set-theoretic encodings of mathematical objects which we wouldn't naturally consider to be sets. May it be the "definition" of a function from $A$ to $B$ as a relation ...
- 27
1
vote
0
answers
238
views
A universal framework for Game Theory?
Ever since the seminal work of Von Neumann and Morgestern Game Theory has grown into a formidable sector of pure and applied mathematics.
There are all sorts of games: perfect information, ...
- 7,853
4
votes
1
answer
688
views
HoTT without Funext, Univalence
Are there any models of Martin-Löf's intensional type theory in which univalence or function extensionality fails?
In the HoTT book, axioms like $\mathsf{LEM}_{\infty}$ (in Section 3.4) are proved to ...
- 369
50
votes
4
answers
6k
views
Do set-theorists use informal set theory as their meta-theory when talking about models of ZFC?
Here, Noah Schweber writes the following:
Most mathematics is not done in ZFC. Most mathematics, in fact, isn't done axiomatically at all: rather, we simply use propositions which seem "intuitively ...
- 509
4
votes
3
answers
915
views
Compactness of existential second order logic and definability of certain quantifiers
It is known (as a slogan) that the "existential fragment of second-order logic (ESO) is compact".
My first question is:
(1) Is ESO compact for:
(a) uncountable languages
(b) languages with ...
- 135
4
votes
1
answer
401
views
What do we call this quantifier ("binder")?
There's a quantifier ("binder", whatever), call it $\alpha$, defined as follows: $\alpha x.\tau$ is the (usually infinite) expression obtained by applying the substitution $\{x \mapsto \tau\}$ to the ...
- 3,793
2
votes
0
answers
264
views
About the limitation by size
This could be a big post, so I'll try to summarize my thoughts and divide them into several questions.
When working in category theory, I used to choose the following definition. A category $C$ is ...
- 1,017
10
votes
4
answers
1k
views
Direct axiomatization of ordinal and cardinal numbers
Again, this question is related (**) to a previous one:
in standard books on basic set theory, after stating the axioms of ZFC, ordinal numbers are introduced early on. Afterwards cardinals appear: ...
- 7,853
9
votes
1
answer
856
views
Taller models of ZFC
This question is somewhat related to a previous one, where I asked for new forms of infinite beyond the cardinal hierarchy.
Using forcing techniques, at least the ones I know of, one starts from a ...
- 7,853
1
vote
1
answer
397
views
What restriction(s) of Goedel's primitive recursive functionals is (are) necessary and sufficient to prove the consistency of $PRA$
It is well known that one can use Goedel's primitive recursive functionals of finite type to prove the consistency of $PA$ (Peano Arithmetic). As such, one can certainly use them to prove the ...
- 6,132
2
votes
1
answer
335
views
A question regarding the consistency of Nelson's Predicative Arithmetic
Following Dan Willard (from his paper "Self-Verifying Axiom Systems, the Incompleteness Theorem, and Related Reflection Systems", found on his homepage, pdf here):
"Define an axiom ...
- 6,132
8
votes
1
answer
1k
views
Ill-founded models of set theory with well-founded ordinals
Let $(\mathcal{M},E)$ be an internally non-well-founded model of set theory i.e of $ZFC^{\neg f}=ZFC\setminus \mathrm{foundation}+\neg \mathrm{foundation}$, then $\mathcal{M}$ includes an infinite ...
- 2,381
1
vote
1
answer
777
views
Does mathematical induction presuppose the existence of a completed infinity?
Consider the following statement by Edward Nelson--this from the "Outline" of his 'proof' of the inconsistency of $PA$ (which Terry Tao found to contain an error):
"The induction axiom ...
- 6,132
2
votes
1
answer
186
views
Is there a simpler axiomatization for the quantifiers? [closed]
There is those one Q5 to Q7 in https://en.wikipedia.org/wiki/Hilbert_system#Formal_deductions
But I know the axioms of Boolean algebra were simplified to this https://en.wikipedia.org/wiki/...
- 139
7
votes
1
answer
429
views
How many closed measure zero sets are needed to cover the real line, really?
This is a refinement of an earlier question.
This question assumes familiarity with combinatorial cardinal characteristics of the continuum.
For the reader's convenience, I reproduce below the ...
- 3,104
9
votes
1
answer
603
views
How many closed measure zero sets are needed to cover the real line?
This question assumes familiarity with combinatorial cardinal characteristics of the continuum.
Let $\mathcal{E}$ be the $\sigma$-ideal generated by closed measure zero subsets of the real line. It ...
- 3,104
2
votes
0
answers
179
views
Some questions regarding an alteration of Grzegorczyk's theory of concatenation, $\operatorname{TC}$
Consider Grzegorczyk's concatenation theory $\operatorname{TC}$, a "weak theory of words over the two letter alphabet $\Sigma=\{a,b\}$" (this from Grzegorczyk and Zdanowski's paper Undecidability and ...
- 6,132
1
vote
2
answers
547
views
Was "arithmetical translation" (coding in the Goedel sense) ever a part of Hilbert's Program?
Was "arithmetical translation" (that is, coding in the Goedel sense) ever a part of Hilbert's Program? I ask this question for several reasons:
i) it gives the numerals |, ||, |||,.... an ersatz '...
- 6,132
16
votes
2
answers
816
views
Can a stochastic Turing machine output a consistent extension of PA with positive probability?
Suppose that we interpret the output tape of a Turing machine as an assignment of true or false to all sentences of PA, taking the $n$th output bit as the truth value of the sentence with Goedel ...
- 163
4
votes
1
answer
301
views
internalization of the concept of large and small category
I have been poking around the internet and nlab looking at the concept of large and small categories. My original focus was locally presentable categories of categories and I was thinking of finding ...
- 1,313
19
votes
0
answers
703
views
The cofinality of $(\mathbb{N}^\kappa,\le)$ for uncountable $\kappa$?
For a partially ordered set $P$, a set $A\subseteq P$ is cofinal if for each element of $P$ there is a larger element in $A$. The cofinality of $P$, ${\rm cof}(P)$, is the minimal cardinality of a ...
- 3,104
5
votes
0
answers
243
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 "...
- 443
0
votes
0
answers
410
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 ...
- 438
24
votes
1
answer
5k
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 ...
- 469
36
votes
6
answers
6k
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 \...
- 35.4k
10
votes
1
answer
2k
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 ...
- 755
3
votes
0
answers
142
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, ...
- 1,313
8
votes
0
answers
248
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)$ ...
- 211
5
votes
2
answers
566
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 ...
- 23.3k
-3
votes
1
answer
262
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 ...
- 201
9
votes
1
answer
1k
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 ...
- 28.2k
16
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:
...
6
votes
2
answers
1k
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 ...
- 820
20
votes
5
answers
2k
views
Does formalizing math require search and creativity, or is it near-mechanical?
I remember reading somewhere that it takes about a week to convert a page of math into something a proof-assistant like Isabelle or HOL Light would accept.
Is this type of conversion something that ...
5
votes
1
answer
191
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) = \underline{n}...
- 3,793
2
votes
1
answer
609
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 ...
- 297
9
votes
3
answers
2k
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 ...
- 297
13
votes
3
answers
2k
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 ...
- 32.1k
5
votes
1
answer
868
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 ...
- 4,587
3
votes
0
answers
853
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 ...
- 4,587
3
votes
2
answers
814
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 ...
- 4,587
12
votes
3
answers
648
views
Has the Ramified Theory of Types been applied to NBG?
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,587
5
votes
3
answers
897
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,587
5
votes
1
answer
719
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 ...
- 4,587