We present a formalization of first-order predicate calculus with equality which, unlike traditional systems with axiom schemata or substitution rules, is finitely axiomatized in the sense that each step in a formal proof admits only finitely many choices. This formalization is primarily based on the inference rule of condensed detachment of Meredith. The usual primitive notions of free variable and proper substitution are absent, making it easy to verify proofs in a machine-oriented application. Completeness results are presented. The example of (...) Zermelo-Fraenkel set theory is shown to be finitely axiomatized under the formalization. The relationship with resolution-based theorem provers is briefly discussed. A closely related axiomatization of traditional predicate calculus is shown to be complete in a strong metamathematical sense. (shrink)

A principal type-scheme of a -term is the most general type-scheme for the term. The converse principal type-scheme theorem (J.R. Hindley, The principal typescheme of an object in combinatory logic, Trans. Amer. Math. Soc. 146 (1969) 29–60) states that every type-scheme of a combinatory term is a principal type-scheme of some combinatory term.This paper shows a simple proof for the theorem in -calculus, by constructing an algorithm which transforms a type assignment to a -term into a principal type assignment to (...) another -term that has the type as its principal type-scheme. The clearness of the algorithm is due to the characterization theorem of principal type-assignment figures. The algorithm is applicable to BCIW--terms as well. Thus a uniform proof is presented for the converse principal type-scheme theorem for general -terms and BCIW--terms. (shrink)

There is an intimate connection between proofs of the natural deduction systems and typed lambda calculus. It is well-known that in simply typed lambda calculus, the notion of formulae-as-types makes it possible to find fine structure of the implicational fragment of intuitionistic logic, i.e., relevant logic, BCK-logic and linear logic. In this paper, we investigate three classical substructural logics (GL, GLc, GLw) of Gentzen's sequent calculus consisting of implication and negation, which contain some of the right structural rules. In terms (...) of Parigot's -calculus with proper restrictions, we introduce a proof term assignment to these classical substructural logics. According to these notions, we can classify the -terms into four categories. It is proved that well-typed GLx--terms correspond to GLx proofs, and that a GLx--term has a principal type if stratified where x is nil, c, w or cw. Moreover, we investigate embeddings of classical substructural logics into the corresponding intuitionistic substructural logics. It is proved that the Gödel-style translations of GLx--terms are embeddings preserving substructural logics. As by-products, it is obtained that an inhabitation problem is decidable and well-typed GLx--terms are strongly normalizable. (shrink)

This paper provides a finer analysis of the well-known form of the Local Deduction Theorem in contraction-free logics . An infinite hierarchy of its natural strengthenings is introduced and studied. The main results are the separation of its initial four members and the subsequent collapse of the hierarchy.

This paper gives a simple, elegant statement of the condensed detachment rule that is independent of most general unifiers and proves that this is equivalent to the longer, more usual, formulation.

This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none of its deduced steps contains a term of the formn(n(t)) for some term t, where n denotes negation. The first question asks for conditions on the hypotheses that, if satisfied, guarantee the existence of a double-negation-free proof when the conclusion is free of double negation. The second question asks about the existence (...) of an axiom system for classical propositional calculus whose use, for theorems with a conclusion free of double negation, guarantees the existence of a double-negation-free proof. After giving conditions that answer the first question, we answer the second question by focusing on the Lukasiewicz three-axiom system. We then extend our studies to infinite-valued sentential calculus and to intuitionistic logic and generalize the notion of being double-negation free. The double-negation proofs of interest rely exclusively on the inference rule condensed detachment, a rule that combines modus ponens with an appropriately general rule of substitution. The automated reasoning program Otter played an indispensable role in this study. (shrink)

Although ‘glue semantics’ is the most extensively developed theory of semantic composition for LFG, it is not very well integrated into the LFG projection architecture, due to the absence of a simple and well-explained correspondence between glue-proofs and f-structures. In this paper I will show that we can improve this situation with two steps: (1) Replace the current quantificational formulations of glue (either Girard’s system F, or first order linear logic) with strictly propositional linear logic (the quantifier, unit and exponential (...) free version of either MILL or ILL, depending on whether or not tensors are used). (2) Reverse the direction of the standard σ-projection from f-structure to meaning, giving one going from the (atomic nodes of) the glue-proof to the f-structure, rather than from the f-structure to a ‘semantic projection’ which is itself somehow related to the glue-proof. As a side effect, the standard semantic projection of LFG glue semantics can be dispensed with. A result is that LFG sentence structures acquire a level composed of strictly binary trees, constructed out of nodes representing function application and lambda abstraction, with a significant resemblance to external and internal merge in the Minimalist Program. This increased resemblance between frameworks might assist in making useful comparisons. (shrink)