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 | |
Results tagged with lo.logic
Search options questions only
not deleted
user 49
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.
6
votes
0
answers
147
views
Linear logic with storage preserving positives
Has anyone studied a version of linear logic in which the storage modality $!$ preserves the positive connectives and quantifiers $\otimes,\oplus,\exists$? That is, such that we have $!(A\otimes B) = …
- 66.8k
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; …
- 66.8k
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 …
- 66.8k
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 …
- 66.8k
8
votes
1
answer
331
views
Distributivity of ! over?
Has anyone studied a variant of linear logic, or of its semantic counterpart (exponential modalities on linearly distributive categories / $\ast$-autonomous categories / polycategories) for which ther …
- 66.8k
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 …
- 66.8k
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 …
- 66.8k
7
votes
3
answers
784
views
Can a typing judgment admit essentially different derivations?
In any sort of type theory, there are a bunch of rules for constructing derivations of typing judgments such as $x:A,\; y:B(x) \;\vdash\; z:C(x,y)$. (I intend to include also judgments of the form $B …
- 66.8k
7
votes
2
answers
1k
views
Recursively dependent types?
Is there such a thing as "recursively dependent types"? Specifically, I would like a dependent type theory containing a type $A(x)$ which depends on a variable $x: A(z)$, where $z$ is a particular co …
- 66.8k
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 …
- 66.8k
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 …
- 66.8k
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$ …
- 66.8k
7
votes
2
answers
957
views
Can models of set theory contain extra ordinals?
In the paper "Complete topoi representing models of set theory" by Blass and Scedrov, they consider a general notion of Boolean-valued model of set theory, and one of the conditions they impose is tha …
- 66.8k
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 …
- 66.8k
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 …
- 66.8k