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.
36
votes
3
answers
2k
views
Internal logic of the topos of simplicial sets
I am looking for a closed statement (i.e. not depending on any parameter objects) which is true in the internal logic of the topos of simplicial sets, but is not an intuitionistic tautology. Ideally, …
32
votes
1
answer
2k
views
Can ZFC → NBG be iterated?
von Neumann-Bernays-Gödel set theory (NBG) is a conservative extension of ZFC which contains "classes" (such as the class of all sets) as basic objects. "Conservative" means that anything provable in …
30
votes
6
answers
3k
views
Mathematics without the principle of unique choice
The principle of unique choice (PUC), also called the principle of function comprehension, says that if $R$ is a relation between two sets $A,B$, and for every $x\in A$ there exists a unique $y\in B$ …
24
votes
1
answer
3k
views
When does collection imply replacement?
In ordinary membership-based set theory, the axiom schema of replacement states that if $\phi$ is a first-order formula, and $A$ is a set such that for any $x\in A$ there exists a unique $y$ such that …
21
votes
3
answers
3k
views
Approximate intermediate value theorem in pure constructive mathematics
The ordinary intermediate value theorem (IVT) is not provable in constructive mathematics. To show this, one can construct a Brouwerian "weak counterexample" and also promote it to a precise counterm …
18
votes
1
answer
1k
views
Can Vopenka's principle be violated definably?
One form of Vopenka's principle (a large cardinal axiom) states that no locally presentable category contains a full subcategory which is large (= a proper class) and discrete (= contains no nonidenti …
16
votes
2
answers
839
views
Cauchy real numbers with and without modulus
In constructive mathematics there are many possible inequivalent definitions of real numbers. The greatest variety seems to be in Dedekind-style approaches: in addition to "the" Dedekind real numbers …
15
votes
3
answers
1k
views
A rigid type of structure that can be put on every set?
Call a type of structure rigid if any automorphism of such a structure is an identity. (This is a bit different from some other uses of the word, but hopefully I'll be forgiven.) For example, well-o …
14
votes
1
answer
603
views
Ordinal realizability vs the constructible universe
Koepke's paper Turing Computations on Ordinals defines a notion of "ordinal computability" using Turing machines with a tape the length of Ord and that can run for Ord-many steps, and shows that a set …
13
votes
3
answers
2k
views
Intuitionistic Lowenheim-Skolem?
Is there a version of the Löwenheim-Skolem theorem in intuitionistic logic? I'm particularly interested in the "downward" form. The standard proof I know uses the Tarski-Vaught test for elementary s …
12
votes
1
answer
780
views
Is Girard's LU just an embedding of classical and intuitionistic logic into linear logic?
This question is about Girard's system LU, presented in his paper On the unity of logic. Girard starts by giving a "modal" sequent calculus with two zones of both hypotheses and consequents, $\Gamma; …
12
votes
4
answers
823
views
A well-founded relation on lists
Let $A$ be a set equipped with a well-founded relation $<$, let $LA$ be the set of finite lists of elements of $A$, and define a relation $\prec$ on $LA$ such that $\ell \prec m$ if $\ell$ is obtained …
10
votes
3
answers
1k
views
Is set-induction relatively consistent?
One way to state the axiom of foundation is that the $\in$ relation on any transitive set is well-founded in the following sense:
A relation $(X,\prec)$ is well-founded if for any subset $S\subseteq …
9
votes
1
answer
832
views
Axiom of class collection
One version of the Axiom of Collection says that any surjection $A\to B$ from a class $A$ to a set $B$ is factored through by some surjection $C\to B$ where $C$ is a set.
Note that assuming $B$ is a …
9
votes
1
answer
979
views
constructive Serre classes
A Serre class (of abelian groups) is a class of abelian groups closed under subgroups, quotients, and extensions. For instance, finitely generated groups and finite groups are both Serre classes.
Ho …