Uniqueness of normal proofs of minimal formulas

Journal of Symbolic Logic 58 (3):789-799 (1993)
  Copy   BIBTEX

Abstract

A minimal formula is a formula which is minimal in provable formulas with respect to the substitution relation. This paper shows the following: (1) A β-normal proof of a minimal formula of depth 2 is unique in NJ. (2) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NJ. (3) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NK

Categories

Keywords

Reprint years

DOI

10.2307/2275097

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,471

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

A note on the normal form of closed formulas of interpretability logic.Petr Hájek & Vítězslav Švejdar - 1991 - Studia Logica 50 (1):25 - 28.
On Kueker Simple Theories.Ziv Shami - 2005 - Journal of Symbolic Logic 70 (1):216 - 222.
Reduction to first degree in quantificational S5.Michael J. Carroll - 1979 - Journal of Symbolic Logic 44 (2):207-214.
Les automorphismes d'un ensemble fortement minimal.Daniel Lascar - 1992 - Journal of Symbolic Logic 57 (1):238-251.
Conservative reduction classes of Krom formulas.Stål O. Aanderaa, Egon Börger & Harry R. Lewis - 1982 - Journal of Symbolic Logic 47 (1):110-130.
Transfer methods for o-minimal topology.Alessandro Berarducci & Margarita Otero - 2003 - Journal of Symbolic Logic 68 (3):785-794.
Minimal forms in λ-calculus computations.Corrado Böhm & Silvio Micali - 1980 - Journal of Symbolic Logic 45 (1):165-171.
Uniqueness of normal proofs in implicational intuitionistic logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.

Analytics

Added to PP
2009-01-28

Downloads
232 (#88,463)

6 months
13 (#204,126)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Propositional glue and the projection architecture of LFG.Avery D. Andrews - 2010 - Linguistics and Philosophy 33 (3):141-170.
Uniqueness of normal proofs in implicational intuitionistic logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.

Add more citations

References found in this work

The Lambda Calculus. Its Syntax and Semantics.E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.
The formulae-as-types notion of construction.William Alvin Howard - 1980 - In Haskell Curry, Hindley B., Seldin J. Roger & P. Jonathan (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press.
Introduction to Combinators and λ-Calculus.J. Roger Hindley & Jonathan P. Seldin - 1988 - Journal of Symbolic Logic 53 (3):985-986.

Add more references