Proof and Canonical Proof

Certain anti-realisms about mathematics are distinguished by their taking proof rather than truth as the central concept in the account of the meaning of mathematical statements. This notion of proof which is meaning determining or canonical must be distinguished from a notion of demonstration as more generally conceived. This paper raises a set of objections to Dummett's characterisation of the notion via the notion of a normalised natural deduction proof. The main complaint is that Dummett's use of normalised natural deduction proofs relies on formalisation playing a role for which it is unfit. Instead I offer an alternative account which does not rely on formalisation and go on to examine the relation of proof to canonical proof, arguing that rather than requiring an explicit characterisation of canonical proofs we need to be more aware of the complexities of that relation.     

Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic

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.     

Diagrams as sketches

This article puts forward the notion of ??evolving diagram?? as an important case of mathematical diagram. An evolving diagram combines, through a dynamic graphical enrichment, the representation of an object and the representation of a piece of reasoning based on the representation of that object. Evolving diagrams can be illustrated in particular with category-theoretic diagrams (hereafter ??diagrams*??) in the context of ??sketch theory,?? a branch of modern category theory. It is argued that sketch theory provides a diagrammatic* theory of diagrams*, that it helps to overcome the rivalry between set theory and category theory as a general semantical framework, and that it suggests a more flexible understanding of the opposition between formal proofs and diagrammatic reasoning. Thus, the aim of the paper is twofold. First, it claims that diagrams* provide a clear example of evolving diagrams, and shed light on them as a general phenomenon. Second, in return, it uses sketches, understood as evolving diagrams, to show how diagrams* in general should be re-evaluated positively.     

论开放域的表征(英文)

本文通过引入开放域的概念来拓展文恩-i图系统(带个体的文恩图)。"隐无(absence)"的概念在本论文中被当做独立的范畴加以讨论。"隐无"和开放域的概念共同不相容于集合论中绝对补的概念。     

Strategic Construction of Fitch-style Proofs

Symlog is a system for learning symbolic logic by computer that allows students to interactively construct proofs in Fitch-style natural deduction. On request, Symlog can provide guidance and advice to help a student narrow the gap between goal theorem and premises. To effectively implement this capability, the program was equipped with a theorem prover that constructs proofs using the same methods and techniques the students are being taught. This paper discusses some of the aspects of the theorem prover's design, including its set of proof-construction strategies, its unification algorithm as well as some of the tradeoffs between efficiency and pedagogy.     

Applications of weak Kripke semantics to intermediate consequences

Section 1 contains a Kripke-style completeness theorem for arbitrary intermediate consequences. In Section 2 we apply weak Kripke semantics to splittings in order to obtain generalized axiomatization criteria of the Jankov-type. Section 3 presents new and short proofs of recent results on implicationless intermediate consequences. In Section 4 we prove that these consequences admit no deduction theorem. In Section 5 all maximal logics in the 3 ^rd counterslice are determined. On these results we reported at the 1980 meeting on Mathematical Logic at Oberwolfach. This paper concerns propositional logic only.     

Mathematical Method and Proof

On a traditional view, the primary role of a mathematical proof is to warrant the truth of the resulting theorem. This view fails to explain why it is very often the case that a new proof of a theorem is deemed important. Three case studies from elementary arithmetic show, informally, that there are many criteria by which ordinary proofs are valued. I argue that at least some of these criteria depend on the methods of inference the proofs employ, and that standard models of formal deduction are not well-equipped to support such evaluations. I discuss a model of proof that is used in the automated deduction community, and show that this model does better in that respect.     

Compositional Z: Confluence Proofs for Permutative Conversion

This paper gives new confluence proofs for several lambda calculi with permutation-like reduction, including lambda calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions, and a lambda calculus with explicit substitutions. For lambda calculi with permutative conversion, naïve parallel reduction technique does not work, and (if we consider untyped terms, and hence we do not use strong normalization) traditional notion of residuals is required as Ando pointed out. This paper shows that the difficulties can be avoided by extending the technique proposed by Dehornoy and van Oostrom, called the Z theorem: existence of a mapping on terms with the Z property concludes the confluence. Since it is still hard to directly define a mapping with the Z property for the lambda calculi with permutative conversions, this paper extends the Z theorem to compositional functions, called compositional Z, and shows that we can adopt it to the calculi.     

