An induction principle and pigeonhole principles for K-finite sets

Authors

Andreas Blass

Type: Article

Publication Date: 1995-12-01

Citations: 2

DOI: https://doi.org/10.2307/2275881

View Ask PDF

Abstract

Abstract We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Bénabou and Loiseau. We also comment on some variants of this pigeonhole principle.

Locations

Journal of Symbolic Logic
View
arXiv (Cornell University)
PDF

Ask a Question About This Paper

Summary

An Induction Principle and Pigeonhole Principles for K-Finite Sets

1994-01-01

Andreas Blass

We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Benabou and Loiseau. We also comment on … We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Benabou and Loiseau. We also comment on some variants of this pigeonhole principle.

AN INDUCTION PRINCIPLE IN SET THEORY I.

1969-01-01

Moto-o Takahashi

Intuitionistic Type Theory

1995-01-01

W. S. Anglin , J. Lambek

Intuitionistic fixed point logic

2020-10-09

Ulrich Berger , Hideki Tsuiki

View PDF Chat

An induction principle for pure type systems

2001-09-01

Gilles Barthe , John Hatcliff , Morten Heine Sørensen

A new model construction by making a detour via intuitionistic theories III: Ultrafinitistic proofs of conservations of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" altimg="si1.svg"><mml:msubsup><mml:mrow><mml:mi mathvariant="normal">Σ</mml:mi></mml:mrow><mml:mrow><mml:mn>1</mml:mn></mml:mrow><mml:mrow><mml:mn>1</mml:mn></mml:mrow></mml:msubsup></mml:math> collection

2022-10-28

Kentaro Sato

On the k-Boundedness for Existential Rules

2018-01-01

Stathis Delivorias , Michel Leclère , Marie-Laure Mugnier +1 more

View PDF Chat

Intuitionistic fixed point theories over set theories

2015-03-30

Toshiyasu Arai

View PDF Chat

A Formalization of Brouwer’s Argument for Bar Induction

2018-01-01

Ryota Akiyoshi

Intuitionistic Logic

2017-08-18

Dirk van Dalen

There are basically two ways to view intuitionistic logic: as a philosophical-foundational issue in mathematics; or as a technical discipline within mathematical logic. Considering first the philosophical aspects, for they … There are basically two ways to view intuitionistic logic: as a philosophical-foundational issue in mathematics; or as a technical discipline within mathematical logic. Considering first the philosophical aspects, for they will provide the motivation for the subject, this chapter follows L. E. J. Brouwer, the founding father of intuitionism. Although Brouwer himself contributed little to intuitionistic logic as seen from textbooks and papers, he did point the way for his successors.

Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory

2000-01-01

Gilles Dowek

View PDF Chat

Induction Principles for Sets

2008-05-01

Janusz Czelakowski

Eliminability of cuts in the intuitionistic simple theory of types in the form of a sequent calculus with extensionality

1988-12-31

View PDF Chat

The Implications of the No-Free-Lunch Theorems for Meta-induction

2023-03-13

David H. Wolpert

View PDF Chat

Fragments of Kripke–Platek set theory and the metamathematics of $$\alpha $$ α -recursion theory

2016-09-06

Sy‐David Friedman , Wei Li , Tin Lok Wong

View PDF Chat

The intuitionistic fragment of computability logic at the propositional level

2007-05-24

Giorgi Japaridze

View PDF Chat

Fixed point theorems and semantics: a folk tale

1982-05-01

J.-L. Lassez , V.L. Nguyen , Ea Sonenberg

Intuitionistic Open Induction and Least Number Principle and the Buss Operator

1998-04-01

Mohammad Ardeshir , Mojtaba Moniri

