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.

MML Identifier: QC_LANG1

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]