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.
2
votes
Finitistic interpretation of Nelson's internal set theory
Building on work by Benno van den Berg et al, the quantifiers $(\forall^{st}x)$ and $(\exists^{st}x)$ can be interpreted as "for all computationally relevant objects $x$" and "there exists a computati …
10
votes
Uniqueness results that follow from CH
Assuming $\textsf{CH}$, a lot of natural fourth-order functionals are computationally equivalent (Kleene's S1-S9) to $\exists^3$. These equivalences do not seem to go through without the former. ([ …
4
votes
Negating fundamental axioms
At the very bottom of logical strength, there is the following example.
Julian Hook's PhD thesis with title A Many-Sorted Approach to Predicative Mathematics, written under the supervision of Ed Nelso …
4
votes
Why does Weihrauch reducibility make use of multi-functions?
In a nutshell, the reason one uses 'multi-functions', i.e. mappings that do not satisfy the axiom of function extensionality, is that otherwise things would be fairly trivial, as shown essentially by …
4
votes
A conservative extension of Peano Arithmetic
I believe Feferman's theory S (under a different name) is used here by Feferman to formalise mathematics in a predicative setting.
Erik Palmgren used to have a list on his webpage with papers on (cons …
9
votes
Church–Turing thesis for higher order functions
Dag Normann (and myself) have written in many places that:
there is no Church-Turing thesis for computability of (even just) type 2 objects.
As noted here by others, John Longley has explored this the …
6
votes
Trading Choice for Comprehension (or Replacement)
Most of the examples I know can be found in [1,2] and are joint work with Dag Normann. The prettiest examples we have are perhaps the following:
Let RCA$_0^\omega$ be Kohlenbach's base theory of RM a …
8
votes
Lists as a foundation of mathematics
The original question was:
Can we use lists as the primary notion and build mathematics around it?
My answer is that any such approach runs into trouble very quickly, as can be gleaned from the follow …
2
votes
Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?
Against my better judgement, I would answer your question in the negative.
My motivation is that even rather strong classical theories cannot prove that
"there is no injection from Cantor space (or: t …
8
votes
How much of mathematical General Relativity depends on the Axiom of Choice?
My (attempt at an) answer goes in the direction of "2. natural restrictions".
First of all, as noted in the comments, provable in ZF are restrictions of AC to the language of second-order arithmetic. …
10
votes
Set-theoretical reverse mathematics of the reals
TL;DR: A most basic property of $\mathbb{R}$ is that it is not countable, which is surprisingly hard to prove (namely far beyond the Big Five you
mention), as explored in [1, 2, 3].
The longer version …
3
votes
Axiomatic system made just for playing
I guess you should take a look at the work of John Conway. In particular, his game of life seems to be exactly what you are looking for, a pioneering part of recreational mathematics.
9
votes
Simpler proofs using the axiom of choice
Many examples from set theory are known, but here is a very basic (third-order) theorem from most ordinary mathematics:
"A regulated$f:[0,1]\rightarrow \mathbb{R}$ is bounded", (&)
where 'regulated' m …
7
votes
Does anyone still seriously doubt the consistency of $ZFC$?
Some more detail about Nelson's work:
For most of his life, Ed Nelson tried to show that Peano Arithmetic (and weaker systems) was somehow inconsistent.
This was (initially) based on the idea that one …
4
votes
Accepted
"At most one" versus "at most finitely many"
The answer is positive, assuming extra induction, and a sketch is as follows.
Let $\varphi(X,n)$ be as in (*).
Define an analytic code $A_n$ as follows $X\in A_n\leftrightarrow \varphi(X, n)$.
Use i …