Questions tagged [metamathematics]

the mathematical discipline that applies mathematical methods to the study of mathematical theories themselves.

Filter by
Sorted by
Tagged with
-1 votes
0 answers
78 views

Minimal metatheory for Gödel's first incompleteness theorem [duplicate]

When studying the complete proof of Gödel's first incompleteness theorem, I started to harbor a metamathematical worry of circularity. For reference, I am studying the proof in A Concise Introduction ...
God bless's user avatar
  • 107
4 votes
0 answers
140 views

Are the relations of being homeomorphic or being homotopy equivalent on the compact polyhedra definable in the structure of the natural numbers?

Let $ K(\mathbb{N}) $ denote the set of all finite simplicial complexes with vertices in $\mathbb{N}$. Let $ f\colon \mathbb{N} \to K(\mathbb{N}) $ be a computable bijection. Let $ R $ = { $ (m, n) $ |...
Juan Atacama's user avatar
-5 votes
1 answer
460 views

How much would a mathematician cost? [closed]

Recently our department lost one of the best professors who was attracted by a better University. If we were a football club, and he were a leading player, we would receive many millions of ...
3 votes
1 answer
149 views

Does CZF prove there is a minimal cauchy completion of the rationals?

In IZF, we can easily prove there is a minimal cauchy complete field extending the rationals: the dedekind reals are cauchy complete, so just intersect all of its cauchy complete subfields. CZF can ...
Christopher King's user avatar
2 votes
0 answers
230 views

A formal definition of a useful theorem?

Sorry if this feels a bit squishy, but I'm wondering if there is any published work trying to give a fully formal definition of the notion of a useful theorem. I mean, in mathematics we all know that ...
Peter Gerdes's user avatar
  • 2,551
2 votes
0 answers
95 views

How restrained are we in terms of metatheories when working with higher order logics with full semantics?

When working in the realm of first order logic one can use very basic mathematical backgrounds(in reverse mathematical sense) to prove interesting things about more "structures". In what ...
H.C Manu's user avatar
  • 733
7 votes
2 answers
406 views

Equivalences of $n$-categories

This question is an extension of my previous question last year (see [2020]) in which I asked about the (consensus of a) definition of a weak $n$-category. Here are some background: while strict $n$-...
Student's user avatar
  • 5,008
33 votes
3 answers
5k views

Top-down mathematics, or "Where it all begins"

Sorry if this is off-topic. It was my attempt to take a top-down approach to mathematics. Being an inexperienced undergraduate (so please take my writing here lightly), I've been presented with ZFC as ...
steve's user avatar
  • 447
13 votes
1 answer
912 views

So after all, what is this thing about topos theory and non-binary truth?

Disclaimer. The question below is necessarily vague. I understand neither the subject matter topos theory nor the object about which my question is (the construction of a fractional / non-binary / ...
dohmatob's user avatar
  • 6,706
16 votes
3 answers
1k views

Is there a semantics for intuitionistic logic that is meta-theoretically "self-hosting"?

One can study the standard semantics of classical propositional logic within classical logic set theory, so we can say that the semantics of classical logic is meta-theoretically "self-hosting&...
ttbo's user avatar
  • 163
3 votes
1 answer
434 views

Is there an equivalent of the incompleteness theorems/halting problem in category theory?

Taking the doctrine of computational trinitarianism ( https://ncatlab.org/nlab/show/computational+trinitarianism ), if one understands the incompleteness theorems as the "logic" version, and ...
Tristan Duquesne's user avatar
26 votes
3 answers
3k views

What sorts of extra axioms might we add to ZFC to compute higher Busy Beaver numbers?

First, some context. Ever since I was a high schooler, I have been fascinated with large numbers. As I have grown in mathematical maturity, I have become both disappointed and fascinated to see that ...
exfret's user avatar
  • 479
4 votes
0 answers
400 views

How can I prove that primitive recursion “preserves” representability in Peano Arithmetic?

I'm working on my thesis about Gödel's Incompleteness Theorems, and at some point I need to prove that the $\textsf{PA}$ system is able to represent all the recursive functions. By recursive function ...
Ranopano's user avatar
8 votes
1 answer
443 views

Natural $\Pi_1$ sentence independent of PA

Order invariant graphs and finite incompleteness by Harvey Friedman gives an example of a combinatorial/non-metamathematical $\Pi_1$ sentence that is independent of ZFC. Is there a simpler example of ...
user76284's user avatar
  • 1,793
-4 votes
1 answer
195 views

Is there a procedure to derive models from axiomatic systems? [closed]

Is there a systematic procedure to construct a model of an axiomatic system from the system itself? For example given the abstract postulates of a ring we can show that the integers satisfies them ...
Ivan Meir's user avatar
  • 4,762
2 votes
1 answer
269 views

Possible to prove a lemma from Godel's completeness theorem in intuitionistic logic?

I am trying to determine whether a particular theorem used in the course of Godel’s (1930) proof of the completeness of predicate logic could be proven in an intuitionistic metatheory. Theorem VI (p....
Mallik's user avatar
  • 583
8 votes
0 answers
649 views

Is there any theorem achieving Conway's "Mathematician's Liberation Movement"

John Conway on in the appendix to part zero of ONAG describes a "Mathematician's Liberation Movement". The goal would be to give mathematicians the freedom to create mathematical theories with the ...
Christopher King's user avatar
2 votes
1 answer
401 views

ZFC ability to express truth and $\omega$ - consistency

Some theories can lie about their own consistency (for example, if $PA$ is consistent then the theory $PA + \lnot CON(PA)$ is consistent, although it proves its own inconsistency). Now working with ...
D. Hershko's user avatar
1 vote
0 answers
94 views

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

I've been working through a textbook, often encountering difficulties with the exercises. On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution. As I understand, ...
Ettore's user avatar
  • 121
0 votes
0 answers
158 views

Are the HBL derivability conditions necessary for Gödel's incompleteness theorems? (For Löb's theorem?)

I've been working through a textbook, often encountering difficulties with the exercises. On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution. As I understand, ...
Ettore's user avatar
  • 121
1 vote
0 answers
106 views

n-consistency - provability/truth of $\Sigma^0_n$ and $\Pi^0_{n+1}$ -formulas; n-consistent extensions, etc

I've been working through a textbook, often encountering difficulties with the exercises. On mathstackexchange, with most of them I haven't arrived yet at a satisfactory solution. As I understand, ...
Ettore's user avatar
  • 121
18 votes
1 answer
356 views

Proof as a Σ₁ approximation to truth: what about higher degrees?

Let us posit that the goal of mathematics is to study mathematical truths, and let us stick to arithmetic for simplicity: so let $\mathscr{T} \subseteq \mathbb{N}$ be the set of (Gödel codes of) true ...
Gro-Tsen's user avatar
  • 29.8k
5 votes
4 answers
1k views

How can you formalize the metamathematics conventionally used to state Godel’s theorem?

Gödel’s incompleteness theorem states that for any sufficiently strong formal system $T$ there exists a statement $G$ such that if $T$ is consistent, then $G$ is true but not provable in $T$. But I’m ...
Keshav Srinivasan's user avatar
3 votes
1 answer
294 views

Unorthodox constructive reasoning: The Kleene Getaway

KG (the Kleene Getaway) is the name I improvised (in my answer to a question on MO on constructive Perron-Frobenius) for a constructive principle which enables the direct constructive use of a ...
Franka Waaldijk's user avatar
3 votes
0 answers
271 views

Can we prove the epsilon theorems without the axiom of choice?

Hilbert's epsilon $\epsilon$ is a quantifier. It follows the rule that if $\exists x. p(x)$, for some predicate $p$, we can infer $p(\epsilon x. p(x))$. Semantically, it represents picking some ...
Christopher King's user avatar
7 votes
2 answers
663 views

Is every true statement independent of $PA$ equivalent to some consistency statement?

Most true statements independent of PA that I know of is equivalent to some consistency statement. For example Con(PA), Con(PA + Con(PA)), Con(PA + Con(PA) + Con (PA + Con(PA)), $\dots$ Goodstein's ...
Christopher King's user avatar
17 votes
1 answer
2k views

What is known about the relationship between Fermat's last theorem and Peano Arithmetic?

As far as I know, whether Fermat's Last Theorem is provable in Peano Arithmetic is an open problem. What is known about this problem? In particular, what is known about the arithmetic systems $PA + \...
Christopher King's user avatar
4 votes
2 answers
473 views

Experiments physically performable in a finite amount of time whose results are independent of ZFC [closed]

In On independence and large cardinal strength of physical statements we see that their are physical statements which are independent of ZFC, and even strong cardinal axioms. There were many answers, ...
Christopher King's user avatar
2 votes
1 answer
170 views

Internal operations on uncomputable functions

Is there know set of operations for which uncomputable functions are, let's name it down-unclosed? I mean a set of operations which takes two ( or more) uncomputable functions and return computable ...
kakaz's user avatar
  • 1,596
4 votes
2 answers
776 views

What things does ZFC not know if it knows?

The statement "ZFC $\vdash 0=1$" is independent of ZFC due to Goedel's second incompleteness theorem. That got me wondering, for what other statements $\phi$ is "ZFC $\vdash \phi$" independent of ZFC? ...
Christopher King's user avatar
85 votes
4 answers
21k views

The enigmatic complexity of number theory

One of the most salient aspects of the discipline of number theory is that from a very small number of definitions, entities and axioms one is led to an extraordinary wealth and diversity of theorems, ...
1 vote
1 answer
1k views

Question about the validity of Michael Grossman, Robert Katz and Jane Grossman Non-Newtonian / Meta / Multiplicative Calculus [closed]

I am no mathematician by far, but I have studied diff. and integral calc and beyond, in my undergrad years. I recently came upon this book: "The First Systems of Weighted Differential and ...
LastTribunal's user avatar
4 votes
1 answer
512 views

Can adding Hilbert's epsilon to a theory, and then expanding that theories axiom schema to include the new language, cause it to become inconsistent?

Epsilon Calculus is a formalism developed by Hilbert adding his $\epsilon$ operator to predicate logic. $\epsilon x. A(x)$ is a term such that $\exists x.A(x) \implies A(\epsilon x.A(x))$. In can ...
Christopher King's user avatar
1 vote
2 answers
753 views

Can you remove all the extra arithmetic from ZFC (or other theories)?

Let $\mathbb{N}$ be the standard model of the natural numbers. For any statement in the language of arithmetic, we can translate into a statement in the language of set theory by asking if it is true ...
Christopher King's user avatar
6 votes
1 answer
363 views

What drawbacks are there to using NF(U) for category theory?

In category theory, you often run into what is known as "size" issues. That is, you run into the issue that the categories you try to define are too "big" to be sets, and so you need to use classes or ...
Christopher King's user avatar
25 votes
1 answer
2k views

Can you have a type theory where there is type of all types?

Normally in a type theory, you can not have a type of all types, due to Girard's paradox. This is somewhat similar to how in set theory, you cannot have a set of all sets. Therefore, usually you just ...
Christopher King's user avatar
3 votes
1 answer
347 views

Can you formulate a theory stating that a truth predicate does not exist for first order set theory?

A truth predicate for first order set theory would allow you to determine the truth of statements in first order set theory. A definition is given here. My question is, can you formulate a statement ...
Christopher King's user avatar
3 votes
0 answers
251 views

A theory which denies the existence of a truth predicate

Is there a paper or other reference that explores the implications of a theory that denying the existence of a truth predicate in its own language (perhaps based on ZFC or PA)? I know that a theory ...
Christopher King's user avatar
2 votes
1 answer
639 views

Is ZFC plus a truth predicate capable of variable substitution consistent?

Let us define a truth predicate that allows one to substitute in variables. For example, for a 3-ary predicate $p$ and sets $A$, $B$, and $C$, then $\text{true}(\ulcorner p \urcorner, A, B, C)$ (where ...
Christopher King's user avatar
7 votes
2 answers
678 views

What two ordinals are these (based on definable ordinals)?

Let $D$ be the set of definable ordinals. An ordinal s is definable if there is a predicate $p$ (in the language of (first-order) set theory), such that $p(x) \iff x=s$ for all $x$. This is definitely ...
Christopher King's user avatar
7 votes
3 answers
499 views

On structures that are not submitted to compatibility conditions

In mathematics, it seems that 100 % of the time, we deal with objects that have a number of different structures that are "compatible" with each other. For example, a Lie group is a manifold and a ...
Phil-W's user avatar
  • 975
1 vote
0 answers
124 views

Can $GPK^{+}_{\infty}$ + $AC_{WF}$ prove "$ZFC$ proves that the class of ordinals is not weakly compact for definable classes?

Consider the topological set theory $GPK^{+}_{\infty}$ +$AC_{WF}$, where $GPK^{+}_{\infty}$ is defined as follows (this from Olivier Esser's papers, "An Interpretation of the Zermelo-Fraenkel Set ...
Thomas Benjamin's user avatar
7 votes
3 answers
305 views

Automatic transfer of pointwise metric computations to bundle computations

$\newcommand{\M}{\mathcal{M}}$ $\newcommand{\N}{\mathcal{N}}$ $\newcommand{\deriv}[2]{\frac{d#1}{d#2}}$ $\newcommand{\sAverage}[1]{\langle#1\rangle} $ $\newcommand{\IP}[2]{\sAverage{#1,#2}}$ $\...
Asaf Shachar's user avatar
  • 6,611
4 votes
0 answers
283 views

the strength of saying "each sentence of true arithmetic has a recursive proof"

Let $PA_{\omega}$ be just like $PA$ except that $PA_{\omega}$-proofs can use any number of applications of the recursive $\omega$-rule. The recursive $\omega$-rule allows the following: For each ...
Haidar's user avatar
  • 449
19 votes
2 answers
2k views

Which kind of foundation are mathematicians using when proving metatheorems?

Zermelo-Fraenkel set theory (with choice) is commonly accepted as the standard foundation of mathematics. It is a material set theory. For every two objects/sets $a,b$ one can ask whether $a=b$ or not....
user avatar
9 votes
1 answer
859 views

Is there any set theory $T$ such that $T$ plus true arithmetic is complete with respect to statements in set theory?

Is there an effective set theory $T$ such that $T + $$TA$ is consistient and complete. It should at least prove all theorems of $ZF$ true, so that it is a "standard" set theory. In particular, the ...
Christopher King's user avatar
2 votes
0 answers
362 views

The theory of frames and locales as elementary topology [closed]

In What is elementary geometry? (pdf) Alfred Tarski defined elementary geometry to be that part of Euclidean geometry which can be formulated and established without the help of any set-...
Rafał Gruszczyński's user avatar
8 votes
0 answers
300 views

Gleason’s Theorem for non-separable Hilbert spaces: On a theorem of Solovay

Gleason’s theorem plays an important role in the foundations of quantum mechanics. On the positive side it demonstrates how the probabilistic structure of quantum theory follows from its logical ...
Mohammad Golshani's user avatar
5 votes
1 answer
212 views

Is it possible to prove concentration bounds from optional stopping theorem?

It is known that the optional stopping theorem from martingale theory is a very powerful theorem in probability theory in statistics. I have heard of a probability course at Stanford where ...
TomTom's user avatar
  • 103
17 votes
3 answers
5k views

Is there a compendium of the consistency strength between the most important formal theories?

Preliminar Notions: A formal system is a tuple $(\Sigma,G,A,R)$ where $\Sigma$ is an alphabet (set of symbols), $G$ is a formal grammar on $\Sigma$ that generates a formal language $L$ (set of well ...
Jonathan Julian's user avatar