bio  website  math.cas.cz/~jerabek 

location  Prague  
age  37  
visits  member for  3 years, 8 months 
seen  1 hour ago  
stats  profile views  6,085 
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).
1d

awarded  Sportsmanship 
Oct 13 
comment 
Boolean Valued Models of PA
I don't think the assertion is well defined. Definable ultrapower is a method, not just one specific construction. Anyway, the models I'm thinking about do not have full induction (but no, $I\Sigma_n$ is not a weak arithmetic in my book), however the principal reason they are not elementary is that one does not include all definable functions in the ultrapower, and I see no a priori reason this couldn't give a nonelementary model of PA. (That every countable model of PA has an elementary endextension is an almost trivial consequence of the omitting types theorem.) 
Oct 13 
comment 
Boolean Valued Models of PA
Not at all, I don't recall ever seeing a definable ultrapower in the context of weak arithmetic. Definable ultrapowers used in the study of strong fragments are nonelementary. I'm not in the office, but IIRC a typical such construction is given e.g. in Kossak and Schmerl's "The Structure of Models of Peano Arithmetic". 
Oct 13 
comment 
Generalized Hlawka inequality
See mathoverflow.net/questions/167685 , especially Bill Johnson's comments. 
Oct 11 
revised 
Another question on Borel sets and projections
fix formatting 
Oct 11 
comment 
Forcing is intuitionistic
An explicit presentation of forcing in terms of intuitionistic Kripke models is given in Melvin Fitting’s “Intuitionistic logic model theory and forcing”. 
Oct 11 
comment 
Does this construction yield the surreal numbers?
.. this for the same $(A_\beta,B_\beta)$ as long as there are any more algebraic elements in the original gap, it’s not enough to do it once. By the same token, you need to add these algebraic elements even if a transcendental element has been inserted in the gap, so Case 1 as formulated is incorrect. On the other hand, you are making the construction unnecessarily complicated. There is no point in distinguishing different kinds of Dedekind cuts. If you formulate (the fixed versions of) cases 2 and 3 for all cuts, the initial step of taking $F_\alpha^*$, and the $X_\infty$ step, are redundant. 
Oct 11 
comment 
Does this construction yield the surreal numbers?
In case 2, there may be more than one such polynomial (iow, more than one element of the real closure may fall into the gap). You need to take a polynomial $p$ of minimal degree that changes sign across the gap (which implies its irreducibility). Then there is a welldefined order on the extension of $F_{\alpha,\beta}$ by a root $X$ of $p$: if $f$ is a polynomial of degree less than the degree of $p$, we can put $f(X)>0$ iff $f$ is positive across the gap. There still may be more than one such minimaldegree polynomial, as shown in David Speyer’s example, hence you need to keep repeating ... 
Oct 9 
awarded  Nice Answer 
Oct 8 
comment 
Computing basis of a lower set given basis of complementary upper set
The problem is equivalent to conversion of a monotone DNF to a monotone CNF. Since the output may be exponentially larger than the input, you cannot do better than exponential time. 
Oct 7 
comment 
Does this construction yield the surreal numbers?
The reason $\bigcup_{\alpha\in\mathrm{Ord}}F_\alpha$ yields the surreal numbers is that by construction, it is a realclosed field, and for every two subsets $X<Y$, there exists an element $X<u<Y$, which means the field is “$\mathrm{Ord}$saturated”. Such a structure is unique up to isomorphism. 
Oct 7 
comment 
Does this construction yield the surreal numbers?
Yes. Something like the following would work. Assuming global choice, fix an enumeration $V=\{A_\alpha:\alpha\in\mathrm{Ord}\}$ where each set occurs cofinally. Put $F_0=\mathbb R$ (actually $\mathbb Q$ suffices), $F_\alpha=\bigcup_{\beta<\alpha}F_\beta$ for limit $\alpha$, and for successor steps, let $F_{\alpha+1}$ be the real closure of the rational function field $F_\alpha(X)$, ordered so that $\{a\in F_\alpha:a<X\}=\{a\in F_\alpha:\exists b\in F_\alpha\,(a\le b\in A_\alpha)\}$. (This makes order completion redundant.) 
Oct 7 
comment 
Does this construction yield the surreal numbers?
Right. I got momentarily confused by the fact that the Puiseux series field has an infinitesimal variable, but this does not really make a difference: the field is in any case contained in the completion of the real closure of $F_{\lambda1}(t)=F_{\lambda1}(t^{1})$. 
Oct 7 
comment 
Does this construction yield the surreal numbers?
It is perhaps worth mentioning that if you modify the construction to also take real closure at each step, it still will not work: in terms of value groups, this makes $\Gamma_{\alpha+1}=\mathbb Q\times\Gamma_\alpha$, hence all the value groups will contain the $\mathbb Q$ from $F_1$ as a convex subgroup, untouched. What is needed is to generalize the purely transcendenttal step: one can order $F(X)$ by wedging $X$ into an arbitrary Dedekind cut in $F$ (without the “good cut” condition). 
Oct 7 
answered  Does this construction yield the surreal numbers? 
Oct 3 
comment 
What is the Shortest Axiom of Classical ConditionalNegation Propositional Calculus?
Buffalo buffalo Buffalo buffalo buffalo buffalo Buffalo buffalo? 
Oct 3 
comment 
What is the Shortest Axiom of Classical ConditionalNegation Propositional Calculus?
No, I find it much easier. There is no way I can visually count 20+ letters of line noise without making a mistake, whereas the redundant structure of the infix formula makes the task feasible. Anyway, this is quite besides the point. You are communicating with humans, and thus you should strive to use notation that is clearly readable for others. When the length of a formal expression is an issue, you need to state it in the post, not make people count it themselves. 
Oct 3 
awarded  Nice Answer 
Oct 3 
comment 
Boolean Valued Models of PA
All right, what I mainly meant by the remark about set theory was that ultrapowers appear in set theory much more often than elsewhere in logic. Definable ultrapowers are certainly not pervasive in arithmetic. Definable ultrapowers are sometimes useful in arithmetic, but as they are not elementary extensions, that actually proves my point. 
Oct 3 
awarded  peanoarithmetic 