A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Artur Korni{\l}owicz.
{M}azur-{U}lam Theorem,
Formalized Mathematics 19(3),
pages 127-130, 2011. MML Identifier:
MAZURULM Summary:
The Mazur-Ulam theorem \cite{MazurUlam} has been formulated as two
registrations: {\verb!cluster bijective isometric -> midpoints-preserving
Function!} {\verb!of E,F;!} and {\verb!cluster isometric midpoints-preserving ->
Affine Function!} {\verb!of E,F;!} A proof given by
Jussi V\"{a}is\"{a}l\"{a} \cite{Jussi} has been formalized.
Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama.
Set of Points on Elliptic Curve in Projective Coordinates,
Formalized Mathematics 19(3),
pages 131-138, 2011. MML Identifier:
EC_PF_1 Summary:
In this article, we formalize a set of points on an elliptic curve
over $\bf{GF}(p)$. Elliptic curve cryptography \cite{BSS99}, whose
security is based on a difficulty of discrete logarithm problem of elliptic
curves, is important for information security.
Karol P\k{a}k.
Continuity of Barycentric Coordinates in {E}uclidean Topological Spaces,
Formalized Mathematics 19(3),
pages 139-144, 2011. MML Identifier:
RLAFFIN3 Summary:
In this paper we present selected properties of barycentric coordinates in the
Euclidean topological space. We prove the topological correspondence between a
subset of an affine closed space of ${\cal E}^n$ and the set of vectors created
from barycentric coordinates of points of this subset.
Karol P\k{a}k.
{B}rouwer Fixed Point Theorem for Simplexes,
Formalized Mathematics 19(3),
pages 145-150, 2011. MML Identifier:
SIMPLEX2 Summary:
In this article we prove the Brouwer fixed point theorem for an arbitrary
simplex which is the convex hull of its $n + 1$ affinely indepedent vertices
of ${\cal E}^n$. First we introduce the Lebesgue number, which for an arbitrary
open cover of a compact metric space $\mathfrak{M}$ is a positive real number so
that any ball of about such radius must be completely contained in a member of the
cover. Then we introduce the notion of a bounded simplicial complex and the diameter
of a bounded simplicial complex. We also prove the estimation of diameter decrease
which is connected with the barycentric subdivision. Finally, we prove the Brouwer
fixed point theorem and compute the small inductive dimension of ${\cal E}^n$.
This article is based on \cite{DUDA:BM61}.
Karol P\k{a}k.
Brouwer Fixed Point Theorem in the General Case,
Formalized Mathematics 19(3),
pages 151-153, 2011. MML Identifier:
BROUWER2 Summary:
In this article we prove the Brouwer fixed point theorem for an arbitrary convex
compact subset of ${\cal E}^n$ with a non empty interior. This article is based
on \cite{SIEKLUCKI:BM53}.
Marco B. Caminati.
Preliminaries to Classical First Order Model Theory,
Formalized Mathematics 19(3),
pages 155-167, 2011. MML Identifier:
FOMODEL0 Summary:
First of a series of articles laying down the bases for classical first order model theory.
These articles introduce a framework for treating arbitrary languages with equality.
This framework is kept as generic and modular as possible: both the language and the
derivation rule are introduced as a type, rather than a fixed functor; definitions
and results regarding syntax, semantics, interpretations and sequent derivation rules,
respectively, are confined to separate articles, to mark out the hierarchy of dependences
among different definitions and constructions. \par
As an application limited to countable languages, satisfiability theorem and a full
version of the G\"odel completeness theorem are delivered, with respect to a fixed,
remarkably thrifty, set of correct rules. Besides the self-referential significance
for the Mizar project itself of those theorems being formalized with respect to a generic,
equality-furnished, countable language, this is the first step to work out other milestones
of model theory, such as Lowenheim-Skolem and compactness theorems. Being the receptacle
of all results of broader scope stemmed during the various formalizations, this first
article stays at a very generic level, with results and registrations about objects
already in the Mizar Mathematical Library. \par
Without introducing the Language structure yet, three fundamental definitions of wide
applicability are also given: the `unambiguous' attribute
(see \cite{lothaire2002algebraic},
definition on page 5), the functor `-multiCat', which is the iteration
of `\^\,' over a FinSequence of FinSequence, and the functor SubstWith, which
realizes the substitution of a single symbol inside a generic FinSequence.
Marco B. Caminati.
Definition of First Order Language with Arbitrary Alphabet. {S}yntax of Terms, Atomic Formulas and their Subterms,
Formalized Mathematics 19(3),
pages 169-178, 2011. MML Identifier:
FOMODEL1 Summary:
Second of a series of articles laying down the bases for classical first order model
theory. A language is defined basically as a tuple made of an integer-valued
function (adicity), a symbol of equality and a symbol for the NOR logical connective.
The only requests for this tuple to be a language is that the value of the adicity
in = is -2 and that its preimage (i.e. the variables set) in 0 is infinite.
Existential quantification will be rendered
(see \cite{FOMODEL2.ABS}) by mere
prefixing a formula with a letter. Then the hierarchy among symbols according
to their adicity is introduced, taking advantage of attributes and clusters.\par
The strings of symbols of a language are depth-recursively classified as terms
using the standard approach (see for example \cite{pohlers1992introduction},
definition 1.1.2); technically, this is done here by deploying the `-multiCat'
functor and the `unambiguous' attribute previously introduced
in \cite{FOMODEL0.ABS},
and the set of atomic formulas is introduced. The set of all terms is shown to be
unambiguous with respect to concatenation; we say that it is a prefix set. This fact
is exploited to uniquely define the subterms both of a term and of an atomic formula
without resorting to a parse tree.
Marco B. Caminati.
First Order Languages: Further Syntax and Semantics,
Formalized Mathematics 19(3),
pages 179-192, 2011. MML Identifier:
FOMODEL2 Summary:
Third of a series of articles laying down the bases for classical first order
model theory. Interpretation of a language in a universe set. Evaluation of a term in
a universe. Truth evaluation of an atomic formula. Reassigning the value of a symbol
in a given interpretation. Syntax and semantics of a non atomic formula are then
defined concurrently (this point is explained in \cite{caminati2010basic}, 4.2.1).
As a consequence, the evaluation of any w.f.f. string and the relation of logical
implication are introduced. Depth of a formula. Definition of satisfaction and
entailment (aka entailment or logical implication) relations,
see \cite{ebbinghaus1994mathematical} III.3.2 and III.4.1 respectively.
Marco B. Caminati.
Free Interpretation, Quotient Interpretation and Substitution of a Letter with a Term for First Order Languages,
Formalized Mathematics 19(3),
pages 193-203, 2011. MML Identifier:
FOMODEL3 Summary:
Fourth of a series of articles laying down the bases for classical first order model
theory. This paper supplies a toolkit of constructions to work with languages and
interpretations, and results relating them. The free interpretation of a language,
having as a universe the set of terms of the language itself, is defined.\par
The quotient of an interpreteation with respect to an equivalence relation is
built, and shown to remain an interpretation when the relation respects it.
Both the concepts of quotient and of respecting relation are defined in broadest
terms, with respect to objects as general as possible.\par
Along with the trivial symbol substitution generally defined
in \cite{FOMODEL0.ABS},
the more complex substitution of a letter with a term is defined, basing right on
the free interpretation just introduced, which is a novel approach, to the author's
knowledge. A first important result shown is that the quotient operation commute in
some sense with term evaluation and reassignment functors, both introduced
in \cite{FOMODEL2.ABS}
(theorem 3, theorem 15). A second result proved is substitution
lemma (theorem 10, corresponding to III.8.3 of \cite{ebbinghaus1994mathematical}).
This will be vital for proving satisfiability theorem and correctness of a certain
sequent derivation rule in \cite{FOMODEL4.ABS}.
A third result supplied is that if
two given languages coincide on the letters of a given FinSequence, their evaluation
of it will also coincide. This too will be instrumental
in \cite{FOMODEL4.ABS} for
proving correctness of another rule. Also, the Depth functor is shown to be invariant
with respect to term substitution in a formula.
Marco B. Caminati.
Sequent Calculus, Derivability, Provability. {G}\"odel's Completeness Theorem,
Formalized Mathematics 19(3),
pages 205-222, 2011. MML Identifier:
FOMODEL4 Summary:
Fifth of a series of articles laying down the bases for classical first order model
theory. This paper presents multiple themes: first it introduces sequents, rules and
sets of rules for a first order language L as L-dependent types. Then defines
derivability and provability according to a set of rules, and gives several technical
lemmas binding all those concepts. Following that, it introduces a fixed set D of
derivation rules, and proceeds to convert them to Mizar functorial cluster registrations
to give the user a slick interface to apply them.\par
The remaining goals summon all the definitions and results introduced in this series
of articles. First: D is shown to be correct and having the requisites to deliver
a sensible definition of Henkin model (see \cite{ebbinghaus1994mathematical}).
Second: as a particular application of all the machinery built thus far, the
satisfiability and G\"odel completeness theorems are shown when restricting to
countable languages. The techniques used to attain this are inspired
from \cite{ebbinghaus1994mathematical}, then heavily modified with the twofold
goal of embedding them into the more flexible framework of a variable ruleset
here introduced, and of proving completeness of a set of rules more sparing than
the one there used; in particular the simpler ruleset allowed to avoid the definition
and tractation of free occurence of a literal, a fact which, along with shortening proofs,
is remarkable in its own right. A preparatory account of some of the ideas used in the
proofs given here can be found in \cite{caminati2009yet}.