{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T12:12:38Z","timestamp":1649160758068},"reference-count":27,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":4210,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2002,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The Logic of Partial Terms<jats:bold>LPT<\/jats:bold>is a strict negative free logic that provides an economical framework for developing many traditional mathematical theories having partial functions. In these traditional theories, all functions and predicates are strict. For example, if a unary function (predicate) is applied to an undefined argument, the result is undefined (respectively, false). On the other hand, every practical programming language incorporates at least one nonstrict or lazy construct, such as the if-then-else, but nonstrict functions cannot be either primitive or introduced in definitional extensions in<jats:bold>LPT<\/jats:bold>. Consequently, lazy programming language constructs do not fit the traditional mathematical mold inherent in<jats:bold>LPT<\/jats:bold>. A nonstrict (positive free) logic is required to handle nonstrict functions and predicates.<\/jats:p><jats:p>Previously developed nonstrict logics are not fully satisfactory because they are verbose in describing strict functions (which predominate in many programming languages), and some logicians find their semantics philosophically unpalatable. The newly developed Lazy Logic of Partial Terms<jats:bold>LL<\/jats:bold>is as concise as<jats:bold>LPT<\/jats:bold>in describing strict functions and predicates, and strict and nonstrict functions and predicates can be introduced in definitional extensions of traditional mathematical theories.<jats:bold>LL<\/jats:bold>is \u201cbuilt on top of\u201d<jats:bold>LPT<\/jats:bold>. and, like<jats:bold>LPT<\/jats:bold>, admits only one domain in the semantics. In the semantics, for the case of a nonstrict unary function<jats:italic>h<\/jats:italic>in an LL theory<jats:italic>T<\/jats:italic>, we have \u22a8<jats:sub>T<\/jats:sub><jats:italic>h<\/jats:italic>(\u22a5) =<jats:italic>y<\/jats:italic>\u2194 \u2200<jats:italic>x(h(x) = y)<\/jats:italic>, where \u22a5 is a canonical undefined term. Correspondingly, in the axiomatization, the \u201cindifference\u201d (to the value of the argument) axiom<jats:italic>h<\/jats:italic>(\u22a5) =<jats:italic>y<\/jats:italic>\u2194 \u2200<jats:italic>x(h(x) = y)<\/jats:italic>guarantees a proper fit with the semantics. The price paid for<jats:bold>LL<\/jats:bold>'s naturalness is that it is tailored for describing a specific area of computer science, program specification and verification, possibly limiting its role in explicating classical mathematical and philosophical subjects.<\/jats:p>","DOI":"10.2178\/jsl\/1190150149","type":"journal-article","created":{"date-parts":[[2007,12,13]],"date-time":"2007-12-13T19:14:26Z","timestamp":1197573266000},"page":"1065-1077","source":"Crossref","is-referenced-by-count":0,"title":["The lazy logic of partial terms"],"prefix":"10.1017","volume":"67","author":[{"given":"Raymond D.","family":"Gumb","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200009427_ref024","volume-title":"Logics without existence assumptions","author":"Schock","year":"1968"},{"key":"S0022481200009427_ref019","volume-title":"Free logics: Their foundations, character, and some applications thereof","author":"Lambert","year":"1997"},{"key":"S0022481200009427_ref027","volume-title":"Constructivity in mathematics","volume":"II","author":"Troelstra","year":"1988"},{"key":"S0022481200009427_ref021","doi-asserted-by":"publisher","DOI":"10.1109\/32.241769"},{"key":"S0022481200009427_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"S0022481200009427_ref011","unstructured":"ESPRIT CoFI Working Group, Cofi: The Common Framework Initiative for algebraic specification and development (various documents), Available at http:\/\/www.briks.dk\/Projects\/CoFI."},{"key":"S0022481200009427_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9"},{"key":"S0022481200009427_ref002","first-page":"51","volume-title":"Logic, methodology, and philosophy of science vii","author":"Beeson","year":"1985"},{"key":"S0022481200009427_ref020","volume-title":"Truth-value semantics","author":"Leblanc","year":"1976"},{"key":"S0022481200009427_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-5203-4_6"},{"key":"S0022481200009427_ref004","unstructured":"Burge Tyler , Truth and some referential devices, Ph.D. thesis , Princeton University, 1971."},{"key":"S0022481200009427_ref005","volume-title":"Model theory","author":"Chang","year":"1973"},{"key":"S0022481200009427_ref006","volume-title":"A mathematical introduction to logic","author":"Enderton","year":"2001"},{"key":"S0022481200009427_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/BF01135375"},{"key":"S0022481200009427_ref018","volume-title":"Philosophical applications of free logic","author":"Lambert","year":"1991"},{"key":"S0022481200009427_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/BF03024381"},{"key":"S0022481200009427_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BF01135376"},{"key":"S0022481200009427_ref012","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093882539"},{"key":"S0022481200009427_ref013","volume-title":"Programming logics: An introduction to verification and semantics","author":"Gumb","year":"1989"},{"key":"S0022481200009427_ref014","first-page":"717","volume":"59","author":"Gumb","year":"1994","journal-title":"Free arithmetic (abstract)"},{"key":"S0022481200009427_ref015","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/10722086_22","volume-title":"Automated reasoning with analytic tableaux and related methods, international conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 2000 proceedings","volume":"1847","author":"Gumb","year":"2000"},{"key":"S0022481200009427_ref016","doi-asserted-by":"publisher","DOI":"10.1023\/A:1013822008159"},{"key":"S0022481200009427_ref017","first-page":"435","article-title":"Definitions in nonstrict positive free logic","volume":"7","author":"Gumb","year":"1997","journal-title":"Modern Logic"},{"key":"S0022481200009427_ref022","unstructured":"Scales Ronald , Attribution and existence, Ph.D. thesis , University of California, Irvine, 1969."},{"key":"S0022481200009427_ref026","volume-title":"Introduction to logic","author":"Suppes","year":"1957"},{"key":"S0022481200009427_ref023","doi-asserted-by":"publisher","DOI":"10.1007\/BF01987833"},{"key":"S0022481200009427_ref025","volume-title":"Mathematical logic","author":"Schoenfield","year":"1967"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200009427","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,29]],"date-time":"2020-04-29T11:45:41Z","timestamp":1588160741000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200009427\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["S0022481200009427"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1190150149","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}