W BIAŁYMSTOKU
Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/21362Pełny rekord metadanych
| Pole DC | Wartość | Język |
|---|---|---|
| dc.contributor.author | Braselmann, Patrick | - |
| dc.contributor.author | Koepke, Peter | - |
| dc.date.accessioned | 2026-10-29T09:10:31Z | - |
| dc.date.available | 2026-10-29T09:10:31Z | - |
| dc.date.issued | 2005 | - |
| dc.identifier.citation | Formalized Mathematics, Volume 13, Issue 1, Pages 5-15 | pl |
| dc.identifier.issn | 1426-2630 | - |
| dc.identifier.uri | http://hdl.handle.net/11320/21362 | - |
| dc.description.abstract | This articleis part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt Godel’s famous completeness theorem (K. Godel, “Die Vollstandigkeit der Axiome des logischen Funktionenkalkuls”, Monatshefte fur Mathematik und Physik 37 (1930), 349-360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article introduces the basic concepts of substitution of a variable for a variable in a first-order formula. The contents of this article correspond to Chapter III par. 8, Definition 8.1, 8.2 of Ebbinghaus, Flum, Thomas. | pl |
| dc.language.iso | en | pl |
| dc.publisher | University of Białystok | pl |
| dc.rights | Attribution-ShareAlike 4.0 International | - |
| dc.rights.uri | https://creativecommons.org/licenses/by-sa/4.0/ | - |
| dc.title | Substitution in First-Order Formulas: Elementary Properties | pl |
| dc.type | Article | pl |
| dc.rights.holder | © 2005 University of Białystok | pl |
| dc.rights.holder | This work is licensed under the Creative Commons License. | pl |
| dc.description.Affiliation | Patrick Braselmann - University of Bonn | pl |
| dc.description.Affiliation | Peter Koepke - University of Bonn | pl |
| dc.description.references | Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990. | pl |
| dc.description.references | Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990. | pl |
| dc.description.references | Czeslaw Byliński. A classical first order language. Formalized Mathematics, 1(4):669–676, 1990. | pl |
| dc.description.references | Czeslaw Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. | pl |
| dc.description.references | Czeslaw Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990. | pl |
| dc.description.references | Czeslaw Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990. | pl |
| dc.description.references | Czeslaw Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. | pl |
| dc.description.references | Czeslaw Byliński and Grzegorz Bancerek. Variables in formulae of the first order language. Formalized Mathematics, 1(3):459–469, 1990. | pl |
| dc.description.references | Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. | pl |
| dc.description.references | Agata Darmochwał and Andrzej Trybulec. Similarity of formulae. Formalized Mathematics, 2(5):635–642, 1991. | pl |
| dc.description.references | Piotr Rudnicki and Andrzej Trybulec. A first order language. Formalized Mathematics, 1(2):303–311, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics. | pl |
| dc.description.references | Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1(3):495–500, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990. | pl |
| dc.description.references | Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. | pl |
| dc.description.references | Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990. | pl |
| dc.description.references | Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990. | pl |
| dc.identifier.eissn | 1898-9934 | - |
| dc.description.volume | 13 | pl |
| dc.description.issue | 1 | pl |
| dc.description.firstpage | 5 | pl |
| dc.description.lastpage | 15 | pl |
| dc.identifier.citation2 | Formalized Mathematics | pl |
| Występuje w kolekcji(ach): | Formalized Mathematics, 2005, Volume 13, Issue 1 | |
Pliki w tej pozycji:
| Plik | Opis | Rozmiar | Format | |
|---|---|---|---|---|
| Substitution_in_First_Order_Formulas.pdf | 139,6 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL
