Hello!

Inspiré(e) de prendre part à la discussion ? Ou de poser une question ou demander de l’aide ?

Alors bienvenues dans les grands sujets des forums de La Bulle : m’inscrire.

Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires

Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.

Les logiques : notes en vrac
Auteur Message
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17843
Ven 29 Nov 2019 15:40
Message Re: Les logiques : notes en vrac
Une notation apparemment utilisée pour la réduction, est une flèche vers la droite à double‑tête, comme ou peut‑être aussi .

Par exemple 2 + 3 ↠ 5 , qui ne doit pas être confondu avec la flèche simple des fonctions, par exemple x → x + 1 (ou une autre flèche simple, par exemple x ⟼ x + 1 ), bien qu’il y ait un lien entre les deux.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17843
Ven 29 Nov 2019 16:03
Message Re: Les logiques : notes en vrac
Dans la théorie intuitionniste des types, désigne le type inhabité, c’est à dire le type pour lequel il n’existe aucun terme, aucun élément. Il est appelé en Anglais, bottom type, du nom du symbole qui s’appel bottom tack.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17843
Ven 29 Nov 2019 16:20
Message Re: Les logiques : notes en vrac
Une liste des plus importants paradoxes en logique.

Paradoxe :
  • de Curry
  • de Girard
  • de Kleene‑Rosser
  • de Richard
  • de Russel

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17843
Ven 29 Nov 2019 18:02
Message Re: Les logiques : notes en vrac
Je crois que c’est la plus simple présentation des systèmes à la Hilbert :

Le document ci‑dessous a écrit : 
The Hilbert proof systems are systems based on a language with implication and contain a Modus Ponens rule as a rule of inference. They are usually called Hilbert style formalizations. We will call them here Hilbert style proof systems, or Hilbert systems, for short.

Modus Ponens is probably the oldest of all known rules of inference as it was already known to the Stoics (3rd century B.C.). It is also considered as the most ”natural” to our intuitive thinking and the proof systems containing it as the inference rule play a special role in logic. The Hilbert proof systems put major emphasis on logical axioms, keeping the rules of inference to minimum, often in propositional case, admitting only Modus Ponens, as the sole inference rule.


Source : Hilbert Proof Systems, Formal Proofs, Deduction Theorem (stonybrook.edu) [PDF].

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17843
Ven 29 Nov 2019 19:22
Message Re: Les logiques : notes en vrac
Maintenant, ce qui me semble être la comparaison la plus simple des quatre systèmes de démonstrations les plus couramment mentionnés :

La page ci‑dessous a écrit : 
  • Hilbert style. Every line is an unconditional tautology (or theorem).
  • Gentzen style. Every line is a conditional tautology (or theorem) with zero or more conditions on the left.
    • Natural deduction. Every (conditional) line has exactly one asserted proposition on the right.
    • Sequent calculus. Every (conditional) line has zero or more asserted propositions on the right.

In other words, natural deduction and sequent calculus systems are particular distinct kinds of Gentzen-style systems. Hilbert-style systems typically have a very small number of inference rules, relying more on sets of axioms. Gentzen-style systems typically have very few axioms, if any, relying more on sets of rules.


Le calcul des séquents et la déduction naturelle, sont deux cas de système à la Gentzen.

Source : Sequent calculus (wikipedia.org)

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17843
Ven 29 Nov 2019 20:34
Message Re: Les logiques : notes en vrac
On peut donc dire que les systèmes à la Gentzen sont plus généraux que les systèmes à la Hilbert (comme une condition implicite toujours vraie est un cas particulier de condition), et que dans les systèmes à la Gentzen, le calcul des séquents est plus général que la déduction naturelle (comme une conclusion est un cas particulier de zéro ou plusieurs conclusions). Ça expliquerait pourquoi c’est le calcul des séquents qui revient le plus souvent.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17843
Ven 29 Nov 2019 20:44
Message Re: Les logiques : notes en vrac
Sur le calcul des séquents : Le théorème fondamental de Gentzen (persee.fr), Jean Ladrière, 1951.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17843
Lun 2 Déc 2019 17:05
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Il semble que ce qui est appelé kind, est le type d’un type.

Pas tout à fait. Un kind, c’est plutôt le type d’un constructeur de type. Il prend en argument des types, et les types du langage utilisé en pratique, sont appelés des types propres. On a donc des kind s qui appliqués à des type s, donnent des proper type s (types propres). Un kind peut ne prendre aucun paramètre type et produire un proper type, directement. Pour aider à bien s’embrouiller, il peut exister un kind qui s’appel type.

Un exemple : (type, type) -> type ou type -> (type -> type), pourrait être le kind d’un tuple générique et en l’appliquant à (real, real) on pourrait avoir un proper type pour des coordonnées.

Ceci, sous réserve que je ne me trompe pas encore une fois, mais ça semble déjà plus précis.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17843
Lun 2 Déc 2019 19:39
Message Re: Les logiques : notes en vrac
“ Not all collections we can define are sets. ”

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17843
Mer 4 Déc 2019 00:30
Message Re: Les logiques : notes en vrac
Polytype est une abbreviation de polymorphic type et monotype est une abbreviation de monomorphic type.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
cron