Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems---such as for instance natural deduction---are applied. Therefore, the reasoning that is intrinsic of the theory does not appear in t...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2011-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/861/pdf |
| _version_ | 1797268754613141504 |
|---|---|
| author | Guillaume Burel |
| author_facet | Guillaume Burel |
| author_sort | Guillaume Burel |
| collection | DOAJ |
| description | In deduction modulo, a theory is not represented by a set of axioms but by a
congruence on propositions modulo which the inference rules of standard
deductive systems---such as for instance natural deduction---are applied.
Therefore, the reasoning that is intrinsic of the theory does not appear in the
length of proofs. In general, the congruence is defined through a rewrite
system over terms and propositions. We define a rigorous framework to study
proof lengths in deduction modulo, where the congruence must be computed in
polynomial time. We show that even very simple rewrite systems lead to
arbitrary proof-length speed-ups in deduction modulo, compared to using axioms.
As higher-order logic can be encoded as a first-order theory in deduction
modulo, we also study how to reinterpret, thanks to deduction modulo, the
speed-ups between higher-order and first-order arithmetics that were stated by
G\"odel. We define a first-order rewrite system with a congruence decidable in
polynomial time such that proofs of higher-order arithmetic can be linearly
translated into first-order arithmetic modulo that system. We also present the
whole higher-order arithmetic as a first-order system without resorting to any
axiom, where proofs have the same length as in the axiomatic presentation. |
| first_indexed | 2024-04-25T01:37:30Z |
| format | Article |
| id | doaj.art-3ad5e525821f48e681f55f323ca36e45 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:30Z |
| publishDate | 2011-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-3ad5e525821f48e681f55f323ca36e452024-03-08T09:14:52ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742011-03-01Volume 7, Issue 110.2168/LMCS-7(1:3)2011861Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory ModuloGuillaume BurelIn deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems---such as for instance natural deduction---are applied. Therefore, the reasoning that is intrinsic of the theory does not appear in the length of proofs. In general, the congruence is defined through a rewrite system over terms and propositions. We define a rigorous framework to study proof lengths in deduction modulo, where the congruence must be computed in polynomial time. We show that even very simple rewrite systems lead to arbitrary proof-length speed-ups in deduction modulo, compared to using axioms. As higher-order logic can be encoded as a first-order theory in deduction modulo, we also study how to reinterpret, thanks to deduction modulo, the speed-ups between higher-order and first-order arithmetics that were stated by G\"odel. We define a first-order rewrite system with a congruence decidable in polynomial time such that proofs of higher-order arithmetic can be linearly translated into first-order arithmetic modulo that system. We also present the whole higher-order arithmetic as a first-order system without resorting to any axiom, where proofs have the same length as in the axiomatic presentation.https://lmcs.episciences.org/861/pdfcomputer science - logic in computer sciencecomputer science - computational complexitycs.cc |
| spellingShingle | Guillaume Burel Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo Logical Methods in Computer Science computer science - logic in computer science computer science - computational complexity cs.cc |
| title | Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo |
| title_full | Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo |
| title_fullStr | Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo |
| title_full_unstemmed | Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo |
| title_short | Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo |
| title_sort | efficiently simulating higher order arithmetic by a first order theory modulo |
| topic | computer science - logic in computer science computer science - computational complexity cs.cc |
| url | https://lmcs.episciences.org/861/pdf |
| work_keys_str_mv | AT guillaumeburel efficientlysimulatinghigherorderarithmeticbyafirstordertheorymodulo |