Mathematical logic
>From Wikipedia, the free encyclopedia
Mathematical logic is a discipline within mathematics, studying formal
systems in relation to the way they encode intuitive concepts of proof and
computation as part of the foundations of mathematics.
Although the layperson may think that mathematical logic is the logic of
mathematics, the truth is rather that it more closely resembles the
mathematics of logic. It comprises those parts of logic that can be modelled
mathematically. Earlier appellations were symbolic logic (as opposed to
philosophical logic), and metamathematics, which is now restricted as a term
to some aspects of proof theory.
Contents
* 1 History
* 2 Topics in mathematical logic
* 3 Some fundamental results
* 4 Technical reference
* 4.1 First-order languages and structures
* 4.2 Terms, formulas and sentences
* 4.3 Assignment functions
* 4.4 Logical satisfaction
* 4.5 Logical implication and truth
* 4.6 Variable substitution
* 4.7 Substitutability
* 5 References
* 6 External links
* 7 See also
[edit]
History
Mathematical logic was the name given by Giuseppe Peano to what is also
known as symbolic logic. In essentials, it is still the logic of Aristotle,
but from the point of view of notation it is written as a branch of abstract
algebra.
Attempts to treat the operations of formal logic in a symbolic or algebraic
way were made by some of the more philosophical mathematicians, such as
Leibniz and Lambert; but their labors remained little known and isolated. It
was George Boole and then Augustus De Morgan, in the middle of the
nineteenth century, who presented a systematic mathematical (of course
non-quantitative) way of regarding logic. The traditional, Aristotelian
doctrine of logic was reformed and completed; and out of it developed an
adequate instrument for investigating the fundamental concepts of
mathematics. It would be misleading to say that the foundational
controversies that were alive in the period 19001925 have all been settled;
but philosophy of mathematics was greatly clarified by the "new" logic.
While the traditional development of logic (see list of topics in logic) put
heavy emphasis on forms of arguments, the attitude of current mathematical
logic might be summed up as the combinatorial study of content. This covers
both the syntactic (for example, sending a string from a formal language to
a compiler program to write it as sequence of machine instructions), and the
semantic (constructing specific models or whole sets of them, in model
theory).
Some landmark publications were the Begriffsschrift by Gottlob Frege,
Studies in Logic by Charles Peirce, Principia Mathematica by Bertrand
Russell and Alfred North Whitehead, and On Formally Undecidable Propositions
of Principia Mathematica and Related Systems by Kurt Gödel.
[edit]
Topics in mathematical logic
The main areas of mathematical logic include model theory, proof theory and
recursion theory (often now referred to as computability theory). Axiomatic
set theory is sometimes considered too. There are many overlaps with
computer science, since many early pioneers in computer science, such as
Alan Turing, were mathematicians and logicians.
The study of programming language semantics derives from model theory, as
does program verification, in particular model checking.
The Curry-Howard isomorphism between proofs and programs relates to proof
theory; intuitionistic logic and linear logic are significant here. Calculi
such as the lambda calculus and combinatory logic are nowadays studied
mainly as idealized programming languages.
Computer science also contributes to logic by developing techniques for the
automatic checking or even finding of proofs, such as automated theorem
proving and logic programming.
[edit]
Some fundamental results
Some important results are:
* The set of valid first-order formulas is recursively enumerable.
This follows from Gödel's completeness theorem (which establishes the
equivalence of validity and provability), because the set of proofs for
first-order logic formulas is recursively enumerable ("semi-decidable").
Therefore, there is a procedure that behaves as follows: Given a first-order
formula as its input, the procedure eventually halts if the formula is
valid, and runs forever otherwise. Some first-order theorem provers have
this completeness property.
* The set of valid first-order formulas is not recursive, i.e., there
is no algorithm for checking for universal validity. This follows from
Gödel's incompleteness theorem.
* The set of all universally valid second-order formulas is not even
recursively enumerable. This is also a consequence of Gödel's incompleteness
theorem.
* The Löwenheim-Skolem theorem.
* Cut-elimination in sequent calculus.
* The independence of the continuum hypothesis, proved by Paul Cohen
in 1963.
[edit]
Technical reference
[edit]
First-order languages and structures
Definition. A first-order language \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> is a collection of distinct typographical symbols classified as follows:
1. The equality symbol =\,
<http://upload.wikimedia.org/math/4/4/8/4488ba5f7e82e2d8c136b559d95283d5.png
> ; the connectives \lor\,
<http://upload.wikimedia.org/math/3/3/9/3399e64b18fc2268b6c34e4157db0385.png
> , \lnot\,
<http://upload.wikimedia.org/math/0/d/9/0d993a95fd56351789c805d4891305e6.png
> ; the universal quantifier \forall\,
<http://upload.wikimedia.org/math/7/1/a/71a682de227582a7134c80c457c1316f.png
> and the parentheses (\,
<http://upload.wikimedia.org/math/6/9/1/691331faa27ed30d57393aa42d1074d7.png
> , )\,
<http://upload.wikimedia.org/math/2/b/3/2b3f8215bdc94429403cdeab0c38412c.png
> .
2. A countable set of variable symbols \{v_i\}_{i = 0}^\infty\,
<http://upload.wikimedia.org/math/3/a/2/3a23ddde52dfbf46a83c082f2faabfe6.png
> .
3. A set of constant symbols \{c_\alpha\}_{\alpha \in \Alpha}\,
<http://upload.wikimedia.org/math/8/d/2/8d2206c604a41f071c548b6e2e8baea3.png
> .
4. A set of function symbols \{f_\beta\}_{\beta \in \Beta}\,
<http://upload.wikimedia.org/math/0/4/e/04eea3d911a0930615091bbddb609214.png
> .
5. A set of relation symbols \{R_\gamma\}_{\gamma \in \Gamma}\,
<http://upload.wikimedia.org/math/7/b/2/7b2dd54f5138b6fe33df1eabf2e46996.png
> .
Thus, in order to specify a language, it is often sufficient to specify only
the collection of constant symbols, function symbols and relation symbols,
since the first set of symbols is standard. The parentheses serve the only
purpose of forming groups of symbols, and are not to be formally used when
writing down functions and relations in formulas.
These symbols are just that, symbols. They don't stand for anything. They do
not mean anything. However, that deviates further into semantics and
linguistic issues not useful to the formalization of mathematical language,
yet.
Yet, because it will indeed be necessary to get some meaning out of this
formalization. The concept of model over a language provides with such a
semantics.
Definition. An \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -structure over the language \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> , is a bundle consisting of a nonempty set A\,
<http://upload.wikimedia.org/math/7/b/8/7b80ebccd4420d9579e7d488396b7f5c.png
> , the universe of the structure, together with:
1. For each constant symbol c\,
<http://upload.wikimedia.org/math/0/8/1/08163b03d3a58471d7f88fc4e581a282.png
> from \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> , an element c^{\mathfrak{A}} \in A\,
<http://upload.wikimedia.org/math/9/9/3/99345d1637363bd88777aff9273333e3.png
> .
2. For each n\,
<http://upload.wikimedia.org/math/a/9/5/a957404c96e59f1746f97ab668c8e1f8.png
> -ary function symbol f\,
<http://upload.wikimedia.org/math/1/8/f/18f63800376271ee4b0efe1545744cd6.png
> from \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> , an n\,
<http://upload.wikimedia.org/math/a/9/5/a957404c96e59f1746f97ab668c8e1f8.png
> -ary function f^{\mathfrak{A}} : A^n \longrightarrow A\,
<http://upload.wikimedia.org/math/2/8/5/285341977cfcae12b42bd5967d52ac2c.png
> .
3. For each n\,
<http://upload.wikimedia.org/math/a/9/5/a957404c96e59f1746f97ab668c8e1f8.png
> -ary relation symbol R\,
<http://upload.wikimedia.org/math/1/5/3/153fc2a5a0a49d52dda62d96ae0a293f.png
> from \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> , an n\,
<http://upload.wikimedia.org/math/a/9/5/a957404c96e59f1746f97ab668c8e1f8.png
> -ary relation on A\,
<http://upload.wikimedia.org/math/7/b/8/7b80ebccd4420d9579e7d488396b7f5c.png
> , that is, a subset R^{\mathfrak{A}} \subseteq A^n\,
<http://upload.wikimedia.org/math/d/8/f/d8fbdbc454f83490a96bc53aa12db421.png
> .
Often, the word model is used for that of structure in this context.
However, it is important to understand perhaps its motivation, as follows.
[edit]
Terms, formulas and sentences
Definition. An \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -term is a nonempty finite string t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> of symbols from \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> such that either
* t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is a variable symbol.
* t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is a constant symbol.
* t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is a string of the form f t_1 ... t_n\,
<http://upload.wikimedia.org/math/3/8/a/38a2e513d7390f9d637e52468450f3c2.png
> where f\,
<http://upload.wikimedia.org/math/1/8/f/18f63800376271ee4b0efe1545744cd6.png
> is an n\,
<http://upload.wikimedia.org/math/a/9/5/a957404c96e59f1746f97ab668c8e1f8.png
> -ary function symbol and t_1\,
<http://upload.wikimedia.org/math/c/b/a/cba084e41991e170fe00f0301effd235.png
> , ..., t_n\,
<http://upload.wikimedia.org/math/4/0/0/4004ae2a14b3951ebac60b75f9503b08.png
> are terms of \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> .
Definition. An \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -formula is a nonempty finite string \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> of symbols from \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> such that either
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is a string of the form t_1 = t_2\,
<http://upload.wikimedia.org/math/c/3/1/c317267c171075e93c5a6a6e8191c53e.png
> where t_1\,
<http://upload.wikimedia.org/math/c/b/a/cba084e41991e170fe00f0301effd235.png
> and t_2\,
<http://upload.wikimedia.org/math/4/8/7/48796fa47d285773342c850aedb974ef.png
> are terms of \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> .
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is a string of the form R t_1 ... t_n\,
<http://upload.wikimedia.org/math/c/0/b/c0b481d6438ac55ce1824bbfb75a32f2.png
> where R\,
<http://upload.wikimedia.org/math/1/5/3/153fc2a5a0a49d52dda62d96ae0a293f.png
> is an n\,
<http://upload.wikimedia.org/math/a/9/5/a957404c96e59f1746f97ab668c8e1f8.png
> -ary relation symbol and t_1\,
<http://upload.wikimedia.org/math/c/b/a/cba084e41991e170fe00f0301effd235.png
> , ..., t_n\,
<http://upload.wikimedia.org/math/4/0/0/4004ae2a14b3951ebac60b75f9503b08.png
> are terms of \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> .
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form \lnot(\alpha)\,
<http://upload.wikimedia.org/math/1/d/4/1d4a9b92c5c9721f64b677dc149af0ff.png
> where \alpha\,
<http://upload.wikimedia.org/math/b/2/7/b27abc434a11d07b390df859d7aa782a.png
> is an \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -formula.
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form (\alpha \lor \beta)\,
<http://upload.wikimedia.org/math/c/2/8/c28084294f57f812dfa8942985e5645c.png
> where both \alpha\,
<http://upload.wikimedia.org/math/b/2/7/b27abc434a11d07b390df859d7aa782a.png
> and \beta\,
<http://upload.wikimedia.org/math/8/1/b/81b4c8dd7cbec41cae5ef37da5644e99.png
> are \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -formulas.
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form (\forall y)(\alpha)\,
<http://upload.wikimedia.org/math/d/6/e/d6ece3c71990012b0e34dddc296dd8fe.png
> where y\,
<http://upload.wikimedia.org/math/e/c/9/ec9ff0a12771e750c2685d3b89a37c79.png
> is a variable symbol from \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> and \alpha\,
<http://upload.wikimedia.org/math/b/2/7/b27abc434a11d07b390df859d7aa782a.png
> is an \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -formula.
Definition. An \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -formula that is characterized by either the first or the second clause is
called an atomic.
Definition. Let \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> be an \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -formula. A variable symbol x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> from \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> is said to be free in \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> if either
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is atomic and x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> occurs in \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> .
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form \lnot(\alpha)\,
<http://upload.wikimedia.org/math/1/d/4/1d4a9b92c5c9721f64b677dc149af0ff.png
> and x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> is free in \alpha\,
<http://upload.wikimedia.org/math/b/2/7/b27abc434a11d07b390df859d7aa782a.png
> .
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form (\alpha \lor \beta)\,
<http://upload.wikimedia.org/math/c/2/8/c28084294f57f812dfa8942985e5645c.png
> and x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> is free in \alpha\,
<http://upload.wikimedia.org/math/b/2/7/b27abc434a11d07b390df859d7aa782a.png
> or \beta\,
<http://upload.wikimedia.org/math/8/1/b/81b4c8dd7cbec41cae5ef37da5644e99.png
> .
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form (\forall y)(\alpha)\,
<http://upload.wikimedia.org/math/d/6/e/d6ece3c71990012b0e34dddc296dd8fe.png
> where x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> and y\,
<http://upload.wikimedia.org/math/e/c/9/ec9ff0a12771e750c2685d3b89a37c79.png
> are not the same variable symbols and x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> is free in \alpha\,
<http://upload.wikimedia.org/math/b/2/7/b27abc434a11d07b390df859d7aa782a.png
> .
Definition. A sentence is a formula with no free variables.
[edit]
Assignment functions
Hereafter, \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> will denote a first-order language, \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> will be an \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -structure with underlying universe set denoted by A\,
<http://upload.wikimedia.org/math/7/b/8/7b80ebccd4420d9579e7d488396b7f5c.png
> . Every formula will be understood to be an \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -formula.
Definition. A variable assignment function (v.a.f.) into \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> is a function from the set of variables of \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> into A\,
<http://upload.wikimedia.org/math/7/b/8/7b80ebccd4420d9579e7d488396b7f5c.png
> .
Definition. Let s\,
<http://upload.wikimedia.org/math/d/0/4/d0438646c1f482faffdd1bac9a841799.png
> be a v.a.f. into \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> . We define the term assignment function (t.a.f.) \overline{s}\,
<http://upload.wikimedia.org/math/1/c/2/1c2560f781c6c5bcd239020747979d28.png
> , from the set of \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -terms into A\,
<http://upload.wikimedia.org/math/7/b/8/7b80ebccd4420d9579e7d488396b7f5c.png
> , as follows:
* If t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is the variable symbol x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> , then \overline{s}(t) = s(x)\,
<http://upload.wikimedia.org/math/9/5/0/950f5380923b493bef9a41e00bb6c371.png
> .
* If t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is the constant symbol c\,
<http://upload.wikimedia.org/math/0/8/1/08163b03d3a58471d7f88fc4e581a282.png
> , then \overline{s}(t) = c^{\mathfrak{A}}\,
<http://upload.wikimedia.org/math/2/d/c/2dc83dea2cc9d809f2b2631ec515930d.png
> .
* If t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is of the form f t_1 ... t_n\,
<http://upload.wikimedia.org/math/3/8/a/38a2e513d7390f9d637e52468450f3c2.png
> , then \overline{s}(t) = f^{\mathfrak{A}}(\overline{s}(t_1), ...,
\overline{s}(t_n))\,
<http://upload.wikimedia.org/math/c/5/a/c5a1e0ab0ea2c97e03d4ea1db5f28e50.png
> .
Definition. Let s\,
<http://upload.wikimedia.org/math/d/0/4/d0438646c1f482faffdd1bac9a841799.png
> be a v.a.f. into \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> and suppose that x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> is a variable and that a \in A\,
<http://upload.wikimedia.org/math/0/7/b/07be1540cef90b89e34d94b5ed531960.png
> . We define the v.a.f. s[x|a]\,
<http://upload.wikimedia.org/math/d/a/1/da116b8242d4ca40db633f20c9435f79.png
> , referred to as an x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> -modification of the assignment funtion s\,
<http://upload.wikimedia.org/math/d/0/4/d0438646c1f482faffdd1bac9a841799.png
> , by
s[x|a](v) = \begin{cases} s(v) & \mbox{if } v \ne x \\ a & \mbox{if } v = x
\end{cases} \,
<http://upload.wikimedia.org/math/3/e/9/3e95b55f035cdce6f0299857d374dc86.png
>
[edit]
Logical satisfaction
Definition. Let \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> be formula and suppose s\,
<http://upload.wikimedia.org/math/d/0/4/d0438646c1f482faffdd1bac9a841799.png
> is a v.a.f. into \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> . We say that \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> satisfies \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> with assignment s\,
<http://upload.wikimedia.org/math/d/0/4/d0438646c1f482faffdd1bac9a841799.png
> , and write \mathfrak{A} \models \phi[s]\,
<http://upload.wikimedia.org/math/9/f/1/9f1472ed3db5928cfdacd6bc3f04b5d3.png
> , if either:
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form t_1 = t_2\,
<http://upload.wikimedia.org/math/c/3/1/c317267c171075e93c5a6a6e8191c53e.png
> and \overline{s}(t_1) = \overline{s}(t_2)\,
<http://upload.wikimedia.org/math/0/d/c/0dcc23ebaa081ffadfab65731e71937a.png
> .
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form R t_1 ... t_n\,
<http://upload.wikimedia.org/math/c/0/b/c0b481d6438ac55ce1824bbfb75a32f2.png
> and (\overline{s}(t_1), ..., \overline{s}(t_n)) \in R^{\mathfrak{A}}\,
<http://upload.wikimedia.org/math/9/a/4/9a451fe268d9b1beb9dda2c67388bb3f.png
> .
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form \lnot(\alpha)\,
<http://upload.wikimedia.org/math/1/d/4/1d4a9b92c5c9721f64b677dc149af0ff.png
> and \mathfrak{A}\mbox{ }\not\models\mbox{ }\alpha[s]\,
<http://upload.wikimedia.org/math/3/e/3/3e3072ab11e422b1b87207d09770d125.png
> .
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form (\alpha \lor \beta)\,
<http://upload.wikimedia.org/math/c/2/8/c28084294f57f812dfa8942985e5645c.png
> and \mathfrak{A} \models \alpha[s]\,
<http://upload.wikimedia.org/math/6/8/1/681839a57652b86b33bc1872ab07fef6.png
> or \mathfrak{A} \models \beta[s]\,
<http://upload.wikimedia.org/math/6/a/d/6adc33d5d798ff8d61da6d998cdbd224.png
> .
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form (\forall y)(\alpha)\,
<http://upload.wikimedia.org/math/d/6/e/d6ece3c71990012b0e34dddc296dd8fe.png
> and for each element a \in A\,
<http://upload.wikimedia.org/math/0/7/b/07be1540cef90b89e34d94b5ed531960.png
> , \mathfrak{A} \models \alpha[s[y|a]]\,
<http://upload.wikimedia.org/math/9/c/9/9c90e70967d5834162ebbc849efaeaa8.png
> .
Definition. Let \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> be formula and suppose that \mathfrak{A} \models \phi[s]\,
<http://upload.wikimedia.org/math/9/f/1/9f1472ed3db5928cfdacd6bc3f04b5d3.png
> for every v.a.f. s\,
<http://upload.wikimedia.org/math/d/0/4/d0438646c1f482faffdd1bac9a841799.png
> into \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> . Then we say that \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> models \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> , and write \mathfrak{A} \models \phi\,
<http://upload.wikimedia.org/math/0/1/c/01cdeeee7c62a9e5a5b37ae9e2e8cf4e.png
> .
Definition. Let \Phi\,
<http://upload.wikimedia.org/math/c/e/2/ce20a96e27e0ab27104fd0982088f344.png
> be a set of formulas and suppose that \mathfrak{A} \models \phi\,
<http://upload.wikimedia.org/math/0/1/c/01cdeeee7c62a9e5a5b37ae9e2e8cf4e.png
> for every formula \phi \in \Phi\,
<http://upload.wikimedia.org/math/a/a/0/aa0e87e953b9d099d83c76f20e4e26ef.png
> then we say that \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> models \Phi\,
<http://upload.wikimedia.org/math/c/e/2/ce20a96e27e0ab27104fd0982088f344.png
> , and write \mathfrak{A} \models \Phi\,
<http://upload.wikimedia.org/math/0/d/e/0de1c41fbc325fa4a848b484218700cd.png
> .
In the case that \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is a sentence, that is, a formula with no free variables, the existence of
a single v.a.f. for which \mathfrak{A} \models \phi[s]\,
<http://upload.wikimedia.org/math/9/f/1/9f1472ed3db5928cfdacd6bc3f04b5d3.png
> immediately implies that \mathfrak{A} \models \phi\,
<http://upload.wikimedia.org/math/0/1/c/01cdeeee7c62a9e5a5b37ae9e2e8cf4e.png
> .
Definition. Let \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> be a sentence and suppose that \mathfrak{A} \models \phi\,
<http://upload.wikimedia.org/math/0/1/c/01cdeeee7c62a9e5a5b37ae9e2e8cf4e.png
> . Then we say that \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is true in \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> .
[edit]
Logical implication and truth
Definition. Let \Psi\,
<http://upload.wikimedia.org/math/7/1/1/71122cff2b8174ae337ecf3907a75a5d.png
> and \Phi\,
<http://upload.wikimedia.org/math/c/e/2/ce20a96e27e0ab27104fd0982088f344.png
> be sets of formulas. We say that \Psi\,
<http://upload.wikimedia.org/math/7/1/1/71122cff2b8174ae337ecf3907a75a5d.png
> logically implies \Phi\,
<http://upload.wikimedia.org/math/c/e/2/ce20a96e27e0ab27104fd0982088f344.png
> , and write \Psi \models \Phi\,
<http://upload.wikimedia.org/math/b/c/9/bc9b58689e62795a175b27d01a870e64.png
> , if for every structure \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> , \mathfrak{A} \models \Psi\,
<http://upload.wikimedia.org/math/3/7/6/376d948944d76fc7d2e76b64e94e030b.png
> implies \mathfrak{A} \models \Phi\,
<http://upload.wikimedia.org/math/0/d/e/0de1c41fbc325fa4a848b484218700cd.png
> .
As a shortcut, when dealing with singletons, we often write \Psi \models
\phi\,
<http://upload.wikimedia.org/math/4/8/4/484470c8ec280eea7200ea260b85a7fd.png
> instead of \Psi \models \{\phi\}\,
<http://upload.wikimedia.org/math/1/7/e/17e3a761b6398cf83ae6ea99865f1b48.png
> .
Definition. Let \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> be a formula and suppose that \varnothing \models \phi\,
<http://upload.wikimedia.org/math/c/a/1/ca1a1b869cab03ecf2fec47f32bde997.png
> . Then we say that \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is universally valid, or simply valid, and in this case we simply write
\models \phi\,
<http://upload.wikimedia.org/math/b/5/c/b5cdcb131ec2739fdfb6ee39287dd825.png
> .
To say that a formula \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is valid really means that every \mathfrak{L}\,
<http://upload.wikimedia.org/math/0/b/9/0b90bc40a16ff30c97e6163ef6614b34.png
> -structure \mathfrak{A}\,
<http://upload.wikimedia.org/math/b/f/5/bf5da5533ad3c70348d49f8b85e7389a.png
> models \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> .
Definition. Let \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> be a sentence and suppose that \models \phi\,
<http://upload.wikimedia.org/math/b/5/c/b5cdcb131ec2739fdfb6ee39287dd825.png
> . Then we say that \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is true.
[edit]
Variable substitution
Definition. Let u\,
<http://upload.wikimedia.org/math/6/1/e/61efad693efe8e0ffd7d7bc042b427ef.png
> be a term and suppose x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> is a variable and t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is another term. We define the term u_t^x\,
<http://upload.wikimedia.org/math/0/c/3/0c39cbbd1b08a7ecf68689f54b9d3680.png
> , read u\,
<http://upload.wikimedia.org/math/6/1/e/61efad693efe8e0ffd7d7bc042b427ef.png
> with x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> replaced by t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> , as follows:
* If u\,
<http://upload.wikimedia.org/math/6/1/e/61efad693efe8e0ffd7d7bc042b427ef.png
> is the variable symbol x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> , then u_t^x\,
<http://upload.wikimedia.org/math/0/c/3/0c39cbbd1b08a7ecf68689f54b9d3680.png
> is defined to be the term t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> .
* If u\,
<http://upload.wikimedia.org/math/6/1/e/61efad693efe8e0ffd7d7bc042b427ef.png
> is a variable symbol other than x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> , then u_t^x\,
<http://upload.wikimedia.org/math/0/c/3/0c39cbbd1b08a7ecf68689f54b9d3680.png
> is defined to be the term u\,
<http://upload.wikimedia.org/math/6/1/e/61efad693efe8e0ffd7d7bc042b427ef.png
> .
* If u\,
<http://upload.wikimedia.org/math/6/1/e/61efad693efe8e0ffd7d7bc042b427ef.png
> is a constant symbol, then u_t^x\,
<http://upload.wikimedia.org/math/0/c/3/0c39cbbd1b08a7ecf68689f54b9d3680.png
> is defined to be the term u\,
<http://upload.wikimedia.org/math/6/1/e/61efad693efe8e0ffd7d7bc042b427ef.png
> .
* If u\,
<http://upload.wikimedia.org/math/6/1/e/61efad693efe8e0ffd7d7bc042b427ef.png
> is of the form f t_1 ... t_n\,
<http://upload.wikimedia.org/math/3/8/a/38a2e513d7390f9d637e52468450f3c2.png
> , then u_t^x\,
<http://upload.wikimedia.org/math/0/c/3/0c39cbbd1b08a7ecf68689f54b9d3680.png
> is defined to be the term f {t_1}_t^x ... {t_n}_t^x\,
<http://upload.wikimedia.org/math/d/c/9/dc94dc16204ca5a501122c817d47d22b.png
> .
Definition. Let \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> be a formula and suppose x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> is a variable and t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is a term. We define the formula \phi_t^x\,
<http://upload.wikimedia.org/math/3/8/b/38bf972db869e8939d64af445a7a569c.png
> , read \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> with x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> replaced by t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> , as follows:
* If \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form t_1 = t_2\,
<http://upload.wikimedia.org/math/c/3/1/c317267c171075e93c5a6a6e8191c53e.png
> , then \phi_t^x\,
<http://upload.wikimedia.org/math/3/8/b/38bf972db869e8939d64af445a7a569c.png
> is defined to be the formula {t_1}_t^x = {t_2}_t^x\,
<http://upload.wikimedia.org/math/f/4/9/f49a8d4e7f3c2189e0d76ae022408301.png
> .
* If \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form R t_1 ... t_n\,
<http://upload.wikimedia.org/math/c/0/b/c0b481d6438ac55ce1824bbfb75a32f2.png
> , then \phi_t^x\,
<http://upload.wikimedia.org/math/3/8/b/38bf972db869e8939d64af445a7a569c.png
> is defined to be the formula R {t_1}_t^x, ..., {t_n}_t^x\,
<http://upload.wikimedia.org/math/6/0/8/608030a8da5fd6e9e753afbc1fad36dc.png
> .
* If \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form \lnot(\alpha)\,
<http://upload.wikimedia.org/math/1/d/4/1d4a9b92c5c9721f64b677dc149af0ff.png
> , then \phi_t^x\,
<http://upload.wikimedia.org/math/3/8/b/38bf972db869e8939d64af445a7a569c.png
> is defined to be the formula \lnot(\alpha_t^x)\,
<http://upload.wikimedia.org/math/7/2/3/723d473f14e5d23001e0ec4892b0e0db.png
> .
* If \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form (\alpha \lor \beta)\,
<http://upload.wikimedia.org/math/c/2/8/c28084294f57f812dfa8942985e5645c.png
> , then \phi_t^x\,
<http://upload.wikimedia.org/math/3/8/b/38bf972db869e8939d64af445a7a569c.png
> is defined to be the formula (\alpha_t^x \lor \beta_t^x)\,
<http://upload.wikimedia.org/math/4/6/4/4648b1050d8908aaefe4031e22f6164d.png
> .
* If \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form (\forall y)(\alpha)\,
<http://upload.wikimedia.org/math/d/6/e/d6ece3c71990012b0e34dddc296dd8fe.png
> , then
* if x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> and y\,
<http://upload.wikimedia.org/math/e/c/9/ec9ff0a12771e750c2685d3b89a37c79.png
> are the same variable symbol, \phi_t^x\,
<http://upload.wikimedia.org/math/3/8/b/38bf972db869e8939d64af445a7a569c.png
> is defined to be the formula \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> .
* else, \phi_t^x\,
<http://upload.wikimedia.org/math/3/8/b/38bf972db869e8939d64af445a7a569c.png
> is defined to be the formula (\forall y)(\alpha_t^x)\,
<http://upload.wikimedia.org/math/8/c/7/8c712e7f2dea93ddd81b6f75b9674ceb.png
> .
[edit]
Substitutability
Definition. Let \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> be a formula and suppose x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> is a variable and t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is a term. We say that t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is substitutable for x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> in \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> , if either:
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is atomic.
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form \lnot(\alpha)\,
<http://upload.wikimedia.org/math/1/d/4/1d4a9b92c5c9721f64b677dc149af0ff.png
> and t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is substitutable for x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> in \alpha\,
<http://upload.wikimedia.org/math/b/2/7/b27abc434a11d07b390df859d7aa782a.png
> .
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form (\alpha \lor \beta)\,
<http://upload.wikimedia.org/math/c/2/8/c28084294f57f812dfa8942985e5645c.png
> and t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is substitutable for x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> in both \alpha\,
<http://upload.wikimedia.org/math/b/2/7/b27abc434a11d07b390df859d7aa782a.png
> and \beta\,
<http://upload.wikimedia.org/math/8/1/b/81b4c8dd7cbec41cae5ef37da5644e99.png
> .
* \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> is of the form (\forall y)(\alpha)\,
<http://upload.wikimedia.org/math/d/6/e/d6ece3c71990012b0e34dddc296dd8fe.png
> and either
* x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> is not a free variable in \phi\,
<http://upload.wikimedia.org/math/c/d/0/cd014731964c742c274df08d7cc238fb.png
> .
* y\,
<http://upload.wikimedia.org/math/e/c/9/ec9ff0a12771e750c2685d3b89a37c79.png
> does not occur in t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> and t\,
<http://upload.wikimedia.org/math/0/c/6/0c68620ee2ea4f1286fcd672a47ea080.png
> is substitutable for x\,
<http://upload.wikimedia.org/math/6/b/2/6b206a28e60f665e235f89f460448467.png
> in \alpha\,
<http://upload.wikimedia.org/math/b/2/7/b27abc434a11d07b390df859d7aa782a.png
> .
The notion of substitutability of terms for variables corresponds to that of
the preservation of truth after substitution is carried out in terms or
formulas. Strictly speaking, substitution is always allowed, but
substitutability will be imperative in order to yield a formula which
meaning was not deformed by the substitution.
[edit]
References
* A. S. Troelstra & H. Schwichtenberg (2000). Basic Proof Theory
(Cambridge Tracts in Theoretical Computer Science) (2nd ed.). Cambridge
University Press. ISBN 0521779111.
* George Boolos & Richard Jeffrey (1989). Computability and Logic (3rd
ed.). Cambridge University Press. ISBN 0521007585.
* Elliott Mendelson (1997). Introduction to Mathematical Logic (4th
ed.) Chapman & Hall.
* A. G. Hamilton (1988). Logic for Mathematicians Cambridge University
Press.
[edit]
External links
* Mathematical Logic around the world <http://world.logic.at/>
* Polyvalued logic
<http://home.swipnet.se/~w-33552/logic/home/index.htm>
* Introduction to Mathematical Logic,Hyper-textbook for students,
Vilnis Detlovs and Karlis Podnieks,University of Latvia
<http://www.ltn.lv/~podnieks/mlog/ml.htm>
[edit]
See also
* Logic
* Model theory
* Sequent calculus
* Predicate logic
* Intuitionistic logic
* Theory of institutions
* Infinitary logic
* Provability logic
* Computability logic
* Table of mathematical symbols
* Foundational status of arithmetic
_______________________________________________
Marxism-Thaxis mailing list
[email protected]
To change your options or unsubscribe go to:
http://lists.econ.utah.edu/mailman/listinfo/marxism-thaxis
