User:Gregbard/Sandbox/Formal language (logic)

From Wikipedia, the free encyclopedia

This article is about a term in logic. For related articles see Formal language (disambiguation)

A formal language is an organized set of symbols the essential feature of which is that it can be precisely defined in terms of just the shapes and locations of those symbols. Such a language can be defined, then, without any reference to any meanings of any of its expressions; it can exist before any interpretation is assigned to it -- that is, before it has any meaning.

In logic the idea of constructing such languages is at least as early as Leibniz but the first successful attempt was the Begriffsschrift ("concept writing") of Gottlob Frege. ^[1]

A formal language can be identified with the set of its well formed formulas (wffs). If the set of all wffs of a formal language L is exactly the same as the set of all wffs of a formal language L', then L is the same formal language as L'. If they do not have the same set of wffs, then they are not the same language.

The set of well-formed formula of a particular formal language is determined by a fiat of its creator. Usually, the determination of what is and is not a wff is laid down by designating a) a set of symbols which are the alphabet of the language and b) a set of formation rules which determine what sequences of symbols from the alphabet are wffs of the language.^[2]

The vocabulary (basic expressions) of formal languages of logic typically consists of constants, variables and the auxiliary signs. The constants are either logical constants or non-logical constants. The non-logical constants have no fixed meaning ("semantic content") in a language except under an interpretation. The auxiliary signs are such as brackets needed to give the langauage structure.

1 Formal grammar
2 Formal systems
3 Formal proofs
4 Interpreted formal languages
- 4.1 A simple example
5 Interpreted formal systems

[edit] Formal grammar

Main article: Formal grammar

A formal grammar (also called formation rules) is a precise description of a the well-formed formulas of a formal language. It is synonymous with the set of strings over the alphabet of the formal language which constitute well formed formulas. However, it does not describe their semantics (i.e. what they mean).

[edit] Formal systems

Main article: Formal system

A formal system (also called a logical calculus, or a logical system) consists of a formal language together with a deductive apparatus (also called a deductive system). The deductive apparatus may consist of a set of transformation rules (also called inference rules) or a set of axioms, or have both. A formal system is used to derive one expression from one or more other expressions.

A formal system can be formally defined as an ordered triple <α, $\mathcal{I}$ , $\mathcal{D}$ d>, where $\mathcal{D}$ d is the relation of direct derivability. This relation is understood in a comprehensive sense such that the primitive sentences of the formal system are taken as directly derivable from the empty set of sentences. Direct derivability is a relation between a sentence and a finite, possibly empty set of sentences. Axioms are laid down in such a way that every first place member of $\mathcal{D}$ d is a member of $\mathcal{I}$ and every second place member is a finite subset of $\mathcal{I}$ .

It is also possible to define a formal system using only the relation $\mathcal{D}$ d. In this way we can omit $\mathcal{I}$ , and α in the definitions of interpreted formal language, and interpreted formal system. However, this method can be more difficult to understand and work with. ^[3]

[edit] Formal proofs

Main article: Formal proof

A formal proof is a sequences of well-formed formulas of a formal language, the last one of which is a theorem of a formal system. The theorem is a syntactic consequence of all the well formed formulae preceding it in the proof. For a well formed formula to qualify as part of a proof, it must be the result of applying a rule of the deductive apparatus of some formal system to the previous well formed formulae in the proof sequence.

[edit] Interpreted formal languages

Main articles: Formal semantics and Formal interpretation

An interpreted formal language can defined as the ordered triple <α, $\mathcal{I}$ , $\mathcal{D}$ >. The first domain of the relation $\mathcal{D}$ is identical with the class $\mathcal{I}$ .

If an extensional metalanguage is used for semantics, then $\mathcal{D}$ is the relation of value assignment for the sentences of the language.

For example, " $\mathcal{D}$ ( $\mathcal{I}$ ₁,grass is green)" means the same as "The sentence $\mathcal{I}$ ₁ is true if and only if grass is green." For any p and q and any element $\mathcal{I}$ ₁ of the class $\mathcal{I}$ , if $\mathcal{D}$ ( $\mathcal{I}$ ₁,p) and $\mathcal{D}$ ( $\mathcal{I}$ ₁,q) then p if and only if q.

If on the other hand, an intensional metalanguage, containing a modal operator, such as "it is necessary that", then D is taken as the relation of designation, That is, the relation between an expression and its intension.

For example, " $\mathcal{D}$ ( $\mathcal{I}$ ₁, grass is green)" means the same as "The sentence $\mathcal{I}$ ₁ designates the proposition that grass is green." For any p and q and any element $\mathcal{I}$ ₁ of the class $\mathcal{I}$ , if $\mathcal{D}$ ( $\mathcal{I}$ ₁,p) and $\mathcal{D}$ ( $\mathcal{I}$ ₁,q) then p and q are identical, i.e it is logically necessary that p if and only if q.

In either of these two metalanguages extensional, or intensional, truth with respect to any given interpreted language (α, $\mathcal{I}$ , $\mathcal{D}$ ) can be defined as follows: A sentence $\mathcal{I}$ ₁ is true if and only if for some p, $\mathcal{D}$ ( $\mathcal{I}$ ₁,p), and p.

There is another method applicable to either of these two metalanguages which takes the relation $\mathcal{D}$ as applying not only to sentences but to a more comprehensive class d of designators. By this method, an interpreted formal language is an ordered quadruple (α, $\mathcal{I}$ ,d, $\mathcal{D}$ ).

In these metalanguages, d is the class of finite sequences of elements of the class α, the class of the first place members of $\mathcal{D}$ is the class d, and that $\mathcal{I}$ is a subclass of d.

There is also a third method, which is more explicit, which demands that in order to specify an interpreted formal language a class ds of descriptive signs of the language must be indicated. In this method, an interpreted formal language can be defined as the ordered quintuple <α,ds, $\mathcal{I}$ ,d, $\mathcal{D}$ >

Using this method, ds is a subclass of a. This most explicit method is convenient as a basis for definitions of concepts such as "model", "value assignment", "range of a sentence", "logical truth", and other logical concepts.^[4]

[edit] A simple example

The formal language $\mathcal{W}$ is defined as follows:

Alphabet α : { $\triangle$ , $\square$ }

Formal grammar : Any finite string of symbols from the alphabet of $\mathcal{W}$ that begins with a ' $\triangle$ ' is a formula.

A possible interpretation of $\mathcal{W}$ would be to take ' $\triangle$ ' as meaning the same as the decimal digit '1', ' $\square$ ' as meaning the same as the digit '0', and each formula as meaning the same as a decimal numeral composed exclusively of '1's and '0's. Therefore ' $\triangle$ $\square$ $\triangle$ ' means '101' under this interpretation of $\mathcal{W}$ .^[5]

[edit] Interpreted formal systems

An interpreted formal system is a formal language for which both syntactical rules for deduction, and semantical rules of interpretation are given. An interpreted formal system can be defined as the ordered quadruple <α, $\mathcal{I}$ , $\mathcal{D}$ d, $\mathcal{D}$ >. Here axioms are stated, some similar to those stated for a formal system, and some like those for an interpreted formal language. Usually, we wish for $\mathcal{D}$ d to be truth-preserving (that is, any sentence which is directly derivable from true sentences is itself true), however other modalities can also preserved in such a system. We can formulate an axiom for these purposes with use of the term "true". For any $\mathcal{I}$ _i_₁,..., $\mathcal{I}$ _i_{_n}, $\mathcal{I}$ _j, p₁,...,p_n,q if $\mathcal{D}$ d( $\mathcal{I}$ _j,{ $\mathcal{I}$ _i_₁,..., $\mathcal{I}$ _i_{_n}}), $\mathcal{D}$ ( $\mathcal{I}$ _i_₁,p₁) and ... and $\mathcal{D}$ ( $\mathcal{I}$ _i_{_n},p_n) and p₁ and ... and p_n, q.

For interpreted formal systems there are also alternative, more explicit definitions which include ds, or both ds and D, analogous to those given for interpreted formal languages. ^[3]

User:Gregbard/Sandbox/Formal language (logic)

From Wikipedia, the free encyclopedia

Contents

[edit] Formal grammar

[edit] Formal systems

[edit] Formal proofs

[edit] Interpreted formal languages

[edit] A simple example

[edit] Interpreted formal systems

Views

Navigation

Interaction

Search