Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [foundations]

This tag is for questions about the foundations of mathematics, and the formalization of mathematical concepts in foundational theories (e.g. set theory, category theory, and type theory).

1
vote
1answer
80 views

Why do mathematicians generally write definitions in “declarative” rather than “imperative style?

In programming, we can make the distinction between declarative / functional and procedural / imperative programming. The distinction is not exact, but nevertheless meaningful. One major difference ...
8
votes
0answers
48 views

Natural examples of “set-theorems” provable in MK but not ZFC and NBG

NBG set theory proves nothing additional about sets relative to ZFC. MK set theory, on the other hand, is stronger, meaning it should prove statements about sets that NBG and ZFC don't. Are there ...
0
votes
0answers
34 views

Finite axiomatization of second-order NBG

First-order NBG set theory is finitely axiomatizable. The proof of this basically shows that the axiom schemas, in the presence of the other axioms, can be reduced to a finite set of cases, and are ...
0
votes
1answer
73 views

Definitions in metamathematics

In model theory, the satisfiability relation $ \vDash$ between a model $M= (D,f)$ and a set of formulas tells us when a formula $\varphi$ is true or not in the model ("interpretation") $M$. This ...
0
votes
1answer
62 views

Why is the Axiom of Well-ordered Choice not strong enough to prove Zorn's Lemma?

This is based on this question: How strong is the axiom of well-ordered choice? The "axiom of well-ordered choice" says that any transfinitely-indexed family of sets has a choice function. The ...
11
votes
1answer
171 views

How strong is the axiom of well-ordered choice?

I sometimes see references to the "Axiom of Well-Ordered Choice," but I'm not sure how strong it is. It states that every well-ordered family of sets has a choice function. By "well-ordered family," ...
1
vote
1answer
87 views

What is the most expressive logic?

What is the most expressive logic studied in the literature (in terms of expressing properties about a structure in the sense of model theory)? Many people talk about second-order logic, but third-...
1
vote
1answer
81 views

Is there a notion differentiating $\frac1{\mbox{countable }\infty}$ and $\frac1{\mbox{uncountable }\infty}$?

