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, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Chapitre d'ouvrage
Jean-Yves Beziau. Logica Universalis, Birkhäuser, pp.135-145, 2005, 978-3-7643-7259-0
Liste complète des métadonnées

Littérature citée [41 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00130523
Contributeur : Lutz Straßburger <>
Soumis le : vendredi 30 novembre 2012 - 11:29:16
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : vendredi 1 mars 2013 - 02:25:10

Fichier

WhatLogicProof.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

384

Téléchargements de fichiers

240