Feasible Operations on Proofs: The Logic of Proofs for Bounded Arithmetic
| Autor: | Evan Goris |
|---|---|
| Rok vydání: | 2007 |
| Předmět: |
Discrete mathematics
Bounded arithmetic Semantics (computer science) Mathematical proof Theoretical Computer Science TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computable function Computational Theory and Mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Completeness (logic) Peano axioms Theory of computation Explicit knowledge Mathematics |
| Zdroj: | Theory of Computing Systems. 43:185-203 |
| ISSN: | 1433-0490 1432-4350 |
| DOI: | 10.1007/s00224-007-9058-x |
| Popis: | This paper presents a semantics for the logic of proofs $\mathsf{LP}$ in which all the operations on proofs are realized by feasibly computable functions. More precisely, we will show that the completeness of $\mathsf{LP}$ for the semantics of proofs of Peano Arithmetic extends to the semantics of proofs in Buss’ bounded arithmetic $\mathsf{S}^{1}_{2}$. In view of applications in epistemology of $\mathsf{LP}$ in particular and justification logics in general this result shows that explicit knowledge in the propositional framework can be made computationally feasible. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink