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.
34
votes
3
answers
3k
views
What is the theory of local rings and local ring homomorphisms?
It is well-known that the category of local rings and ring homomorphisms admits an axiomatisation in coherent logic. Explicitly, it is the coherent theory over the signature $0, 1, -, +, \times$ with …
- 15.9k
23
votes
1
answer
962
views
Are there axioms satisfied in commutative rings and distributive lattices but not satisfied ...
Consider the language of rigs (also called semirings): it has constants $0$ and $1$ and binary operations $+$ and $\times$. The theory of commutative rigs is generated by the usual axioms: $+$ is asso …
- 15.9k
17
votes
Major applications of the internal language of toposes
I don't know if this counts as an application of the internal language or as an avoidance of it, but I think it is worth listing anyway.
In the development of homological algebra and homotopy theory i …
16
votes
2
answers
674
views
How to formulate the univalence axiom without universes?
The standard formulation of the univalence axiom for a universe type $U$ is that, for all $X : U$ and $Y : U$, the canonical map $(X =_U Y) \to (X \simeq Y)$ is an equivalence.
As we (usually) cannot …
- 15.9k
14
votes
1
answer
1k
views
Is it possible for a theorem to be constructive only in a non-constructive metatheory?
There are several theorems in category-theoretic logic which say something like, "any proposition in X logic that is provable in topos logic assuming (the law of excluded middle and) the axiom of choi …
- 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
11
votes
1
answer
414
views
Examples of natural algebraic irreflexive relations
To motivate the question, consider the theory of rings.
Define $x \parallel y$ to mean $\exists w \exists z .((x - y) z = w (x - y) = 1)$, or in words, "$x - y$ is a unit".
Then $\parallel$ is a binar …
- 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
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
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
8
votes
Accepted
Posets (partially ordered sets) in equational logic
No. The category of models of an equational theory (i.e. a variety in the sense of universal algebra) is always a regular category, but the category of posets is not regular.
- 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
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
7
votes
0
answers
130
views
Finitely presented algebras with isomorphic semilattices of congruences
Let $\mathbb{T}$ be a finitary algebraic theory. For each $\mathbb{T}$-algebra $A$, let $Q (A)$ be the join semilattice of finitely generated congruences on $A$. There is an evident pushforward opera …
- 15.9k