Questions tagged [metamathematics]

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

15 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
8 votes
0 answers
650 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
8 votes
0 answers
301 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
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
4 votes
0 answers
402 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
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
3 votes
0 answers
272 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
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
0 answers
231 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
1 vote
0 answers
95 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
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
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
1 vote
0 answers
222 views

Classification of properties of structures

Is there a sensible classification of the properties of structures with a given signature $\sigma$, e.g. graphs with $\sigma = \lbrace R \rbrace$? For example like this: properties defined by first-...
Hans-Peter Stricker's user avatar
1 vote
1 answer
579 views

Is there any current development of a first order formalization of metamathematics?

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 ...
dezakin's user avatar
  • 223
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