Skip to Main content Skip to Navigation
Book sections

What is a logic, and what is a proof ?

Lutz Straßburger 1, 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : I will discuss the two problems of how to define identity between logics and how to define identity between proofs. For the identity of logics, I propose to simply use the notion of preorder equivalence. This might be considered to be folklore, but is exactly what is needed from the viewpoint of the problem of the identity of proofs: If the proofs are considered to be part of the logic, then preorder equivalence becomes equivalence of categories, whose arrows are the proofs. For identifying these, the concept of proof nets is discussed.
Complete list of metadata

Cited literature [41 references]  Display  Hide  Download

https://hal.inria.fr/inria-00130523
Contributor : Lutz Straßburger <>
Submitted on : Friday, November 30, 2012 - 11:29:16 AM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Friday, March 1, 2013 - 2:25:10 AM

File

WhatLogicProof.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00130523, version 1

Collections

Citation

Lutz Straßburger. What is a logic, and what is a proof ?. Jean-Yves Beziau. Logica Universalis, Birkhäuser, pp.135-145, 2005, 978-3-7643-7259-0. ⟨inria-00130523⟩

Share

Metrics

Record views

711

Files downloads

634