A constructive valuation semantics for classical logic
type: Item
instance of: scholarly article
title: A constructive valuation semantics for classical logic
zbMATH Open document ID: 0882.03007
author: Franco Barbanera
author: Stefano Berardi
published in: Notre Dame Journal of Formal Logic
publication date: 1998-03-12T00:00:00Z
review text: The goal is to find a witness for \(x\) from a classical proof of \(\exists xP(x)\) from Horn assumptions \(\forall y(Q_1(Y)\&\cdots\& Q_n(y)\to Q_{n+1}(y))\). For this fragment classical and intuitionistic provability coincide, and it is difficult to invent a classical proof which is not already intuitionistic (if obvious redundancies are deleted).
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 1011146
zbMATH Keywords: fragment of classical logic
zbMATH Keywords: classical provability
zbMATH Keywords: intuitionistic provability
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1305/ndjfl/1039886522
OpenAlex ID: W2000752486
cites work: Q4179016
cites work: Q4405122
cites work: Mathematical significance of consistency proofs
cites work: Zur Deutung der intuitionistischen Logik
cites work: Q4099613
cites work: Q5559220
cites work: Q5537599
DOI: 10.1305/NDJFL/1039886522
description: scientific article; zbMATH DE number 1011146