Completeness and cut-elimination theorems for high-order classical logic. Constructive method
type: Item
instance of: scholarly article
title: Completeness and cut-elimination theorems for high-order classical logic. Constructive method
zbMATH Open document ID: 0831.03031
author: Albert G. Dragalin
published in: Russian Mathematics
publication date: 1996-01-03T00:00:00Z
review text: We are interested in the relation of the truth in models and the deducibility (both with cuts and without cuts) in theories of higher order, i.e., in theories with type-theoretic structure, with (in general, impredicative) the axiom of convolution and, probably, with the axiom of extensionality. We offer a special form of Boolean-valued or Heyting- valued semantics for these theories, which is used for the proof of completeness theorems and cut-elimination theorems. Our main purpose is constructivity of the metamathematics we apply.
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03C90
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 815629
zbMATH Keywords: Boolean-valued semantics
zbMATH Keywords: deducibility
zbMATH Keywords: axiom of convolution
zbMATH Keywords: axiom of extensionality
zbMATH Keywords: Heyting-valued semantics
zbMATH Keywords: completeness
zbMATH Keywords: cut-elimination
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 815629