PlanetMath: definable

(more info)

Math for the people, by the people.

Main Menu

sections Encyclopædia
Papers
Books
Expositions

meta Requests (200)
Orphanage
Unclass'd
Unproven (490)
Corrections (6)
Classification

talkback Polls
Forums
Feedback
Bug Reports

downloads Snapshots
PM Book

information News
Docs
Wiki
ChangeLog
TODO List
Legalese
About

Entry average rating: No information on entry rating

definable

(Definition)

Definable sets and functions

Definability In Model Theory

Let $\mathcal{L}$ be a first order language. Let

be an $\mathcal{L}$ -structure. Denote $x_1, \ldots, x_n$ by $\vec{x}$ and $y_1, \ldots, y_m$ by $\vec{y}$ , and suppose $\phi(\vec{x},\vec{y})$ is a formula from $\mathcal{L}$ , and $b_1, \ldots, b_m$ is some sequence from

Then we write $\phi(M^{n},\vec{b})$ to denote $\{\vec{a} \in M^{n}:M \models \phi(\vec{a},\vec{b})\}$ . We say that $\phi(M^{n},\vec{b})$ is $\vec{b}$ -definable. More generally if is some set and $B \subseteq M$ , and there is some $\vec{b}$ from so that is $\vec{b}$ -definable then we say that is -definable.

In particular we say that a set is $\emptyset$ -definable or zero definable iff it is the solution set of some formula without parameters.

Let be a function, then we say is -definable iff the graph of (i.e. $\{(x,y):f(x)=y\}$ ) is a -definable set.

If is -definable then any automorphism of that fixes pointwise, fixes setwise.

A set or function is definable iff it is -definable for some parameters .

Some authors use the term definable to mean what we have called $\emptyset$ -definable here. If this is the convention of a paper, then the term parameter definable will refer to sets that are definable over some parameters.

Sometimes in model theory it is not actually very important what language one is using, but merely what the definable sets are, or what the definability relation is.

Definability of functions in Proof Theory

In proof theory, given a theory

in the language $\mathcal{L}$ , for a function $f:M\rightarrow M$ to be definable in the theory

, we have two conditions:

(i) There is a formula in the language $\mathcal{L}$ s.t. is definable over the model , as in the above definition; i.e., its graph is definable in the language $\mathcal{L}$ over the model , by some formula $\phi(\vec{x}, y)$ .

(ii) The theory proves that is indeed a function, that is $T\vdash \forall \vec{x} \exists ! y. \phi(\vec{x}, y)$ .

For example: the graph of exponentiation function is definable by the language of the theory $I\Delta_0$ (a subsystem of PA, with induction axiom restricted to bounded formulas only), however the function itself is not definable in this theory.

"definable" is owned by CWoo. [ full author list (3) | owner history (6) ]

(view preamble)

Also defines:

definable set, definable function, definable relation

Keywords:

definable

Log in to rate this entry.
(view current ratings)

Cross-references: bounded, restricted, induction axiom, PA, theory, relation, language, model theory, term, pointwise, fixes, automorphism, graph, function, parameters, solution, iff, sequence, formula, first order language
There are 20 references to this entry.

This is version 14 of definable, born on 2003-02-10, modified 2004-04-01.
Object id is 4012, canonical name is Definable2.
Accessed 7048 times total.

Classification:

AMS MSC:	03C07 (Mathematical logic and foundations :: Model theory :: Basic properties of first-order languages and structures)
	03F03 (Mathematical logic and foundations :: Proof theory and constructive mathematics :: Proof theory, general)

Pending Errata and Addenda

None.[ View all 4 ]

Discussion

forum policy

Interact