2
$\begingroup$

What is the name of the following property of a system $T$?

If $\vdash_{T}\exists x F(x)$ then there is a term $a$ such that $\vdash_{T} F(a)$

If I recall correctly Heyting Arithmetics has the property, and clearly also Omega Logic has it. Are there other important examples?

$\endgroup$
6
  • 7
    $\begingroup$ This is called the existence property. $\endgroup$
    – Zhen Lin
    Aug 3, 2015 at 9:44
  • $\begingroup$ Thanks. Consequently, the following Wikipedia article becomes useful: en.wikipedia.org/wiki/Disjunction_and_existence_properties $\endgroup$ Aug 3, 2015 at 12:48
  • 1
    $\begingroup$ You might also be interested in Herbrand logic. This is a modified semantics for first-order logic in which the underlying set of a model is always the set of terms in the language. Hence if $M\models \exists x\,\varphi(x)$, then $M \models \varphi(a)$ for some term $a$. $\endgroup$ Aug 3, 2015 at 19:12
  • $\begingroup$ If you require this property only for closed formulas of the form $\exists x\, F(x)$, then I would call $T$ a Henkin theory. $\endgroup$
    – Goldstern
    Aug 4, 2015 at 10:41
  • 1
    $\begingroup$ @FrodeBjørdal Rather than quoting my own book I can point to Shoenfield's book (4.2, page 45), which uses this notation. (But requires constants, not just any terms.) Also Hinman (Fundamentals of Math.Logic 3.1, page 196) calls a complete theory "Henkin complete" if there are "Henkin witnesses" for every closed existential formula. This concept is used for Henkin's proof of Gödel's completeness theorem. $\endgroup$
    – Goldstern
    Aug 5, 2015 at 8:49

1 Answer 1

1
$\begingroup$

Perhaps "$T$ has witnesses"?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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