21,040 reputation
25891
bio website math.cas.cz/~jerabek
location Prague
age 38
visits member for 4 years, 5 months
seen 3 hours ago

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.