Virtual Evidence: A Constructive Semantics for Classical Logics

This article presents a computational semantics for classical logic using constructive type theory. Such semantics seems impossible because classical logic allows the Law of Excluded Middle (LEM), not accepted in constructive logic since it does not have computational meaning. However, the apparentl...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2014-08
Main Author: Constable, Robert L
Format: Article
Language:English
Subjects:
Computation
Construction standards
Logic
Semantics
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by
cites
container_end_page
container_issue
container_start_page
container_title arXiv.org
container_volume
creator Constable, Robert L
description This article presents a computational semantics for classical logic using constructive type theory. Such semantics seems impossible because classical logic allows the Law of Excluded Middle (LEM), not accepted in constructive logic since it does not have computational meaning. However, the apparently oracular powers expressed in the LEM, that for any proposition P either it or its negation, not P, is true can also be explained in terms of constructive evidence that does not refer to "oracles for truth." Types with virtual evidence and the constructive impossibility of negative evidence provide sufficient semantic grounds for classical truth and have a simple computational meaning. This idea is formalized using refinement types, a concept of constructive type theory used since 1984 and explained here. A new axiom creating virtual evidence fully retains the constructive meaning of the logical operators in classical contexts. Key Words: classical logic, constructive logic, intuitionistic logic, propositions-as-types, constructive type theory, refinement types, double negation translation, computational content, virtual evidence
format article
fullrecord <record><control><sourceid>proquest</sourceid><recordid>TN_cdi_proquest_journals_2084601151</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>2084601151</sourcerecordid><originalsourceid>FETCH-proquest_journals_20846011513</originalsourceid><addsrcrecordid>eNpjYuA0MjY21LUwMTLiYOAtLs4yMDAwMjM3MjU15mSwD8ssKilNzFFwLctMSc1LTrVScFRwzs8rLikqTS7JLEtVCE7NTcwryUwuVkjLL1JwzkksLs5MBmrwyU8HCvIwsKYl5hSn8kJpbgZlN9cQZw_dgqL8wtLU4pL4rPzSojygVLyRgYWJmYGhoamhMXGqANCNOEg</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>2084601151</pqid></control><display><type>article</type><title>Virtual Evidence: A Constructive Semantics for Classical Logics</title><source>Publicly Available Content Database</source><creator>Constable, Robert L</creator><creatorcontrib>Constable, Robert L</creatorcontrib><description>This article presents a computational semantics for classical logic using constructive type theory. Such semantics seems impossible because classical logic allows the Law of Excluded Middle (LEM), not accepted in constructive logic since it does not have computational meaning. However, the apparently oracular powers expressed in the LEM, that for any proposition P either it or its negation, not P, is true can also be explained in terms of constructive evidence that does not refer to "oracles for truth." Types with virtual evidence and the constructive impossibility of negative evidence provide sufficient semantic grounds for classical truth and have a simple computational meaning. This idea is formalized using refinement types, a concept of constructive type theory used since 1984 and explained here. A new axiom creating virtual evidence fully retains the constructive meaning of the logical operators in classical contexts. Key Words: classical logic, constructive logic, intuitionistic logic, propositions-as-types, constructive type theory, refinement types, double negation translation, computational content, virtual evidence</description><identifier>EISSN: 2331-8422</identifier><language>eng</language><publisher>Ithaca: Cornell University Library, arXiv.org</publisher><subject>Computation ; Construction standards ; Logic ; Semantics</subject><ispartof>arXiv.org, 2014-08</ispartof><rights>2014. This work is published under http://arxiv.org/licenses/nonexclusive-distrib/1.0/ (the “License”). Notwithstanding the ProQuest Terms and Conditions, you may use this content in accordance with the terms of the License.</rights><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktohtml>$$Uhttps://www.proquest.com/docview/2084601151?pq-origsite=primo$$EHTML$$P50$$Gproquest$$Hfree_for_read</linktohtml><link.rule.ids>780,784,25753,37012,44590</link.rule.ids></links><search><creatorcontrib>Constable, Robert L</creatorcontrib><title>Virtual Evidence: A Constructive Semantics for Classical Logics</title><title>arXiv.org</title><description>This article presents a computational semantics for classical logic using constructive type theory. Such semantics seems impossible because classical logic allows the Law of Excluded Middle (LEM), not accepted in constructive logic since it does not have computational meaning. However, the apparently oracular powers expressed in the LEM, that for any proposition P either it or its negation, not P, is true can also be explained in terms of constructive evidence that does not refer to "oracles for truth." Types with virtual evidence and the constructive impossibility of negative evidence provide sufficient semantic grounds for classical truth and have a simple computational meaning. This idea is formalized using refinement types, a concept of constructive type theory used since 1984 and explained here. A new axiom creating virtual evidence fully retains the constructive meaning of the logical operators in classical contexts. Key Words: classical logic, constructive logic, intuitionistic logic, propositions-as-types, constructive type theory, refinement types, double negation translation, computational content, virtual evidence</description><subject>Computation</subject><subject>Construction standards</subject><subject>Logic</subject><subject>Semantics</subject><issn>2331-8422</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2014</creationdate><recordtype>article</recordtype><sourceid>PIMPY</sourceid><recordid>eNpjYuA0MjY21LUwMTLiYOAtLs4yMDAwMjM3MjU15mSwD8ssKilNzFFwLctMSc1LTrVScFRwzs8rLikqTS7JLEtVCE7NTcwryUwuVkjLL1JwzkksLs5MBmrwyU8HCvIwsKYl5hSn8kJpbgZlN9cQZw_dgqL8wtLU4pL4rPzSojygVLyRgYWJmYGhoamhMXGqANCNOEg</recordid><startdate>20140831</startdate><enddate>20140831</enddate><creator>Constable, Robert L</creator><general>Cornell University Library, arXiv.org</general><scope>8FE</scope><scope>8FG</scope><scope>ABJCF</scope><scope>ABUWG</scope><scope>AFKRA</scope><scope>AZQEC</scope><scope>BENPR</scope><scope>BGLVJ</scope><scope>CCPQU</scope><scope>DWQXO</scope><scope>HCIFZ</scope><scope>L6V</scope><scope>M7S</scope><scope>PIMPY</scope><scope>PQEST</scope><scope>PQQKQ</scope><scope>PQUKI</scope><scope>PRINS</scope><scope>PTHSS</scope></search><sort><creationdate>20140831</creationdate><title>Virtual Evidence: A Constructive Semantics for Classical Logics</title><author>Constable, Robert L</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-proquest_journals_20846011513</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2014</creationdate><topic>Computation</topic><topic>Construction standards</topic><topic>Logic</topic><topic>Semantics</topic><toplevel>online_resources</toplevel><creatorcontrib>Constable, Robert L</creatorcontrib><collection>ProQuest SciTech Collection</collection><collection>ProQuest Technology Collection</collection><collection>Materials Science &amp; Engineering Collection</collection><collection>ProQuest Central (Alumni)</collection><collection>ProQuest Central</collection><collection>ProQuest Central Essentials</collection><collection>AUTh Library subscriptions: ProQuest Central</collection><collection>Technology Collection</collection><collection>ProQuest One Community College</collection><collection>ProQuest Central</collection><collection>SciTech Premium Collection</collection><collection>ProQuest Engineering Collection</collection><collection>Engineering Database</collection><collection>Publicly Available Content Database</collection><collection>ProQuest One Academic Eastern Edition (DO NOT USE)</collection><collection>ProQuest One Academic</collection><collection>ProQuest One Academic UKI Edition</collection><collection>ProQuest Central China</collection><collection>Engineering collection</collection></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Constable, Robert L</au><format>book</format><genre>document</genre><ristype>GEN</ristype><atitle>Virtual Evidence: A Constructive Semantics for Classical Logics</atitle><jtitle>arXiv.org</jtitle><date>2014-08-31</date><risdate>2014</risdate><eissn>2331-8422</eissn><abstract>This article presents a computational semantics for classical logic using constructive type theory. Such semantics seems impossible because classical logic allows the Law of Excluded Middle (LEM), not accepted in constructive logic since it does not have computational meaning. However, the apparently oracular powers expressed in the LEM, that for any proposition P either it or its negation, not P, is true can also be explained in terms of constructive evidence that does not refer to "oracles for truth." Types with virtual evidence and the constructive impossibility of negative evidence provide sufficient semantic grounds for classical truth and have a simple computational meaning. This idea is formalized using refinement types, a concept of constructive type theory used since 1984 and explained here. A new axiom creating virtual evidence fully retains the constructive meaning of the logical operators in classical contexts. Key Words: classical logic, constructive logic, intuitionistic logic, propositions-as-types, constructive type theory, refinement types, double negation translation, computational content, virtual evidence</abstract><cop>Ithaca</cop><pub>Cornell University Library, arXiv.org</pub><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier EISSN: 2331-8422
ispartof arXiv.org, 2014-08
issn 2331-8422
language eng
recordid cdi_proquest_journals_2084601151
source Publicly Available Content Database
subjects Computation
Construction standards
Logic
Semantics
title Virtual Evidence: A Constructive Semantics for Classical Logics
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-27T14%3A59%3A02IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest&rft_val_fmt=info:ofi/fmt:kev:mtx:book&rft.genre=document&rft.atitle=Virtual%20Evidence:%20A%20Constructive%20Semantics%20for%20Classical%20Logics&rft.jtitle=arXiv.org&rft.au=Constable,%20Robert%20L&rft.date=2014-08-31&rft.eissn=2331-8422&rft_id=info:doi/&rft_dat=%3Cproquest%3E2084601151%3C/proquest%3E%3Cgrp_id%3Ecdi_FETCH-proquest_journals_20846011513%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=2084601151&rft_id=info:pmid/&rfr_iscdi=true