Similarity of Formulae

Agata Darmochwal

Warsaw University

Andrzej Trybulec

Warsaw University, Bialystok

Summary.

The main objective of the paper is to define the concept of the similarity of formulas. We mean by similar formulas the two formulas that differs only in the names of bound variables. Some authors (compare [14]) call such formulas {\em congruent}. We use the word {\em similar} following [12], [11], [13]. The concept is unjustfully neglected in many logical handbooks. It is intuitively quite clear, however the exact definition is not simple. As far as we know, only W.A.~Pogorzelski and T.~Prucnal [13] define it in the precise way. We follow basically the Pogorzelski's definition (compare [12]). We define renumeration of bound variables and we say that two formulas are similar if after renumeration are equal. Therefore we need a rule of chosing bound variables independent of the original choice. Quite obvious solution is to use consecutively variables $x_{k+1},x_{k+2},\dots$, where $k$ is the maximal index of free variable occurring in the formula. Therefore after the renumeration we get the new formula in which different quantifiers bind different variables. It is the reason that the result of renumeration applied to a formula $\varphi$ we call {\em $\varphi$ with variables separated}.

MML Identifier: CQC_SIM1

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. Connectives and subformulae of the first order language. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[5] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[7] Czeslaw Bylinski. A classical first order language. Journal of Formalized Mathematics, 2, 1990.

[8] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.

[9] Czeslaw Bylinski and Grzegorz Bancerek. Variables in formulae of the first order language. Journal of Formalized Mathematics, 1, 1989.

[10] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[11] Wlodzimierz Lesisz and Witold A. Pogorzelski. A simplified definition of the notion of similarity between formulas of the first order predicate calculus. \em Reports on Mathematical Logic, (7):63--69, 1976.

[12] Witold A. Pogorzelski. \em Klasyczny Rachunek Predykat ow. PWN, Warszawa, 1981.

[13] Witold A. Pogorzelski and Tadeusz Prucnal. The substitution rule for predicate letters in the first-order predicate calculus. \em Reports on Mathematical Logic, (5):77--90, 1975.

[14] Helena Rasiowa and Roman Sikorski. \em The Mathematics of Metamathematics, volume 41 of \em Monografie Matematyczne. PWN, Warszawa, 1968.

[15] Piotr Rudnicki and Andrzej Trybulec. A first order language. Journal of Formalized Mathematics, 1, 1989.

[16] Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.

[17] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[18] Andrzej Trybulec. Semilattice operations on finite subsets. Journal of Formalized Mathematics, 1, 1989.

[19] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[20] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[21] Andrzej Trybulec. Function domains and Fr\aenkel operator. Journal of Formalized Mathematics, 2, 1990.

[22] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[23] Andrzej Trybulec and Agata Darmochwal. Boolean domains. Journal of Formalized Mathematics, 1, 1989.

[24] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[25] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[26] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.