PlanetMath (more info)
 Math for the people, by the people.
Encyclopedia | Requests | Forums | Docs | Wiki | Random | RSS  
Login
create new user
name:
pass:
forget your password?
Main Menu
sections
Encyclopædia
Papers
Books
Expositions

meta
Requests (197)
Orphanage
Unclass'd
Unproven (498)
Corrections (25)
Classification

talkback
Polls
Forums
Feedback
Bug Reports

downloads
Snapshots
PM Book

information
News
Docs
Wiki
ChangeLog
TODO List
Legalese
About
Owner confidence rating: Very high Entry average rating: Very high
first order language (Definition)

Let $ \Sigma$ be a signature. The first order language $ \operatorname{FO}(\Sigma)$ on $ \Sigma$ contains the following:

  1. the set $ S(\Sigma)$ of symbols of $ \operatorname{FO}(\Sigma)$, which is the disjoint union of the following sets:
    1. $ \Sigma$ (the non-logical symbols),
    2. a countably infinite set $ V$ of variables,
    3. the set of logical symbols $ \lbrace \wedge , \vee , \neg, \Rightarrow , \Leftrightarrow , \forall, \exists \rbrace$,
    4. the singleton consisting of the equality symbol $ \lbrace =\rbrace$, and
    5. the set of parentheses (left and right) $ \lbrace (, )\rbrace$;
  2. the set $ T(\Sigma)$ of terms of $ \operatorname{FO}(\Sigma)$, which is built inductively from $ S(\Sigma)$, as follows:
    1. Any variable $ v\in V$ is a term;
    2. Any constant symbol in $ \Sigma$ is a term;
    3. If $ f$ is an $ n$-ary function symbol in $ \Sigma$, and $ t_1,...,t_n$ are terms, then $ f(t_1,...,t_n)$ is a term.
  3. the set $ F(\Sigma)$ of formulas of $ \operatorname{FO}(\Sigma)$, which is built inductively from $ T(\Sigma)$, as follows:
    1. If $ t_1$ and $ t_2$ are terms, then $ (t_1=t_2)$ is a formula;
    2. If $ R$ is an $ n$-ary relation symbol and $ t_1,...,t_n$ are terms, then $ (R(t_1,...,t_n))$ is a formula;
    3. If $ \varphi$ is a formula, then so is $ (\neg\varphi)$;
    4. If $ \varphi$ and $ \psi$ are formulas, then so is $ (\varphi\vee \psi)$;
    5. If $ \varphi$ is a formula, and $ x$ is a variable, then $ (\exists x(\varphi))$ is a formula.
In other words, $ T(\Sigma)$ and $ F(\Sigma)$ are the smallest sets, among all sets satisfying the conditions given for terms and formulas, respectively.

For example, in the first order language of partially ordered rings, expressions such as

$\displaystyle 0,\quad x^2,$    and $\displaystyle \quad y+zx$
are terms, while
$\displaystyle (x=xy),\quad (x+y \le yz),$    and $\displaystyle \quad (\exists x ((x\le 0) \vee (0\le x)))$
are formulas.

Remarks.

  1. Generally, one omits parentheses in formulas, when there is no ambiguity. For example, a formula $ (\varphi)$ can be simply written $ \varphi$. As such, the parentheses are also called the auxiliary symbols.
  2. The first two types of formulas, not involving logical connectives, are the atomic formulas. It is evident that formulas are inductively built from atomic formulas.
  3. The other logical symbols are obtained in the following way :
    $\displaystyle \varphi\wedge \psi$ $\displaystyle \overset{\operatorname{def}}{:=}\neg(\neg\varphi\vee \neg\psi)$ $\displaystyle \qquad \varphi\Rightarrow \psi$ $\displaystyle \overset{\operatorname{def}}{:=}\neg\varphi\vee \psi$    
    $\displaystyle \varphi\Leftrightarrow \psi$ $\displaystyle \overset{\operatorname{def}}{:=}(\varphi\Rightarrow \psi)\wedge (\psi\Rightarrow \varphi)$ $\displaystyle \qquad \forall x(\varphi)$ $\displaystyle \overset{\operatorname{def}}{:=}\neg(\exists x(\neg\varphi))$    

    where $ \varphi$ and $ \psi$ are formulas. All logical symbols are used when building formulas.
  4. In the literature, it is a common practice to write $ \Sigma_{\omega \omega}$ for $ \operatorname{FO}(\Sigma)$. The first subscript means that every formula in $ \operatorname{FO}(\Sigma)$ contains a finite number of $ \vee$'s (less than $ \omega$), while the second subscript signifies that every formula has a finite number of $ \exists$'s. In general, $ \Sigma_{\alpha\beta}$ denotes a language built from $ \Sigma$ such that, in any given formula, the number of occurrences of $ \vee$ is less than $ \alpha$ and the number of occurrences of $ \exists$ is less than $ \beta$. When the number of occurrences of $ \vee$ (or $ \exists$) in a formula is not limited, we use the symbol $ \infty$ in place of $ \alpha$ (or $ \beta$). Clearly, if $ \alpha$ and $ \beta$ are not $ \omega$, we get a language that is not first-order.
  5. Also a common practice in the literature, $ \Sigma$ is used to identify a signature and the first-order language it uniquely determines.

Bibliography

1
W. Hodges, A Shorter Model Theory, Cambridge University Press, (1997).
2
D. Marker, Model Theory, An Introduction, Springer, (2002).



"first order language" is owned by CWoo. [ full author list (3) | owner history (2) ]
(view preamble)

View style:

See Also: type, language, atomic formula

Other names:  auxiliary symbol, first-order language
Also defines:  first order language, term, formula

Attachments:
prenex form (Definition) by rspuzio
many-sorted language (Definition) by CWoo
Log in to rate this entry.
(view current ratings)

Cross-references: place, occurrences, language, number, finite, subscript, atomic formulas, logical connectives, types, expressions, partially ordered rings, relation symbol, function symbol, constant symbol, right, equality, singleton, variables, countably infinite, disjoint union, contains, signature
There are 143 references to this entry.

This is version 23 of first order language, born on 2002-06-02, modified 2008-01-16.
Object id is 2999, canonical name is TermsAndFormulas.
Accessed 34643 times total.

Classification:
AMS MSC: 03B10 (Mathematical logic and foundations :: General logic :: Classical first-order logic)
 03C07 (Mathematical logic and foundations :: Model theory :: Basic properties of first-order languages and structures)
Pending Errata and Addenda
None.
[ View all 11 ]
Discussion
Style: Expand: Order:
forum policy
"logic" topic? by akrowne on 2002-06-02 15:09:26
Perhaps it would be good to have a "logic" topic-type entry, which gives an overview of mathematical logic. Entries like this one could be attached to it.

apk
[ reply | up ]
Interact
post | correct | update request | add derivation | add example | add (any)