In "Intuitionistic validity in $T$-normal Kripke structures," Buss asked whether every intuitionistic theory is, for some classical theory $T$, that of all $T$-normal Kripke structures ${\cal H}(T)$ for which he … In "Intuitionistic validity in $T$-normal Kripke structures," Buss asked whether every intuitionistic theory is, for some classical theory $T$, that of all $T$-normal Kripke structures ${\cal H}(T)$ for which he gave an r.e. axiomatization. In the language of arithmetic $\mathit{Iop}$ and $\mathit{Lop}$ denote PA$^{-}$ plus Open Induction or Open LNP, $\mathit{iop}$ and $\mathit{lop}$ are their intuitionistic deductive closures. We show $\mathcal{H}\mathit{(Iop)}$ $=\mathit{lop}$ is recursively axiomatizable and $\mathit{lop}\vdash_{i\ c}\dashv \mathit{iop}$, while $i\forall_{1}\not\vdash \mathit{lop}$. If $iT$ proves PEM $_{\mathrm{atomic}}$ but not totality of a classically provably total Diophantine function of $T$, then $\mathcal{H}(T)\not\subseteq iT$ and so $iT\not\in \mathrm{range({\cal H})}$. A result due to Wehmeier then implies $i\Pi_{1}\not\in\mbox{range}({\cal H})$. We prove $\mathit{Iop}$ is not $\forall_{2}$-conservative over $i\forall_{1}$. If $\mathit{Iop}\subseteq T\subseteq I\forall_{1}$, then $iT$ is not closed under MR $_{\mathrm{open}}$ or Friedman's translation, so $iT\not\in$ range (${\cal H}$). Both $\mathit{Iop}$ and $I\forall_{1}$ are closed under the negative translation.

View PDF Chat

Fixed-Point Elimination in the Intuitionistic Propositional Calculus

2016-01-01

Silvio Ghilardi , Maria João Gouveia , Luigi Santocanale

View PDF Chat

A Lindström theorem for intuitionistic first-order logic

2023-07-26

Grigory K. Olkhovikov , Guillermo Badía , Reihane Zoghifard

View PDF Chat

Finite sets in homotopy type theory

2018-01-08

Dan Frumin , Herman Geuvers , Léon Gondelman +1 more

We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. … We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of "finite sets over type A" à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.

View PDF Chat

Finite sets in homotopy type theory

2017-12-22

Dan Frumin , Herman Geuvers , Léon Gondelman +1 more

View PDF Chat

Sheaves and logic

1979-01-01

Michael Fourman , Dana Scott

Orbits and monoids in a topos

1994-02-01

Jean Bénabou , Bruno Loiseau

Toposes without points

1974-12-01

Michael Barr

La logique des topos

1981-03-01

André Boileau , André Joyal

Les synthèses nouvelles par le rapprochement de disciplines mathématiques différentes constituent des événements remarquables dans l'histoire des mathématiques. Une telle synthèse semble émerger actuellement du rapprochement de: (1) La géométrie … Les synthèses nouvelles par le rapprochement de disciplines mathématiques différentes constituent des événements remarquables dans l'histoire des mathématiques. Une telle synthèse semble émerger actuellement du rapprochement de: (1) La géométrie algébrique sous la forme élaborée par Grothendieck. (2) La logique formelle. Le point de contact s'est effectué aux environs de 1970 par W. Lawvere et M. Tierney et l'instrument de rapprochement a été la théorie des catégories, plus particulièrement la théorie des faisceaux. Depuis ce moment, une dialectique incessante imprime un mouvement dynamique à toute une série de recherches qui visent à rapprocher les méthodes suivantes: (1) Mathématique intuitionniste. (2) Forcing de Cohen et Robinson. (3) Logique algébrique. (4) Géométrie algébrique. (5) Géométrie différentielle et analytique. (6) Topologie algébrique: cohomologie, homotopie. (7) Théorie de Galois. Certains rapprochements sont dans un stade avancé, d'autres encore embryonnaires: (6) ↔ (3). La structure centrale qui joue le rôle d'élément provocateur et unificateur est celle de topos. Avant d'être axiomatisée par Lawvere, celle-ci a été étudiée systématiquement par l'école de Grothendieck (voir [1]) et c'est dans le contexte de la géométrie algébrique qu'elle fit son apparition. Dans cet article nous utiliserons cependant la définition de Lawvere telle qu'améliorée par Mikkelsen [12] et Kock [8]. Le but de ce travail est de présenter une version (au sens de la logique formelle) du concept de topos et d'examiner brièvement les rapports entre la théorie des topos, la logique et les mathématiques. Cette version a déjà été exposée par l'un des auteurs lors du Séminaire de Mathématiques Supérieures de l'Université de Montréal, à l'été 1974. Depuis elle a fait l'objet d'une thèse où elle a été améliorée et sa cohérence vérifiée [2]. Des systèmes différents ont été proposés simultanément par Fourman [4] et Coste [3].

Some topos theoretic concepts of finiteness

1975-01-01

Anders Kock , P. Lecouturier , Chr. Juul Mikkelsen

Logical and set theoretical tools in elementary topoi

1975-01-01

Gerhard Osius