19,170 reputation
25384
bio website math.cas.cz/~jerabek
location Prague
age 37
visits member for 3 years, 10 months
seen 1 hour 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).


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 Henkin-style 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 one-sorted first-order theories still has a different meaning than the kind of skolemization you consider in the higher-order (multi-sorted first-order) 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 first-order 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 first-order 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 first-order 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
@Christoph-SimonSenjak: 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 research-level 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