Editing Metalogic (section)

== Overview ==

=== Formal language ===
{{Main|Formal language}}

A ''formal language'' is an organized set of [[symbol (formal)|symbols]], the symbols of which precisely define it by shape and place. Such a language therefore can be defined without [[reference]] to the [[meaning (linguistics)|meanings]] of its expressions; it can exist before any [[Interpretation (logic)|interpretation]] is assigned to it—that is, before it has any meaning. [[First-order logic]] is expressed in some formal language. A [[formal grammar]] determines which symbols and sets of symbols are [[well-formed formula|formulas]] in a formal language.

A formal language can be formally defined as a set ''A'' of strings (finite sequences) on a fixed alphabet α. Some authors, including [[Rudolf Carnap]], define the language as the ordered pair <α, ''A''>.<ref name="itslaia">[[Rudolf Carnap]] (1958) ''[https://books.google.com/books?id=hAvVAgAAQBAJ Introduction to Symbolic Logic and its Applications]'', p.&nbsp;102.</ref> Carnap also requires that each element of α must occur in at least one string in ''A''.

=== Formation rules ===
{{Main|Formation rule}}

''Formation rules'' (also called ''formal grammar'') are a precise description of the [[well-formed formula]]s of a formal language. They are synonymous with the [[set (mathematics)|set]] of [[String (computer science)|strings]] over the [[alphabet]] of the formal language that constitute well formed formulas. However, it does not describe their [[semantics]] (i.e. what they mean).

=== Formal systems ===
{{Main|Formal system}}

A ''formal system'' (also called a ''logical calculus'', or a ''logical system'') consists of a formal language together with a [[Deductive system|deductive apparatus]] (also called a ''deductive system''). The deductive apparatus may consist of a set of [[Rule of inference|transformation rule]]s (also called ''inference rules'') or a set of [[axiom]]s, or have both. A formal system is used to [[Proof theory|derive]] one expression from one or more other expressions.

A ''formal system'' can be formally defined as an ordered triple <α,<math>\mathcal{I}</math>,<math>\mathcal{D}</math>d>, where <math>\mathcal{D}</math>d is the relation of direct derivability. This relation is understood in a comprehensive [[Sense and reference|sense]] such that the primitive sentences of the formal system are taken as directly [[formal proof|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 so chosen that every first place member of <math>\mathcal{D}</math>d is a member of <math>\mathcal{I}</math> and every second place member is a finite subset of <math>\mathcal{I}</math>.

A ''formal system'' can also be defined with only the relation <math>\mathcal{D}</math>d.   Thereby can be omitted <math>\mathcal{I}</math>  and α in the definitions of ''interpreted formal language'', and ''interpreted formal system''. However, this method can be more difficult to understand and use.<ref name = "itslaia"/>

=== Formal proofs ===
{{Main|Formal proof}}

A ''formal proof'' is a sequence of well-formed formulas of a formal language, the last of which is a [[theorem]] of a formal system. The theorem is a [[Logical consequence|syntactic consequence]] of all the well formed formulae that precede it in the proof system. For a well formed formula to qualify as part of a proof, it must result from applying a rule of the deductive apparatus of some formal system to the previous well formed formulae in the proof sequence.

=== Interpretations ===
{{Main|Interpretation (logic)|Formal semantics (logic)}}

An ''interpretation'' of a formal system is the assignment of meanings to the symbols and [[Truth value|truth-value]]s to the sentences of the formal system. The study of interpretations is called [[Formal semantics (logic)|Formal semantics]]. ''Giving an interpretation'' is synonymous with ''constructing a [[Structure (mathematical logic)|model]]''.