A Mixed λ-calculus

The aim of this paper is to define a λ-calculus typed in aMixed (commutative and non-commutative) Intuitionistic Linear Logic. The terms of such a calculus are the labelling of proofs of a linear intuitionistic mixed natural deduction NILL, which is based on the non-commutative linear multiplicative sequent calculus MNL [RuetAbrusci 99]. This linear λ-calculus involves three linear arrows: two directional arrows and a nondirectional one (the usual linear arrow). Moreover, the -terms are provided with seriesparallel orders on free variables. We prove a normalization theorem which explicitly gives the behaviour of the order during the normalization procedure. Special Issue Categorial Grammars and Pregroups Edited by Wojciech Buszkowski and Anne Preller     

A framework for the transfer of proofs,lemmas and strategies from classical to non classical logics

There exist valuable methods for theorem proving in non classical logics based on translation from these logics into first-order classical logic (abbreviated henceforth FOL). The key notion in these approaches istranslation from aSource Logic (henceforth abbreviated SL) to aTarget Logic (henceforth abbreviated TL). These methods are concerned with the problem offinding a proof in TL by translating a formula in SL, but they do not address the very important problem ofpresenting proofs in SL via a backward translation. We propose a framework for presenting proofs in SL based on a partial backward translation of proofs obtained in a familiar TL: Order-Sorted Predicate Logic. The proposed backward translation transfers some formulasF _TL belonging to the proof in TL into formulasF _SL , such that the formulasF _SL either (a) belong to a corresponding deduction in SL (in the best case) or, (b) are semantically related in some precise way, to formulas in the corresponding deduction in SL (in the worst case). The formulasF _TL andF _SL can obviously be considered aslemmas of their respective proofs. Therefore the transfer of lemmas of TL gives at least a skeleton of the corresponding proof in SL. Since the formulas of a proof keep trace of the strategy used to obtain the proof, clearly the framework can also help in solving another fundamental and difficult problem:the transfer of strategies from classical to non classical logics. We show how to apply the proposed framework, at least to S5, S4(p), K, T, K4. Two conjectures are stated and we propose sufficient (and in general satisfactory) conditions in order to obtain formulas in the proof in SL. Two particular cases of the conjectures are proved to be theorems. Three examples are treated in full detail. The main lines of future research are given.     

Does the deduction theorem fail for modal logic?

Various sources in the literature claim that the deduction theorem does not hold for normal modal or epistemic logic, whereas others present versions of the deduction theorem for several normal modal systems. It is shown here that the apparent problem arises from an objectionable notion of derivability from assumptions in an axiomatic system. When a traditional Hilbert-type system of axiomatic logic is generalized into a system for derivations from assumptions, the necessitation rule has to be modified in a way that restricts its use to cases in which the premiss does not depend on assumptions. This restriction is entirely analogous to the restriction of the rule of universal generalization of first-order logic. A necessitation rule with this restriction permits a proof of the deduction theorem in its usual formulation. Other suggestions presented in the literature to deal with the problem are reviewed, and the present solution is argued to be preferable to the other alternatives. A contraction- and cut-free sequent calculus equivalent to the Hilbert system for basic modal logic shows the standard failure argument untenable by proving the underivability of ${\square\,A}$ from A.     

Marginalia on Sequent Calculi

The paper discusses the relationship between normal natural deductions and cutfree proofs in Gentzen (sequent) calculi in the absence of term labeling. For Gentzen calculi this is the usual version; for natural deduction this is the version under the complete discharge convention, where open assumptions are always discharged as soon as possible. The paper supplements work by Mints, Pinto, Dyckhoff, and Schwichtenberg on the labeled calculi.     

Socratic Trees

The method of Socratic proofs (SP-method) simulates the solving of logical problem by pure questioning. An outcome of an application of the SP-method is a sequence of questions, called a Socratic transformation. Our aim is to give a method of translation of Socratic transformations into trees. We address this issue both conceptually and by providing certain algorithms. We show that the trees which correspond to successful Socratic transformations—that is, to Socratic proofs—may be regarded, after a slight modification, as Gentzen-style proofs. Thus proof-search for some Gentzen-style calculi can be performed by means of the SP-method. At the same time the method seems promising as a foundation for automated deduction.     

Seeing the language: a diagrammatic approach to natural discourse

The key idea behind the diagrammatic approach presented in the paper is that the sophisticated mechanisms of human visual construction also play an important role in natural languages. We propose a diagrammatic representation of English, giving examples, translation rules, and semantics. Special attention will be paid to anaphoric phenomena, in particular, the possibility of a uniform treatment of anaphoric pronouns.     

Normal Natural Deduction Proofs (in classical logic)

Natural deduction (for short: nd-) calculi have not been used systematically as a basis for automated theorem proving in classical logic. To remove objective obstacles to their use we describe (1) a method that allows to give semantic proofs of normal form theorems for nd-calculi and (2) a framework that allows to search directly for normal nd-proofs. Thus, one can try to answer the question: How do we bridge the gap between claims and assumptions in heuristically motivated ways? This informal question motivates the formulation of intercalation calculi. Ic-calculi are the technical underpinnings for (1) and (2), and our paper focuses on their detailed presentation and meta-mathematical investigation in the case of classical predicate logic. As a central theme emerges the connection between restricted forms of nd-proofs and (strategies for) proof search: normal forms are not obtained by removing local "detours", but rather by constructing proofs that directly reflect proof-strategic considerations. That theme warrants further investigation.

     

Harmonising natural deduction

Prawitz proved a theorem, formalising ‘harmony’ in Natural Deduction systems, which showed that, corresponding to any deduction there is one to the same effect but in which no formula occurrence is both the consequence of an application of an introduction rule and major premise of an application of the related elimination rule. As Gentzen ordered the rules, certain rules in Classical Logic had to be excepted, but if we see the appropriate rules instead as rules for Contradiction, then we can extend the theorem to the classical case. Properly arranged there is a thoroughgoing ‘harmony’, in the classical rules. Indeed, as we shall see, they are, all together, far more ‘harmonious’ in the general sense than has been commonly observed. As this paper will show, the appearance of disharmony has only arisen because of the illogical way in which natural deduction rules for Classical Logic have been presented.     

Commuting Conversions vs. the Standard Conversions of the “Good” Connectives

Commuting conversions were introduced in the natural deduction calculus as ad hoc devices for the purpose of guaranteeing the subformula property in normal proofs. In a well known book, Jean-Yves Girard commented harshly on these conversions, saying that ‘one tends to think that natural deduction should be modified to correct such atrocities.’ We present an embedding of the intuitionistic predicate calculus into a second-order predicative system for which there is no need for commuting conversions. Furthermore, we show that the redex and the conversum of a commuting conversion of the original calculus translate into equivalent derivations by means of a series of bidirectional applications of standard conversions. Presented by Heinrich Wansing and Jacek Malinowski     

Harmony and Autonomy in Classical Logic

Michael Dummett and Dag Prawitz have argued that a constructivist theory of meaning depends on explicating the meaning of logical constants in terms of the theory of valid inference, imposing a constraint of harmony on acceptable connectives. They argue further that classical logic, in particular, classical negation, breaks these constraints, so that classical negation, if a cogent notion at all, has a meaning going beyond what can be exhibited in its inferential use.I argue that Dummett gives a mistaken elaboration of the notion of harmony, an idea stemming from a remark of Gerhard Gentzen"s. The introduction-rules are autonomous if they are taken fully to specify the meaning of the logical constants, and the rules are harmonious if the elimination-rule draws its conclusion from just the grounds stated in the introduction-rule. The key to harmony in classical logic then lies in strengthening the theory of the conditional so that the positive logic contains the full classical theory of the conditional. This is achieved by allowing parametric formulae in the natural deduction proofs, a form of multiple-conclusion logic.     

Deduction theorems for RM and its extensions

In this paper logics defined by finite Sugihara matrices, as well as RM itself, are discussed both in their matrix (semantical) and in syntactical version. For each such a logic a deduction theorem is proved, and a few applications are given.