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?

Improve this question
$\endgroup$
6
  • 7
    $\begingroup$ This is called the existence property. $\endgroup$
    – Zhen Lin
    Commented Aug 3, 2015 at 9:44
  • $\begingroup$ Thanks. Consequently, the following Wikipedia article becomes useful: en.wikipedia.org/wiki/Disjunction_and_existence_properties $\endgroup$
    – Frode Alfson Bjørdal
    Commented 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$
    – Alex Kruckman
    Commented 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
    Commented 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
    Commented Aug 5, 2015 at 8:49

1 Answer 1

Reset to default
1
$\begingroup$

Perhaps "$T$ has witnesses"?

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .