Object language

Last updated

An object language is a language which is the "object" of study in various fields including logic (or metalogic), linguistics, mathematics (or metamathematics), and theoretical computer science. The language being used to talk about an object language is called a metalanguage. [1] An object language may be a formal or natural language. [2]

Contents

Forms of object language

Formal languages

Mathematical logic and linguistics make use of metalanguages, which are languages for describing the nature of other languages. In mathematical logic, the object language is usually a formal language. The language which a metalanguage is used to describe is the object language. It is called that because that language is the object under discussion using the metalanguage.

For instance, someone who says "In French, you say Bonjour to greet someone" uses English as a metalanguage to describe the object language French.

Computer languages

There are two ways the term object language can be used in computing: a language which is the object of formal specification, and a language which is the object (goal) of a compiler or interpreter.

Formal specification

Computer languages are object languages of the metalanguage in which their specification is written. In computer science this is referred to as the specification language. Backus–Naur form was one of the earliest used specification languages.

When compilers are written using systems like lex and yacc, the rules the programmer writes look much like a formal specification, but it is considered an implementation instead. Many programming language implementations are not strictly the same as their specifications, adding features or making implementation-dependent design decisions.

Object code

At their basic level, computers act on what is given to them through a limited set of instructions which are understood by their CPUs. In the earliest computers, that meant programmers sometimes composed actual 1's and 0's to program. Since this requires considerable programmer training (and patience) to create instructions, later computer languages have gone to great lengths to simplify the programmer's task. For example, a high level programming language may allow a programmer to assign a value to a variable without specifying a memory location or a CPU instruction.

In this context, the high level programming language is the source language, which is then translated by a compiler into object code that the CPU can read directly. This object code is the object language, and varies depending on what CPU is being given the instructions.

Object language in this context means something akin to "the object of what the programmer is trying to achieve". If the source language and object languages are viewed as formal (logical) languages, what the compiler does is interpret the source into the target language (this is different from the computer science use of interpreted language meaning one which is not compiled).

Object language in this context is synonymous with target language. The object language of a translation most often is a machine language, but can be some other kind of language, such as assembly language.

Because the object language of compilation has usually been machine language, the term object file has come to mean a file containing machine instructions, and sometimes the translated program itself is simply called an object.

Object language should also not be confused with object-oriented language , which is a type of computer programming language which changes the programmer's environment into convenient objects which can be used in something similar to a drag-and-drop fashion.

Expressions in an object language

Symbols

A symbol is an idea, abstraction or concept, tokens of which may be marks or a configuration of marks which form a particular pattern. Although the term "symbol" in common use refers at some times to the idea being symbolized, and at other times to the marks on a piece of paper or chalkboard which are being used to express that idea; in the formal languages studied in mathematics and logic, the term "symbol" refers to the idea, and the marks are considered to be a token instance of the symbol.

Formulas

In the formal languages used in mathematical logic and computer science, a well-formed formula or simply formula is an idea, abstraction or concept which is expressed using the symbols and formation rules (also called the formal grammar) of a particular formal language. To say that a string of symbols is a well-formed formula with respect to a given formal grammar is equivalent to saying that belongs to the language generated by .

Formal systems

A formal system is a formal language together with a deductive system which consists of a set of inference rules and/or axioms. A formal system is used to derive one expression from one or more other expressions previously expressed in the system. These expressions are called axioms, in the case of those previously supposed to be true, or theorems, in the case of those derived. A formal system may be formulated and studied for its intrinsic properties, or it may be intended as a description (i.e. a model) of external phenomena.

Theorems

A theorem is a symbol or string of symbols which is derived by using a formal system. The string of symbols is a logical consequence of the axioms and rules of the system.

Formal proofs

A formal proof or derivation is a finite sequence of propositions (called well-formed formulas in the case of a formal language) each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system. The concept of natural deduction is a generalization of the concept of proof. [3]

Theories

A theory is a set of sentences in a formal language.

See also

Related Research Articles

An axiom, postulate or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Greek axíōma 'that which is thought worthy or fit' or 'that which commends itself as evident.'

Formal language Words whose letters are taken from an alphabet and are well-formed according to a specific set of rules

