Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

If one were to verify that

$$ \sqrt{2} < 3 $$

would the underlying formalisation require a logic more expressive than first-order? Or, is FOL sufficient since real numbers can be formalised in set theory?

How about evaluating differentials, like

$$ \frac{d}{dy} (3x+2) $$

what how expressive does the logic need to be?


share|cite|improve this question

Comparing particular algebraic numbers (localized away from their Galois conjugates by inequalities, such as the positive root of $X^2=2$) can be done in any theory that supports arithmetic calculation. For example, the first-order theory of real-closed fields is decidable and that includes decisions about statements of the form $a > b$ comparing two real algebraic numbers.

Model theory of differential (and difference) fields and rings usually takes place in a first-order logic context similar to fields. Theorems are proved by second-order methods but the object of study is a first-order theory.

share|cite|improve this answer
I see. Why are theorems proved by second-order methods? Can you name some example objects of study that are second or higher order theories? – Kar Sep 7 '11 at 0:31

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.