Définition de la science

Le contenu va décevoir les théoriciens, mais j'ai fait exprès de mettre ce titre provocateur.

En fait, je ne vais pas du tout parler, contrairement à d'habitude, de "trucs élevés" :-D , mais juste tenter d'arrêter des règles du jeu qui soient le plus possible compatibles avec les souris d'ordinateur et la façon dont marchent les navigateurs aujourd'hui, avec java script. Mais vous pouvez continuer de lire, ça renseigne quand-même, je suis un grand logicien :-D :-D

L'utilité c'est que je me reconnecterai à ce fil quand j'aurai "enfin" le courage de me dire que je vais torcher un exécutable Lazarus avec "tout" dedans (j'ai parfois des manies totalement maladives, je ne veux plus utiliser Lazarus pour faire "un seule truc", parce que même pour "Hello World", il me pond un exe de 14 mégas que je ne peux pas envoyer par mail) J'avais trouvé des solutions, mais les ai oubliées (pour "vider" les exe de leur 99.9% de contenus inutiles. Et franchement les concepteurs IDE font c***r avec leur flemme de configurer bien (ils mettent tout dans le fichierà la compilation pour être sûr qu'il ne manque rien)

Je pense que je vais pencher pour le "si .. alors" bien que l'écriture polonaise soit bien meilleure pour la polarité. Si je publie sur le forum c'est pour dire que toutes les améliorations sont bienvenues.

La suite des éléments que je décris sont complets pour la science, ie un énoncé ne pouvant être prouvé avec ces règles n'est pas scientifique (il a un contre-modèlee concret) ne peut être prouvé avec aucune règle.

Je commence ce post avec le propositionnel. Je ne traire que l'écriture polonaise ici parce que la polarité logique y est immédiatement visible (un signe sur 2 est positif, selon son rang: les impairs sont positifs, les paires négatifs).

1/ Formation des phrases:

1.1/ Quand une personne commence par taper un implique, (ie un $\to$ ) deux rectangles se mettent en surbrillance. Cela force l'auteur à écriture des phrases syntaxiquement correctes.

1.2/ Je ne cache pas que j'aimerais un système linguistique qui accepte toute suite de signes comme phrases correctes, mais la vie est dure. Ce sera pour plus tard.

1.3/ Si elle ne remplit pas les rectangles, ils sont automatiquement remplis par une phrase par défaut (je ne sais pas encore si je vais prendre le vrai ou le faux pour ce rôle)

1.4/ La longueur éditable (enfin écrivable) est limitée. Par exemple, si l'auteur ne clique pas sur $\to$, il ne peut taper qu'un symbole. Comme je ne sais pas si je vais accepter une infinité de variables, symbole peut vouloir dire "mot sans espace" et les séparateurs seront des espaces

2/ Une fois tapé sa phrase, un bouton permet de la doubler et mettre un $\to $ devant. Cela est fait dans l'option de la fenètre principale (il y a deux fenètres) où on ne peut valider que des théorèmes. Ainsi, après avoir tapé $X$, le bouton validé envoie $\to$ X X

3/ Théorèmes:

3.0/ Polarité avec les couleurs: les occurrences négatives sont en vertes et les positives en rouge (sur fond noir). L'occurrence d'une sous-phrase est donnée par le rang de son premier symbole. Exemple:

$\to $ $\to $ A B $\to$ C D

3.1/ Une fois un théorème présent sur le board, on peut le modifier avec les règles suivantes:

3.2/ On peut permuter des hypothèses dans une sous-phrase.

$\to$ A $\to $ B
peut devenir
$\to$ B $\to $ A

il suffit pour ça de cliquer sur la première flèche verte ou rouge. A noter qu'avec "si .. alors si .. ", ce serait ici plus joli, puisqu'on cliquerait "au milieu" sur le "alors si" (qui est littéralement synonyme de "et" sur la Terre entière)

3.3/ On peut modifier où on veut n'importe quelle sous-phrase (c'est pourquoi il y a deux fenètres) . Il suffit de cliquer sur son premier symbole. Attention, le logiciel ajoute alors tout à gauche l'implication de l'ancienne par la nouvelle phrase et une flèche rouge suivie d'une verte tout à gauche, quand la position était négative et sinon l'implication de la nouvelle par l'ancienne. Exemple:

$\to$ A B
peut devenir
$\to$ $\to$ B C $\to $ A C

car ayant modifié B (occurrence positive) en C

3.4/ Le logiciel peut cacher les hypothèses en les faisant apparaître dans une fenêtre déroulante et en les appelant "axiome", exemple:

$ \to $ $\to$ A X R
devient juste
R

et $\to$ A X est mis dans les axiomes. (la liste appelée "axiomes", mais qui est personnelle à l'auteur(e))

La coloration négative est gardée (le fait de commencer par une flèche verte): 2 raisons.
R1/ Pratique (rien à programmer
R2/ Rappeler que les axiome sont attaqués par la science (et non pas défendus, comme le croient bcp de gens)

3.5/ On peut SI on le souhaite, fusionner dans :

Debut $\to $ A $\to $ A Fin
en cliquant sur la première flèche verte, du coup ça devient
Debut $\to $ A Fin

4/ Vous avez là un système complet pour la logique intuitionniste en ce sens que quelque soit $P$ un théorème intuitionniste, il est possible de le faire s'afficher sur le board en respectant ces règles et en n'envoyant dans les axiomes que des phrases de la forme $\to $ X X

5/ Je vais encore faire des choix graphiques pour l'insertion de l'axiome du RPA (afin que la logique soit vraiment complète). De même la commutativité m'ennuie, car elle oblige la logiciel à parser "salement", donc je vais voir si je peux arranger ça

Je poste donc sans avoir encore décidé la graphie du RPA.

Et :-D ça va de soi, ce programme n'est pas très long à faire en Lazarus (30 mn? environ, sans compter la doc pour me remémorer les lectures d'événements clavier et souris), mais comme je n'ai aucune ambition de devenir un codeur, il va de soi :-D :-D :-D que si quelqu'un veut le faire en 15 mn en java script pour insertion directe sur les pages web, Her or He is megawelcome