Questions tagged [metamathematics]
the mathematical discipline that applies mathematical methods to the study of mathematical theories themselves.
96
questions
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, ...
72
votes
31
answers
9k
views
Can infinity shorten proofs a lot?
I've just been asked for a good example of a situation in maths where using infinity can greatly shorten an argument. The person who wants the example wants it as part of a presentation to the general ...
- 28.7k
35
votes
1
answer
3k
views
Is there a common genesis for ADE classifications?
Recall that a certain type of object admits an ADE classification if there is a notion of equivalence relative to which equivalence classes of objects of the given type can be placed in one-to-one ...
- 28.8k
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 ...
- 447
30
votes
8
answers
2k
views
Cryptomorphisms
I am curious to collect examples of equivalent axiomatizations of mathematical structures. The two examples that I have in mind are
Topological Spaces. These can be defined in terms of open sets, ...
27
votes
13
answers
3k
views
Are there any good nonconstructive "existential metatheorems"?
Are there any good examples of theorems in reasonably expressive theories (like Peano arithmetic) for which it is substantially easier to prove (in a metatheory) that a proof exists than it is ...
26
votes
9
answers
5k
views
Proofs of Gödel's theorem
I am interested in different contexts in which Gödel's incompleteness theorems arise. Besides traditional Gödelian proof via arithmetization and formalization of liar paradox it may also be obtained ...
- 1,177
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 ...
- 479
26
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 ...
- 5,831
23
votes
8
answers
3k
views
Intuitive and/or philosophical explanation for set theory paradoxes
Every student of set theory knows that the early axiomatization of the theory
had to deal with spectacular paradoxes such as Russel's, Burali-Forti's etc.
This is why the (self-contradictory) ...
- 3,565
21
votes
6
answers
2k
views
Consistency strength needed for applied mathematics
Given that we can never proof the consistency of a theory for the foundations of mathematics in a weaker system, one could seriously doubt whether any of the commonly used foundational frameworks (ZFC ...
- 1,218
21
votes
4
answers
4k
views
Don't the axioms of set theory implicitly assume numbers?
When one writes down the axioms of ZFC, or any other axiomatic theory for that matter, and making statements like "let x, y ..." doesn't this assume an understanding (and thus existence) of natural ...
- 387
20
votes
12
answers
10k
views
The best text to study both incompleteness theorems
Hi!
What text on both incompleteness theorems you would recommend for beginner?
Specifically, I'm looking for the text with the following properties:
1) The proofs should be finitistic, in Godel's ...
19
votes
6
answers
2k
views
Complete mathematics
Hello, I would like to ask you if there is a mathematical theory, that is complete (in the sense of Goedel's theorem) but practically applicable. I know about Robinson arithmetic that is very limited ...
- 305
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....
user103598
18
votes
3
answers
1k
views
Are there examples of nonconstructive metaproofs?
This came up in a question on the xkcd forums. Is it possible to have a nonconstructive metaproof, i.e. a proof that there exists a proof in some formal system which does not construct said proof? Are ...
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 ...
- 30.2k
17
votes
5
answers
5k
views
Bourbaki's epsilon-calculus notation
Bourbaki used a very very strange notation for the epsilon-calculus consisting of $\tau$s and $\blacksquare$. In fact, that box should not be filled in, but for some reason, I can't produce a \Box.
...
- 19.4k
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 + \...
- 5,831
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 ...
- 273
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&...
- 163
14
votes
2
answers
4k
views
Meta$^{n{-}th}$ mathematics [duplicate]
Metamathematics has a reasonably clear connotation,
enough to have a Wikipedia page,
with Gödel, Tarski, and Turing playing leading roles;
Kleene's book (Introduction to Metamathematics (Amazon link));...
- 149k
14
votes
1
answer
919
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 / ...
- 6,726
13
votes
5
answers
1k
views
"Let $x \in A$", beginning a proof of "$\forall x \in A$ ...", if A were empty [closed]
I work at a four-year teaching school, where we pride ourselves on teaching pure math, proof, and a rather obsessive carefulness of work. Recently I have been criticized for saying that "Let $x \in A$...
- 139
13
votes
3
answers
2k
views
Are there natural examples of mathematical statements which follow from consistency statements?
Motivation
One of the methods for strictly extending a theory $T$ (which is axiomatizable and consistent, and includes enough arithmetic) is adding the sentence expressing the consistency of $T$ ( $...
- 5,362
12
votes
2
answers
2k
views
Existential statement without witness
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 \...
- 223
12
votes
2
answers
928
views
How necessary is Godel's Condensation Lemma
It seems that the Godel's Condensation Lemma is typically used to show that certain constructible sets will appear by some stage of the construction of $L$. For example in the proof that CH holds in $...
- 281
11
votes
4
answers
2k
views
Embedding Theorem for topological spaces, and in general
There are many examples throughout mathematics of abstracting the formal properties of a "familiar" structure, but then having a theorem stating that all models of the abstract axioms embed into one ...
- 1,513
10
votes
4
answers
1k
views
Complete extensions of first order logic (or language)
Lindstrom's theorem states that any extension of first order logic (FOL) more expressible than FOL fails to have either compactness or Lowenheim-Skolem. When I first read Lindstrom's theorem my first ...
- 1,177
10
votes
3
answers
1k
views
Is there a formal notion of what we do when we 'Let X be ...'?
This is likely an elementary question to logicians or theoretical computer scientists, but I'm less than adequately informed on either topic and don't know where to find the answer. Please excuse the ...
- 1,376
9
votes
2
answers
1k
views
"Requires axiom of choice" vs. "explicitly constructible"
I think I'm a bit confused about the relationship between some concepts in mathematical logic, namely constructions that require the axiom of choice and "explicit" results.
For example, let's take ...
- 5,932
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 ...
- 5,831
8
votes
1
answer
452
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 ...
- 1,803
8
votes
0
answers
655
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 ...
- 5,831
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 ...
7
votes
3
answers
500
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 ...
- 975
7
votes
1
answer
1k
views
Is there a known way to formalise notion that certain theorems are essential ones?
Suppose You ask a question beginning from "Why some structure is..." or "Why some object has property..." and several
answers arises. Which criteria do You
use to qualify which answer is correct?
For ...
7
votes
2
answers
691
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 ...
- 5,831
7
votes
2
answers
409
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$-...
- 5,038
7
votes
2
answers
666
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 ...
- 5,831
7
votes
2
answers
845
views
Are computable models sufficient?
What I mean is this. By downward Lowenheim-Skolem theorem, first-order formula Q is a always true iff it is true in every countable structure. But is there some first-order formula Q which is true in ...
- 1,177
7
votes
3
answers
728
views
What assumptions and methodology do metaproofs of logic theorems use and employ?
In logic modules, theorems like Soundness and completeness of first order logic are proved. Later, Godel's incompleteness theorem is proved. May I ask what are assumed at the metalevel to prove such ...
user2529
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}}$
$\...
- 6,621
6
votes
6
answers
2k
views
Formal proof of Con(ZFC) => Con(ZFC + not CH) in ZFC
Is it possible to prove $Con(ZFC) \rightarrow Con(ZFC + \neg CH)$ purely within ZFC? To prove this (using forcing) one seems to need a countable transitive model of ZFC. The texts I am reading avoid ...
- 345
6
votes
5
answers
3k
views
A meta-mathematical question related to Hilbert tenth problem
I am reading Bjorn Poonen's very nice survey on Hilbert's Tenth problem
(http://www-math.mit.edu/~poonen/papers/uniform.pdf), and while I believe I understand the mathematics well, I have widespread ...
- 25.7k
6
votes
7
answers
2k
views
The isomorphism inference rule
Suppose we are writing very detailed proofs, absolutely without any gaps (for example, for checking proofs by computer).
In such formal proofs every step (even a trivial one) must be justified.
For ...
- 897
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 ...
- 5,831
5
votes
9
answers
2k
views
Are there any important mathematical concepts without discrete analog?
In "continuous" mathematics there are several important notions such as covering space, fibre bundle, Morse theory, simplicial complex, differential equation, real numbers, real projective plane, etc. ...
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 ...
- 4,529
5
votes
1
answer
701
views
Does ZF prove that a finite subtheory axiomatizes it over transitive proper class models?
If $\text{ZF}$ is consistent, then it is not finitely axiomatizable. For if $\Gamma$ is a finite axiomatization, then $\text{ZF}$ proves by reflection that $\Gamma$ has a set model, and hence (since $...
- 1,101