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.
7
votes
Can tests for the convergence and divergence of series be used to create undecidable sentences?
Let $\phi(n)$ be any bounded formula in the language of arithmetic. The sequence of rational numbers $$a_m = \begin{cases} 1/m & \text{if $\exists n \lt m\,\phi(n)$} \\ 1/2^m & \text{if $\forall n \lt …
7
votes
Accepted
A couple of questions about Turing machines that are bounded in space but have an infinite a...
An SBTM has only finitely many possible combinations of internal state and tape configuration. Moreover, the next internal state and tape configuration is completely determined by the current internal …
18
votes
Unprovable statements S where the only way to prove S is to assume S
Here is a classical example of a theory that has minimal unprovable statements. Let $T$ be the theory of (nontrivial) dense linear orders:
$$\exists x \exists y (x \lt y), \qquad \forall x (x \not\lt …
2
votes
Accepted
logics restricted in arithmetic hierarchy
$\Pi_2$ statements can be modeled in the form of a "question and answer." Specifically, the statement $(\forall a \in A)(\exists b \in B)\phi(a,b)$ can be thought of as follows: $A$ is a set of questi …
2
votes
"local variables" in first-order formulas
Yet another approach is to have distinct sets of symbols for free variables and bound variables. This is the approach used by Takeuti in Proof Theory, but it probably originates from earlier than that …
7
votes
Accepted
Extension of the Peano Axioms?
There is no hope for a first-order theory to eliminate non-standard models. If a first-order theory over a countable language has an infinite model then it has models of all infinite cardinalities (Lö …
18
votes
Independence of being an integer
Here is a conditional answer. It was shown by Macintyre and Wilkie that if (a weak variant of) Schanuel's Conjecture is true, then the first-order theory of the real exponential field $(\mathbb{R};0,1 …
4
votes
Accepted
Ultimate limits of Tennenbaum's Theorem
This is equivalent to saying that $T$ is complete. Let $M$ be a recursively presentable model of $T$. If $T$ is not complete, then we can find $\phi$ which is not provable from $T$ but is true in $M$. …
11
votes
A Model where Dedekind Reals and Cauchy Reals are Different
Coincidentally, I am preparing to talk about some of this tomorrow. Here is some of what I will say about this. A good way to think about Dedekind vs Cauchy reals is to think about what kind of inform …
12
votes
Accepted
candidate for rigorous _mathematical_ definition of "canonical"?
Although the Bourbaki formulation of set theory is very seldom used in foundations, the existence of a definable Hilbert $\varepsilon$ operator has been well studied by set theorists but under a diffe …
12
votes
Accepted
Robinson Arithmetic and Composite Numbers
The nonnegative part of a discrete ordered ring always satisfies Robinson Arithmetic, so many examples can be found there. For a specific one, take the ring $R$ of formal Puiseux polynominals of the f …
36
votes
Accepted
Propositional Logic, First-Order Logic, and Higher-Order Logics
This is a long list of questions! These are all related to a certain extent, but you might consider breaking it up into separate questions next time.
Proof theorists tend to prefer systems with many …
4
votes
Which Heyting algbras arise out of some elementary topos which satisfies the ultrafilter pri...
Yes, plenty! But this is subtle since it's hard to define what an ultrafilter is in constructive settings.
An ultrafilter $\mathcal{U}$ on $\mathbb{N}$, in the classical sense, easily allows the Limi …
4
votes
Accepted
A Question related to the Formula Hierarchy
There is an additional twist in the case where $\alpha$ is $\Sigma^0_1$. Assuming $\mathsf{WKL}_0$ (Weak König Lemma), $\forall Y\alpha(X,Y,n)$ is equivalent to a $\Sigma^0_1$ statement and hence so a …
7
votes
Natural examples of Reverse Mathematics outside classical analysis?
This is mostly a comment on the proposed example of Pappian planes.
One of the aspects of the Reverse Mathematics methodology is to analyze results in their natural setting, which is then distilled t …