CINXE.COM

(PDF) On the Provability Logic of Bounded Arithmetic

<!DOCTYPE html> <html > <head> <meta charset="utf-8"> <meta rel="search" type="application/opensearchdescription+xml" href="/open_search.xml" title="Academia.edu"> <meta content="width=device-width, initial-scale=1" name="viewport"> <meta name="google-site-verification" content="bKJMBZA7E43xhDOopFZkssMMkBRjvYERV-NaN4R6mrs"> <meta name="csrf-param" content="authenticity_token" /> <meta name="csrf-token" content="OfZfWsEKoCHnWJo4P0pUVdAWE0VhtST1QVYZFKOWsR4K1-PvR5oVHtslidPdhdKtWfhY1vnVz9M6_sE_OZStIQ" /> <meta name="citation_title" content="On the Provability Logic of Bounded Arithmetic" /> <meta name="citation_publication_date" content="1993/01/01" /> <meta name="citation_journal_title" content="Annals of Pure and Applied Logic" /> <meta name="citation_author" content="Rineke Verbrugge" /> <meta name="citation_author" content="Alessandro Berarducci" /> <meta name="twitter:card" content="summary" /> <meta name="twitter:url" content="https://www.academia.edu/2405515/On_the_Provability_Logic_of_Bounded_Arithmetic" /> <meta name="twitter:title" content="On the Provability Logic of Bounded Arithmetic" /> <meta name="twitter:description" content="A. and R. Verbrugge, On the provability logic of bounded arithmetic, Annals of Pure and Applied Logic 61 (1993) 75-93." /> <meta name="twitter:image" content="http://a.academia-assets.com/images/twitter-card.jpeg" /> <meta property="fb:app_id" content="2369844204" /> <meta property="og:type" content="article" /> <meta property="og:url" content="https://www.academia.edu/2405515/On_the_Provability_Logic_of_Bounded_Arithmetic" /> <meta property="og:title" content="On the Provability Logic of Bounded Arithmetic" /> <meta property="og:image" content="http://a.academia-assets.com/images/open-graph-icons/fb-paper.gif" /> <meta property="og:description" content="A. and R. Verbrugge, On the provability logic of bounded arithmetic, Annals of Pure and Applied Logic 61 (1993) 75-93." /> <meta property="article:author" content="https://rug.academia.edu/RinekeVerbrugge" /> <meta property="article:author" content="https://independent.academia.edu/AlessandroBerarducci" /> <meta name="description" content="A. and R. Verbrugge, On the provability logic of bounded arithmetic, Annals of Pure and Applied Logic 61 (1993) 75-93." /> <title>(PDF) On the Provability Logic of Bounded Arithmetic</title> <link rel="canonical" href="https://www.academia.edu/2405515/On_the_Provability_Logic_of_Bounded_Arithmetic" /> <script async src="https://www.googletagmanager.com/gtag/js?id=G-5VKX33P2DS"></script> <script> window.dataLayer = window.dataLayer || []; function gtag(){dataLayer.push(arguments);} gtag('js', new Date()); gtag('config', 'G-5VKX33P2DS', { cookie_domain: 'academia.edu', send_page_view: false, }); gtag('event', 'page_view', { 'controller': "single_work", 'action': "show", 'controller_action': 'single_work#show', 'logged_in': 'false', 'edge': 'unknown', // Send nil if there is no A/B test bucket, in case some records get logged // with missing data - that way we can distinguish between the two cases. // ab_test_bucket should be of the form <ab_test_name>:<bucket> 'ab_test_bucket': null, }) </script> <script> var $controller_name = 'single_work'; var $action_name = "show"; var $rails_env = 'production'; var $app_rev = 'e2ee979b3ba78bfbfccdcb914b329d3b1311d3c1'; var $domain = 'academia.edu'; var $app_host = "academia.edu"; var $asset_host = "academia-assets.com"; var $start_time = new Date().getTime(); var $recaptcha_key = "6LdxlRMTAAAAADnu_zyLhLg0YF9uACwz78shpjJB"; var $recaptcha_invisible_key = "6Lf3KHUUAAAAACggoMpmGJdQDtiyrjVlvGJ6BbAj"; var $disableClientRecordHit = false; </script> <script> window.require = { config: function() { return function() {} } } </script> <script> window.Aedu = window.Aedu || {}; window.Aedu.hit_data = null; window.Aedu.serverRenderTime = new Date(1741374868000); window.Aedu.timeDifference = new Date().getTime() - 1741374868000; </script> <script type="application/ld+json">{"@context":"https://schema.org","@type":"ScholarlyArticle","author":[{"@context":"https://schema.org","@type":"Person","name":"Rineke Verbrugge","url":"https://rug.academia.edu/RinekeVerbrugge","sameAs":[]},{"@context":"https://schema.org","@type":"Person","name":"Alessandro Berarducci","url":"https://independent.academia.edu/AlessandroBerarducci","image":"https://0.academia-photos.com/18337933/22540702/21734456/s200_alessandro.berarducci.jpg","sameAs":[]}],"contributor":[{"@context":"https://schema.org","@type":"Person","name":"Alessandro Berarducci","url":"https://independent.academia.edu/AlessandroBerarducci","image":"https://0.academia-photos.com/18337933/22540702/21734456/s200_alessandro.berarducci.jpg","sameAs":[]}],"dateCreated":"2013-01-15","datePublished":"1993-01-01","headline":"On the Provability Logic of Bounded Arithmetic","image":"https://attachments.academia-assets.com/50643683/thumbnails/1.jpg","inLanguage":"en","keywords":["Pure Mathematics","Bounded Arithmetic"],"publication":"Annals of Pure and Applied Logic","publisher":{"@context":"https://schema.org","@type":"Organization","name":null},"sourceOrganization":[{"@context":"https://schema.org","@type":"EducationalOrganization","name":"rug"},{"@context":"https://schema.org","@type":"EducationalOrganization","name":null}],"thumbnailUrl":"https://attachments.academia-assets.com/50643683/thumbnails/1.jpg","url":"https://www.academia.edu/2405515/On_the_Provability_Logic_of_Bounded_Arithmetic"}</script><style type="text/css">@media(max-width: 567px){:root{--token-mode: Rebrand;--dropshadow: 0 2px 4px 0 #22223340;--primary-brand: #0645b1;--error-dark: #b60000;--success-dark: #05b01c;--inactive-fill: #ebebee;--hover: #0c3b8d;--pressed: #082f75;--button-primary-fill-inactive: #ebebee;--button-primary-fill: #0645b1;--button-primary-text: #ffffff;--button-primary-fill-hover: #0c3b8d;--button-primary-fill-press: #082f75;--button-primary-icon: #ffffff;--button-primary-fill-inverse: #ffffff;--button-primary-text-inverse: #082f75;--button-primary-icon-inverse: #0645b1;--button-primary-fill-inverse-hover: #cddaef;--button-primary-stroke-inverse-pressed: #0645b1;--button-secondary-stroke-inactive: #b1b1ba;--button-secondary-fill: #eef2f9;--button-secondary-text: #082f75;--button-secondary-fill-press: #cddaef;--button-secondary-fill-inactive: #ebebee;--button-secondary-stroke: #cddaef;--button-secondary-stroke-hover: #386ac1;--button-secondary-stroke-press: #0645b1;--button-secondary-text-inactive: #b1b1ba;--button-secondary-icon: #082f75;--button-secondary-fill-hover: #e6ecf7;--button-secondary-stroke-inverse: #ffffff;--button-secondary-fill-inverse: rgba(255, 255, 255, 0);--button-secondary-icon-inverse: #ffffff;--button-secondary-icon-hover: #082f75;--button-secondary-icon-press: #082f75;--button-secondary-text-inverse: #ffffff;--button-secondary-text-hover: #082f75;--button-secondary-text-press: #082f75;--button-secondary-fill-inverse-hover: #043059;--button-xs-stroke: #141413;--button-xs-stroke-hover: #0c3b8d;--button-xs-stroke-press: #082f75;--button-xs-stroke-inactive: #ebebee;--button-xs-text: #141413;--button-xs-text-hover: #0c3b8d;--button-xs-text-press: #082f75;--button-xs-text-inactive: #91919e;--button-xs-icon: #141413;--button-xs-icon-hover: #0c3b8d;--button-xs-icon-press: #082f75;--button-xs-icon-inactive: #91919e;--button-xs-fill: #ffffff;--button-xs-fill-hover: #f4f7fc;--button-xs-fill-press: #eef2f9;--buttons-button-text-inactive: #91919e;--buttons-button-focus: #0645b1;--buttons-button-icon-inactive: #91919e;--buttons-small-buttons-corner-radius: 16px;--buttons-small-buttons-l-r-padding: 20px;--buttons-small-buttons-height: 48px;--buttons-small-buttons-gap: 8px;--buttons-small-buttons-icon-only-width: 48px;--buttons-small-buttons-icon-size: 20px;--buttons-small-buttons-stroke-default: 1px;--buttons-small-buttons-stroke-thick: 2px;--buttons-large-buttons-l-r-padding: 32px;--buttons-large-buttons-height: 64px;--buttons-large-buttons-icon-only-width: 64px;--buttons-large-buttons-icon-size: 20px;--buttons-large-buttons-gap: 8px;--buttons-large-buttons-corner-radius: 16px;--buttons-large-buttons-stroke-default: 1px;--buttons-large-buttons-stroke-thick: 2px;--buttons-extra-small-buttons-l-r-padding: 8px;--buttons-extra-small-buttons-height: 32px;--buttons-extra-small-buttons-icon-size: 16px;--buttons-extra-small-buttons-gap: 4px;--buttons-extra-small-buttons-corner-radius: 8px;--buttons-stroke-default: 1px;--buttons-stroke-thick: 2px;--background-beige: #f9f7f4;--error-light: #fff2f2;--text-placeholder: #6d6d7d;--stroke-dark: #141413;--stroke-light: #dddde2;--stroke-medium: #535366;--accent-green: #ccffd4;--accent-turquoise: #ccf7ff;--accent-yellow: #f7ffcc;--accent-peach: #ffd4cc;--accent-violet: #f7ccff;--accent-purple: #f4f7fc;--text-primary: #141413;--secondary-brand: #141413;--text-hover: #0c3b8d;--text-white: #ffffff;--text-link: #0645b1;--text-press: #082f75;--success-light: #f0f8f1;--background-light-blue: #f4f7fc;--background-white: #ffffff;--premium-dark: #877440;--premium-light: #f9f6ed;--stroke-white: #ffffff;--inactive-content: #b1b1ba;--annotate-light: #a35dff;--annotate-dark: #824acc;--grid: #eef2f9;--inactive-stroke: #ebebee;--shadow: rgba(34, 34, 51, 0.25);--text-inactive: #6d6d7d;--text-error: #b60000;--stroke-error: #b60000;--background-error: #fff2f2;--background-black: #141413;--icon-default: #141413;--icon-blue: #0645b1;--background-grey: #dddde2;--icon-grey: #b1b1ba;--text-focus: #082f75;--brand-colors-neutral-black: #141413;--brand-colors-neutral-900: #535366;--brand-colors-neutral-800: #6d6d7d;--brand-colors-neutral-700: #91919e;--brand-colors-neutral-600: #b1b1ba;--brand-colors-neutral-500: #c8c8cf;--brand-colors-neutral-400: #dddde2;--brand-colors-neutral-300: #ebebee;--brand-colors-neutral-200: #f8f8fb;--brand-colors-neutral-100: #fafafa;--brand-colors-neutral-white: #ffffff;--brand-colors-blue-900: #043059;--brand-colors-blue-800: #082f75;--brand-colors-blue-700: #0c3b8d;--brand-colors-blue-600: #0645b1;--brand-colors-blue-500: #386ac1;--brand-colors-blue-400: #cddaef;--brand-colors-blue-300: #e6ecf7;--brand-colors-blue-200: #eef2f9;--brand-colors-blue-100: #f4f7fc;--brand-colors-gold-500: #877440;--brand-colors-gold-400: #e9e3d4;--brand-colors-gold-300: #f2efe8;--brand-colors-gold-200: #f9f6ed;--brand-colors-gold-100: #f9f7f4;--brand-colors-error-900: #920000;--brand-colors-error-500: #b60000;--brand-colors-success-900: #035c0f;--brand-colors-green: #ccffd4;--brand-colors-turquoise: #ccf7ff;--brand-colors-yellow: #f7ffcc;--brand-colors-peach: #ffd4cc;--brand-colors-violet: #f7ccff;--brand-colors-error-100: #fff2f2;--brand-colors-success-500: #05b01c;--brand-colors-success-100: #f0f8f1;--text-secondary: #535366;--icon-white: #ffffff;--background-beige-darker: #f2efe8;--icon-dark-grey: #535366;--type-font-family-sans-serif: DM Sans;--type-font-family-serif: Gupter;--type-font-family-mono: IBM Plex Mono;--type-weights-300: 300;--type-weights-400: 400;--type-weights-500: 500;--type-weights-700: 700;--type-sizes-12: 12px;--type-sizes-14: 14px;--type-sizes-16: 16px;--type-sizes-18: 18px;--type-sizes-20: 20px;--type-sizes-22: 22px;--type-sizes-24: 24px;--type-sizes-28: 28px;--type-sizes-30: 30px;--type-sizes-32: 32px;--type-sizes-40: 40px;--type-sizes-42: 42px;--type-sizes-48-2: 48px;--type-line-heights-16: 16px;--type-line-heights-20: 20px;--type-line-heights-23: 23px;--type-line-heights-24: 24px;--type-line-heights-25: 25px;--type-line-heights-26: 26px;--type-line-heights-29: 29px;--type-line-heights-30: 30px;--type-line-heights-32: 32px;--type-line-heights-34: 34px;--type-line-heights-35: 35px;--type-line-heights-36: 36px;--type-line-heights-38: 38px;--type-line-heights-40: 40px;--type-line-heights-46: 46px;--type-line-heights-48: 48px;--type-line-heights-52: 52px;--type-line-heights-58: 58px;--type-line-heights-68: 68px;--type-line-heights-74: 74px;--type-line-heights-82: 82px;--type-paragraph-spacings-0: 0px;--type-paragraph-spacings-4: 4px;--type-paragraph-spacings-8: 8px;--type-paragraph-spacings-16: 16px;--type-sans-serif-xl-font-weight: 400;--type-sans-serif-xl-size: 32px;--type-sans-serif-xl-line-height: 46px;--type-sans-serif-xl-paragraph-spacing: 16px;--type-sans-serif-lg-font-weight: 400;--type-sans-serif-lg-size: 30px;--type-sans-serif-lg-line-height: 36px;--type-sans-serif-lg-paragraph-spacing: 16px;--type-sans-serif-md-font-weight: 400;--type-sans-serif-md-line-height: 30px;--type-sans-serif-md-paragraph-spacing: 16px;--type-sans-serif-md-size: 24px;--type-sans-serif-xs-font-weight: 700;--type-sans-serif-xs-line-height: 24px;--type-sans-serif-xs-paragraph-spacing: 0px;--type-sans-serif-xs-size: 18px;--type-sans-serif-sm-font-weight: 400;--type-sans-serif-sm-line-height: 32px;--type-sans-serif-sm-paragraph-spacing: 16px;--type-sans-serif-sm-size: 20px;--type-body-xl-font-weight: 400;--type-body-xl-size: 24px;--type-body-xl-line-height: 36px;--type-body-xl-paragraph-spacing: 0px;--type-body-sm-font-weight: 400;--type-body-sm-size: 14px;--type-body-sm-line-height: 20px;--type-body-sm-paragraph-spacing: 8px;--type-body-xs-font-weight: 400;--type-body-xs-size: 12px;--type-body-xs-line-height: 16px;--type-body-xs-paragraph-spacing: 0px;--type-body-md-font-weight: 400;--type-body-md-size: 16px;--type-body-md-line-height: 20px;--type-body-md-paragraph-spacing: 4px;--type-body-lg-font-weight: 400;--type-body-lg-size: 20px;--type-body-lg-line-height: 26px;--type-body-lg-paragraph-spacing: 16px;--type-body-lg-medium-font-weight: 500;--type-body-lg-medium-size: 20px;--type-body-lg-medium-line-height: 32px;--type-body-lg-medium-paragraph-spacing: 16px;--type-body-md-medium-font-weight: 500;--type-body-md-medium-size: 16px;--type-body-md-medium-line-height: 20px;--type-body-md-medium-paragraph-spacing: 4px;--type-body-sm-bold-font-weight: 700;--type-body-sm-bold-size: 14px;--type-body-sm-bold-line-height: 20px;--type-body-sm-bold-paragraph-spacing: 8px;--type-body-sm-medium-font-weight: 500;--type-body-sm-medium-size: 14px;--type-body-sm-medium-line-height: 20px;--type-body-sm-medium-paragraph-spacing: 8px;--type-serif-md-font-weight: 400;--type-serif-md-size: 32px;--type-serif-md-paragraph-spacing: 0px;--type-serif-md-line-height: 40px;--type-serif-sm-font-weight: 400;--type-serif-sm-size: 24px;--type-serif-sm-paragraph-spacing: 0px;--type-serif-sm-line-height: 26px;--type-serif-lg-font-weight: 400;--type-serif-lg-size: 48px;--type-serif-lg-paragraph-spacing: 0px;--type-serif-lg-line-height: 52px;--type-serif-xs-font-weight: 400;--type-serif-xs-size: 18px;--type-serif-xs-line-height: 24px;--type-serif-xs-paragraph-spacing: 0px;--type-serif-xl-font-weight: 400;--type-serif-xl-size: 48px;--type-serif-xl-paragraph-spacing: 0px;--type-serif-xl-line-height: 58px;--type-mono-md-font-weight: 400;--type-mono-md-size: 22px;--type-mono-md-line-height: 24px;--type-mono-md-paragraph-spacing: 0px;--type-mono-lg-font-weight: 400;--type-mono-lg-size: 40px;--type-mono-lg-line-height: 40px;--type-mono-lg-paragraph-spacing: 0px;--type-mono-sm-font-weight: 400;--type-mono-sm-size: 14px;--type-mono-sm-line-height: 24px;--type-mono-sm-paragraph-spacing: 0px;--spacing-xs-4: 4px;--spacing-xs-8: 8px;--spacing-xs-16: 16px;--spacing-sm-24: 24px;--spacing-sm-32: 32px;--spacing-md-40: 40px;--spacing-md-48: 48px;--spacing-lg-64: 64px;--spacing-lg-80: 80px;--spacing-xlg-104: 104px;--spacing-xlg-152: 152px;--spacing-xs-12: 12px;--spacing-page-section: 80px;--spacing-card-list-spacing: 48px;--spacing-text-section-spacing: 64px;--spacing-md-xs-headings: 40px;--corner-radius-radius-lg: 16px;--corner-radius-radius-sm: 4px;--corner-radius-radius-md: 8px;--corner-radius-radius-round: 104px}}@media(min-width: 568px)and (max-width: 1279px){:root{--token-mode: Rebrand;--dropshadow: 0 2px 4px 0 #22223340;--primary-brand: #0645b1;--error-dark: #b60000;--success-dark: #05b01c;--inactive-fill: #ebebee;--hover: #0c3b8d;--pressed: #082f75;--button-primary-fill-inactive: #ebebee;--button-primary-fill: #0645b1;--button-primary-text: #ffffff;--button-primary-fill-hover: #0c3b8d;--button-primary-fill-press: #082f75;--button-primary-icon: #ffffff;--button-primary-fill-inverse: #ffffff;--button-primary-text-inverse: #082f75;--button-primary-icon-inverse: #0645b1;--button-primary-fill-inverse-hover: #cddaef;--button-primary-stroke-inverse-pressed: #0645b1;--button-secondary-stroke-inactive: #b1b1ba;--button-secondary-fill: #eef2f9;--button-secondary-text: #082f75;--button-secondary-fill-press: #cddaef;--button-secondary-fill-inactive: #ebebee;--button-secondary-stroke: #cddaef;--button-secondary-stroke-hover: #386ac1;--button-secondary-stroke-press: #0645b1;--button-secondary-text-inactive: #b1b1ba;--button-secondary-icon: #082f75;--button-secondary-fill-hover: #e6ecf7;--button-secondary-stroke-inverse: #ffffff;--button-secondary-fill-inverse: rgba(255, 255, 255, 0);--button-secondary-icon-inverse: #ffffff;--button-secondary-icon-hover: #082f75;--button-secondary-icon-press: #082f75;--button-secondary-text-inverse: #ffffff;--button-secondary-text-hover: #082f75;--button-secondary-text-press: #082f75;--button-secondary-fill-inverse-hover: #043059;--button-xs-stroke: #141413;--button-xs-stroke-hover: #0c3b8d;--button-xs-stroke-press: #082f75;--button-xs-stroke-inactive: #ebebee;--button-xs-text: #141413;--button-xs-text-hover: #0c3b8d;--button-xs-text-press: #082f75;--button-xs-text-inactive: #91919e;--button-xs-icon: #141413;--button-xs-icon-hover: #0c3b8d;--button-xs-icon-press: #082f75;--button-xs-icon-inactive: #91919e;--button-xs-fill: #ffffff;--button-xs-fill-hover: #f4f7fc;--button-xs-fill-press: #eef2f9;--buttons-button-text-inactive: #91919e;--buttons-button-focus: #0645b1;--buttons-button-icon-inactive: #91919e;--buttons-small-buttons-corner-radius: 16px;--buttons-small-buttons-l-r-padding: 20px;--buttons-small-buttons-height: 48px;--buttons-small-buttons-gap: 8px;--buttons-small-buttons-icon-only-width: 48px;--buttons-small-buttons-icon-size: 20px;--buttons-small-buttons-stroke-default: 1px;--buttons-small-buttons-stroke-thick: 2px;--buttons-large-buttons-l-r-padding: 32px;--buttons-large-buttons-height: 64px;--buttons-large-buttons-icon-only-width: 64px;--buttons-large-buttons-icon-size: 20px;--buttons-large-buttons-gap: 8px;--buttons-large-buttons-corner-radius: 16px;--buttons-large-buttons-stroke-default: 1px;--buttons-large-buttons-stroke-thick: 2px;--buttons-extra-small-buttons-l-r-padding: 8px;--buttons-extra-small-buttons-height: 32px;--buttons-extra-small-buttons-icon-size: 16px;--buttons-extra-small-buttons-gap: 4px;--buttons-extra-small-buttons-corner-radius: 8px;--buttons-stroke-default: 1px;--buttons-stroke-thick: 2px;--background-beige: #f9f7f4;--error-light: #fff2f2;--text-placeholder: #6d6d7d;--stroke-dark: #141413;--stroke-light: #dddde2;--stroke-medium: #535366;--accent-green: #ccffd4;--accent-turquoise: #ccf7ff;--accent-yellow: #f7ffcc;--accent-peach: #ffd4cc;--accent-violet: #f7ccff;--accent-purple: #f4f7fc;--text-primary: #141413;--secondary-brand: #141413;--text-hover: #0c3b8d;--text-white: #ffffff;--text-link: #0645b1;--text-press: #082f75;--success-light: #f0f8f1;--background-light-blue: #f4f7fc;--background-white: #ffffff;--premium-dark: #877440;--premium-light: #f9f6ed;--stroke-white: #ffffff;--inactive-content: #b1b1ba;--annotate-light: #a35dff;--annotate-dark: #824acc;--grid: #eef2f9;--inactive-stroke: #ebebee;--shadow: rgba(34, 34, 51, 0.25);--text-inactive: #6d6d7d;--text-error: #b60000;--stroke-error: #b60000;--background-error: #fff2f2;--background-black: #141413;--icon-default: #141413;--icon-blue: #0645b1;--background-grey: #dddde2;--icon-grey: #b1b1ba;--text-focus: #082f75;--brand-colors-neutral-black: #141413;--brand-colors-neutral-900: #535366;--brand-colors-neutral-800: #6d6d7d;--brand-colors-neutral-700: #91919e;--brand-colors-neutral-600: #b1b1ba;--brand-colors-neutral-500: #c8c8cf;--brand-colors-neutral-400: #dddde2;--brand-colors-neutral-300: #ebebee;--brand-colors-neutral-200: #f8f8fb;--brand-colors-neutral-100: #fafafa;--brand-colors-neutral-white: #ffffff;--brand-colors-blue-900: #043059;--brand-colors-blue-800: #082f75;--brand-colors-blue-700: #0c3b8d;--brand-colors-blue-600: #0645b1;--brand-colors-blue-500: #386ac1;--brand-colors-blue-400: #cddaef;--brand-colors-blue-300: #e6ecf7;--brand-colors-blue-200: #eef2f9;--brand-colors-blue-100: #f4f7fc;--brand-colors-gold-500: #877440;--brand-colors-gold-400: #e9e3d4;--brand-colors-gold-300: #f2efe8;--brand-colors-gold-200: #f9f6ed;--brand-colors-gold-100: #f9f7f4;--brand-colors-error-900: #920000;--brand-colors-error-500: #b60000;--brand-colors-success-900: #035c0f;--brand-colors-green: #ccffd4;--brand-colors-turquoise: #ccf7ff;--brand-colors-yellow: #f7ffcc;--brand-colors-peach: #ffd4cc;--brand-colors-violet: #f7ccff;--brand-colors-error-100: #fff2f2;--brand-colors-success-500: #05b01c;--brand-colors-success-100: #f0f8f1;--text-secondary: #535366;--icon-white: #ffffff;--background-beige-darker: #f2efe8;--icon-dark-grey: #535366;--type-font-family-sans-serif: DM Sans;--type-font-family-serif: Gupter;--type-font-family-mono: IBM Plex Mono;--type-weights-300: 300;--type-weights-400: 400;--type-weights-500: 500;--type-weights-700: 700;--type-sizes-12: 12px;--type-sizes-14: 14px;--type-sizes-16: 16px;--type-sizes-18: 18px;--type-sizes-20: 20px;--type-sizes-22: 22px;--type-sizes-24: 24px;--type-sizes-28: 28px;--type-sizes-30: 30px;--type-sizes-32: 32px;--type-sizes-40: 40px;--type-sizes-42: 42px;--type-sizes-48-2: 48px;--type-line-heights-16: 16px;--type-line-heights-20: 20px;--type-line-heights-23: 23px;--type-line-heights-24: 24px;--type-line-heights-25: 25px;--type-line-heights-26: 26px;--type-line-heights-29: 29px;--type-line-heights-30: 30px;--type-line-heights-32: 32px;--type-line-heights-34: 34px;--type-line-heights-35: 35px;--type-line-heights-36: 36px;--type-line-heights-38: 38px;--type-line-heights-40: 40px;--type-line-heights-46: 46px;--type-line-heights-48: 48px;--type-line-heights-52: 52px;--type-line-heights-58: 58px;--type-line-heights-68: 68px;--type-line-heights-74: 74px;--type-line-heights-82: 82px;--type-paragraph-spacings-0: 0px;--type-paragraph-spacings-4: 4px;--type-paragraph-spacings-8: 8px;--type-paragraph-spacings-16: 16px;--type-sans-serif-xl-font-weight: 400;--type-sans-serif-xl-size: 42px;--type-sans-serif-xl-line-height: 46px;--type-sans-serif-xl-paragraph-spacing: 16px;--type-sans-serif-lg-font-weight: 400;--type-sans-serif-lg-size: 32px;--type-sans-serif-lg-line-height: 36px;--type-sans-serif-lg-paragraph-spacing: 16px;--type-sans-serif-md-font-weight: 400;--type-sans-serif-md-line-height: 34px;--type-sans-serif-md-paragraph-spacing: 16px;--type-sans-serif-md-size: 28px;--type-sans-serif-xs-font-weight: 700;--type-sans-serif-xs-line-height: 25px;--type-sans-serif-xs-paragraph-spacing: 0px;--type-sans-serif-xs-size: 20px;--type-sans-serif-sm-font-weight: 400;--type-sans-serif-sm-line-height: 30px;--type-sans-serif-sm-paragraph-spacing: 16px;--type-sans-serif-sm-size: 24px;--type-body-xl-font-weight: 400;--type-body-xl-size: 24px;--type-body-xl-line-height: 36px;--type-body-xl-paragraph-spacing: 0px;--type-body-sm-font-weight: 400;--type-body-sm-size: 14px;--type-body-sm-line-height: 20px;--type-body-sm-paragraph-spacing: 8px;--type-body-xs-font-weight: 400;--type-body-xs-size: 12px;--type-body-xs-line-height: 16px;--type-body-xs-paragraph-spacing: 0px;--type-body-md-font-weight: 400;--type-body-md-size: 16px;--type-body-md-line-height: 20px;--type-body-md-paragraph-spacing: 4px;--type-body-lg-font-weight: 400;--type-body-lg-size: 20px;--type-body-lg-line-height: 26px;--type-body-lg-paragraph-spacing: 16px;--type-body-lg-medium-font-weight: 500;--type-body-lg-medium-size: 20px;--type-body-lg-medium-line-height: 32px;--type-body-lg-medium-paragraph-spacing: 16px;--type-body-md-medium-font-weight: 500;--type-body-md-medium-size: 16px;--type-body-md-medium-line-height: 20px;--type-body-md-medium-paragraph-spacing: 4px;--type-body-sm-bold-font-weight: 700;--type-body-sm-bold-size: 14px;--type-body-sm-bold-line-height: 20px;--type-body-sm-bold-paragraph-spacing: 8px;--type-body-sm-medium-font-weight: 500;--type-body-sm-medium-size: 14px;--type-body-sm-medium-line-height: 20px;--type-body-sm-medium-paragraph-spacing: 8px;--type-serif-md-font-weight: 400;--type-serif-md-size: 40px;--type-serif-md-paragraph-spacing: 0px;--type-serif-md-line-height: 48px;--type-serif-sm-font-weight: 400;--type-serif-sm-size: 28px;--type-serif-sm-paragraph-spacing: 0px;--type-serif-sm-line-height: 32px;--type-serif-lg-font-weight: 400;--type-serif-lg-size: 58px;--type-serif-lg-paragraph-spacing: 0px;--type-serif-lg-line-height: 68px;--type-serif-xs-font-weight: 400;--type-serif-xs-size: 18px;--type-serif-xs-line-height: 24px;--type-serif-xs-paragraph-spacing: 0px;--type-serif-xl-font-weight: 400;--type-serif-xl-size: 74px;--type-serif-xl-paragraph-spacing: 0px;--type-serif-xl-line-height: 82px;--type-mono-md-font-weight: 400;--type-mono-md-size: 22px;--type-mono-md-line-height: 24px;--type-mono-md-paragraph-spacing: 0px;--type-mono-lg-font-weight: 400;--type-mono-lg-size: 40px;--type-mono-lg-line-height: 40px;--type-mono-lg-paragraph-spacing: 0px;--type-mono-sm-font-weight: 400;--type-mono-sm-size: 14px;--type-mono-sm-line-height: 24px;--type-mono-sm-paragraph-spacing: 0px;--spacing-xs-4: 4px;--spacing-xs-8: 8px;--spacing-xs-16: 16px;--spacing-sm-24: 24px;--spacing-sm-32: 32px;--spacing-md-40: 40px;--spacing-md-48: 48px;--spacing-lg-64: 64px;--spacing-lg-80: 80px;--spacing-xlg-104: 104px;--spacing-xlg-152: 152px;--spacing-xs-12: 12px;--spacing-page-section: 104px;--spacing-card-list-spacing: 48px;--spacing-text-section-spacing: 80px;--spacing-md-xs-headings: 40px;--corner-radius-radius-lg: 16px;--corner-radius-radius-sm: 4px;--corner-radius-radius-md: 8px;--corner-radius-radius-round: 104px}}@media(min-width: 1280px){:root{--token-mode: Rebrand;--dropshadow: 0 2px 4px 0 #22223340;--primary-brand: #0645b1;--error-dark: #b60000;--success-dark: #05b01c;--inactive-fill: #ebebee;--hover: #0c3b8d;--pressed: #082f75;--button-primary-fill-inactive: #ebebee;--button-primary-fill: #0645b1;--button-primary-text: #ffffff;--button-primary-fill-hover: #0c3b8d;--button-primary-fill-press: #082f75;--button-primary-icon: #ffffff;--button-primary-fill-inverse: #ffffff;--button-primary-text-inverse: #082f75;--button-primary-icon-inverse: #0645b1;--button-primary-fill-inverse-hover: #cddaef;--button-primary-stroke-inverse-pressed: #0645b1;--button-secondary-stroke-inactive: #b1b1ba;--button-secondary-fill: #eef2f9;--button-secondary-text: #082f75;--button-secondary-fill-press: #cddaef;--button-secondary-fill-inactive: #ebebee;--button-secondary-stroke: #cddaef;--button-secondary-stroke-hover: #386ac1;--button-secondary-stroke-press: #0645b1;--button-secondary-text-inactive: #b1b1ba;--button-secondary-icon: #082f75;--button-secondary-fill-hover: #e6ecf7;--button-secondary-stroke-inverse: #ffffff;--button-secondary-fill-inverse: rgba(255, 255, 255, 0);--button-secondary-icon-inverse: #ffffff;--button-secondary-icon-hover: #082f75;--button-secondary-icon-press: #082f75;--button-secondary-text-inverse: #ffffff;--button-secondary-text-hover: #082f75;--button-secondary-text-press: #082f75;--button-secondary-fill-inverse-hover: #043059;--button-xs-stroke: #141413;--button-xs-stroke-hover: #0c3b8d;--button-xs-stroke-press: #082f75;--button-xs-stroke-inactive: #ebebee;--button-xs-text: #141413;--button-xs-text-hover: #0c3b8d;--button-xs-text-press: #082f75;--button-xs-text-inactive: #91919e;--button-xs-icon: #141413;--button-xs-icon-hover: #0c3b8d;--button-xs-icon-press: #082f75;--button-xs-icon-inactive: #91919e;--button-xs-fill: #ffffff;--button-xs-fill-hover: #f4f7fc;--button-xs-fill-press: #eef2f9;--buttons-button-text-inactive: #91919e;--buttons-button-focus: #0645b1;--buttons-button-icon-inactive: #91919e;--buttons-small-buttons-corner-radius: 16px;--buttons-small-buttons-l-r-padding: 20px;--buttons-small-buttons-height: 48px;--buttons-small-buttons-gap: 8px;--buttons-small-buttons-icon-only-width: 48px;--buttons-small-buttons-icon-size: 20px;--buttons-small-buttons-stroke-default: 1px;--buttons-small-buttons-stroke-thick: 2px;--buttons-large-buttons-l-r-padding: 32px;--buttons-large-buttons-height: 64px;--buttons-large-buttons-icon-only-width: 64px;--buttons-large-buttons-icon-size: 20px;--buttons-large-buttons-gap: 8px;--buttons-large-buttons-corner-radius: 16px;--buttons-large-buttons-stroke-default: 1px;--buttons-large-buttons-stroke-thick: 2px;--buttons-extra-small-buttons-l-r-padding: 8px;--buttons-extra-small-buttons-height: 32px;--buttons-extra-small-buttons-icon-size: 16px;--buttons-extra-small-buttons-gap: 4px;--buttons-extra-small-buttons-corner-radius: 8px;--buttons-stroke-default: 1px;--buttons-stroke-thick: 2px;--background-beige: #f9f7f4;--error-light: #fff2f2;--text-placeholder: #6d6d7d;--stroke-dark: #141413;--stroke-light: #dddde2;--stroke-medium: #535366;--accent-green: #ccffd4;--accent-turquoise: #ccf7ff;--accent-yellow: #f7ffcc;--accent-peach: #ffd4cc;--accent-violet: #f7ccff;--accent-purple: #f4f7fc;--text-primary: #141413;--secondary-brand: #141413;--text-hover: #0c3b8d;--text-white: #ffffff;--text-link: #0645b1;--text-press: #082f75;--success-light: #f0f8f1;--background-light-blue: #f4f7fc;--background-white: #ffffff;--premium-dark: #877440;--premium-light: #f9f6ed;--stroke-white: #ffffff;--inactive-content: #b1b1ba;--annotate-light: #a35dff;--annotate-dark: #824acc;--grid: #eef2f9;--inactive-stroke: #ebebee;--shadow: rgba(34, 34, 51, 0.25);--text-inactive: #6d6d7d;--text-error: #b60000;--stroke-error: #b60000;--background-error: #fff2f2;--background-black: #141413;--icon-default: #141413;--icon-blue: #0645b1;--background-grey: #dddde2;--icon-grey: #b1b1ba;--text-focus: #082f75;--brand-colors-neutral-black: #141413;--brand-colors-neutral-900: #535366;--brand-colors-neutral-800: #6d6d7d;--brand-colors-neutral-700: #91919e;--brand-colors-neutral-600: #b1b1ba;--brand-colors-neutral-500: #c8c8cf;--brand-colors-neutral-400: #dddde2;--brand-colors-neutral-300: #ebebee;--brand-colors-neutral-200: #f8f8fb;--brand-colors-neutral-100: #fafafa;--brand-colors-neutral-white: #ffffff;--brand-colors-blue-900: #043059;--brand-colors-blue-800: #082f75;--brand-colors-blue-700: #0c3b8d;--brand-colors-blue-600: #0645b1;--brand-colors-blue-500: #386ac1;--brand-colors-blue-400: #cddaef;--brand-colors-blue-300: #e6ecf7;--brand-colors-blue-200: #eef2f9;--brand-colors-blue-100: #f4f7fc;--brand-colors-gold-500: #877440;--brand-colors-gold-400: #e9e3d4;--brand-colors-gold-300: #f2efe8;--brand-colors-gold-200: #f9f6ed;--brand-colors-gold-100: #f9f7f4;--brand-colors-error-900: #920000;--brand-colors-error-500: #b60000;--brand-colors-success-900: #035c0f;--brand-colors-green: #ccffd4;--brand-colors-turquoise: #ccf7ff;--brand-colors-yellow: #f7ffcc;--brand-colors-peach: #ffd4cc;--brand-colors-violet: #f7ccff;--brand-colors-error-100: #fff2f2;--brand-colors-success-500: #05b01c;--brand-colors-success-100: #f0f8f1;--text-secondary: #535366;--icon-white: #ffffff;--background-beige-darker: #f2efe8;--icon-dark-grey: #535366;--type-font-family-sans-serif: DM Sans;--type-font-family-serif: Gupter;--type-font-family-mono: IBM Plex Mono;--type-weights-300: 300;--type-weights-400: 400;--type-weights-500: 500;--type-weights-700: 700;--type-sizes-12: 12px;--type-sizes-14: 14px;--type-sizes-16: 16px;--type-sizes-18: 18px;--type-sizes-20: 20px;--type-sizes-22: 22px;--type-sizes-24: 24px;--type-sizes-28: 28px;--type-sizes-30: 30px;--type-sizes-32: 32px;--type-sizes-40: 40px;--type-sizes-42: 42px;--type-sizes-48-2: 48px;--type-line-heights-16: 16px;--type-line-heights-20: 20px;--type-line-heights-23: 23px;--type-line-heights-24: 24px;--type-line-heights-25: 25px;--type-line-heights-26: 26px;--type-line-heights-29: 29px;--type-line-heights-30: 30px;--type-line-heights-32: 32px;--type-line-heights-34: 34px;--type-line-heights-35: 35px;--type-line-heights-36: 36px;--type-line-heights-38: 38px;--type-line-heights-40: 40px;--type-line-heights-46: 46px;--type-line-heights-48: 48px;--type-line-heights-52: 52px;--type-line-heights-58: 58px;--type-line-heights-68: 68px;--type-line-heights-74: 74px;--type-line-heights-82: 82px;--type-paragraph-spacings-0: 0px;--type-paragraph-spacings-4: 4px;--type-paragraph-spacings-8: 8px;--type-paragraph-spacings-16: 16px;--type-sans-serif-xl-font-weight: 400;--type-sans-serif-xl-size: 42px;--type-sans-serif-xl-line-height: 46px;--type-sans-serif-xl-paragraph-spacing: 16px;--type-sans-serif-lg-font-weight: 400;--type-sans-serif-lg-size: 32px;--type-sans-serif-lg-line-height: 38px;--type-sans-serif-lg-paragraph-spacing: 16px;--type-sans-serif-md-font-weight: 400;--type-sans-serif-md-line-height: 34px;--type-sans-serif-md-paragraph-spacing: 16px;--type-sans-serif-md-size: 28px;--type-sans-serif-xs-font-weight: 700;--type-sans-serif-xs-line-height: 25px;--type-sans-serif-xs-paragraph-spacing: 0px;--type-sans-serif-xs-size: 20px;--type-sans-serif-sm-font-weight: 400;--type-sans-serif-sm-line-height: 30px;--type-sans-serif-sm-paragraph-spacing: 16px;--type-sans-serif-sm-size: 24px;--type-body-xl-font-weight: 400;--type-body-xl-size: 24px;--type-body-xl-line-height: 36px;--type-body-xl-paragraph-spacing: 0px;--type-body-sm-font-weight: 400;--type-body-sm-size: 14px;--type-body-sm-line-height: 20px;--type-body-sm-paragraph-spacing: 8px;--type-body-xs-font-weight: 400;--type-body-xs-size: 12px;--type-body-xs-line-height: 16px;--type-body-xs-paragraph-spacing: 0px;--type-body-md-font-weight: 400;--type-body-md-size: 16px;--type-body-md-line-height: 20px;--type-body-md-paragraph-spacing: 4px;--type-body-lg-font-weight: 400;--type-body-lg-size: 20px;--type-body-lg-line-height: 26px;--type-body-lg-paragraph-spacing: 16px;--type-body-lg-medium-font-weight: 500;--type-body-lg-medium-size: 20px;--type-body-lg-medium-line-height: 32px;--type-body-lg-medium-paragraph-spacing: 16px;--type-body-md-medium-font-weight: 500;--type-body-md-medium-size: 16px;--type-body-md-medium-line-height: 20px;--type-body-md-medium-paragraph-spacing: 4px;--type-body-sm-bold-font-weight: 700;--type-body-sm-bold-size: 14px;--type-body-sm-bold-line-height: 20px;--type-body-sm-bold-paragraph-spacing: 8px;--type-body-sm-medium-font-weight: 500;--type-body-sm-medium-size: 14px;--type-body-sm-medium-line-height: 20px;--type-body-sm-medium-paragraph-spacing: 8px;--type-serif-md-font-weight: 400;--type-serif-md-size: 40px;--type-serif-md-paragraph-spacing: 0px;--type-serif-md-line-height: 48px;--type-serif-sm-font-weight: 400;--type-serif-sm-size: 28px;--type-serif-sm-paragraph-spacing: 0px;--type-serif-sm-line-height: 32px;--type-serif-lg-font-weight: 400;--type-serif-lg-size: 58px;--type-serif-lg-paragraph-spacing: 0px;--type-serif-lg-line-height: 68px;--type-serif-xs-font-weight: 400;--type-serif-xs-size: 18px;--type-serif-xs-line-height: 24px;--type-serif-xs-paragraph-spacing: 0px;--type-serif-xl-font-weight: 400;--type-serif-xl-size: 74px;--type-serif-xl-paragraph-spacing: 0px;--type-serif-xl-line-height: 82px;--type-mono-md-font-weight: 400;--type-mono-md-size: 22px;--type-mono-md-line-height: 24px;--type-mono-md-paragraph-spacing: 0px;--type-mono-lg-font-weight: 400;--type-mono-lg-size: 40px;--type-mono-lg-line-height: 40px;--type-mono-lg-paragraph-spacing: 0px;--type-mono-sm-font-weight: 400;--type-mono-sm-size: 14px;--type-mono-sm-line-height: 24px;--type-mono-sm-paragraph-spacing: 0px;--spacing-xs-4: 4px;--spacing-xs-8: 8px;--spacing-xs-16: 16px;--spacing-sm-24: 24px;--spacing-sm-32: 32px;--spacing-md-40: 40px;--spacing-md-48: 48px;--spacing-lg-64: 64px;--spacing-lg-80: 80px;--spacing-xlg-104: 104px;--spacing-xlg-152: 152px;--spacing-xs-12: 12px;--spacing-page-section: 152px;--spacing-card-list-spacing: 48px;--spacing-text-section-spacing: 80px;--spacing-md-xs-headings: 40px;--corner-radius-radius-lg: 16px;--corner-radius-radius-sm: 4px;--corner-radius-radius-md: 8px;--corner-radius-radius-round: 104px}}</style><link rel="stylesheet" media="all" href="//a.academia-assets.com/assets/single_work_page/loswp-369df59c8124f51e480079869c157eba45d12fcd3f65e2af6d7f44b33daec50d.css" /><link rel="stylesheet" media="all" href="//a.academia-assets.com/assets/design_system/body-170d1319f0e354621e81ca17054bb147da2856ec0702fe440a99af314a6338c5.css" /><link rel="stylesheet" media="all" href="//a.academia-assets.com/assets/design_system/button-8c9ae4b5c8a2531640c354d92a1f3579c8ff103277ef74913e34c8a76d4e6c00.css" /><link rel="stylesheet" media="all" href="//a.academia-assets.com/assets/design_system/heading-95367dc03b794f6737f30123738a886cf53b7a65cdef98a922a98591d60063e3.css" /><link rel="stylesheet" media="all" href="//a.academia-assets.com/assets/design_system/text_button-d1941ab08e91e29ee143084c4749da4aaffa350a2ac6eec2306b1d7a352d911a.css" /><link crossorigin="" href="https://fonts.gstatic.com/" rel="preconnect" /><link href="https://fonts.googleapis.com/css2?family=DM+Sans:ital,opsz,wght@0,9..40,100..1000;1,9..40,100..1000&amp;family=Gupter:wght@400;500;700&amp;family=IBM+Plex+Mono:wght@300;400&amp;family=Material+Symbols+Outlined:opsz,wght,FILL,GRAD@20,400,0,0&amp;display=swap" rel="stylesheet" /><link rel="stylesheet" media="all" href="//a.academia-assets.com/assets/design_system/common-57f9da13cef3fd4e2a8b655342c6488eded3e557e823fe67571f2ac77acd7b6f.css" /> </head> <body> <div id='react-modal'></div> <div class="js-upgrade-ie-banner" style="display: none; text-align: center; padding: 8px 0; background-color: #ebe480;"><p style="color: #000; font-size: 12px; margin: 0 0 4px;">Academia.edu no longer supports Internet Explorer.</p><p style="color: #000; font-size: 12px; margin: 0;">To browse Academia.edu and the wider internet faster and more securely, please take a few seconds to&nbsp;<a href="https://www.academia.edu/upgrade-browser">upgrade your browser</a>.</p></div><script>// Show this banner for all versions of IE if (!!window.MSInputMethodContext || /(MSIE)/.test(navigator.userAgent)) { document.querySelector('.js-upgrade-ie-banner').style.display = 'block'; }</script> <div class="bootstrap login"><div class="modal fade login-modal" id="login-modal"><div class="login-modal-dialog modal-dialog"><div class="modal-content"><div class="modal-header"><button class="close close" data-dismiss="modal" type="button"><span aria-hidden="true">&times;</span><span class="sr-only">Close</span></button><h4 class="modal-title text-center"><strong>Log In</strong></h4></div><div class="modal-body"><div class="row"><div class="col-xs-10 col-xs-offset-1"><button class="btn btn-fb btn-lg btn-block btn-v-center-content" id="login-facebook-oauth-button"><svg style="float: left; width: 19px; line-height: 1em; margin-right: .3em;" aria-hidden="true" focusable="false" data-prefix="fab" data-icon="facebook-square" class="svg-inline--fa fa-facebook-square fa-w-14" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 448 512"><path fill="currentColor" d="M400 32H48A48 48 0 0 0 0 80v352a48 48 0 0 0 48 48h137.25V327.69h-63V256h63v-54.64c0-62.15 37-96.48 93.67-96.48 27.14 0 55.52 4.84 55.52 4.84v61h-31.27c-30.81 0-40.42 19.12-40.42 38.73V256h68.78l-11 71.69h-57.78V480H400a48 48 0 0 0 48-48V80a48 48 0 0 0-48-48z"></path></svg><small><strong>Log in</strong> with <strong>Facebook</strong></small></button><br /><button class="btn btn-google btn-lg btn-block btn-v-center-content" id="login-google-oauth-button"><svg style="float: left; width: 22px; line-height: 1em; margin-right: .3em;" aria-hidden="true" focusable="false" data-prefix="fab" data-icon="google-plus" class="svg-inline--fa fa-google-plus fa-w-16" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M256,8C119.1,8,8,119.1,8,256S119.1,504,256,504,504,392.9,504,256,392.9,8,256,8ZM185.3,380a124,124,0,0,1,0-248c31.3,0,60.1,11,83,32.3l-33.6,32.6c-13.2-12.9-31.3-19.1-49.4-19.1-42.9,0-77.2,35.5-77.2,78.1S142.3,334,185.3,334c32.6,0,64.9-19.1,70.1-53.3H185.3V238.1H302.2a109.2,109.2,0,0,1,1.9,20.7c0,70.8-47.5,121.2-118.8,121.2ZM415.5,273.8v35.5H380V273.8H344.5V238.3H380V202.8h35.5v35.5h35.2v35.5Z"></path></svg><small><strong>Log in</strong> with <strong>Google</strong></small></button><br /><style type="text/css">.sign-in-with-apple-button { width: 100%; height: 52px; border-radius: 3px; border: 1px solid black; cursor: pointer; } .sign-in-with-apple-button > div { margin: 0 auto; / This centers the Apple-rendered button horizontally }</style><script src="https://appleid.cdn-apple.com/appleauth/static/jsapi/appleid/1/en_US/appleid.auth.js" type="text/javascript"></script><div class="sign-in-with-apple-button" data-border="false" data-color="white" id="appleid-signin"><span &nbsp;&nbsp;="Sign Up with Apple" class="u-fs11"></span></div><script>AppleID.auth.init({ clientId: 'edu.academia.applesignon', scope: 'name email', redirectURI: 'https://www.academia.edu/sessions', state: "fea1e5dd9f78db239cd3ddeb10df1d09e415f4d830e3509c377944cc9b99d6c2", });</script><script>// Hacky way of checking if on fast loswp if (window.loswp == null) { (function() { const Google = window?.Aedu?.Auth?.OauthButton?.Login?.Google; const Facebook = window?.Aedu?.Auth?.OauthButton?.Login?.Facebook; if (Google) { new Google({ el: '#login-google-oauth-button', rememberMeCheckboxId: 'remember_me', track: null }); } if (Facebook) { new Facebook({ el: '#login-facebook-oauth-button', rememberMeCheckboxId: 'remember_me', track: null }); } })(); }</script></div></div></div><div class="modal-body"><div class="row"><div class="col-xs-10 col-xs-offset-1"><div class="hr-heading login-hr-heading"><span class="hr-heading-text">or</span></div></div></div></div><div class="modal-body"><div class="row"><div class="col-xs-10 col-xs-offset-1"><form class="js-login-form" action="https://www.academia.edu/sessions" accept-charset="UTF-8" method="post"><input type="hidden" name="authenticity_token" value="MinbqeWgUwxv2Sf3D1SW_3ItiqLYvkwqXrYsjcRqicIBCGccYzDmM1OkNBztmxAH-8PBMUDepwwlHvSmXmiV_Q" autocomplete="off" /><div class="form-group"><label class="control-label" for="login-modal-email-input" style="font-size: 14px;">Email</label><input class="form-control" id="login-modal-email-input" name="login" type="email" /></div><div class="form-group"><label class="control-label" for="login-modal-password-input" style="font-size: 14px;">Password</label><input class="form-control" id="login-modal-password-input" name="password" type="password" /></div><input type="hidden" name="post_login_redirect_url" id="post_login_redirect_url" value="https://www.academia.edu/2405515/On_the_Provability_Logic_of_Bounded_Arithmetic" autocomplete="off" /><div class="checkbox"><label><input type="checkbox" name="remember_me" id="remember_me" value="1" checked="checked" /><small style="font-size: 12px; margin-top: 2px; display: inline-block;">Remember me on this computer</small></label></div><br><input type="submit" name="commit" value="Log In" class="btn btn-primary btn-block btn-lg js-login-submit" data-disable-with="Log In" /></br></form><script>typeof window?.Aedu?.recaptchaManagedForm === 'function' && window.Aedu.recaptchaManagedForm( document.querySelector('.js-login-form'), document.querySelector('.js-login-submit') );</script><small style="font-size: 12px;"><br />or <a data-target="#login-modal-reset-password-container" data-toggle="collapse" href="javascript:void(0)">reset password</a></small><div class="collapse" id="login-modal-reset-password-container"><br /><div class="well margin-0x"><form class="js-password-reset-form" action="https://www.academia.edu/reset_password" accept-charset="UTF-8" method="post"><input type="hidden" name="authenticity_token" value="9ZphM2FXiP8QjnRRrNd22pEjml2gtxtBBkk5QYUyzSTGu92G58c9wCzzZ7pOGPAiGM3RzjjX8Gd94eFqHzDRGw" autocomplete="off" /><p>Enter the email address you signed up with and we&#39;ll email you a reset link.</p><div class="form-group"><input class="form-control" name="email" type="email" /></div><input class="btn btn-primary btn-block g-recaptcha js-password-reset-submit" data-sitekey="6Lf3KHUUAAAAACggoMpmGJdQDtiyrjVlvGJ6BbAj" type="submit" value="Email me a link" /></form></div></div><script> require.config({ waitSeconds: 90 })(["https://a.academia-assets.com/assets/collapse-45805421cf446ca5adf7aaa1935b08a3a8d1d9a6cc5d91a62a2a3a00b20b3e6a.js"], function() { // from javascript_helper.rb $("#login-modal-reset-password-container").on("shown.bs.collapse", function() { $(this).find("input[type=email]").focus(); }); }); </script> </div></div></div><div class="modal-footer"><div class="text-center"><small style="font-size: 12px;">Need an account?&nbsp;<a rel="nofollow" href="https://www.academia.edu/signup">Click here to sign up</a></small></div></div></div></div></div></div><script>// If we are on subdomain or non-bootstrapped page, redirect to login page instead of showing modal (function(){ if (typeof $ === 'undefined') return; var host = window.location.hostname; if ((host === $domain || host === "www."+$domain) && (typeof $().modal === 'function')) { $("#nav_log_in").click(function(e) { // Don't follow the link and open the modal e.preventDefault(); $("#login-modal").on('shown.bs.modal', function() { $(this).find("#login-modal-email-input").focus() }).modal('show'); }); } })()</script> <div id="fb-root"></div><script>window.fbAsyncInit = function() { FB.init({ appId: "2369844204", version: "v8.0", status: true, cookie: true, xfbml: true }); // Additional initialization code. if (window.InitFacebook) { // facebook.ts already loaded, set it up. window.InitFacebook(); } else { // Set a flag for facebook.ts to find when it loads. window.academiaAuthReadyFacebook = true; } };</script> <div id="google-root"></div><script>window.loadGoogle = function() { if (window.InitGoogle) { // google.ts already loaded, set it up. window.InitGoogle("331998490334-rsn3chp12mbkiqhl6e7lu2q0mlbu0f1b"); } else { // Set a flag for google.ts to use when it loads. window.GoogleClientID = "331998490334-rsn3chp12mbkiqhl6e7lu2q0mlbu0f1b"; } };</script> <div class="header--container" id="main-header-container"><div class="header--inner-container header--inner-container-ds2"><div class="header-ds2--left-wrapper"><div class="header-ds2--left-wrapper-inner"><a data-main-header-link-target="logo_home" href="https://www.academia.edu/"><img class="hide-on-desktop-redesign" style="height: 24px; width: 24px;" alt="Academia.edu" src="//a.academia-assets.com/images/academia-logo-redesign-2015-A.svg" width="24" height="24" /><img width="145.2" height="18" class="hide-on-mobile-redesign" style="height: 24px;" alt="Academia.edu" src="//a.academia-assets.com/images/academia-logo-redesign-2015.svg" /></a><div class="header--search-container header--search-container-ds2"><form class="js-SiteSearch-form select2-no-default-pills" action="https://www.academia.edu/search" accept-charset="UTF-8" method="get"><svg style="width: 14px; height: 14px;" aria-hidden="true" focusable="false" data-prefix="fas" data-icon="search" class="header--search-icon svg-inline--fa fa-search fa-w-16" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M505 442.7L405.3 343c-4.5-4.5-10.6-7-17-7H372c27.6-35.3 44-79.7 44-128C416 93.1 322.9 0 208 0S0 93.1 0 208s93.1 208 208 208c48.3 0 92.7-16.4 128-44v16.3c0 6.4 2.5 12.5 7 17l99.7 99.7c9.4 9.4 24.6 9.4 33.9 0l28.3-28.3c9.4-9.4 9.4-24.6.1-34zM208 336c-70.7 0-128-57.2-128-128 0-70.7 57.2-128 128-128 70.7 0 128 57.2 128 128 0 70.7-57.2 128-128 128z"></path></svg><input class="header--search-input header--search-input-ds2 js-SiteSearch-form-input" data-main-header-click-target="search_input" name="q" placeholder="Search" type="text" /></form></div></div></div><nav class="header--nav-buttons header--nav-buttons-ds2 js-main-nav"><button class="ds2-5-button ds2-5-button--secondary js-header-login-url header-button-ds2 header-login-ds2 hide-on-mobile-redesign react-login-modal-opener" data-signup-modal="{&quot;location&quot;:&quot;login-button--header&quot;}" rel="nofollow">Log In</button><button class="ds2-5-button ds2-5-button--secondary header-button-ds2 hide-on-mobile-redesign react-login-modal-opener" data-signup-modal="{&quot;location&quot;:&quot;signup-button--header&quot;}" rel="nofollow">Sign Up</button><button class="header--hamburger-button header--hamburger-button-ds2 hide-on-desktop-redesign js-header-hamburger-button"><div class="icon-bar"></div><div class="icon-bar" style="margin-top: 4px;"></div><div class="icon-bar" style="margin-top: 4px;"></div></button></nav></div><ul class="header--dropdown-container js-header-dropdown"><li class="header--dropdown-row"><a class="header--dropdown-link" href="https://www.academia.edu/login" rel="nofollow">Log In</a></li><li class="header--dropdown-row"><a class="header--dropdown-link" href="https://www.academia.edu/signup" rel="nofollow">Sign Up</a></li><li class="header--dropdown-row js-header-dropdown-expand-button"><button class="header--dropdown-button">more<svg aria-hidden="true" focusable="false" data-prefix="fas" data-icon="caret-down" class="header--dropdown-button-icon svg-inline--fa fa-caret-down fa-w-10" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 320 512"><path fill="currentColor" d="M31.3 192h257.3c17.8 0 26.7 21.5 14.1 34.1L174.1 354.8c-7.8 7.8-20.5 7.8-28.3 0L17.2 226.1C4.6 213.5 13.5 192 31.3 192z"></path></svg></button></li><li><ul class="header--expanded-dropdown-container"><li class="header--dropdown-row"><a class="header--dropdown-link" href="https://www.academia.edu/about">About</a></li><li class="header--dropdown-row"><a class="header--dropdown-link" href="https://www.academia.edu/press">Press</a></li><li class="header--dropdown-row"><a class="header--dropdown-link" href="https://www.academia.edu/documents">Papers</a></li><li class="header--dropdown-row"><a class="header--dropdown-link" href="https://www.academia.edu/terms">Terms</a></li><li class="header--dropdown-row"><a class="header--dropdown-link" href="https://www.academia.edu/privacy">Privacy</a></li><li class="header--dropdown-row"><a class="header--dropdown-link" href="https://www.academia.edu/copyright">Copyright</a></li><li class="header--dropdown-row"><a class="header--dropdown-link" href="https://www.academia.edu/hiring"><svg aria-hidden="true" focusable="false" data-prefix="fas" data-icon="briefcase" class="header--dropdown-row-icon svg-inline--fa fa-briefcase fa-w-16" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M320 336c0 8.84-7.16 16-16 16h-96c-8.84 0-16-7.16-16-16v-48H0v144c0 25.6 22.4 48 48 48h416c25.6 0 48-22.4 48-48V288H320v48zm144-208h-80V80c0-25.6-22.4-48-48-48H176c-25.6 0-48 22.4-48 48v48H48c-25.6 0-48 22.4-48 48v80h512v-80c0-25.6-22.4-48-48-48zm-144 0H192V96h128v32z"></path></svg>We&#39;re Hiring!</a></li><li class="header--dropdown-row"><a class="header--dropdown-link" href="https://support.academia.edu/hc/en-us"><svg aria-hidden="true" focusable="false" data-prefix="fas" data-icon="question-circle" class="header--dropdown-row-icon svg-inline--fa fa-question-circle fa-w-16" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M504 256c0 136.997-111.043 248-248 248S8 392.997 8 256C8 119.083 119.043 8 256 8s248 111.083 248 248zM262.655 90c-54.497 0-89.255 22.957-116.549 63.758-3.536 5.286-2.353 12.415 2.715 16.258l34.699 26.31c5.205 3.947 12.621 3.008 16.665-2.122 17.864-22.658 30.113-35.797 57.303-35.797 20.429 0 45.698 13.148 45.698 32.958 0 14.976-12.363 22.667-32.534 33.976C247.128 238.528 216 254.941 216 296v4c0 6.627 5.373 12 12 12h56c6.627 0 12-5.373 12-12v-1.333c0-28.462 83.186-29.647 83.186-106.667 0-58.002-60.165-102-116.531-102zM256 338c-25.365 0-46 20.635-46 46 0 25.364 20.635 46 46 46s46-20.636 46-46c0-25.365-20.635-46-46-46z"></path></svg>Help Center</a></li><li class="header--dropdown-row js-header-dropdown-collapse-button"><button class="header--dropdown-button">less<svg aria-hidden="true" focusable="false" data-prefix="fas" data-icon="caret-up" class="header--dropdown-button-icon svg-inline--fa fa-caret-up fa-w-10" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 320 512"><path fill="currentColor" d="M288.662 352H31.338c-17.818 0-26.741-21.543-14.142-34.142l128.662-128.662c7.81-7.81 20.474-7.81 28.284 0l128.662 128.662c12.6 12.599 3.676 34.142-14.142 34.142z"></path></svg></button></li></ul></li></ul></div> <script src="//a.academia-assets.com/assets/webpack_bundles/fast_loswp-bundle-e7904fe51b852a27691e0923489baf74c1a3b49cd3005fc4c21e0bc8ff60f4e6.js" defer="defer"></script><script>window.loswp = {}; window.loswp.author = 41333; window.loswp.bulkDownloadFilterCounts = {}; window.loswp.hasDownloadableAttachment = true; window.loswp.hasViewableAttachments = true; // TODO: just use routes for this window.loswp.loginUrl = "https://www.academia.edu/login?post_login_redirect_url=https%3A%2F%2Fwww.academia.edu%2F2405515%2FOn_the_Provability_Logic_of_Bounded_Arithmetic%3Fauto%3Ddownload"; window.loswp.translateUrl = "https://www.academia.edu/login?post_login_redirect_url=https%3A%2F%2Fwww.academia.edu%2F2405515%2FOn_the_Provability_Logic_of_Bounded_Arithmetic%3Fshow_translation%3Dtrue"; window.loswp.previewableAttachments = [{"id":50643683,"identifier":"Attachment_50643683","shouldShowBulkDownload":false}]; window.loswp.shouldDetectTimezone = true; window.loswp.shouldShowBulkDownload = true; window.loswp.showSignupCaptcha = false window.loswp.willEdgeCache = false; window.loswp.work = {"work":{"id":2405515,"created_at":"2013-01-15T17:24:15.881-08:00","from_world_paper_id":116728057,"updated_at":"2024-11-13T11:03:33.541-08:00","_data":{"grobid_abstract":"A. and R. Verbrugge, On the provability logic of bounded arithmetic, Annals of Pure and Applied Logic 61 (1993) 75-93.","publication_date":"1993,,","publication_name":"Annals of Pure and Applied Logic","grobid_abstract_attachment_id":"50643683"},"document_type":"paper","pre_hit_view_count_baseline":null,"quality":"high","language":"en","title":"On the Provability Logic of Bounded Arithmetic","broadcastable":true,"draft":null,"has_indexable_attachment":true,"indexable":true,"seo_quality":null}}["work"]; window.loswp.workCoauthors = [41333,18337933]; window.loswp.locale = "en"; window.loswp.countryCode = "SG"; window.loswp.cwvAbTestBucket = ""; window.loswp.designVariant = "ds_vanilla"; window.loswp.fullPageMobileSutdModalVariant = "full_page_mobile_sutd_modal"; window.loswp.useOptimizedScribd4genScript = false; window.loginModal = {}; window.loginModal.appleClientId = 'edu.academia.applesignon'; window.userInChina = "false";</script><script defer="" src="https://accounts.google.com/gsi/client"></script><div class="ds-loswp-container"><div class="ds-work-card--grid-container"><div class="ds-work-card--container js-loswp-work-card"><div class="ds-work-card--cover"><div class="ds-work-cover--wrapper"><div class="ds-work-cover--container"><button class="ds-work-cover--clickable js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;swp-splash-paper-cover&quot;,&quot;attachmentId&quot;:50643683,&quot;attachmentType&quot;:&quot;pdf&quot;}"><img alt="First page of “On the Provability Logic of Bounded Arithmetic”" class="ds-work-cover--cover-thumbnail" src="https://0.academia-photos.com/attachment_thumbnails/50643683/mini_magick20190128-10991-1gs91cc.png?1548695472" /><img alt="PDF Icon" class="ds-work-cover--file-icon" src="//a.academia-assets.com/images/single_work_splash/adobe_icon.svg" /><div class="ds-work-cover--hover-container"><span class="material-symbols-outlined" style="font-size: 20px" translate="no">download</span><p>Download Free PDF</p></div><div class="ds-work-cover--ribbon-container">Download Free PDF</div><div class="ds-work-cover--ribbon-triangle"></div></button></div></div></div><div class="ds-work-card--work-information"><h1 class="ds-work-card--work-title">On the Provability Logic of Bounded Arithmetic</h1><div class="ds-work-card--work-authors ds-work-card--detail"><a class="ds-work-card--author js-wsj-grid-card-author ds2-5-body-md ds2-5-body-link" data-author-id="41333" href="https://rug.academia.edu/RinekeVerbrugge"><img alt="Profile image of Rineke Verbrugge" class="ds-work-card--author-avatar" src="//a.academia-assets.com/images/s65_no_pic.png" />Rineke Verbrugge</a><a class="ds-work-card--author js-wsj-grid-card-author ds2-5-body-md ds2-5-body-link" data-author-id="18337933" href="https://independent.academia.edu/AlessandroBerarducci"><img alt="Profile image of Alessandro Berarducci" class="ds-work-card--author-avatar" src="https://0.academia-photos.com/18337933/22540702/21734456/s65_alessandro.berarducci.jpg" />Alessandro Berarducci</a></div><div class="ds-work-card--detail"><p class="ds-work-card--detail ds2-5-body-sm">1993, Annals of Pure and Applied Logic</p><div class="ds-work-card--work-metadata"><div class="ds-work-card--work-metadata__stat"><span class="material-symbols-outlined" style="font-size: 20px" translate="no">visibility</span><p class="ds2-5-body-sm" id="work-metadata-view-count">…</p></div><div class="ds-work-card--work-metadata__stat"><span class="material-symbols-outlined" style="font-size: 20px" translate="no">description</span><p class="ds2-5-body-sm">19 pages</p></div><div class="ds-work-card--work-metadata__stat"><span class="material-symbols-outlined" style="font-size: 20px" translate="no">link</span><p class="ds2-5-body-sm">1 file</p></div></div><script>(async () => { const workId = 2405515; const worksViewsPath = "/v0/works/views?subdomain_param=api&amp;work_ids%5B%5D=2405515"; const getWorkViews = async (workId) => { const response = await fetch(worksViewsPath); if (!response.ok) { throw new Error('Failed to load work views'); } const data = await response.json(); return data.views[workId]; }; // Get the view count for the work - we send this immediately rather than waiting for // the DOM to load, so it can be available as soon as possible (but without holding up // the backend or other resource requests, because it's a bit expensive and not critical). const viewCount = await getWorkViews(workId); const updateViewCount = (viewCount) => { try { const viewCountNumber = parseInt(viewCount, 10); if (viewCountNumber === 0) { // Remove the whole views element if there are zero views. document.getElementById('work-metadata-view-count')?.parentNode?.remove(); return; } const commaizedViewCount = viewCountNumber.toLocaleString(); const viewCountBody = document.getElementById('work-metadata-view-count'); if (!viewCountBody) { throw new Error('Failed to find work views element'); } viewCountBody.textContent = `${commaizedViewCount} views`; } catch (error) { // Remove the whole views element if there was some issue parsing. document.getElementById('work-metadata-view-count')?.parentNode?.remove(); throw new Error(`Failed to parse view count: ${viewCount}`, error); } }; // If the DOM is still loading, wait for it to be ready before updating the view count. if (document.readyState === "loading") { document.addEventListener('DOMContentLoaded', () => { updateViewCount(viewCount); }); // Otherwise, just update it immediately. } else { updateViewCount(viewCount); } })();</script></div><div class="ds-work-card--button-container"><div class="primary-buttons "><button class="ds2-5-button js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;continue-reading-button--work-card&quot;,&quot;attachmentId&quot;:50643683,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;workUrl&quot;:&quot;https://www.academia.edu/2405515/On_the_Provability_Logic_of_Bounded_Arithmetic&quot;}"><span class="material-symbols-outlined" style="font-size: 20px" translate="no">description</span>See full PDF</button><button class="ds2-5-button ds2-5-button--secondary js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;download-pdf-button--work-card&quot;,&quot;attachmentId&quot;:50643683,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;workUrl&quot;:&quot;https://www.academia.edu/2405515/On_the_Provability_Logic_of_Bounded_Arithmetic&quot;}"><span class="material-symbols-outlined" style="font-size: 20px" translate="no">download</span>Download PDF</button></div></div><div class="ds-signup-banner-trigger-container"><div class="ds-signup-banner-trigger ds-signup-banner-trigger-control"></div></div><div class="ds-signup-banner ds-signup-banner-control"><div id="ds-signup-banner-close-button"><button class="ds2-5-button ds2-5-button--secondary ds2-5-button--inverse"><span class="material-symbols-outlined" style="font-size: 20px" translate="no">close</span></button></div><div class="ds-signup-banner-ctas" data-impression-entity-id="2405515" data-impression-entity-type="2" data-impression-source="signup-banner"><img src="//a.academia-assets.com/images/academia-logo-capital-white.svg" /><h4 class="ds2-5-heading-serif-sm">Sign up for access to the world's latest research</h4><button class="ds2-5-button ds2-5-button--inverse ds2-5-button--full-width js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;signup-banner&quot;}">Sign up for free<span class="material-symbols-outlined" style="font-size: 20px" translate="no">arrow_forward</span></button></div><div class="ds-signup-banner-divider"></div><div class="ds-signup-banner-reasons"><div class="ds-signup-banner-reasons-item"><span class="material-symbols-outlined" style="font-size: 24px" translate="no">check</span><span>Get notified about relevant papers</span></div><div class="ds-signup-banner-reasons-item"><span class="material-symbols-outlined" style="font-size: 24px" translate="no">check</span><span>Save papers to use in your research</span></div><div class="ds-signup-banner-reasons-item"><span class="material-symbols-outlined" style="font-size: 24px" translate="no">check</span><span>Join the discussion with peers</span></div><div class="ds-signup-banner-reasons-item"><span class="material-symbols-outlined" style="font-size: 24px" translate="no">check</span><span>Track your impact</span></div></div></div><script>(() => { // Set up signup banner show/hide behavior: // 1. If the signup banner trigger (a 242px-high* invisible div underneath the 'See Full PDF' / 'Download PDF' buttons) // is already fully scrolled above the viewport, show the banner by default // 2. If the signup banner trigger is fully visible, show the banner // 3. If the signup banner trigger has even a few pixels scrolled below the viewport, hide the banner // // * 242px is the empirically determined height of the signup banner. It's better to be a bit taller than // necessary than too short, so it's fine that the mobile (small breakpoint) banner is shorter. // First check session storage for the signup banner's visibility state const signupBannerHidden = sessionStorage.getItem('ds-signup-banner-hidden'); if (signupBannerHidden === 'true') { return; } const signupBanner = document.querySelector('.ds-signup-banner'); const signupBannerTrigger = document.querySelector('.ds-signup-banner-trigger'); if (!signupBannerTrigger) { window.Sentry.captureMessage("Signup banner trigger not found"); return; } let footerShown = false; window.addEventListener('load', () => { const rect = signupBannerTrigger.getBoundingClientRect(); // If page loaded up already scrolled below the trigger (via scroll restoration), show the banner by default if (rect.bottom < 0) { footerShown = true; signupBanner.classList.add('ds-signup-banner-visible'); } }); // Wait for trigger to fully enter viewport before showing banner (ensures PDF CTAs are never covered by banner) const observer = new IntersectionObserver((entries) => { entries.forEach(entry => { if (entry.isIntersecting && !footerShown) { footerShown = true; signupBanner.classList.add('ds-signup-banner-visible'); } else if (!entry.isIntersecting && footerShown) { if (signupBannerTrigger.getBoundingClientRect().bottom > 0) { footerShown = false; signupBanner.classList.remove('ds-signup-banner-visible'); } } }); }); observer.observe(signupBannerTrigger); // Set up signup banner close button event handler: const signupBannerCloseButton = document.querySelector('#ds-signup-banner-close-button'); signupBannerCloseButton.addEventListener('click', () => { signupBanner.classList.remove('ds-signup-banner-visible'); observer.unobserve(signupBannerTrigger); // Store the signup banner's visibility state in session storage sessionStorage.setItem('ds-signup-banner-hidden', 'true'); }); })();</script></div></div></div><div data-auto_select="false" data-client_id="331998490334-rsn3chp12mbkiqhl6e7lu2q0mlbu0f1b" data-doc_id="50643683" data-landing_url="https://www.academia.edu/2405515/On_the_Provability_Logic_of_Bounded_Arithmetic" data-login_uri="https://www.academia.edu/registrations/google_one_tap" data-moment_callback="onGoogleOneTapEvent" id="g_id_onload"></div><div class="ds-abstract--grid-container"><div class="ds-abstract--container"><h2 class="ds-abstract--heading ds2-5-heading-sans-serif-lg">Abstract</h2><p class="ds2-5-body-md">A. and R. Verbrugge, On the provability logic of bounded arithmetic, Annals of Pure and Applied Logic 61 (1993) 75-93.</p></div></div><div class="ds-top-related-works--grid-container"><div class="ds-related-content--container ds-top-related-works--container"><h2 class="ds-related-content--heading">Related papers</h2><div class="ds-related-work--container js-wsj-grid-card" data-collection-position="0" data-entity-id="112245398" data-sort-order="default"><a class="ds-related-work--title js-wsj-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/112245398/The_Modal_Logic_of_Consistency_Assertions_of_Peano_Arithmetic">The Modal Logic of Consistency Assertions of Peano Arithmetic</a><div class="ds-related-work--metadata"><a class="js-wsj-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="34208831" href="https://unipd.academia.edu/SilvioValentini">Silvio Valentini</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 1983</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;The Modal Logic of Consistency Assertions of Peano Arithmetic&quot;,&quot;attachmentId&quot;:109534497,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/112245398/The_Modal_Logic_of_Consistency_Assertions_of_Peano_Arithmetic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-wsj-grid-card-view-pdf" href="https://www.academia.edu/112245398/The_Modal_Logic_of_Consistency_Assertions_of_Peano_Arithmetic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-wsj-grid-card" data-collection-position="1" data-entity-id="3084012" data-sort-order="default"><a class="ds-related-work--title js-wsj-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/3084012/A_note_on_some_explicit_modal_logics">A note on some explicit modal logics</a><div class="ds-related-work--metadata"><a class="js-wsj-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="809285" href="https://umcp.academia.edu/EricPacuit">Eric Pacuit</a></div><p class="ds-related-work--metadata ds2-5-body-xs">2006</p><p class="ds-related-work--abstract ds2-5-body-sm">Artemov introduced the Logic of Proofs (LP) as a logic of explicit proofs. We can also offer an epistemic reading of this formula: &quot;t is a possible justification of φ&quot;. Motivated, in part, by this epistemic reading, Fitting introduced a Kripke style semantics for LP in . In this note, we prove soundness and completeness of some axiom systems which are not covered in [8].</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;A note on some explicit modal logics&quot;,&quot;attachmentId&quot;:31010716,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/3084012/A_note_on_some_explicit_modal_logics&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-wsj-grid-card-view-pdf" href="https://www.academia.edu/3084012/A_note_on_some_explicit_modal_logics"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-wsj-grid-card" data-collection-position="2" data-entity-id="33478818" data-sort-order="default"><a class="ds-related-work--title js-wsj-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/33478818/Notes_on_Incompleteness_Results_and_Provability_Logic">Notes on Incompleteness Results and Provability Logic</a><div class="ds-related-work--metadata"><a class="js-wsj-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="3776341" href="https://cambridge.academia.edu/liu">Yang Liu</a></div><p class="ds-related-work--abstract ds2-5-body-sm">This notes provides a brief survey that reflects the early development of provability logic. It includes a detailed exposition of Gödel&#39;s incompleteness results, the Löb theorem, and the arithmetical completeness theorems of Solovay.</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Notes on Incompleteness Results and Provability Logic&quot;,&quot;attachmentId&quot;:53521496,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/33478818/Notes_on_Incompleteness_Results_and_Provability_Logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-wsj-grid-card-view-pdf" href="https://www.academia.edu/33478818/Notes_on_Incompleteness_Results_and_Provability_Logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-wsj-grid-card" data-collection-position="3" data-entity-id="59275289" data-sort-order="default"><a class="ds-related-work--title js-wsj-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/59275289/On_Provability_Logics_with_Linearly_Ordered_Modalities">On Provability Logics with Linearly Ordered Modalities</a><div class="ds-related-work--metadata"><a class="js-wsj-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="98896487" href="https://scopus.academia.edu/LevBeklemishev">Lev Beklemishev</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Studia Logica, 2014</p><p class="ds-related-work--abstract ds2-5-body-sm">We introduce the logics GLP Λ , a generalization of Japaridze&#39;s polymodal provability logic GLP ω where Λ is any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP ω yielding among other things a finitary proof of the normal form theorem for the variablefree fragment of GLP Λ and the decidability of GLP Λ for recursive orderings Λ. Further, we give a restricted axiomatization of the variable-free fragment of GLP Λ .</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;On Provability Logics with Linearly Ordered Modalities&quot;,&quot;attachmentId&quot;:73282234,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/59275289/On_Provability_Logics_with_Linearly_Ordered_Modalities&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-wsj-grid-card-view-pdf" href="https://www.academia.edu/59275289/On_Provability_Logics_with_Linearly_Ordered_Modalities"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-wsj-grid-card" data-collection-position="4" data-entity-id="73467650" data-sort-order="default"><a class="ds-related-work--title js-wsj-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/73467650/14_On_Logic_of_Formal_Provability_and_Explicit_Proofs">14 On Logic of Formal Provability and Explicit Proofs</a><div class="ds-related-work--metadata"><a class="js-wsj-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="7039580" href="https://independent.academia.edu/ElenaNogina">Elena Nogina</a></div><p class="ds-related-work--metadata ds2-5-body-xs">2016</p><p class="ds-related-work--abstract ds2-5-body-sm">In 1933, Gödel considered two modal approaches to describing provability. One captured formal provability and resulted in the logic GL and Solovay&#39;s Completeness Theorem. The other was based on the modal logic S4 and led to Artemov&#39;s Logic of Proofs LP. In this paper, we study introduced by the author logic GLA, which is a fusion of GL and LP in the union of their languages. GLA is supplied with a Kripke-style semantics and the corresponding completeness theorem. Soundness and completeness of GLA with respect to the arithmetical provability semantics is established.</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;14 On Logic of Formal Provability and Explicit Proofs&quot;,&quot;attachmentId&quot;:81979205,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/73467650/14_On_Logic_of_Formal_Provability_and_Explicit_Proofs&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-wsj-grid-card-view-pdf" href="https://www.academia.edu/73467650/14_On_Logic_of_Formal_Provability_and_Explicit_Proofs"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-wsj-grid-card" data-collection-position="5" data-entity-id="59275271" data-sort-order="default"><a class="ds-related-work--title js-wsj-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/59275271/On_the_complexity_of_arithmetical_interpretations_of_modal_formulae">On the complexity of arithmetical interpretations of modal formulae</a><div class="ds-related-work--metadata"><a class="js-wsj-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="98896487" href="https://scopus.academia.edu/LevBeklemishev">Lev Beklemishev</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Archive for Mathematical Logic, 1993</p><p class="ds-related-work--abstract ds2-5-body-sm">It is a well-known fact that for any arithmetic sentence A A c Z1PA ~ PA k A-+ PrrA ~. Here Pr stands for G6del&#39;s formula expressing provability in Peano Arithmetic PA and Z~ A denotes the class of sentences PA-equivalent to those in ~l-f~ Kent [1] showed that the converse implication does not hold. Moreover, he found that for each natural number r~ there exists an arithmetic sentence A such that PAFA-~Pff-A = and A f{ A PA. Guaspari [2] rediscovered (a sharpened version of) this result applying his own techniques of partially conservative sentences. He also showed that arithmetically complex sentences implying their own provability cannot be constructed by some class of restricted means. Guaspari posed a few problems generalizing the one solved by Kent and himself, which are formulated in terms of provability interpretations of propositional modal logic. Definition. Let c~ be the language consisting of propositional variables p, q, ...; boolean connectives A, V,-% +-+, ~ and • modal operator []. An arithmetical interpretation f is a mapping of ~C&lt;formulae to arithmetic sentences which commutes with boolean connectives and translates [] as provability, i.e. for every modal formula q~ f([]~) = Prrf(~)&quot; .</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;On the complexity of arithmetical interpretations of modal formulae&quot;,&quot;attachmentId&quot;:73282230,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/59275271/On_the_complexity_of_arithmetical_interpretations_of_modal_formulae&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-wsj-grid-card-view-pdf" href="https://www.academia.edu/59275271/On_the_complexity_of_arithmetical_interpretations_of_modal_formulae"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-wsj-grid-card" data-collection-position="6" data-entity-id="41133178" data-sort-order="default"><a class="ds-related-work--title js-wsj-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/41133178/A_Proof_Theory_for_the_Logic_of_Provability_in_True_Arithmetic">A Proof Theory for the Logic of Provability in True Arithmetic</a><div class="ds-related-work--metadata"><a class="js-wsj-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="512336" href="https://mlit.academia.edu/HirohikoKushida%E4%B8%B2%E7%94%B0%E8%A3%95%E5%BD%A6">Hirohiko Kushida 串田裕彦</a></div><p class="ds-related-work--metadata ds2-5-body-xs">STUDIA LOGICA, vol.108(4), pp 857-875, 2020</p><p class="ds-related-work--abstract ds2-5-body-sm">[Attached is an accepted version.] In a classical 1976 paper, Solovay proved the arithmetical completeness of the modal logic GL; provability of a formula in GL coincides with provability of its arithmetical interpretations in Peano Arithmetic. In that paper, he also provided an axiomatic system GLS and proved arithmetical completeness for GLS; provability of a formula in GLS coincides with truth of its arithmetical interpretations in the standard model of arithmetic. Proof theory for GL has been studied intensively up to the present day. However, it might sound somewhat strange that no proof theory for GLS was ever developed nor even suggested thus far, except for the axiomatic system offered by Solovay. In this paper, we develop a proof theory for GLS based on the sequent calculus method. We provide a sequent calculus for GLS and prove the cut- elimination and some standard consequences of it: the interpolation and de- finability theorems. As another consequence of cut-elimination, we also prove the equivalence of GL and GLS with respect to a special form of formulas which we call G ̈odel sentences, using a purely proof-theoretical method.</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;A Proof Theory for the Logic of Provability in True Arithmetic&quot;,&quot;attachmentId&quot;:65120834,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/41133178/A_Proof_Theory_for_the_Logic_of_Provability_in_True_Arithmetic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-wsj-grid-card-view-pdf" href="https://www.academia.edu/41133178/A_Proof_Theory_for_the_Logic_of_Provability_in_True_Arithmetic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-wsj-grid-card" data-collection-position="7" data-entity-id="17714192" data-sort-order="default"><a class="ds-related-work--title js-wsj-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/17714192/On_Some_Completeness_Theorems_in_Modal_Logic">On Some Completeness Theorems in Modal Logic</a><div class="ds-related-work--metadata"><a class="js-wsj-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="31418790" href="https://204.academia.edu/DavidMakinson">David Makinson</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 1966</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;On Some Completeness Theorems in Modal Logic&quot;,&quot;attachmentId&quot;:39670180,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/17714192/On_Some_Completeness_Theorems_in_Modal_Logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-wsj-grid-card-view-pdf" href="https://www.academia.edu/17714192/On_Some_Completeness_Theorems_in_Modal_Logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-wsj-grid-card" data-collection-position="8" data-entity-id="19269804" data-sort-order="default"><a class="ds-related-work--title js-wsj-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/19269804/Proving_unprovability_in_some_normal_modal_logics">Proving unprovability in some normal modal logics</a><div class="ds-related-work--metadata"><a class="js-wsj-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="39410570" href="https://su-se.academia.edu/ValentinGoranko">Valentin Goranko</a></div><p class="ds-related-work--metadata ds2-5-body-xs">1991</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Proving unprovability in some normal modal logics&quot;,&quot;attachmentId&quot;:40527294,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/19269804/Proving_unprovability_in_some_normal_modal_logics&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-wsj-grid-card-view-pdf" href="https://www.academia.edu/19269804/Proving_unprovability_in_some_normal_modal_logics"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-wsj-grid-card" data-collection-position="9" data-entity-id="2815285" data-sort-order="default"><a class="ds-related-work--title js-wsj-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/2815285/On_propositional_quantifiers_in_provability_logic">On propositional quantifiers in provability logic</a><div class="ds-related-work--metadata"><a class="js-wsj-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="33366" href="https://gc-cuny.academia.edu/SergeiArtemov">Sergei Artemov</a></div><p class="ds-related-work--metadata ds2-5-body-xs">1993</p><p class="ds-related-work--abstract ds2-5-body-sm">Abstract The first order theory of the Diagonalizable Algebra of Peano Arithmetic (DA (PA)) represents a natural fragment of provability logic with propositional quantifiers. We prove that the first order theory of the O-generated subalgebra of DA (PA) is decidable but not elementary recursive; the same theory, enriched by a single free variable ranging over DA (PA), is already undecidable.</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;On propositional quantifiers in provability logic&quot;,&quot;attachmentId&quot;:30767868,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/2815285/On_propositional_quantifiers_in_provability_logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-wsj-grid-card-view-pdf" href="https://www.academia.edu/2815285/On_propositional_quantifiers_in_provability_logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div></div></div><div class="ds-sticky-ctas--wrapper js-loswp-sticky-ctas hidden"><div class="ds-sticky-ctas--grid-container"><div class="ds-sticky-ctas--container"><button class="ds2-5-button js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;continue-reading-button--sticky-ctas&quot;,&quot;attachmentId&quot;:50643683,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;workUrl&quot;:null}">See full PDF</button><button class="ds2-5-button ds2-5-button--secondary js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;download-pdf-button--sticky-ctas&quot;,&quot;attachmentId&quot;:50643683,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;workUrl&quot;:null}"><span class="material-symbols-outlined" style="font-size: 20px" translate="no">download</span>Download PDF</button></div></div></div><div class="ds-below-fold--grid-container"><div class="ds-work--container js-loswp-embedded-document"><div class="attachment_preview" data-attachment="Attachment_50643683" style="display: none"><div class="js-scribd-document-container"><div class="scribd--document-loading js-scribd-document-loader" style="display: block;"><img alt="Loading..." src="//a.academia-assets.com/images/loaders/paper-load.gif" /><p>Loading Preview</p></div></div><div style="text-align: center;"><div class="scribd--no-preview-alert js-preview-unavailable"><p>Sorry, preview is currently unavailable. You can download the paper by clicking the button above.</p></div></div></div></div><div class="ds-sidebar--container js-work-sidebar"><div class="ds-related-content--container"><h2 class="ds-related-content--heading">Related papers</h2><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="0" data-entity-id="47098327" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/47098327/On_Logic_of_Formal_Provability_and_Explicit_Proofs">On Logic of Formal Provability and Explicit Proofs</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="7039580" href="https://independent.academia.edu/ElenaNogina">Elena Nogina</a></div><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;On Logic of Formal Provability and Explicit Proofs&quot;,&quot;attachmentId&quot;:66372396,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/47098327/On_Logic_of_Formal_Provability_and_Explicit_Proofs&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/47098327/On_Logic_of_Formal_Provability_and_Explicit_Proofs"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="1" data-entity-id="3934711" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/3934711/Problems_of_Proof_Theory_in_Modal_Logic">Problems of Proof Theory in Modal Logic</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="96790" href="https://helsinki.academia.edu/SaraNegri">Sara Negri</a></div><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Problems of Proof Theory in Modal Logic&quot;,&quot;attachmentId&quot;:32379117,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/3934711/Problems_of_Proof_Theory_in_Modal_Logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/3934711/Problems_of_Proof_Theory_in_Modal_Logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="2" data-entity-id="85648092" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/85648092/Post_complete_and_0_axiomatizable_modal_logics">Post complete and 0-axiomatizable modal logics</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="184564827" href="https://unisi.academia.edu/FABIOBELLISSIMA">FABIO BELLISSIMA</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Annals of Pure and Applied Logic, 1990</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Post complete and 0-axiomatizable modal logics&quot;,&quot;attachmentId&quot;:90282001,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/85648092/Post_complete_and_0_axiomatizable_modal_logics&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/85648092/Post_complete_and_0_axiomatizable_modal_logics"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="3" data-entity-id="93691945" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/93691945/Chapter_VII_The_logic_of_provability">Chapter VII The logic of provability</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="236404015" href="https://independent.academia.edu/GiorgiJaparidze8">Giorgi Japaridze</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Studies in Logic and the Foundations of Mathematics, 1998</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Chapter VII The logic of provability&quot;,&quot;attachmentId&quot;:96359131,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/93691945/Chapter_VII_The_logic_of_provability&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/93691945/Chapter_VII_The_logic_of_provability"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="4" data-entity-id="113391550" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/113391550/Zero_one_laws_for_provability_logic_Axiomatizing_validity_in_almost_all_models_and_almost_all_frames">Zero-one laws for provability logic: Axiomatizing validity in almost all models and almost all frames</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="55483988" href="https://independent.academia.edu/RinekeVerbrugge">Rineke Verbrugge</a></div><p class="ds-related-work--metadata ds2-5-body-xs">2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Zero-one laws for provability logic: Axiomatizing validity in almost all models and almost all frames&quot;,&quot;attachmentId&quot;:110361629,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/113391550/Zero_one_laws_for_provability_logic_Axiomatizing_validity_in_almost_all_models_and_almost_all_frames&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/113391550/Zero_one_laws_for_provability_logic_Axiomatizing_validity_in_almost_all_models_and_almost_all_frames"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="5" data-entity-id="77340015" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/77340015/_L_Axiomatizability_in_intermediate_and_normal_modal_logics">{\L}-Axiomatizability in intermediate and normal modal logics</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="8370297" href="https://independent.academia.edu/AlexCirkin">Alex Citkin</a></div><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;{\\L}-Axiomatizability in intermediate and normal modal logics&quot;,&quot;attachmentId&quot;:84741402,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/77340015/_L_Axiomatizability_in_intermediate_and_normal_modal_logics&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/77340015/_L_Axiomatizability_in_intermediate_and_normal_modal_logics"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="6" data-entity-id="59275280" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/59275280/A_simplified_proof_of_arithmetical_completeness_theorem_for_provability_logic_GLP">A simplified proof of arithmetical completeness theorem for provability logic GLP</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="98896487" href="https://scopus.academia.edu/LevBeklemishev">Lev Beklemishev</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Proceedings of the Steklov Institute of Mathematics, 2011</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;A simplified proof of arithmetical completeness theorem for provability logic GLP&quot;,&quot;attachmentId&quot;:73282243,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/59275280/A_simplified_proof_of_arithmetical_completeness_theorem_for_provability_logic_GLP&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/59275280/A_simplified_proof_of_arithmetical_completeness_theorem_for_provability_logic_GLP"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="7" data-entity-id="80112894" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/80112894/Provability_logic_models_within_models_in_Peano_Arithmetic">Provability logic: models within models in Peano Arithmetic</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="18337933" href="https://independent.academia.edu/AlessandroBerarducci">Alessandro Berarducci</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Bollettino dell&#39;Unione Matematica Italiana</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Provability logic: models within models in Peano Arithmetic&quot;,&quot;attachmentId&quot;:86603343,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/80112894/Provability_logic_models_within_models_in_Peano_Arithmetic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/80112894/Provability_logic_models_within_models_in_Peano_Arithmetic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="8" data-entity-id="49777200" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/49777200/A_Finitary_Treatment_of_the_Closed_Fragment_of_Japaridzes_Provability_Logic">A Finitary Treatment of the Closed Fragment of Japaridze&#39;s Provability Logic</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="51116229" href="https://independent.academia.edu/JoostJoosten">Joost Joosten</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Journal of Logic and Computation, 2005</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;A Finitary Treatment of the Closed Fragment of Japaridze&#39;s Provability Logic&quot;,&quot;attachmentId&quot;:68014217,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/49777200/A_Finitary_Treatment_of_the_Closed_Fragment_of_Japaridzes_Provability_Logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/49777200/A_Finitary_Treatment_of_the_Closed_Fragment_of_Japaridzes_Provability_Logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="9" data-entity-id="92078326" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/92078326/Provability_Logic_and_the_Completeness_Principle">Provability Logic and the Completeness Principle</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="80365520" href="https://uu.academia.edu/albertvisser">albert visser</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Annals of Pure and Applied Logic, 2019</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Provability Logic and the Completeness Principle&quot;,&quot;attachmentId&quot;:95184805,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/92078326/Provability_Logic_and_the_Completeness_Principle&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/92078326/Provability_Logic_and_the_Completeness_Principle"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="10" data-entity-id="6796734" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/6796734/Canonicity_and_Completeness_Results_for_Many_Valued_Modal_Logics">Canonicity and Completeness Results for Many-Valued Modal Logics</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="11243981" href="https://independent.academia.edu/CostasKoutras">Costas Koutras</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Journal of Applied Non-classical Logics, 2002</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Canonicity and Completeness Results for Many-Valued Modal Logics&quot;,&quot;attachmentId&quot;:48718749,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/6796734/Canonicity_and_Completeness_Results_for_Many_Valued_Modal_Logics&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/6796734/Canonicity_and_Completeness_Results_for_Many_Valued_Modal_Logics"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="11" data-entity-id="1978302" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/1978302/A_proof_theoretic_study_of_the_correspondence_of_classical_logic_and_modal_logic">A proof-theoretic study of the correspondence of classical logic and modal logic</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="512336" href="https://mlit.academia.edu/HirohikoKushida%E4%B8%B2%E7%94%B0%E8%A3%95%E5%BD%A6">Hirohiko Kushida 串田裕彦</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Journal of Symbolic Logic, vol.68(4), pp.1403-1414, 2003</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;A proof-theoretic study of the correspondence of classical logic and modal logic&quot;,&quot;attachmentId&quot;:51009470,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/1978302/A_proof_theoretic_study_of_the_correspondence_of_classical_logic_and_modal_logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/1978302/A_proof_theoretic_study_of_the_correspondence_of_classical_logic_and_modal_logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="12" data-entity-id="19089933" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/19089933/Modal_Languages_and_Bounded_Fragments_of_Predicate_Logic">Modal Languages and Bounded Fragments of Predicate Logic</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="39273769" href="https://renyi.academia.edu/HajnalAndr%C3%A9ka">Hajnal Andréka</a><span>, </span><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="39278596" href="https://independent.academia.edu/AndrekaHajnal">Andreka Hajnal</a><span>, </span><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="51188127" href="https://renyi.academia.edu/Istv%C3%A1nN%C3%A9meti">István Németi</a><span>, </span><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="40536208" href="https://independent.academia.edu/JvanBenthem">Johan van Benthem</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Journal of Philosophical Logic, 1998</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Modal Languages and Bounded Fragments of Predicate Logic&quot;,&quot;attachmentId&quot;:40425858,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/19089933/Modal_Languages_and_Bounded_Fragments_of_Predicate_Logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/19089933/Modal_Languages_and_Bounded_Fragments_of_Predicate_Logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="13" data-entity-id="59181468" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/59181468/Effective_completeness_theorems_for_modal_logic">Effective completeness theorems for modal logic</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="91293964" href="https://cornell.academia.edu/anerode">anil nerode</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Annals of Pure and Applied Logic, 2004</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Effective completeness theorems for modal logic&quot;,&quot;attachmentId&quot;:73237268,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/59181468/Effective_completeness_theorems_for_modal_logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/59181468/Effective_completeness_theorems_for_modal_logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="14" data-entity-id="6543402" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/6543402/A_Godel_Modal_Logic">A Godel Modal Logic</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="10485108" href="https://uba.academia.edu/RicardoOscarRodriguez">Ricardo Oscar Rodriguez</a></div><p class="ds-related-work--metadata ds2-5-body-xs">2009</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;A Godel Modal Logic&quot;,&quot;attachmentId&quot;:33308724,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/6543402/A_Godel_Modal_Logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/6543402/A_Godel_Modal_Logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="15" data-entity-id="4674287" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/4674287/Back_and_Forth_Constructions_in_Modal_Logic_An_Interpolation_Theorem_for_a_Family_of_Modal_Logics">Back and Forth Constructions in Modal Logic: An Interpolation Theorem for a Family of Modal Logics</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="5935270" href="https://independent.academia.edu/JeffreyWelaish">Jeffrey Welaish</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Journal of Symbolic Logic, 1986</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Back and Forth Constructions in Modal Logic: An Interpolation Theorem for a Family of Modal Logics&quot;,&quot;attachmentId&quot;:49703088,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/4674287/Back_and_Forth_Constructions_in_Modal_Logic_An_Interpolation_Theorem_for_a_Family_of_Modal_Logics&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/4674287/Back_and_Forth_Constructions_in_Modal_Logic_An_Interpolation_Theorem_for_a_Family_of_Modal_Logics"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="16" data-entity-id="126356128" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/126356128/Proof_Theory_of_Modal_Logic">Proof Theory of Modal Logic</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="9355757" href="https://rub.academia.edu/HeinrichWansing">Heinrich Wansing</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Applied logic series, 1996</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Proof Theory of Modal Logic&quot;,&quot;attachmentId&quot;:120245001,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/126356128/Proof_Theory_of_Modal_Logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/126356128/Proof_Theory_of_Modal_Logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="17" data-entity-id="5059558" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/5059558/Abstract_modal_logics">Abstract modal logics</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="6757567" href="https://ub.academia.edu/RamonJansana">Ramon Jansana</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Studia Logica - An International Journal for Symbolic Logic, 1995</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Abstract modal logics&quot;,&quot;attachmentId&quot;:49466377,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/5059558/Abstract_modal_logics&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/5059558/Abstract_modal_logics"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="18" data-entity-id="19269869" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/19269869/Proving_unprovability_in_some_normal_modal_logics_Bull_Sect_Logic">Proving unprovability in some normal modal logics. Bull Sect Logic</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="39410570" href="https://su-se.academia.edu/ValentinGoranko">Valentin Goranko</a></div><p class="ds-related-work--metadata ds2-5-body-xs">Bulletin of the Section of Logic</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Proving unprovability in some normal modal logics. Bull Sect Logic&quot;,&quot;attachmentId&quot;:40527335,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/19269869/Proving_unprovability_in_some_normal_modal_logics_Bull_Sect_Logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/19269869/Proving_unprovability_in_some_normal_modal_logics_Bull_Sect_Logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="19" data-entity-id="77340041" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/77340041/%C5%81_Axiomatizability_in_intermediate_and_normal_modal_logics">Ł-Axiomatizability in intermediate and normal modal logics</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="8370297" href="https://independent.academia.edu/AlexCirkin">Alex Citkin</a></div><p class="ds-related-work--metadata ds2-5-body-xs">arXiv: Logic, 2014</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Ł-Axiomatizability in intermediate and normal modal logics&quot;,&quot;attachmentId&quot;:84741414,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/77340041/%C5%81_Axiomatizability_in_intermediate_and_normal_modal_logics&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/77340041/%C5%81_Axiomatizability_in_intermediate_and_normal_modal_logics"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div><div class="ds-related-work--container js-related-work-sidebar-card" data-collection-position="20" data-entity-id="3934657" data-sort-order="default"><a class="ds-related-work--title js-related-work-grid-card-title ds2-5-body-md ds2-5-body-link" href="https://www.academia.edu/3934657/Proof_analysis_in_modal_logic">Proof analysis in modal logic</a><div class="ds-related-work--metadata"><a class="js-related-work-grid-card-author ds2-5-body-sm ds2-5-body-link" data-author-id="96790" href="https://helsinki.academia.edu/SaraNegri">Sara Negri</a></div><p class="ds-related-work--metadata ds2-5-body-xs">2005</p><div class="ds-related-work--ctas"><button class="ds2-5-text-link ds2-5-text-link--inline js-swp-download-button" data-signup-modal="{&quot;location&quot;:&quot;wsj-grid-card-download-pdf-modal&quot;,&quot;work_title&quot;:&quot;Proof analysis in modal logic&quot;,&quot;attachmentId&quot;:43846684,&quot;attachmentType&quot;:&quot;pdf&quot;,&quot;work_url&quot;:&quot;https://www.academia.edu/3934657/Proof_analysis_in_modal_logic&quot;,&quot;alternativeTracking&quot;:true}"><span class="material-symbols-outlined" style="font-size: 18px" translate="no">download</span><span class="ds2-5-text-link__content">Download free PDF</span></button><a class="ds2-5-text-link ds2-5-text-link--inline js-related-work-grid-card-view-pdf" href="https://www.academia.edu/3934657/Proof_analysis_in_modal_logic"><span class="ds2-5-text-link__content">View PDF</span><span class="material-symbols-outlined" style="font-size: 18px" translate="no">chevron_right</span></a></div></div></div><div class="ds-related-content--container"><h2 class="ds-related-content--heading">Related topics</h2><div class="ds-research-interests--pills-container"><a class="js-related-research-interest ds-research-interests--pill" data-entity-id="19997" rel="nofollow" href="https://www.academia.edu/Documents/in/Pure_Mathematics">Pure Mathematics</a><a class="js-related-research-interest ds-research-interests--pill" data-entity-id="165652" rel="nofollow" href="https://www.academia.edu/Documents/in/Bounded_Arithmetic">Bounded Arithmetic</a></div></div></div></div></div><div class="footer--content"><ul class="footer--main-links hide-on-mobile"><li><a href="https://www.academia.edu/about">About</a></li><li><a href="https://www.academia.edu/press">Press</a></li><li><a href="https://www.academia.edu/documents">Papers</a></li><li><a href="https://www.academia.edu/topics">Topics</a></li><li><a href="https://www.academia.edu/hiring"><svg style="width: 13px; height: 13px; position: relative; bottom: -1px;" aria-hidden="true" focusable="false" data-prefix="fas" data-icon="briefcase" class="svg-inline--fa fa-briefcase fa-w-16" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M320 336c0 8.84-7.16 16-16 16h-96c-8.84 0-16-7.16-16-16v-48H0v144c0 25.6 22.4 48 48 48h416c25.6 0 48-22.4 48-48V288H320v48zm144-208h-80V80c0-25.6-22.4-48-48-48H176c-25.6 0-48 22.4-48 48v48H48c-25.6 0-48 22.4-48 48v80h512v-80c0-25.6-22.4-48-48-48zm-144 0H192V96h128v32z"></path></svg>&nbsp;<strong>We&#39;re Hiring!</strong></a></li><li><a href="https://support.academia.edu/hc/en-us"><svg style="width: 12px; height: 12px; position: relative; bottom: -1px;" aria-hidden="true" focusable="false" data-prefix="fas" data-icon="question-circle" class="svg-inline--fa fa-question-circle fa-w-16" role="img" xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512"><path fill="currentColor" d="M504 256c0 136.997-111.043 248-248 248S8 392.997 8 256C8 119.083 119.043 8 256 8s248 111.083 248 248zM262.655 90c-54.497 0-89.255 22.957-116.549 63.758-3.536 5.286-2.353 12.415 2.715 16.258l34.699 26.31c5.205 3.947 12.621 3.008 16.665-2.122 17.864-22.658 30.113-35.797 57.303-35.797 20.429 0 45.698 13.148 45.698 32.958 0 14.976-12.363 22.667-32.534 33.976C247.128 238.528 216 254.941 216 296v4c0 6.627 5.373 12 12 12h56c6.627 0 12-5.373 12-12v-1.333c0-28.462 83.186-29.647 83.186-106.667 0-58.002-60.165-102-116.531-102zM256 338c-25.365 0-46 20.635-46 46 0 25.364 20.635 46 46 46s46-20.636 46-46c0-25.365-20.635-46-46-46z"></path></svg>&nbsp;<strong>Help Center</strong></a></li></ul><ul class="footer--research-interests"><li>Find new research papers in:</li><li><a href="https://www.academia.edu/Documents/in/Physics">Physics</a></li><li><a href="https://www.academia.edu/Documents/in/Chemistry">Chemistry</a></li><li><a href="https://www.academia.edu/Documents/in/Biology">Biology</a></li><li><a href="https://www.academia.edu/Documents/in/Health_Sciences">Health Sciences</a></li><li><a href="https://www.academia.edu/Documents/in/Ecology">Ecology</a></li><li><a href="https://www.academia.edu/Documents/in/Earth_Sciences">Earth Sciences</a></li><li><a href="https://www.academia.edu/Documents/in/Cognitive_Science">Cognitive Science</a></li><li><a href="https://www.academia.edu/Documents/in/Mathematics">Mathematics</a></li><li><a href="https://www.academia.edu/Documents/in/Computer_Science">Computer Science</a></li></ul><ul class="footer--legal-links hide-on-mobile"><li><a href="https://www.academia.edu/terms">Terms</a></li><li><a href="https://www.academia.edu/privacy">Privacy</a></li><li><a href="https://www.academia.edu/copyright">Copyright</a></li><li>Academia &copy;2025</li></ul></div> </body> </html>

Pages: 1 2 3 4 5 6 7 8 9 10