Reputation
4,425
Next privilege 5,000 Rep.
Approve tag wiki edits
Badges
1 18 41
Newest
 Good Answer
Impact
~79k people reached

18h
comment a naive question: is the category of moniods cartesian closed? Why?
Aside from the duplicate, this question should be on math.stackexchange.com — it’s a good question, but it’s certainly not research level, it’s a good exercise for a first course on category theory.
1d
comment Widely accepted mathematical results that were later shown wrong?
@FernandoMuro: The issue (as extensively explored in Lakatos’s book) is that this formula was known “for all polyhedra” before a precise (by modern standards) definition of polyhedron had been established. So the “obvious counterexamples” were not seen as counterexamples, because they obviously weren’t polyhedra. However, when people did start exploring definitions for polyhedron, then (for some of those) this expected result became false.
Feb
4
comment Constructive compactness for countable models?
On the other hand, while constructive model theory casts its net much wider than classical model theory (including Kripke models and much more), it certainly includes ordinary “Tarski” models as a special case of these. So there is no problem with speaking of “compactness for (countable) (Tarski) models”. The reason Tarski models are less-studied constructively isn’t because they’re problematic, it’s just that there may not exist enough of them for completeness, so one is forced (no pun intended) to look at more general kinds of models.
Feb
4
comment Constructive compactness for countable models?
I don’t know the answer, I’m afraid; but unlike other commenters, I think this is a good and well-posed question. Formal constructive reverse mathematics has been investigated by e.g. Ishihara, Nemoto, and colleagues, who have certainly considered what intuitionistic formal systems are required for equivalences between WKL, LLPO, and related principles; I have heard several conference talks by them on such issues, though I don’t remember their results precisely. (cont’d)
Feb
3
comment Ref request: modelling regular theories as an injectivity condition
@ZhenLin: ah, thankyou! Henrik Forssell also pointed out to me that the same converse appears in the Adamek/Rosicky book, in the hint to Exercise 5.e. These would be close enough to serve as a reference if there’s nothing closer, but it would be nice to have this version itself if it’s been set down somewhere.
Feb
3
revised Ref request: modelling regular theories as an injectivity condition
added further info in question
Feb
3
asked Ref request: modelling regular theories as an injectivity condition
Feb
2
comment Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?
It would be nice to find an early reference! The best I can find is Hofmann’s PhD thesis Extensional concepts in intensional type theory, which doesn’t state it explicitly anywhere (at least, not that I see on a quick skim), but uses it in the definition of the stripping map on p.91. (There he simply gives the proof term Refl(Refl(m)) for it; the unhelpfulness of this is a possibly-deliberate illustration of the undecidability of ETT.) I guess it goes back further, at least to Streicher’s Habilitationthesis, but my copy of that isn’t searchable, and on a quick skim, I’m coming up empty.
Feb
2
comment Minimal CNF expression
“Brute force” is the obvious answer, since the set of formulas with length less than a given bound is finite and easy to enumerate. Presumably you don’t just want that, so can you say what further criteria you are hoping for in the algorithm, and more background on what you already know or have considered?
Jan
31
comment A book explaining power and limitations of Peano Axioms?
“One can define some specific coding of finite sequences of numbers and use that, but this is so ugly and so specific to aritmetics” Really? This seems to me like the fact that using the binary logic of transistors, one can encode arbitrary computation, not to mention text and cat videos. Any specific encoding will be ad hoc and a little ugly — but the fact one can do it is fundamental and beautiful!
Jan
30
comment Reference request: Models of isomorphic languages result into isomorphic categories
Not time for a full answer now, but a few pointers. Firstly, the specific result I’d look for is the fact that the category of models is functorial in the signature, i.e. any map of signatures $f : \rho \to \sigma$ induces a functor $f^* : \textbf{Str}(\sigma) \to \textbf{Str}(\rho)$, and this action makes $\mathbf{Str}(-)$ a functor from signatures to categories. The isomorphism result then follows immediately. Secondly, two good books to check are Johnstone’s Elephant, and Makkai and Reyes’ First-order Categorical Logic.
Jan
27
accepted Reference request: eliminating function symbols in predicate logic
Jan
27
answered How can any theory prove well-foundedness of ordinals above $\omega_1^{\text{CK}}$?
Jan
27
asked Reference request: eliminating function symbols in predicate logic
Jan
27
comment Is there an example of integers ($x,p, q ,y$ ) which satisfies the below conditions in this claim?
This question is a bit unclear. The claim is formulated as though it were a universal statement, or at least an implication: “Let p,q,x be such that (1),(2),(3); then gcd(x,y) = 1.” But then you ask for an example of such integers. Do you mean a counterexample to the implication? Or an example with (1),(2),(3) and with gcd(y,x) = 1? This needs to be clarified, or the question is unanswerable.
Jan
24
comment Not especially famous, long-open problems which anyone can understand
“Closed formula” is a bit of a slippery goal — there are specific definitions, but they are mostly somewhat ad hoc. A more mathematically natural goal along similar lines might be to find a polynomial-time algorithm (or some other reasonable sense of “fast”) for computing T(n).
Jan
23
answered A well-founded relation on lists
Jan
17
awarded  Good Answer
Jan
14
comment Pronunciation of ¡ (inverted exclamation mark, historically used for subfactorial)
@Lubin: either as a main actor, as in $¡_X$, or as a prefix, $¡X$.
Jan
13
asked Pronunciation of ¡ (inverted exclamation mark, historically used for subfactorial)