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 answers 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.
5
votes
"local variables" in first-order formulas
I don't think there is any solution to the problem as you pose it. Neil and Carl have mentioned the standard approach, which is to rename bound variables, whenever you perform a substitution, to avoi …
12
votes
Is there a conjunction bias?
A slightly tongue-in-cheek answer: definitions are the hypotheses of theorems. If the hypothesis of a theorem is a disjunction, you can always split the theorem up into two theorems with separate hyp …
8
votes
Accepted
Does this "mixable" property have a standard name in constructive mathematics?
According to this proposition, the property in question is (by "a typical argument with Zorn's lemma") equivalent to flabbiness for sheaves on topological spaces. Thus, the term "flabby" is sometimes …
- 66.8k
10
votes
Accepted
Homotopy type theory: why are $0:\mathbb N$ and $\mathrm{succ}(0):\mathbb N$ not judgemental...
Daniel's answer is correct that the judgmental distinctness of $0$ and $\mathsf{succ}(m)$ is not what justifies a definition by pattern-matching. However, it is still a meaningful question of how to …
- 66.8k
4
votes
Accepted
Can a type in a lower universe be formed from types in higher universes?
I expect you're right that if the only primitive rules for universes are "closure" ones such as
$$\frac{\vdash A:U_i \qquad x:A \vdash B[x] : U_i}{\vdash \prod(x:A). B[x] : U_i}$$
then there should …
- 66.8k
15
votes
Accepted
Category theorists stance on deductive systems
This sentence reads to me like "we will treat Xs as if they were special kinds of of Ys, which will make both X-theorists and Y-theorists unhappy because it is not true". Reminds me of the old joke w …
- 66.8k
14
votes
Does "compact iff projections are closed" require some form of choice?
As a statement about locales, or even toposes, the equivalence is true without any choice and even without excluded middle. A clever construction of an appopriate locale Y can be found in the proof o …
- 66.8k
5
votes
Accepted
What are some interesting hyperdoctrines that are not classical models?
Maybe I am wrong, but it seems to me that the other answers are misunderstanding the question. The emphasis on syntactic hyperdoctrines seems to me beside the point.
A (classical, first-order) hyperd …
- 66.8k
5
votes
Question about higher inductive types and computational rules
If I understand the question correctly, one answer is that the rules of type theory are not (supposed to be) arbitrarily chosen independently of each other like the axioms of set theory are. They com …
- 66.8k
1
vote
Question about higher inductive types and computational rules
A different answer is that one of the purposes of higher inductive types is to define homotopy types containing nontrivial paths. The judgmental equalities coming from computation rules cannot give r …
- 66.8k
5
votes
Conditions for a functor to induce a logical functor between presheaf toposes?
Not really an answer, but maybe a hint as to where to look for one: since $F^\ast$ is the left adjoint part of a geometric morphism $F^\ast \dashv \mathrm{Ran}_F$, it is logical precisely when this ge …
- 66.8k
1
vote
Is set-induction relatively consistent?
I think there shouldn't be a problem showing that the "strongly well-founded" or "class-well-founded" sets satisfy most of the basic axioms of set theory that involve only $\Delta_0$-quantifiers, e.g. …
- 66.8k
3
votes
"classes" with no cardinality; "classes" with no equality notion
Peter's answer is very good, I just wanted to add a little bit. Namely, in addition to "classical" axiomatic set theories such as ZFC and NBG, and type theories such as CoC and MLTT, there is a third …
- 66.8k
5
votes
How different category theories relate
You might be interested in this paper (although it is in need of revising).
- 66.8k
24
votes
What is so special about set theory anyway?
It's not clear to me whether your question is more about the role of sets versus other foundational objects, or about how set theory can be extended with large cardinal axioms to discuss models of str …
- 66.8k