# Questions tagged [metamathematics]

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

91 questions
Filter by
Sorted by
Tagged with
259 views

### Equivalences of $n$-categories

This question is an extension of my previous question last year (see ) in which I asked about the (consensus of a) definition of a weak $n$-category. Here are some background: while strict $n$-...
4k 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 ...
674 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 / ...
767 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&...
247 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 ...
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 ...
232 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 ...
353 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 ...
177 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 ...
245 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....
534 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 ...
283 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 ...
76 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, ...
115 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, ...
92 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, ...
317 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 ...
685 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 ...
254 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 ...
258 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 ...
545 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 ...
1k views

265 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 ...
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....
808 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 ...
349 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-...
237 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 ...
148 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 ...
4k 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 ...