In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules.

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

Gödels completeness theorem Fundamental theorem in mathematical logic

Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic.

Theorem In mathematics, a statement that has been proved

In mathematics, a theorem is a statement that has been proved, or can be proved. The proof of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of the axioms and previously proved theorems.

Mathematical proof Rigorous demonstration that a mathematical statement follows from its premises

A mathematical proof is an inferential argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proof can, in principle, be constructed using only certain basic or original assumptions known as axioms, along with the accepted rules of inference. Proofs are examples of exhaustive deductive reasoning which establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning which establish "reasonable expectation". Presenting many cases in which the statement holds is not enough for a proof, which must demonstrate that the statement is true in all possible cases. An unproven proposition that is believed to be true is known as a conjecture, or a hypothesis if frequently used as an assumption for further mathematical work.

Proof theory is a major branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.

Metalogic is the study of the metatheory of logic. Whereas logic studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems. Logic concerns the truths that may be derived using a logical system; metalogic concerns the truths that may be derived about the languages and systems that are used to express truths.

A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A formal system is essentially an "axiomatic system".

In programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages. It does so by evaluating the meaning of syntactically valid strings defined by a specific programming language, showing the computation involved. In such a case that the evaluation would be of syntactically invalid strings, the result would be non-computation. Semantics describes the processes a computer follows when executing a program in that specific language. This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will be executed on a certain platform, hence creating a model of computation.

In logic and linguistics, a metalanguage is a language used to describe another language, often called the object language. Expressions in a metalanguage are often distinguished from those in the object language by the use of italics, quotation marks, or writing on a separate line. The structure of sentences and phrases in a metalanguage can be described by a metasyntax.

Syntax (logic) Rules used for constructing, or transforming the symbols and words of a language

In logic, syntax is anything having to do with formal languages or formal systems without regard to any interpretation or meaning given to them. Syntax is concerned with the rules used for constructing, or transforming the symbols and words of a language, as contrasted with the semantics of a language which is concerned with its meaning.

Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1933, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics. Informally, the theorem states that arithmetical truth cannot be defined in arithmetic.

Laws of Form is a book by G. Spencer-Brown, published in 1969, that straddles the boundary between mathematics and philosophy. LoF describes three distinct logical systems:

Object theory is a theory in mathematical logic concerning objects and the statements that can be made about objects.

In logic, a metatheorem is a statement about a formal system proven in a metalanguage. Unlike theorems proved within a given formal system, a metatheorem is proved within a metatheory, and may reference concepts that are present in the metatheory but not the object theory.

Logic is the formal science of using reason and is considered a branch of both philosophy and mathematics and to a lesser extent computer science. Logic investigates and classifies the structure of statements and arguments, both through the study of formal systems of inference and the study of arguments in natural language. The scope of logic can therefore be very large, ranging from core topics such as the study of fallacies and paradoxes, to specialized analyses of reasoning such as probability, correct reasoning, and arguments involving causality. One of the aims of logic is to identify the correct and incorrect inferences. Logicians study the criteria for the evaluation of arguments.

An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation. The general study of interpretations of formal languages is called formal semantics.

Logic The study of inference and truth

Logic is an interdisciplinary field which studies truth and reasoning. Informal logic seeks to characterize valid arguments informally, for instance by listing varieties of fallacies. Formal logic represents statements and argument patterns symbolically, using formal systems such as first order logic. Within formal logic, mathematical logic studies the mathematical characteristics of logical systems, while philosophical logic applies them to philosophical problems such as the nature of meaning, knowledge, and existence. Systems of formal logic are also applied in other fields including linguistics, cognitive science, and computer science.

References

  1. Hunter, Geoffrey (1973-06-26). Metalogic: An Introduction to the Metatheory of Standard First Order Logic. University of California Press. p. 11. ISBN   978-0-520-02356-7.
  2. Trask, R. L.; Trask, Robert Lawrence (1999). Key Concepts in Language and Linguistics. Psychology Press. p. 122. ISBN   978-0-415-15741-4.
  3. The Cambridge Dictionary of Philosophy, deduction.