# Questions tagged [metamathematics]

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

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

94
questions

2
votes

1
answer

97
views

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

2
votes

0
answers

205
views

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

2
votes

0
answers

89
views

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

7
votes

2
answers

360
views

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

33
votes

3
answers

4k
views

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

12
votes

1
answer

782
views

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

15
votes

3
answers

893
views

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

3
votes

1
answer

326
views

Taking the doctrine of computational trinitarianism ( https://ncatlab.org/nlab/show/computational+trinitarianism ), if one understands the incompleteness theorems as the "logic" version, and ...

26
votes

3
answers

3k
views

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

4
votes

0
answers

318
views

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

8
votes

1
answer

388
views

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

-4
votes

1
answer

185
views

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

2
votes

1
answer

253
views

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

8
votes

0
answers

579
views

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

2
votes

1
answer

324
views

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

1
vote

0
answers

83
views

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

0
votes

0
answers

141
views

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

1
vote

0
answers

96
views

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

18
votes

1
answer

337
views

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

4
votes

4
answers

887
views

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

3
votes

1
answer

262
views

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

3
votes

0
answers

264
views

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

7
votes

2
answers

584
views

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

15
votes

1
answer

2k
views

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

4
votes

2
answers

459
views

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

2
votes

1
answer

151
views

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

4
votes

2
answers

733
views

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

82
votes

4
answers

21k
views

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

968
views

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

4
votes

1
answer

401
views

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

1
vote

2
answers

720
views

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

6
votes

1
answer

334
views

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

20
votes

1
answer

2k
views

Normally in a type theory, you can not have a type of all types, due to Girad's paradox. This is somewhat similar to how in set theory, you cannot have a set of all sets.
Therefore, usually you just ...

3
votes

1
answer

315
views

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

3
votes

0
answers

239
views

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

2
votes

1
answer

577
views

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

6
votes

2
answers

576
views

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

7
votes

3
answers

487
views

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

1
vote

0
answers

114
views

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

7
votes

3
answers

290
views

$\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}}$
$\...

4
votes

0
answers

277
views

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

19
votes

2
answers

2k
views

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

9
votes

1
answer

830
views

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

2
votes

0
answers

351
views

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

7
votes

0
answers

255
views

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

5
votes

1
answer

158
views

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

16
votes

3
answers

4k
views

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

12
votes

2
answers

1k
views

Are there existential theorems of ZFC, or PA say, with no witnesses?
Ie does there exist a formula $\phi$ such that ZFC $\vdash\exists x \phi(x)$, but for all numerals $\underline{n}$, ZFC $\nvdash \...

1
vote

2
answers

409
views

Hopcroft and Ullman's definition of a Turing machine seems to be standard. This definition defines a Turing machine to be a 7-tupel $T = \langle Q,\Gamma,b,\Sigma,\delta,q_0,F \rangle$ obeying some ...

1
vote

1
answer

536
views

I hope that this post isn't off topic, but I already asked math.stackexchange about first order formalizations of first order logic. There are provability logics and extensions in modal logic's that ...