32
votes
Accepted
Are there any undecidability results that are not known to have a diagonal argument proof?
Let me propose a candidate: Kolmogorov complexity is not computable.
That is, there is no computable procedure that, given a finite sequence $s$, produces the size of the smallest program (with ...
- 216k
21
votes
Are there any undecidability results that are not known to have a diagonal argument proof?
From a point of view your question relates to an "open conjecture" in computability theory.
I think you are asking if there is a specific problem $P$, which can be shown to be undecidable, ...
- 6,127
21
votes
What notable theorems cannot be automatically proven without choice using Shoenfield absoluteness?
$\text{ZF}+ \text{AC}_{\omega}$ is not $\Sigma^1_4$-conservative over ZF and ZF + DC is not $\Sigma^1_4$-conservative over $\text{ZF}+ \text{AC}_{\omega}.$
An example of the former: the sentence $\...
- 3,642
16
votes
Accepted
Propositional calculus, first order theories, models, completeness
Unfortunately I don't quite agree with your summary.
First, in the context of propositional logic, the relevant notion of model is simply a row of the truth table, a propositional world, a valuation ...
- 216k
16
votes
Are there any undecidability results that are not known to have a diagonal argument proof?
Too long to be a comment: Joel's Kolmogorov complexity argument contains what I would consider to be a diagonalization. Here is an essentially equivalent argument which makes the diagonalization more ...
- 113k
16
votes
Accepted
(Very) Large numbers, Chaitin's incompletness theorem and a specific upper bound
One way to provide an explict bound on $L$ is as follows, using the idea of the universal algorithm.
Namely, for any computably axiomatizable theory $T$ in question, consider the algorithm $p$ that ...
- 216k
14
votes
Are there any undecidability results that are not known to have a diagonal argument proof?
I think that the Burali-Forti-like proof of the incomputability of (a minor variation of) Kleene's $\mathcal{O}$ may fit the bill.
Let $\mathcal{W}$ be the set of indices for computable well-orderings;...
- 18.2k
13
votes
Accepted
Can we effectively axiomatize a theory that proves the negation of its own Gödel's sentence?
$\newcommand{\Con}{\operatorname{Con}}$In fact, there is no issue here - already the "naive" approach does the job, and the subtlety you are worried about is irrelevant.
The Godel sentence $...
- 18.2k
13
votes
Are there any undecidability results that are not known to have a diagonal argument proof?
[Edited slightly for (hopefully!) greater clarity.]
This is more of a comment than an answer, but I think it is relevant. In the context of computational complexity theory (rather than computability ...
- 75.8k
13
votes
Accepted
Is the set of permissible numbers of models of various cardinalities computable?
Let $T$ be a complete countable first-order theory. I will write $I(T,\kappa)$ for the number of models of $T$ of cardinality $\kappa$ up to isomorphism. The function $I(T,-)$ is called the spectrum ...
- 4,203
13
votes
Accepted
Why adhere to $\omega$-consistency with respect to Godel's proof of first incompleteness?
To my way of thinking, the principal case of interest with regard to the first incompleteness theorem, the case carrying almost fully the philosophical interest and fascination of the theorem, is the ...
- 216k
12
votes
Accepted
Is the existence of substructures satisfying a theory absolute?
Assuming $T$ is countable (in $V$), the answer is yes.
By downward Lowenheim-Skolem applied to $\mathfrak{B}$, $\varphi(\mathfrak{A},T)$ is equivalent to "$\mathfrak{A}$ has a countable ...
- 18.2k
12
votes
Accepted
Turing degrees of sets separating two computably inseparable sets (theorems and antitheorems)
The class of sets (or rather, degrees of sets) $D$ separating $A$ and $B$ is a well-studied class in computability theory called `PA degrees'. Indeed there PA degrees that are low (hence below $0'$), ...
- 678
11
votes
What is lost in General Relativity without Hahn-Banach axiom in the ZF+HB set theory?
This is perhaps more of an extended comment than a real answer, but I do think it goes a long way towards answering these kinds of questions.
The set-theoretic result referred to as Shoenfield ...
- 9,099
10
votes
Accepted
Is there a consistent, unsound, $\omega$-inconsistent, effective theory that doesn't prove its own inconsistency?
Sure. Consider something like $T=\mathsf{PA}+\neg\mathit{Con}(\mathsf{ZFC})$ (assuming $\mathsf{ZFC}$ is actually consistent of course).
$T$ is consistent but not $\omega$-consistent (it proves that ...
- 18.2k
10
votes
What notable theorems cannot be automatically proven without choice using Shoenfield absoluteness?
This is sort of an anti-answer, which I've accordingly made CW, but here goes:
Whether $\mathsf{ZFC}$ is projectively conservative over $\mathsf{ZF}$ seems open; see Joel's answer from a while ago (...
8
votes
Quantifier complexity of definition of compactness
Often the way you prove that something isn't formalizable in first-order logic is (ironically enough) with a compactness proof. This is how you show, for instance, that there isn't a first-order ...
- 9,099
8
votes
Is the existence of substructures satisfying a theory absolute?
In the general case with uncountable languages, the answer is no.
Let $A$ be a Suslin tree in $V$, considered as a partial order structure in language $\leq$, equipped also with predicates $U_\alpha$ ...
- 216k
8
votes
Turing degrees of sets separating two computably inseparable sets (theorems and antitheorems)
It is a standard consequence of the low basis theorem that $A$ and $B$ (or indeed, any disjoint pair of r.e. sets) have a separating set $D$ that is low, and therefore of Turing degree strictly below $...
- 42.6k
7
votes
Accepted
Thick Canadian trees
$\newcommand{\Add}{\operatorname{Add}}$Start with a model $V$ satisfying $GCH$ (or just $2^{\omega}=\omega_1$ and $2^{\omega_1}=\omega_2$). Force over $V$ with the product $\Add(\omega,\omega_2)\times ...
- 1,058
7
votes
Accepted
Consistency in pure type systems
I think this awkwardness is coming from your “principle of constants”, which is not standard, and doesn’t seem justified by the motivation you give.
You say it’s meant to correspond to the practice (...
- 18.5k
7
votes
Accepted
The additive structure of clusters of nonstandard models of arithmetic
The answer is yes. The additive cluster structure knows the additive structure of the original model up to isomorphism.
Theorem. The additive structure of any countable nonstandard model $M$ of $\...
- 216k
7
votes
The additive structure of clusters of nonstandard models of arithmetic
If you intend literally to recover the addition operation of the given model $M$, then the answer is negative. For every nonstandard model of arithmetic $M$ there is another model $M'$ having exactly ...
- 216k
7
votes
Can we effectively axiomatize a theory that proves the negation of its own Gödel's sentence?
The answer is yes. Let $T$ be the theory PA + $\neg$Con(PA). So this theory proves $\neg$Con(PA) and hence also $\neg$Con(T). But as Noah mentions, Con(T) is provably equivalent in T to the Godel ...
- 216k
7
votes
Accepted
The Parity Principle and $\mathbf{C}_2$ (choice for $2$-sets)
Over ZFA, the Parity Principle is strictly weaker. We'll show it follows from Multiple Choice, the assertion that for any family of nonempty sets $\mathcal{F},$ there is $g: \mathcal{F} \rightarrow [\...
- 3,642
7
votes
Accepted
Impredicativity, definition, recursion and conservatism
The formula $Gx\leftrightarrow A(G,x)$, expressing that $G$ is a fixed-point of the operator defined by $A$, is not sufficient, by itself, to uniquely characterize $G$. That operator may have many ...
- 70.8k
6
votes
Are there any undecidability results that are not known to have a diagonal argument proof?
This is not really an answer but a possible way to formalize your question. In my mind the “essence” of a diagonal-style proof of undecidability is that it explicitly points out the input on which ...
- 111
6
votes
Accepted
What is lost in General Relativity without Hahn-Banach axiom in the ZF+HB set theory?
As Ryan Budney mentioned in a comment, there is some ambiguity about what exactly you mean by "general relativity." General relativity is primarily a physical theory rather than a ...
- 75.8k
6
votes
End-extension which Mostowski collapses a fake well ordering
In Chapter 3 of his PhD thesis, Harvey Friedman showed that there is a recursive linear ordering $\prec$ which has no hyperarithmetic infinite descending sequence and which does not support a jump ...
- 1,545
5
votes
Is the set of permissible numbers of models of various cardinalities computable?
This is really an addendum to Alex's answer. I wrote a program in SageMath (using GAP) that computes these numbers, so I was able to expand Alex's lists considerably. Each of these lists should be ...
- 9,099
Only top scored, non community-wiki answers of a minimum length are eligible