Search Results
Search type | Search syntax |
---|---|
Tags | [tag] |
Exact | "words here" |
Author |
user:1234 user:me (yours) |
Score |
score:3 (3+) score:0 (none) |
Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
Views | views:250 |
Code | code:"if (foo != bar)" |
Sections |
title:apples body:"apples oranges" |
URL | url:"*.example.com" |
Saves | in:saves |
Status |
closed:yes duplicate:no migrated:no wiki:no |
Types |
is:question is:answer |
Exclude |
-[tag] -apples |
For more details on advanced search visit our help page |
first-order and higher-order logic, model theory, set theory, proof theory, computability theory, formal languages, definability, interplay of syntax and semantics, constructive logic, intuitionism, philosophical logic, modal logic, completeness, Gödel incompleteness, decidability, undecidability, theories of truth, truth revision, consistency.
9
votes
Which ordinals can be proof-theoretic ordinals of a reasonable theory?
Regarding the small Veblen ordinal, Rathjen and Weiermann gave an analysis of theories in that range of strength in Proof-theoretic investigations of Kruskal's theorem.1 Working over a reasonable bas …
6
votes
2
answers
476
views
Reconstructing a model from its definable sets
Let $\mathcal{M}$ be an infinite model of a first-order language, and for each $n$, let $\mathcal{B}_n$ be the algebra of definable sets of $n$-tuples from $|\mathcal{M}|$.
Given $\{\mathcal{B}_n\mi …
4
votes
Ultraproduct of Dividing Lines
I'm going to assume we're talking about $\omega$-incomplete ultrafilters.
Others have pointed out that none of the major dividing lines are elementary; that is, these properties are not equivalent to …
11
votes
Accepted
Correspondence between proof-theoretic ordinals and fast growing functions?
Yes: for many theories, $\alpha$ is the proof-theoretic ordinal of T exactly when T proves that $f_\beta$ is total for all $\beta<\alpha$, but does not prove $f_\alpha$ is total. (Where $f_\alpha$ is …
9
votes
Accepted
Reasoning Using Countable Subsets of Real Numbers
Suppose that during some argument (involving ℕ) one switches to real numbers and then back to discrete domain (before completing the argument). My question is, can one give examples where a switch …
9
votes
Accepted
Notable examples of syntactic proofs whose existence is guaranteed by completeness, but havi...
There's a good reason that concrete examples are going to be rare. Existence of a first-order proof (at least in a countable language) is a $\Sigma_1$ property in the language of arithmetic, and it's …
7
votes
Accepted
$f_{\epsilon_0}$ and provably total functions in $PA$
I think usually one adds the condition that $\phi$ be a $\Delta_1$ (i.e. computable) formula.
As Gro-Tsen has pointed out, the answer is no: there are lots of functions which are provably total, domi …
2
votes
Accepted
Elementary functions in a formalized PA
I think your first and last questions more or less answer each other: the elementary functions can be defined using quantifiers, so adding them as symbols makes the quantifier-free formulas more expre …
8
votes
How to construct a constructive proof from a non-constructive proof using prime ideals?
Exactly what kind of answer you get depends on the kind of proof you start with and what exactly you mean by constructive. But the proof mining approach offers an answer to some questions of this kin …
6
votes
Accepted
A derivation in Tait calculus
There's no rule that lets you get from a deduction of $\Gamma$ to a deduction of $\Gamma,\Delta$. However it's an easy lemma that, given a deduction of $\Gamma$, there is also a deduction of $\Gamma, …
3
votes
Can the omega-rule rescue Hilbert's program?
$PA+\omega$-rule certainly proves $Con(PA)$. If $Con(PA)$ is false, PA proves everything. If $Con(PA)$ is true, this is a $\Pi^0_1$-statement, and $PA+\omega$-rule proves every true $\Pi^0_1$-statem …
6
votes
What are the advantages of the more abstract approaches to nonstandard analysis?
For most purposes, I think the premise is wrong: in many situations ultraproducts simply are the preferable approach, so I'll try to discuss some of the purposes which are exceptions. @cody has alrea …
38
votes
Accepted
How undecidable is the spectral gap?
I haven't read the paper carefully, but this appears to be a standard undecidability result, of the sort of which there are dozens if not hundreds in the literature, of the same ilk as the undecidabil …
13
votes
Why is there a need for ordinal analysis?
In addition to the reasons Andreas gives, Gentzen's theorem gives additional information that's interesting even if you don't have any qualms about consistency.
In particular, ordinal analysis gives …
7
votes
Accepted
What are key $\Sigma^0_2$ or $\Pi^0_3$ theorems?
I'm not clear whether you're asking if there are any interesting non-$\Pi_2$ theorems in the literature, or any proofs of $\Pi_2$ theorems with interesting non-$\Pi_2$ intermediate steps which cannot …