bio | website | math.cas.cz/~jerabek |
---|---|---|
location | Prague | |
age | 38 | |
visits | member for | 4 years, 5 months |
seen | 3 hours ago | |
stats | profile views | 7,084 |
I am a researcher at the Institute of Mathematics of the Czech Academy of Sciences. I work in the field of mathematical logic, specifically proof complexity (mainly subsystems of bounded arithmetic, but also propositional proof complexity) and nonclassical logics (admissible rules of modal, superintuitionistic, and other propositional logics).
Jul 17 |
comment |
A question on integers relatively prime to their Euler totien function
@JeremyRouse: I read the condition as “$Y$ be a subset of $X$ containing all prime numbers, and possibly some other numbers”. |
Jul 14 |
comment |
Lattices without prime ideals
Ah, sorry: they are meet-irreducible, but not prime. However, they are most definitely proper ideals, so they need to be dealt with in the answer in one way or another. |
Jul 14 |
comment |
Lattices without prime ideals
The principal ideals generated by any $\alpha\in\kappa$ are all prime. |
Jul 14 |
comment |
Propositional logic without negation
Your implications are a notational variant for monotone sequents, so you might want to look into the monotone sequent calculus. |
Jul 13 |
comment |
Canonical representation of binary decision trees in Ptime?
Cross-posted from cstheory.stackexchange.com/q/31918 , where it already got a conditional negative answer. |
Jul 10 |
comment |
Nice model theoretic properties of a theory after adding predicates
What do you mean by a "suitable interpretation" of $P$? For any theory $T$, there are predicates that preserve all properties of the theory (e.g., the empty predicate), and there are predicates that destroy all nice properties (e.g., an elementhood predicate satisfying ZFC). (And, of course, for most niceness properties except elimination of imaginaries and the like, adding a predicate can never make the theory nicer than it already was.) |
Jul 7 |
revised |
Why is there a $\sqrt{5}$ in Hurwitz's Theorem?
fix spelling of a name |
Jul 1 |
comment |
Ordinals separate from set theory
The first-order theory of ordinals is studied in depth in the Doner, Mostowski, Tarski paper referenced in mathoverflow.net/a/35982 . |
Jun 29 |
comment |
Necessary and sufficient condition for order relations which are realizable as subsets of real numbers
mathoverflow.net/q/199859 |
Jun 29 |
comment |
Cauchy completeness of the real closure
Right. Using these two operators, we can construct from any ordered field $k$ the four fields $\mathcal R(k)$, $\tilde k$, $\mathcal R(\tilde k)$, and $\widetilde{\mathcal R(k)}=\widetilde{\mathcal R(\tilde k)}=\mathcal R(\widetilde{\mathcal R(k)})$. There are natural embeddings $k\to\tilde k\to\mathcal R(\tilde k)$, $k\to\mathcal R(k)\to\mathcal R(\tilde k)$, and $\mathcal R(\tilde k)\to\widetilde{\mathcal R(k)}$, but in general all these may be strict extensions, and there are no other embeddings. |
Jun 28 |
revised |
Cauchy completeness of the real closure
addendum |
Jun 28 |
revised |
Cauchy completeness of the real closure
On second thoughts, I’m not sure finite extensions preserve completeness if the value group is not Z. Also include a few links to disambiguate the terminology. |
Jun 28 |
answered | Cauchy completeness of the real closure |
Jun 21 |
comment |
Lascar strong types in fragments of arithmetic
@tomasz: The point is that full induction implies the existence of definable Skolem functions, in which case $M$ can be fixed as the Skolem hull/definable closure of $A$. |
Jun 20 |
comment |
What lets the Square of Opposition fail in Intuitionistic Logic?
Bell additionally assumes $\forall x\,(x=a\lor x\ne a)$, which you omitted. For all I know, his paper is correct. The model looks as follows. The underlying Kripke frame is a tree with a root and two leaves. The first-order domains in all three worlds are $\{a,b,c,d\}$; one leaf satisfies $a=c$ and $b=d$, and the other leaf satisfies $a=d$ and $b=c$. One leaf satisfies $p$. After unwinding the definitions, the validity of (Q) in the model boils down to the property that each equivalence class in one leaf intersects each equivalence class in the other leaf. |
Jun 20 |
comment |
What lets the Square of Opposition fail in Intuitionistic Logic?
It’s actually not derivable from (Q) (there is a simple finite counter-model), but that’s besides the point, as $\neg(a=b)$ is not a propositional formula. I didn’t mention equality in the translation, but it is supposed to translate to $\top$ (which should be obvious from the semantic interpretation of the translation). See also begthequestion.info . |
Jun 18 |
comment |
What lets the Square of Opposition fail in Intuitionistic Logic?
Because, as I already wrote below, the resulting system is conservative over intuitionistic propositional logic: deleting all quantifiers and variables from a proof and turning all predicates into propositional variables results in a valid propositional proof, and specifically, translates (Q) to a tautology $\neg\phi'\to\neg\phi'$. (In other words, (Q) holds in Kripke models with 1-element object domains.) |
Jun 18 |
comment |
What lets the Square of Opposition fail in Intuitionistic Logic?
Though your argument does not actually use higher-order logic: it only needs closure under quantifier relativization. |
Jun 18 |
comment |
What lets the Square of Opposition fail in Intuitionistic Logic?
This is interesting. However, what I actually wanted to point out was the opposite: if we adjoin (Q) as a schema to ordinary first-order intuitionistic logic, it does not prove the law of excluded middle, and in fact it’s a conservative extension of intuitionistic propositional logic (as can be seen by striking out all quantifiers). |
Jun 18 |
comment |
What lets the Square of Opposition fail in Intuitionistic Logic?
What kind of logics? Obviously, you can just take intuitionistic logic with (Q) as an extra axiom. |