Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Cover of the book

2018 | OriginalPaper | Chapter

Inhabitants of Intuitionistic Implicational Theorems

Author : Katalin Bimbó

Published in: Logic, Language, Information, and Computation

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

The aim of this paper is to define an algorithm that produces a combinatory inhabitant for an implicational theorem of intuitionistic logic from a proof in a sequent calculus. The algorithm is applicable to standard proofs, that exist for every theorem, moreover, non-standard proofs can be straightforwardly transformed into standard ones. We prove that the resulting combinator inhabits the simple type for which it is generated.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
next chapter Symbolic Reasoning Methods in Rewriting Logic and Maude
Footnotes
1
The paper [9] deals with generating \(HRM^n_n\) terms and combinatory inhabitants from proofs of \(T_\rightarrow \) theorems.
 
2
This paper was known for a long time only to a select group of relevance logicians, but nowadays, it is freely available online.
 
3
See [1] for information on relevance logics, in general. Dunn [12] introduced a sequent calculus for \(\mathbf {R}_+\), whereas [7, 8] introduced and used a sequent calculus for https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-57669-4_1/469290_1_En_1_IEq43_HTML.gif . See also [6] for a comprehensive overview of a variety of sequent calculi.
 
4
In combinatory terms, parentheses are omitted by assuming association to the left; for example, xz(yz) is a shorthand for ((xz)(yz)). For more on combinatory logic, see for example [4]. Brackets in a sequent indicate a hole in a structure in the antecedent, with the result of a replacement put into brackets in the lower sequent.
 
5
Parentheses in the antecedent of a sequent are restored as in combinatory terms, but parentheses in simple types are restored by association to the right.
 
6
See [14] as well as [10, 11] for such calculi.
 
7
The multi-cut rule is not the same rule as the mix rule, and its use in the proof of the cut theorem is not necessary. It is possible to use triple induction with a parameter called contraction measure as in [5], for example.
 
8
We omit https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-57669-4_1/469290_1_En_1_IEq181_HTML.gif ’s from above the top sequents, which does not mean that the leaves are instances of the axiom; some of them are obviously not.
 
9
\(\mathcal {B}_i\) is one of \(\mathcal {B}_1,\ldots ,\mathcal {B}_n\), whereas \(\mathcal {C}\) is p (if \(\mathcal {B}_i\) is \(\mathcal {B}_n\)) or \(\mathcal {B}_{i+1}\rightarrow \cdots \,\mathcal {B}_n\rightarrow p\) (otherwise).
 
10
We would have included the analysis earlier, if we would have included all the details of the proof of the cut theorem.
 
11
No application of \((\rightarrow {\vdash })\) and \(({\vdash }\rightarrow )\) can be unified with an application of any other rule, as it is easy to see.
 
12
Of course, this is a futile step to start with, and for instance, in a proof-search tree we would prune proofs to forbid such happenings. However, our present definition for a standard proof does not exclude proofs that contain identical sequents.
 
13
The variable that is introduced at this step cannot be anything else than \(x_0\), that we will later on turn into \(\textsf {{I}}\).
 
14
Incidentally, the combinator that we gave after Example 5 is different. It may be an interesting question how to find sequent calculus proofs given a combinatory inhabitant for a simple type.
 
Literature
1.
Anderson, A.R., Belnap, N.D., Dunn, J.M.: Entailment: The Logic of Relevance and Necessity, vol. II. Princeton University Press, Princeton (1992)MATH
2.
Barendregt, H., Ghilezan, S.: Lambda terms for natural deduction, sequent calculus and cut elimination. J. Funct. Program. 10, 121–134 (2000)MathSciNetCrossRef
3.
4.
5.
6.
7.
8.
9.
10.
Curry, H.B.: A Theory of Formal Deducibility. Notre Dame Mathematical Lectures, no. 6. University of Notre Dame Press, Notre Dame (1950)
11.
Curry, H.B.: Foundations of Mathematical Logic. McGraw-Hill Book Company, New York (1963). (Dover, New York, NY, 1977)MATH
12.
13.
14.
Gentzen, G.: Investigations into logical deduction. Am. Philos. Q. 1(4), 288–306 (1964)
15.
Giambrone, S.: Gentzen systems and decision procedures for relevant logics. Ph.D. thesis, Australian National University, Canberra, ACT, Australia (1983)
16.
17.
18.
Lambek, J.: On the calculus of syntactic types. In: Jacobson, R. (ed.) Structure of Language and its Mathematical Aspects, pp. 166–178. American Mathematical Society, Providence (1961)CrossRef
19.
Meyer, R.K.: A general Gentzen system for implicational calculi. Relevance Log. Newsl. 1, 189–201 (1976)MATH
20.
Schönfinkel, M.: On the building blocks of mathematical logic. In: van Heijenoort, J. (ed.) From Frege to Gödel. A Source Book in Mathematical Logic, pp. 355–366. Harvard University Press, Cambridge (1967)
Metadata
Title
Inhabitants of Intuitionistic Implicational Theorems
Author
Katalin Bimbó
Copyright Year
2018
Publisher
Springer Berlin Heidelberg
Book
Logic, Language, Information, and Computation

Print ISBN: 978-3-662-57668-7

Electronic ISBN: 978-3-662-57669-4

Copyright Year: 2018

DOI
https://doi.org/10.1007/978-3-662-57669-4_1

Premium Partner

    Image Credits