Online research in philosophy

In the 1920s, Ackermann and von Neumann, in pursuit of Hilbert's programme, were working on consistency proofs for arithmetical systems. One proposed method of giving such proofs is Hilbert's epsilon-substitution method. There was, however, a second approach which was not reflected in the publications of the Hilbert school in the 1920s, and which is a direct precursor of Hilbert's first epsilon theorem and a certain ?general consistency result? due to Bernays. An analysis of the form of this so-called ?failed proof? sheds further light on an interpretation of Hilbert's programme as an instrumentalist enterprise with the aim of showing that whenever a ?real? proposition can be proved by ?ideal? means, it can also be proved by ?real?, finitary means.

The II-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the II-calculus and prove the cut-elimination theorem.The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The type-theoretic setting considered here elegantly illustrates the distinction between the processes of normalization in a natural deduction system and cut-elimination in a Gentzen-style sequent calculus.

We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present a proof search strategy which allows it to be used for automated proof search. We prove that this search strategy is terminating and complete by showing how it can be used to mimic derivations obtained from an existing calculus GBiInt for bi intuitionistic logic. As far as we know, our new calculus is the first sequent calculus for bi intuitionistic logic which uses no semantic additions like labels, which has a purely syntactic cut elimination proof, and which can be used naturally for backwards proof search. Keywords: Bi-intuitionistic logic, display calculi, proof search.

We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.

Epsilon Calculi are extended forms of the predicate calculus that incorporate epsilon terms. Epsilon terms are individual terms of the form ‘εxFx’, being defined for all predicates in the language. The epsilon term ‘εxFx’ denotes a chosen F, if there are any F’s, and has an arbitrary reference otherwise. Epsilon calculi were originally developed to study certain forms of Arithmetic, and Set Theory; also to prove some important meta-theorems about the predicate calculus. Later formal developments have included a variety of intensional epsilon calculi, of use in the study of necessity, and more general intensional notions, like belief. An epsilon term such as ‘ εxFx’ was originally read ‘the first F’, and in arithmetical contexts ‘the least F’. More generally it can be read as the demonstrative description ‘that F’, when arising either deictically, i.e. in a pragmatic context where some F is being pointed at, or in linguistic cross-reference situations, as with, for example, ‘There is a red haired man in the room. That red haired man is Caucasian’. The application of epsilon terms to natural language shares some features with the use of iota terms within the theory of descriptions given by Bertrand Russell, but differs in formalising aspects of a slightly different theory of reference, first given by Keith Donnellan. More recently epsilon terms have been used by a number of writers to formalise cross-sentential anaphora, which would arise if ‘that red haired man’ in the linguistic case above was replaced with a pronoun such as ‘he’. There is then also the similar application in intensional cases, like ‘There is a red haired man in the room. Celia believed he was a woman.’.

The epsilon calculus improves upon the predicate calculus by systematically providing complete individual terms. Recent research has shown that epsilon terms are therefore the 'logically proper names' Russell was not able to formalise, but their use improves upon Russell's Theory of Descriptions not just in that way. This paper details relevant formal aspects of the epsilon calculus before tracing its extensive application not just to the theory of descriptions, but also to more general problems with anaphoric reference. It ends by contrasting a Meinongian account of cross-reference in intensional constructions with the epsilon account.

Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in particular it is harder to design cut elimination procedures. In this paper we see a cut elimination procedure for a deep inference system for classical predicate logic. As a consequence we derive Herbrand's Theorem, which we express as a factorisation of derivations.

The epsilon calculus is a logical formalism developed by David Hilbert in the service of his program in the foundations of mathematics. The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. Specifically, in the calculus, a term..