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 not deleted
user 11640
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.
9
votes
Provable(P) ⇒ provable(provable(P))?
(This is really just a comment, but apparently I don't have enough reputation to leave comments yet.)
I think there's some room for more care in the notation. $\Box \phi \implies \Box \Box \phi$ loo …
- 15.9k
6
votes
Accepted
Categories of logical formulae
Classical propositional logic is basically a boolean algebra, which may be viewed as a poset, which may be viewed as a category. We at the very least need to fix the primitive predicates; then the obj …
- 15.9k
4
votes
About logical axioms of propositional logic.
Which propositional logic are you asking about? Axioms K (your axiom 1) and S (your axiom 2) are admissible for the implicational fragment of intuitionistic propositional logic, but your axiom 3 is no …
- 15.9k
3
votes
What are some interesting hyperdoctrines that are not classical models?
Every hyperdoctrine is "syntactic", in the sense that given any hyperdoctrine you can construct a theory whose syntactic hyperdoctrine is equivalent to the one you start with.
Thus, hyperdoctrines cor …
- 15.9k
7
votes
1
answer
412
views
Non-definable elements vs indiscernible elements
Let $\Sigma$ be a one-sorted first-order signature, let $A$ be a $\Sigma$-structure, and let $B \subseteq A$ be a $\Sigma$-substructure. Fix a class $\mathcal{L}$ of formulae over $\Sigma$. We say an …
- 15.9k
8
votes
Accepted
Multiplicative group of a ring as a morphism of theories
The functor sending a (not necessarily commutative) ring to its group of units is induced by a morphism of cartesian (= finite limit) theories.
More generally, suppose given (small!) cartesian theorie …
- 15.9k
5
votes
Set-Theoretic Issues/Categories
Since you don't seem to want to leave ZFC, here's a taste of the issues you might face if you try to work with a stratified universe. (Here I mean the ordinary English word ‘stratified’, rather than a …
- 15.9k
2
votes
0
answers
146
views
Are partial elements necessary in boolean-valued models?
It seems to me that there is a difference in the treatment of "partial" elements in boolean-valued models in set theory vs topos theory: in set theory, one usually only considers "global" elements of …
- 15.9k
6
votes
Barr's theorem and constructivity?
In every Grothendieck topos, the following sequent is valid for the natural numbers object $N$,
$$x : N \vdash \bigvee_{n : \mathbb{N}} x = s^n (z)$$
where $\mathbb{N}$ is the set of natural numbers, …
- 15.9k
12
votes
Accepted
On the large cardinals foundations of categories
Allow me to make some comments as someone who converted to the universeful approach recently; but take it with a pinch of salt, as I have only been studying category theory for 2½ years.
I should bri …
- 15.9k
8
votes
2
answers
590
views
Categorical Brouwer-Heyting-Kolmogorov interpretation
Let $\mathcal{L}$ be the language of intuitionistic propositional logic generated by some atomic propositions $t_1, t_2, \ldots$. The Lindenbaum–Tarski algebra of $\mathcal{L}$ can be regarded as a bi …
- 15.9k
8
votes
1
answer
638
views
The independence of path induction
In §1.12 of the Homotopy type theory book, it is mentioned that indiscernibility of identicals is a consequence of path induction. More precisely, for each type $C$ dependent over a type $A$, there is …
- 15.9k
6
votes
2
answers
451
views
When are all greater cardinals sharply greater?
Makkai and Paré introduced the following binary relation on regular cardinals: given $\kappa$ and $\lambda$, $\kappa \vartriangleleft \lambda$ (read, $\kappa$ is sharply less than $\lambda$) when $\k …
- 15.9k
10
votes
Accepted
If two structures are elementarily equivalent, is there a zigzag of elementary embeddings be...
The Keisler–Shelah theorem implies that the following are equivalent:
$M$ and $N$ are elementarily equivalent.
For some set $X$ and some ultrafilter $U$ on $X$, $M^X / U$ and $N^X / U$ are isomorphi …
- 15.9k
7
votes
1
answer
333
views
What do algebraic theories with strictly terminal trivial models look like?
By algebraic theory I mean one in the sense of Lawvere, i.e. a collection of finitary operations, including projections, together with a multi-composition satisfying the obvious axioms. (I believe uni …
- 15.9k