# Tag Info

### 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
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 ...
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 ...

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'$), ...

### 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 ...

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 ...

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 (...
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 ...

### 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 (...

### 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 ...
Accepted

Accepted

### 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 ...

### 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$ ...
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 ...