logical language (original) (raw)

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:

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:F∪V→T which assignes a type to each function and variable. For each arity n is a function Inputsn:Fn∪Rn→Tn 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 Inputs⟨n1,…,nn⟩ defined on Q⟨n1,…,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 t∈T are built as follows:

    1. If v is a variable such that Type⁡(v)=t then v is a term of type t
    1. 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 f⁢t1,…,tn is a term of type t

The formulas of ℒ are built as follows:

    1. If r is an n-ary relation symbol and t1,…,tn are terms such that Type⁡(ti)=(Inputsn⁡(r))i then r⁢t1,…,tn is a formula
    1. If c is an n-ary connective and f1,…,fn are formulas then c⁢f1,…,fn is a formula
    1. 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)=((Inputs⟨n1,…,nn⟩⁡(q))j)i and f1,…,fn are formulas then q⁢v1,1,…,v1,n1,v2,1,…,vn,1,…,vn,nn⁢f1,…,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).