Reviewed Works:Gaisi Takeuti, Proof Theory.Georg Kreisel, Proof Theory: Some Personal Recollections.Wolfram Pohlers, Contributions of the Schutte School in Munich to Proof Theory.Stephen G. Simpson, Subsystems of $\mathbf{Z}_2$ and Reverse Mathematics.Solomon Feferman, Proof Theory: A Personal Report.

The Aristotelian syllogistic cannot account for the validity of certain inferences involving relational facts. In this paper, we investigate the prospects for providing a relational syllogistic. We identify several fragments based on (a) whether negation is permitted on all nouns, including those in the subject of a sentence; and (b) whether the subject noun phrase may contain a relative clause. The logics we present are extensions of the classical syllogistic, and we pay special attention to the question of whether reductio (...) ad absurdum is needed. Thus our main goal is to derive results on the existence (or nonexistence) of syllogistic proof systems for relational fragments. We also determine the computational complexity of all our fragments. (shrink)

The paper briefly surveys the sentential proof-theoretic semantics for fragment of English. Then, appealing to a version of Frege’s context-principle (specified to fit type-logical grammar), a method is presented for deriving proof-theoretic meanings for sub-sentential phrases, down to lexical units (words). The sentential meaning is decomposed according to the function-argument structure as determined by the type-logical grammar. In doing so, the paper presents a novel proof-theoretic interpretation of simple type, replacing Montague’s model-theoretic type interpretation (in arbitrary Henkin models). The domains (...) of derivations are collections of derivations in the associated “dedicated” natural-deduction proof-system, and functions therein (with no appeal to models, truth-values and elements of a domain). The compositionality of the semantics is analyzed. (shrink)

The evolution of Euler diagrams is examined from Euler's original system through the modifications made by Venn and Peirce. It is shown that these modifications were motivated by an attempt to increase the expressivity of the diagrams, but that a side effect of these modifications was a loss of the visual clarity of Euler's original system. Euler's original system is reconstructed from a modern, logical point of view. Formal semantics and rules of inference are provided for this reconstruction of Euler's (...) system, and basic logical properties are proved. (shrink)

This paper is a brief history of natural logic at the interface of logic, linguistics, and nowadays also other disciplines. It merely summarizes some facts that deserve to be common knowledge.

We propose an approach to natural language inference based on a model of natural logic, which identifies valid inferences by their lexical and syntactic features, without full semantic interpretation. We greatly extend past work in natural logic, which has focused solely on semantic containment and monotonicity, to incorporate both semantic exclusion and implicativity. Our system decomposes an inference problem into a sequence of atomic edits linking premise to hypothesis; predicts a lexical entailment relation for each edit using a statistical classifier; (...) propagates these relations upward through a syntax tree according to semantic properties of intermediate nodes; and composes the resulting entailment relations across the edit sequence. We evaluate our system on the FraCaS test suite, and achieve a 27% reduction in error from previous work. We also show that hybridizing an existing RTE system with our natural logic system yields significant gains on the RTE3 test suite. (shrink)

We implement the extension of the logical consequence relation to a partial order ≤ on arbitary types built from e (entities) and t (Booleans) that was given in [1], and the definition of monotonicity preserving and monotonicity reversing functions in terms of ≤. Next, we present a new algorithm for polarity marking, and implement this for a particular fragment of syntax. Finally, we list the reseach agenda that these definitions and this algorithm suggest. The implementations use Haskell [8], and are (...) given in ‘literate programming’ style [9]. (shrink)

This presentation of Aristotle's natural deduction system supplements earlier presentations and gives more historical evidence. Some fine-tunings resulted from conversations with Timothy Smiley, Charles Kahn, Josiah Gould, John Kearns,John Glanvillle, and William Parry.The criticism of Aristotle's theory of propositions found at the end of this 1974 presentation was retracted in Corcoran's 2009 HPL article "Aristotle's demonstrative logic".