It is accepted belief $\mbox{countable }\infty$ is not $\mbox{uncountable }\infty$. Is there notion differentiating $\frac1{\mbox{countable }\infty}$ and $\frac1{\mbox{uncountable }\infty}$ (latter ...
2
votes
1answer
75 views

Formalizing the deduction theorem in the metatheory

Here is the deduction theorem, in the "$\Leftrightarrow$" version (I'm considering it for first order logic): $$\Delta \cup \lbrace A \rbrace \vdash \lbrace B \rbrace \Longleftrightarrow \Delta \vdash ...
-2
votes
1answer
70 views

Would there be any consequences in accepting conjectures that are essentially true? [closed]

There are many unproven conjectures that if you heuristically took a probability of it being true, it would basically be almost $100\%$ true. I can see why mathematics must be rigorous as many ...
4
votes
0answers
217 views

Metamathematics and the foundations of mathematics

I have some really big doubts about what is the real starting point of all (formal) mathematics. For example: when I search on internet or study texts about the foundations of mathematics such as ...
1
vote
2answers
310 views

What are the other foundations of math?

I know there are at least three foundations of math: Zermelo-Frankel set theory. (Sp?) ECTS Category theory Are there any others? Experimental foundations are welcome.
3
votes
2answers
179 views

The Scope of Axiomatic Set Theory

I am currently studying ZF set theory in terms of first-order logic and I am having trouble understanding the motivation behind this axiomatic formulation of set theory. ZF set theory is a first-...
0
votes
0answers
142 views

How did mathematicans prove things before ZFC or Peano

I do not get it. How was a+b=b+a or a (b +c) = ab + ac proved by ancient mathematicians before set theory or Peano axioms? If you cannot logically prove the laws of arithmetic without Peano or set ...
0
votes
0answers
34 views

Natural Transformation Between Covariant Hom-Functors

Let $\mathscr C$ be a category and $A,B\in Ob_\mathscr C$. I don't think it matters, but assume that $\mathscr C$ is locally small. I want to find a natural transformation between the covariant Hom-...
5
votes
1answer
213 views

Formalist understanding of metalogical proofs

How can a formalist understand a metalogical proof such as the completeness theorem? These proofs exist exclusively outside of a logical system where the "rules of the game" are undefined. These sorts ...
0
votes
0answers
76 views

Can you recommend literature - easy/gentle/for self-study/introductory… - for the following topics…?

I am looking for literature that is as self-explanatory, easy, gentle, readable to the beginner, suitable for self-study, etc.. as possible, in the following fields. (I mean the mathematical part as ...
1
vote
1answer
120 views

Legitimacy of Consistency Proofs

In this question I asked yesterday I put forward two interpretations of a statements such as "System X is consistent". (a) we can think of it as saying no finite sequence of applications of logical ...
3
votes
1answer
105 views

Consistency of PA from a Formalist Perspective

In this lengthy thread there's people bickering back and forth about the consistency of PA (Peano Arithmetic) and misunderstandings abound. In reading it I came to an understanding I found useful, ...
1
vote
2answers
162 views

Well-definedness of uncomputable functions.

I have been reading about Rayo's function and uncomputable functions in general, and have gotten very confused. There is apparently concern over the well-definedness of Rayo's function, but I never ...
1
vote
2answers
37 views

What function $f(n)$ is defined by $f(1)=2$ and $f(n+1)=2f(n)$ for $n\geq 1$

I have to 2 qusetions in a mathematical induction homework: 1-What function $f(n)$ is defined by $f(1)=2$ and $f(n+1)=2f(n)$ for $n\geq 1$ My attempt: $f(1)=2$ $f(2)=2f(1)=2(2)=2^2$ $f(3)=2f(2)=...
2
votes
1answer
74 views

Development of topology and differential geometry in ETCS

I would like to ask for some reference textbooks or articles, or any information that you know about developing topological concepts and differential geometric concepts using as a foundation ETCS ...
6
votes
1answer
93 views

What is the Turing degree of Truth?

First of all by Truth I mean the set $T$ of the Gôdel numbers of the true formulas of first order arithmetic. First order arithmetic is not decidable and $T$ is not decidable, additionally the ...
1
vote
1answer
92 views

Hilbert Program: Consistency vs Soundness

I have been wondering why exactly Hilbert asked for a decidable, complete, and consistent set of axioms for mathematics, rather than a decidable, complete, and sound set of axioms. Consistency being: ...
0
votes
2answers
60 views

How to define substitution using ZFC

One question I've had regarding ZFC is how to define substitution. I cannot see how it's possible, despite the frequent use of substitution within both pure and applied mathematics. Just to be clear, ...
1
vote
1answer
41 views

Question on the reasoning behind determining surjectivity of a function

I understand the idea of surjectivity and its definition: "A function f is surjective if f:A->B if $\forall y\in Y,\exists x \in X$ such that $y=f(x)$" However I have a question on the following ...
1
vote
0answers
61 views

Limit of a sequence related to non-well founded set theory [closed]

Consider the following: $$\alpha_0 = \{\} $$ $$\alpha_1 =\{\{\}\}$$ $$\alpha_2 =\{\{\{\}\}\}$$ $$...$$ Clearly $\alpha_i$ is considered a set for all $i \in \omega$. Then consider $ \alpha=\lim_{i \...
0
votes
2answers
67 views

Need help with proof by contradiction of implication.

Question reads: $$\forall n \in \mathbb{N}, \forall m \in \mathbb{N}, (n^4 + n^2 + 1 \ne m^2)$$ In english, this reads: for every n and m in the set of natural numbers, $n^4 + n^2 + 1$ does not ...
1
vote
0answers
25 views

Sequence of Number System Construction

After constructing the naturals, why construct integers before rationals? Is there a historical explanation? Couldn't ordered pairs of fractions constructed from the naturals be used to represent ...
1
vote
1answer
67 views

What is the difference between the logical formula $\alpha$ and expression “$\alpha$ is true”?

What is the difference between the logical formula $\alpha$ and expression "$\alpha$ is true"? I feel that there is a difference between those expressions. I think this difference is the difference ...
0
votes
0answers
41 views

The length of the sequence concatenated two sequences

Let $\alpha$ be a finite sequence, and $|\alpha|$ be the length of $\alpha$. Let $\alpha_1, \alpha_2$ be two finite sequences. Prove that $|\alpha_1 \alpha_2| = |\alpha_1 |+|\alpha_2|$. Where $\...
1
vote
0answers
110 views

Why the 'natural' consistency proof of PA cannot be carried out $\textbf{in}$ PA

In my proof theory monograph there is this exercise: "The natural proof of PA cannot be carried out in PA. Why? (This proof consists in showing that all theorems of PA are ture.)" Apparently, by '...
0
votes
1answer
19 views

The relation $T$ on $\mathbb{R}\times \mathbb{R}$ given by $(x,y)T(a,b)$ iff $x^2+y^2=a^2+b^2$. Sketch the equivalence class of $(1,2)$; of $(4,0)$.

The relation $T$ on $\mathbb{R}\times \mathbb{R}$ given by $(x,y)T(a,b)$ iff $x^2+y^2=a^2+b^2$. Sketch the equivalence class of $(1,2)$; of $(4,0)$. $T$ is an equivalence relation on $\mathbb{R}\...
0
votes
0answers
52 views

Questions in proof theory (PRA-provability of EA-theorems, Girards book from '87)

I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there. I would be glad if someone can help me with some of the exercises, ...
1
vote
1answer
79 views

Alternative axioms for NBG or MK

While I was thinking about NBG and MK I had the idea for two alternative axioms. As usual $V$ is the class of sets. The first one: For a boolean function $f : \{T,F\}^n \to \{T,F\}$ let $\varphi_f(...
6
votes
2answers
123 views

How badly does foundation fail in NF(etc.)?

The strongest antifoundation axiom I know is due to Boffa. Roughly, it asserts that every graph which could represent a set, does. For example, considering a graph consisting of (a root connected to) ...
8
votes
1answer
98 views

Without foundation: Not transitive model of ZFC?

Let's assume that ZFC is consistent. It is easy to show that there is an illfounded model (with compactness, e.g. here). If we have the axiom of foundation at the background level we can conclude ...
1
vote
1answer
62 views

Questions in proof theory (Definition of an interpretation of one theory in another, Girards Book from '87)

I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there. I would be glad if someone can help me with some of the exercises, ...
1
vote
0answers
64 views

Questions in proof theory (PRA-provability of an EA-axiom, Girards Book from '87)

I am working through the above mentioned book, 'proof theory and logical complexity, volume 1', with some trouble here and there. I would be glad if someone can help me with some of the exercises, ...
1
vote
0answers
50 views

Prospects of teaching/learning elementary math with computed-checked type theory

I've read as much as I can understand about type theory and homotopy type theory (HoTT) and it seems like these are very promising directions for re-foundationalizing mathematics in a way where ...
2
votes
2answers
76 views

Are there mathematical premises that don't hold true whithin other mathematical systems/ways of thinking? [closed]

I do not really know how to phrase the question, but it is as follows: Are there mathematical premises that don't hold truth given different systems? And can someone give me examples? For example ...
3
votes
1answer
95 views

Is every model of MK (Morse-Kelley-Set-Theory) well-founded?

On page 2 in "The Hyperuniverse Project and Maximality" is written: The models $\mathcal{M}$ of MK are of the form $\langle M, \in, \mathcal{C} \rangle$, where $M$ is transitive model of ZFC, $\...
2
votes
0answers
146 views

Principia Mathematica, chapter *117: a false proposition?

I was reading Principia Mathematica of Whitehead and Russell and I have found what I think is a false proposition. The proposition in question is *117.632 click on the link to see the formula and the "...
1
vote
0answers
34 views

Category theory using 2-sorted logic

Can anyone give some reference text that axiomatizes category theory using first order logic using 2 sorts (if that makes sense)? I have found reference about 1 sorted axiomatization but I also found ...
2
votes
3answers
58 views

Proving Equivalence Relations, Constructing and Defining Operations on Equivalence Classes

I think I have an intuitive sense of how ordered pairs can function to specify equivalence classes when used in the construction of integers and rationals, for example. I put the cart before the horse,...
0
votes
1answer
47 views

Definition of < in Construction of Reals

In the section of Spivak's Calculus on the construction of the reals, < is defined: if alpha and beta are real numbers, then a < b means that a is contained in b (that is, every element of a is ...
3
votes
0answers
61 views

Model for the type-theoretic axiom of choice in Coq.

This is the request for references. It is a known fact that there is a model of ZFC in ZF, so ZFC is consistent if ZF is consistent. It is also know that there is a double-negation Godel-Gentzen ...
0
votes
1answer
59 views

Is it possible to prove Regularity with Transfinite Induction only?

Let us assume that we have only statement of transfinite induction. (And maybe some other well-know axioms) My question: "Is it possible to derive from it a regularity axiom as a theorem?". Some of ...
0
votes
1answer
88 views

Formal definition of a functor in $\mathsf{ZFC}$

Let $\mathcal{C}$ and $\mathcal{D}$ be categories. The first thing that comes to mind when considering a definition of a functor between $\mathcal{C}$ and $\mathcal{D}$ in $\mathsf{ZFC}$ is that it ...
1
vote
1answer
92 views

Category of functors $[C,D]$ and Grothendieck universes

A set $U$ is a universe if for any $x \in U$ we have $x \subseteq U$, for any $x,y \in U$ we have $\{x,y\} \in U$, for any $x \in U$ we have $\mathcal{P}(x) \in U$, for any family $(x_i)...