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 : 21370
Ven 18 Mar 2022 22:34
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Des choses à noter.

Comme déjà vu il y a longtemps, ne pas parvenir à vérifier une chose, n’est pas équivalent à prouver que cette chose n’existe pas. Mais c’est seulement dans le cas général, pas dans tous les cas. Avec une hypothèse comme {(nat N)}, une tentative d’unification à (nat (s N)) ne peut que échouer, se concluant par un false (ou le constat devrait‑il être autre chose que false ?), […]

Oui, le constat devrait être autre chose que false : indéterminé.

Mais attention, la seule présence d’une variable non‑résoluble dans un terme, ne fait pas automatiquement conclure indéterminé en cas d’échec de la vérification, ça dépend de la cause de l’échec (attention aussi à la non‑pertinence de l’ordre de vérification des éléments d’un terme). Si V est une variable non‑résoluble, que la règle (r …) n’existe pas, alors la vérification de (r V) se conclue par false, si la règle est « (r V) : (eq V c). », le conclusion est indéterminée, si la règle est « (r V). » la conclusion est true.

Une conclusion suite à un échec, peut dépendre de la cause de l’échec et cette conclusion ne doit pas dépendre de l’ordre des vérifications.

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 : 21370
Ven 18 Mar 2022 23:23
Message Re: Les logiques : notes en vrac
Un type d’équivalence est celle entre deux conjonctions, qu’on obtient par transformations successives (terme vers conjonction et conjonction vers terme). Sans pouvoir l’expliquer, cette équivalence me semble importante, me revient fréquemment.

L’exemple d’équivalence qui avait été rapidement discuté, une liste interprété comme un ensemble à partir de deux règles d’équivalence, l’une pour la non‑pertinence de la l’ordre de ses éléments, l’autre pour la non‑pertinence de leurs duplications, cette équivalence là aussi, ne peut que se vérifier par des transformation successives à partir de ces deux règles. Mais comment le vérifier en général entre deux listes quelconques dont on sait qu’elles sont équivalentes ? Ça ne peut que dépendre de ce qui produit ces deux listes ; parce que là est la raison pour laquelle ont sait qu’elles sont équivalentes.

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 : 21370
Sam 19 Mar 2022 11:52
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Un type d’équivalence est celle entre deux conjonctions, qu’on obtient par transformations successives (terme vers conjonction et conjonction vers terme). Sans pouvoir l’expliquer, cette équivalence me semble importante, me revient fréquemment.

[…]

Une partie de cette équivalence peut représenter les hypothèses à un seul cas. Le brouillon de langage de démonstration utilise une construction nommée “ open hyps ” (*), pour dire qu’on ouvre une hypothèse à plusieurs cas, tout en ayant remarqué que parler de cas avec une hypothèse n’en ayant qu’un seul, est dissonant. Il y a une différence autant importante entre une hypothèse à un seul cas et une hypothèse à plusieurs cas, qu’entre un phénomène déterministe et un phénomène non‑déterministe, ce qui justifie la distinction. La manière de parler d’une hypothèse a un seul cas n’avait pourtant pas été décidée. Peut‑être parler d’expansion de l’hypothèse serait un bon mot et cette expansion est équivalente à l’hypothèse d’origine, comme elle n’a qu’un seul cas. On ne peut parler d’équivalence que pour une hypothèse ayant un seul cas, il n’est pas possible de dire qu’un cas d’une hypothèse à plusieurs cas est équivalent à l’hypothèse d’origine, puisque c’en est une restriction.


(*) Le choix n’était pas le meilleur, le singulier aurait été préférable, comme en cas de plusieurs hypothèses, on ne va pas les ouvrir toutes en même temps, plutôt par exemple ouvrir la seconde sous un cas de la première, et alors on aurait une seconde construction “ open hyp ”, au singulier, imbriquée.

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 : 21370
Sam 19 Mar 2022 15:37
Message Re: Les logiques : notes en vrac
Retour sur l’application d’une règle sous hypothèse à un terme.

Il a été dit que le terme qui est l’argument, doit être vérifié et être autant ou plus spécifique que le terme de l’hypothèse. Ce qui avait justifié la seconde condition, est que si le terme de l’hypothèse lie des variables du terme, le terme n’est plus garanti vérifié. Pourtant, dans l’organisation a deux couches où les conditions des règles de la première couche sont vues comme des hypothèse et les termes de la deuxième, comme des arguments, cette condition n’avait pas été posée. Dans ce cas, le terme peut nécessiter une résolution. Il n’y a pas de raison d’exclure cette possibilité avec l’application d’une règle sous hypothèse à un terme ; le rendre compatible avec le terme de l’hypothèse, pourrait être un but d’une résolution.

On peut objecter qu’il peut y avoir plusieurs solutions, mais ça n’a pas de raison d’être plus un problème que quand il existe plusieurs résolutions possibles pour un terme.

Cette nouvelle approche n’exclue pas la possibilité de l’ancienne, elle est plus générale. L’ancienne approche posait les bonnes conditions sur le terme, mais restreignait arbitrairement le chemin menant à la résolution de ces conditions.

Éventuellement, il faudrait prévoir une construction disant qu’on se restreint à la première approche si c’est vraiment ce qu’on veut pour une raison ou une autre.

Image
Hibou57

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