Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Introduction logique type1

Logique démonstration et théorie des types Cassis November C Avant-propos Ce document a pour objectif de donner une vision de ce qu ? est la logique mathématique des bases de la théorie de la démonstration en construire les objets de base des mathématique puis en ?n d ? établir des liens avec la théorie des types et le lambda-calcul Une précision assez importante le symbole aura plusieurs usages et pour éviter trop d ? ambigu? tés et de confusion nous utiliserons ? pour écrire une égalité dé ?nitionnelle du moins dans les chapitres précédant celui sur la théorie des types c ? est-à-dire qu ? un objet que nous verrons pour la première fois sera en général introduit par ce symbole Par exemple la proposition P ? x y devient plus lisible avec cette notation Si plusieurs preuves sont présentées dans ce document elles le sont à titre principalement indicatif et il n ? est pas nécessaire de les intégrer pleinement pour comprendre les dé ?nitions et exemples En e ?et ce document vise avant tout à ce que le lecteur se familiarise avec la logique et la théorie de la démonstration puis dans un deuxième temps avec la théorie des types A ce propos une partie non négligeable du document est dédiée au lambda-calcul cette partie est une introduction négligeant particulièrement les aspects techniques et il est plus que conseillé de suivre un cours sur ce sujet pour plus de rigueur c ? est aussi le cas de la théorie des types En ?n précisons que le public visé est un public déjà familier avec la pratique des maths donc des élèves avec une abstraction et une aisance avec les notations mathématiques du niveau d ? un bon élève de licence La partie I a avant tout été inspirée de Cor tandis que la partie II a été basée sur Sel pour toute la partie sur le lambda- calcul Le lien profond entre logique et lambda-calcul est aussi développé dans Gir qui m ? a servi avant tout d ? inspiration générale et pour parler de la di ?érence entre la sémantique de Tarski et celle de Heyting En ?n le chapitre provient intégralement de HoTT mais seulement de la partie dédiée à la théorie des types de Per MartinL? f sans inclure la part propre à l ? homotopie Ainsi pour plus de rigueur de précision et de profondeur ces ouvrages sont de bonnes ouvertures CIntroduction La distinction entre la syntaxe et la sémantique Faire des mathématiques c ? est en premier lieu parler d ? objets mathématiques Pour un lycéen par exemple ce terme semble souvent être un fourre-tout signi ?ant quelque chose dont on parle en mathématiques ? C ? est une dé ?nition circulaire Une autre façon de dé ?nir ce terme serait de dire qu ? il s ? agit d ? une construction ensembliste mais cela signi ?erait qu ? un objet mathématique est uniquement un ensemble construit à partir d ? un