logical language

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

A logical language consists of:

  • A set F of function symbols (common examples include + and )

  • A set R of relation symbols (common examples include = and <)

  • A set C of logical connectives (usually ¬, , , and )

  • A set Q of quantifiersMathworldPlanetmath (usuallly and )

  • A set V of variables

Every function symbol, relation symbol, and connective is associated with an arity (the set of n-ary function symbols is denoted Fn, and similarly for relation symbols and connectives). Each quantifier is a generalized quantifier associated with a quantifier type n1,,nn.

The underlying logic has a (possibly empty) set of types T. There is a function Type:FVT which assignes a type to each function and variable. For each arity n is a function Inputsn:FnRnTn which gives the types of each of the arguments to a function symbol or relationMathworldPlanetmath. In additionPlanetmathPlanetmath, for each quantifier type n1,,nn there is a function Inputsn1,,nn defined on Qn1,,nn (the set of quantifiers of that type) which gives an n-tuple of ni-tuples of types of the arguments taken by formulas the quantifier applies to.

The terms of of type tT are built as follows:

  1. 1.

    If v is a variable such that Type(v)=t then v is a term of type t

  2. 2.

    If f is an n-ary function symbol such that Type(f)=t and t1,,tn are terms such that for each i<n Type(ti)=(Inputsn(f))i then ft1,,tn is a term of type t

The formulas of are built as follows:

  1. 1.

    If r is an n-ary relation symbol and t1,,tn are terms such that Type(ti)=(Inputsn(r))i then rt1,,tn is a formula

  2. 2.

    If c is an n-ary connective and f1,,fn are formulas then cf1,,fn is a formula

  3. 3.

    If q is a quantifier of type n1,,nn, v1,1,,v1,n1,v2,1,,vn,1,,vn,nn are a sequenceMathworldPlanetmath of variables such that Type(vi,j)=((Inputsn1,,nn(q))j)i and f1,,fn are formulas then qv1,1,,v1,n1,v2,1,,vn,1,,vn,nnf1,,fn 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 languagesPlanetmathPlanetmath. 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 logicPlanetmathPlanetmath. 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 with appropriate semantics, this is second order logic (a slightly different formulation replaces 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.

Title logical language
Canonical name LogicalLanguage
Date of creation 2013-03-22 12:59:55
Last modified on 2013-03-22 12:59:55
Owner Henry (455)
Last modified by Henry (455)
Numerical id 14
Author Henry (455)
Entry type Definition
Classification msc 03B15
Classification msc 03B10
Related topic QuantifierFree
Defines term
Defines formula
Defines constant