Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
A First Order Language

Piotr Rudnicki

The University of Alberta

Supported in part by NSERC Grant No. OGP 9207.

Andrzej Trybulec

Warsaw University, Bialystok

Supported by NSERC Grant No. OGP 9207.
This work has been done while the author visited The University of Alberta
in Spring 1989.
Summary.

In the paper a first order language is constructed. It includes
the universal quantifier and the
following propositional connectives: truth, negation, and conjunction.
The variables are divided into three kinds:
bound variables, fixed variables, and free variables. An infinite number
of predicates for each arity is provided. Schemes of structural induction
and schemes justifying definitions by structural induction have been proved.
The concept of a closed formula (a formula without free occurrences of
bound variables) is introduced.
The terminology and notation used in this paper have been
introduced in the following articles
[7]
[6]
[5]
[10]
[9]
[8]
[1]
[11]
[3]
[12]
[4]
[2]
Contents (PDF format)
Bibliography
 [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Andrzej Trybulec.
Enumerated sets.
Journal of Formalized Mathematics,
1, 1989.
 [7]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [8]
Andrzej Trybulec.
Tuples, projections and Cartesian products.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [10]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [11]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [12]
Edmund Woronowicz.
Relations defined on sets.
Journal of Formalized Mathematics,
1, 1989.
Received August 8, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]