bio  website  math.cas.cz/~jerabek 

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

comment 
When does Skolemization require the axiom of choice?
... requires a weak (actually, not so weak) form of choice, namely the Boolean prime ideal theorem. But having said that, the choice schema $(*)$ may be true in a Henkinstyle model even if the axiom of choice fails for sequences of subsets of the model, because the validity of the schema only concerns sequences of sets uniformly definable in the model by a formula. 
2d

comment 
When does Skolemization require the axiom of choice?
I’m not sure this is the right way to think about it. First, usual skolemization in onesorted firstorder theories still has a different meaning than the kind of skolemization you consider in the higherorder (multisorted firstorder) theories: the former is a metamathematical closure property of the logic (a form of an admissible rule), whereas the latter is an actual formula (or schema) in the logic. It’s also problematic to involve semantics in the issue, since just like for plain firstorder logic, the completeness and compactness of Henkin semantics (for uncountable languages) ... 
Dec 18 
revised 
When does Skolemization require the axiom of choice?
added 980 characters in body 
Dec 18 
comment 
When does Skolemization require the axiom of choice?
@Joel: Well, it’s not entirely clear to me what is the original question (as I commented on in my answer), but I’m almost certain that properties of skolemization of plain firstorder theories is not what it asks for. I merely mentioned it in the comment above to put things into context. 
Dec 18 
answered  When does Skolemization require the axiom of choice? 
Dec 18 
comment 
When does Skolemization require the axiom of choice?
Right. This is a nice example showing how the completeness theorem fails in absence of the BPIT. 
Dec 18 
comment 
When does Skolemization require the axiom of choice?
You obviously can't talk about uncountable languages directly in arithmetic, but even so, conservativity of Skolem extensions in arbitrary languages is provable without choice (for one thing, a given proof only involves a finite sublanguage). Conservativity does not imply that you can expand an arbitrary model to a model with Skolem functions, this is a stronger property. 
Dec 18 
comment 
When does Skolemization require the axiom of choice?
It might be worth stressing that the usual Skolem theorem for firstorder logic (i.e., that the skolemization of a theory is its conservative extension) does not require any choice, or even set theory for that matter (it can be formalized in a weak fragment of arithmetic). 
Dec 17 
comment 
Is evaluating limits with dual numbers sound?
As far as I can see, there is only one limit in the question, and it takes place in $\mathbb C$, not in $D$. 
Dec 16 
awarded  Nice Answer 
Dec 16 
comment 
Existential statement without witness
@ChristophSimonSenjak: Not really. Goodstein’s theorem is $\Pi^0_2$, so it does not even start with an existential quantifier. And if you substitute a number for the outer universal quantifier to obtain an existential ($\Sigma^0_1$) statement, it will have a witness provable already in Robinson’s $Q$. 
Dec 16 
comment 
Deriving $\Box p \rightarrow \Box \Box p$ if we have $\Box(\Box p \rightarrow p) \rightarrow \Box p$
... It is quite simple, but not obvious to invent from scratch. If you first do it with frames, this might suggest how the substitution should look like. 
Dec 16 
comment 
Deriving $\Box p \rightarrow \Box \Box p$ if we have $\Box(\Box p \rightarrow p) \rightarrow \Box p$
This is not a researchlevel question, so it is not appropriate here. A better fit is math.se, however, you should really try to solve the problem yourself. Some hints: showing that models of the Gödel–Löb axiom (what you call AL) are transitive is easier than actually proving the $\Box p\to\Box\Box p$ axiom. You can fix three points witnessing nontransitivity, and use them to define a valuation violating AL in a similar way as you’d show that models of $\Box p\to\Box\Box p$ are transitive. If you really want to prove $\Box p\to\Box\Box p$ from AL, you have to guess the right substitution. ... 
Dec 16 
comment 
Deriving $\Box p \rightarrow \Box \Box p$ if we have $\Box(\Box p \rightarrow p) \rightarrow \Box p$
Is this homework? 
Dec 16 
reviewed  Edit On Prüfer domains 
Dec 16 
revised 
On Prüfer domains
fix formatting 
Dec 15 
comment 
Maths to take a user chosen number to a predictable number
I am reminded of a story about one of my former professors, who was years ago reprimanded by some sort of communist party committee for working on boundary value problems, on the grounds that every scientist should strive to work on central problems. 
Dec 15 
comment 
Maths to take a user chosen number to a predictable number
Sorry about that :) 
Dec 15 
revised 
Maths to take a user chosen number to a predictable number
edited tags 
Dec 15 
awarded  Nice Answer 