Kuznets, Roman
(2009).
*
A Note on the Use of Sum in the Logic of Proofs.
*
In:
Drossos, Costas; , ; , ; Tsinakis, Constantine
(eds.)
Proceedings of the 7th Panhellenic Logic Symposium (pp. 99-103).
Patras University Press

The Logic of Proofs~LP, introduced by Artemov, encodes the same reasoning as the modal logic~S4 using proofs explicitly present in the language. In particular, Artemov showed that three operations on proofs (application~$\cdot$, positive introspection~!, and sum~+) are sufficient to mimic provability concealed in S4~modality. While the first two operations go back to G{\"o}del, the exact role of~+ remained somewhat unclear. In particular, it was not known whether the other two operations are sufficient by themselves. We provide a positive answer to this question under a very weak restriction on the axiomatization of LP.

## Item Type: |
Conference or Workshop Item (Paper) |
---|---|

## Division/Institute: |
08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG) 08 Faculty of Science > Institute of Computer Science (INF) |

## UniBE Contributor: |
Kuznets, Roman |

## Publisher: |
Patras University Press |

## Language: |
English |

## Submitter: |
Factscience Import |

## Date Deposited: |
04 Oct 2013 15:23 |

## Last Modified: |
05 Dec 2022 14:25 |

## URI: |
https://boris.unibe.ch/id/eprint/37194 (FactScience: 207169) |