New answers tagged lo.logic
2
votes
Extending the class of primitive recursive functions with higher order recursion schema
a constructive (from intuitionistic point of view) of higher order calculus of functionals and relations is at
https://arxiv.org/abs/1501.03043
4
votes
Accepted
MIP*=RE theorem and its impact on logic and proof theory
You wrote:
maybe there is some undecidable problem on which now we can shed some more light …
Depending on what you mean by "shed some more light," the answer is yes; the original paper ...
- 75.8k
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
3
votes
I have a problem about elementary submodels of ZFC
You have to distinguish between $A$ (which is in $M$ and might be uncountable) and $A\cap M$ (which is always countable but might not be in $M$).
Let's look at $A=\omega_1$ for concreteness. Since $\...
- 18.2k
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,632
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
4
votes
How did Szmielew prove that Pasch's axiom is a consequence of the circle axiom?
No luck here with the source (online issues start at 1973), but I did find the abstract:
The Pasch axiom is known to be independent of the remaining axioms of
the plane Euclidean geometry $E$. By ...
- 169k
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
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
4
votes
Words which are not inverted by any endomorphism
This partial answer just covers the case of $\psi$ non-surjective, i.e. not an automorphism.
Just to set some notation: Define $A=\langle w_1, w_2\rangle=\operatorname{im}(\phi)\leq F_2$. We will show ...
- 2,667
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
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
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,632
4
votes
Are there any undecidability results that are not known to have a diagonal argument proof?
EDIT: On reflection, this answer is pretty incorrect. There is a point here, but it's formulated badly enough that I think this should be ignored. I wasn't sure what best practice is for a wrong ...
- 41
1
vote
Is there a consistent, unsound, $\omega$-inconsistent, effective theory that doesn't prove its own inconsistency?
Noah's answer may be the best here. But I'll add this as an additional answer. In particular, the theory in question is not fully formalized in the language of arithmetic.
Let's take theory $\sf PA + \...
- 7,901
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
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 (...
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
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
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
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
0
votes
Accepted
Another implication of the Affine Desargues Axiom
Just to close this question as answered, I will give a sketch of the proof of the parallelity of the lines $\overline{zc}$ and $\overline{yb}$.
As was noticed by @AlexRavsky, it suffices to prove that ...
- 39.6k
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
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
2
votes
Accepted
Are radicals dense in the real closure of an ordered field?
Few years late, but the answer to your 2nd question is negative: let $F=\mathbb{Q}\left(\epsilon\right)$, ordered such that $\epsilon > 0$ is smaller than any positive rational. Let $a_1<a_2<...
- 1,948
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
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
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
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
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
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
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
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
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
0
votes
Set theories without "junk" theorems?
Junk theorems like this are avoided in Type Theory (not just HoTT). This is because I cannot talk about the representation of objects like the natural numbers. This is exploited in Homotopy Type ...
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
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
4
votes
Accepted
Splitting $\Pi^0_2$ Singletons?
It seems to me that every $\Delta^0_2$-set $X$ is a $\Pi^0_2$-singleton. Namely, $X$ satisfies the statement "for all $n$, $n\in X$ implies the $\Pi^0_2$-condition for membership in $X$ and $n\...
- 1,545
3
votes
Quantifier complexity of the definition of continuity of functions
The following should really be a comment rather than an answer, but it's too long:
Continuity is rarely $\exists^*$ or $\forall^*$ characterizable.
Specifically, consider the following two properties ...
- 18.2k
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
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
-1
votes
Mostowski collapses and universal extensional relational classes
There seems to be a reasonable category-theoretic question here, about morphisms between well founded relations and the reflection into the full subcategory of reflective ones.
I am a categorist and I ...
- 7,731
0
votes
A $\Pi^0_1$ class of $\alpha$-subgenerics for all $\alpha < w_1^{CK}$
So I emailed back and forth with Leo about this and, after the usual part where I drag the conversation into confusion by getting overly specific, I believe I understand how this is supposed to work.
...
- 2,419
Top 50 recent answers are included