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 (192)
Orphanage
Unclass'd (1)
Unproven (490)
Corrections (6)
Classification

talkback
Polls
Forums
Feedback
Bug Reports

downloads
Snapshots
PM Book

information
News
Docs
Wiki
ChangeLog
TODO List
Legalese
About
Owner confidence rating: Medium Entry average rating: No information on entry rating
logical language (Definition)

In its most general form, a logical language is a set of rules for constructing formulas for some logic, which can then be assigned truth values based on the rules of that logic.

A logical language $ \mathcal{L}$ consists of:

Every function symbol, relation symbol, and connective is associated with an arity (the set of $ n$-ary function symbols is denoted $ F_n$, and similarly for relation symbols and connectives). Each quantifier is a generalized quantifier associated with a quantifier type $ \langle n_1,\ldots,n_n\rangle$.

The underlying logic has a (possibly empty) set of types $ T$. There is a function $ \operatorname{Type}:F\cup V\rightarrow T$ which assignes a type to each function and variable. For each arity $ n$ is a function $ \operatorname{Inputs}_n:F_n\cup R_n\rightarrow T^n$ which gives the types of each of the arguments to a function symbol or relation. In addition, for each quantifier type $ \langle n_1,\ldots,n_n\rangle$ there is a function $ \operatorname{Inputs}_{\langle n_1,\ldots,n_n\rangle}$ defined on $ Q_{\langle n_1,\ldots,n_n\rangle}$ (the set of quantifiers of that type) which gives an $ n$-tuple of $ n_i$-tuples of types of the arguments taken by formulas the quantifier applies to.

The terms of $ \mathcal{L}$ of type $ t\in T$ are built as follows:

  1. If $ v$ is a variable such that $ \operatorname{Type}(v)=t$ then $ v$ is a term of type $ t$
  2. If $ f$ is an $ n$-ary function symbol such that $ \operatorname{Type}(f)=t$ and $ t_1,\ldots,t_n$ are terms such that for each $ i<n$ $ \operatorname{Type}(t_i)=(\operatorname{Inputs}_n(f))_i$ then $ ft_1,\ldots,t_n$ is a term of type $ t$

The formulas of $ \mathcal{L}$ are built as follows:

  1. If $ r$ is an $ n$-ary relation symbol and $ t_1,\ldots,t_n$ are terms such that $ \operatorname{Type}(t_i)=(\operatorname{Inputs}_n(r))_i$ then $ rt_1,\ldots,t_n$ is a formula
  2. If $ c$ is an $ n$-ary connective and $ f_1,\ldots,f_n$ are formulas then $ cf_1,\ldots,f_n$ is a formula
  3. If $ q$ is a quantifier of type $ \langle n_1,\ldots,n_n\rangle$, $ v_{1,1},\ldots,v_{1,n_1},v_{2,1},\ldots,v_{n,1},\ldots,v_{n,n_n}$ are a sequence of variables such that $ \operatorname{Type}(v_{i,j})=((\operatorname{Inputs}_{\langle n_1,\ldots,n_n\rangle}(q))_j)_i$ and $ f_1,\ldots,f_n$ are formulas then $ qv_{1,1},\ldots,v_{1,n_1},v_{2,1},\ldots,v_{n,1},\ldots,v_{n,n_n}f_1,\ldots,f_n$ is a formula

Generally the connectives, quantifiers, and variables are specified by the appropriate logic, while the function and relation symbols are specified for particular languages. Note that 0-ary functions are usually called constants.

If there is only one type which is equated directly with truth values then this is essentially a propositional logic. If the standard quantifiers and connectives are used, there is only one type, and one of the relations is $ =$ (with its usual semantics), this produces first order logic. If the standard quantifiers and connectives are used, there are two types, and the relations include $ =$ and $ \in$ with appropriate semantics, this is second order logic (a slightly different formulation replaces $ \in$ with a $ 2$-ary function which represents function application; this views second order objects as functions rather than sets).

Note that often connectives are written with infix notation with parentheses used to control order of operations.



"logical language" is owned by Henry.
(view preamble)

View style:

See Also: quantifier free

Also defines:  term, formula, constant
Log in to rate this entry.
(view current ratings)

Cross-references: order of operations, infix notation, objects, application, represents, second order logic, first order logic, semantics, propositional logic, languages, sequence, relation, arguments, function, type, generalized quantifier, arity, variables, quantifiers, logical connectives, relation symbols, function symbols, logic
There are 21 references to this entry.

This is version 11 of logical language, born on 2002-08-28, modified 2007-01-05.
Object id is 3376, canonical name is LogicalLanguage.
Accessed 26690 times total.

Classification:
AMS MSC: 03B15 (Mathematical logic and foundations :: General logic :: Higher-order logic and type theory)
 03B10 (Mathematical logic and foundations :: General logic :: Classical first-order logic)
Pending Errata and Addenda
None.
[ View all 5 ]
Discussion
Style: Expand: Order:
forum policy

No messages.

Interact
post | correct | update request | add derivation | add example | add (any)