{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T20:28:31Z","timestamp":1649017711449},"reference-count":15,"publisher":"Walter de Gruyter GmbH","issue":"4","license":[{"start":{"date-parts":[[2016,12,1]],"date-time":"2016-12-01T00:00:00Z","timestamp":1480550400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,12,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p>This article introduces propositional logic as a formal system ([14], [10], [11]). The formulae of the language are as follows <jats:italic>\u03c6<\/jats:italic> ::= \u22a5 | <jats:italic>p<\/jats:italic> | <jats:italic>\u03c6<\/jats:italic> \u2192 <jats:italic>\u03c6<\/jats:italic>. Other connectives are introduced as abbrevations. The notions of model and satisfaction in model are defined. The axioms are all the formulae of the following schemes\n<jats:list list-type=\"bullet\">\n                     <jats:list-item>\n                        <jats:p>\n                           <jats:italic>\u03b1<\/jats:italic> \u21d2 (<jats:italic>\u03b2<\/jats:italic> \u21d2 <jats:italic>\u03b1<\/jats:italic>),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>(<jats:italic>\u03b1<\/jats:italic> \u21d2 (<jats:italic>\u03b2<\/jats:italic> \u21d2 <jats:italic>\u03b3<\/jats:italic>)) \u21d2 ((<jats:italic>\u03b1<\/jats:italic> \u21d2 <jats:italic>\u03b2<\/jats:italic>) \u21d2 (<jats:italic>\u03b1<\/jats:italic> \u21d2 <jats:italic>\u03b3<\/jats:italic>)),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>(\u00ac<jats:italic>\u03b2<\/jats:italic> \u21d2 \u00ac<jats:italic>\u03b1<\/jats:italic>) \u21d2 ((\u00ac<jats:italic>\u03b2<\/jats:italic> \u21d2 <jats:italic>\u03b1<\/jats:italic>) \u21d2 <jats:italic>\u03b2<\/jats:italic>).<\/jats:p>\n                     <\/jats:list-item>\n                  <\/jats:list>\nModus ponens is the only derivation rule. The soundness theorem and the strong completeness theorem are proved. The proof of the completeness theorem is carried out by a counter-model existence method. In order to prove the completeness theorem, Lindenbaum\u2019s Lemma is proved. Some most widely used tautologies are presented.<\/jats:p>","DOI":"10.1515\/forma-2016-0024","type":"journal-article","created":{"date-parts":[[2017,2,25]],"date-time":"2017-02-25T10:00:53Z","timestamp":1488016853000},"page":"281-290","source":"Crossref","is-referenced-by-count":0,"title":["The Axiomatization of Propositional Logic"],"prefix":"10.1515","volume":"24","author":[{"given":"Mariusz","family":"Giero","sequence":"first","affiliation":[{"name":"Faculty of Economics and Informatics, University of Bia\u0142ystok, Kalvariju 135, LT-08221 Vilnius, Lithuania"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2017,2,23]]},"reference":[{"key":"2021040800042487883_j_forma-2016-0024_ref_001_w2aab2b8b9b1b7b1ab1ab1Aa","unstructured":"[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41\u201346, 1990."},{"key":"2021040800042487883_j_forma-2016-0024_ref_002_w2aab2b8b9b1b7b1ab1ab2Aa","unstructured":"[2] Grzegorz Bancerek. The well ordering relations. Formalized Mathematics, 1(1):123\u2013129, 1990."},{"key":"2021040800042487883_j_forma-2016-0024_ref_003_w2aab2b8b9b1b7b1ab1ab3Aa","unstructured":"[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107\u2013114, 1990."},{"key":"2021040800042487883_j_forma-2016-0024_ref_004_w2aab2b8b9b1b7b1ab1ab4Aa","unstructured":"[4] Leszek Borys. On paracompactness of metrizable spaces. Formalized Mathematics, 3(1): 81\u201384, 1992."},{"key":"2021040800042487883_j_forma-2016-0024_ref_005_w2aab2b8b9b1b7b1ab1ab5Aa","unstructured":"[5] Czes\u0142aw Byli\u0144ski. Binary operations. Formalized Mathematics, 1(1):175\u2013180, 1990."},{"key":"2021040800042487883_j_forma-2016-0024_ref_006_w2aab2b8b9b1b7b1ab1ab6Aa","unstructured":"[6] Czes\u0142aw Byli\u0144ski. Functions and their basic properties. Formalized Mathematics, 1(1): 55\u201365, 1990."},{"key":"2021040800042487883_j_forma-2016-0024_ref_007_w2aab2b8b9b1b7b1ab1ab7Aa","unstructured":"[7] Czes\u0142aw Byli\u0144ski. Functions from a set to a set. Formalized Mathematics, 1(1):153\u2013164, 1990."},{"key":"2021040800042487883_j_forma-2016-0024_ref_008_w2aab2b8b9b1b7b1ab1ab8Aa","unstructured":"[8] Czes\u0142aw Byli\u0144ski. Partial functions. Formalized Mathematics, 1(2):357\u2013367, 1990."},{"key":"2021040800042487883_j_forma-2016-0024_ref_009_w2aab2b8b9b1b7b1ab1ab9Aa","doi-asserted-by":"crossref","unstructured":"[9] Mariusz Giero. Propositional linear temporal logic with initial validity semantics. Formalized Mathematics, 23(4):379\u2013386, 2015. doi:10.1515\/forma-2015-0030.","DOI":"10.1515\/forma-2015-0030"},{"key":"2021040800042487883_j_forma-2016-0024_ref_010_w2aab2b8b9b1b7b1ab1ac10Aa","unstructured":"[10] Witold Pogorzelski. Dictionary of Formal Logic. Wydawnictwo UwB - Bialystok, 1992."},{"key":"2021040800042487883_j_forma-2016-0024_ref_011_w2aab2b8b9b1b7b1ab1ac11Aa","unstructured":"[11] Witold Pogorzelski. Notions and theorems of elementary formal logic. Wydawnictwo UwB - Bialystok, 1994."},{"key":"2021040800042487883_j_forma-2016-0024_ref_012_w2aab2b8b9b1b7b1ab1ac12Aa","unstructured":"[12] Piotr Rudnicki and Andrzej Trybulec. On same equivalents of well-foundedness. Formalized Mathematics, 6(3):339\u2013343, 1997."},{"key":"2021040800042487883_j_forma-2016-0024_ref_013_w2aab2b8b9b1b7b1ab1ac13Aa","unstructured":"[13] Andrzej Trybulec. Defining by structural induction in the positive propositional language. Formalized Mathematics, 8(1):133\u2013137, 1999."},{"key":"2021040800042487883_j_forma-2016-0024_ref_014_w2aab2b8b9b1b7b1ab1ac14Aa","unstructured":"[14] Anita Wasilewska. An Introduction to Classical and Non-Classical Logics. SUNY Stony Brook, 2005."},{"key":"2021040800042487883_j_forma-2016-0024_ref_015_w2aab2b8b9b1b7b1ab1ac15Aa","unstructured":"[15] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73\u201383, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/4\/article-p281.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0024","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,8]],"date-time":"2021-04-08T05:23:22Z","timestamp":1617859402000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0024"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,1]]},"references-count":15,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2017,2,23]]},"published-print":{"date-parts":[[2016,12,1]]}},"alternative-id":["10.1515\/forma-2016-0024"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0024","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2016,12,1]]}}}