Déduction naturelle

[invite6754323456711]

Bonjour,

Je cherche à démonter à partir des règles d'inférences de la déduction naturelle

En latex la syntaxe de la déduction est un peu difficile à écrire mais voici ma démonstration (syntaxe simplifié) :

(1)

(2) utilisation de la règle d'élimination du


(3)

(4) déduite de (3) et (2) élimination de l'implication


(5)

(6) déduit du (5) et (4) élimination du


(7) déduit de 6 et introduction du




Est-ce complet ? Est-ce valide ?

Merci
Patrick
-----

[invite6754323456711]

hej,

Peut être faut-il que je précise la démarche utilisé ?

Le langage est celui des prédicats avec l'égalité.
Les axiomes et règles d'inférences sont ceux de la déduction naturelle.
L'hypothèse est .
La conclusion est .

L'énoncé est donc déductible de l'énoncé au moyen des règles d'inférences. Ce qui est équivalent à dire que est une conséquence de .

Je me place donc dans la théorie de la démonstration (syntaxique / définit des théories formelles) et non dans la théorie des modèles (sémantique / en donne des interprétations)

Patrick

[Médiat]

Je me place donc dans la théorie de la démonstration (syntaxique / définit des théories formelles) et non dans la théorie des modèles (sémantique / en donne des interprétations)

Difficile d'être d'accord avec cela alors que tu utilises des symboles propres aux modèles, si tu veux vraiment faire du pur syntaxique, tu dois préciser dans quelle théorie tu te places, comme tu utilises le symbole d'appartenance, il me semble que la théorie des ensembles est un bon candidat, et remplacer les symboles et par des symboles de variables (en réfléchissant aux quantificateurs à utiliser (ou non)).

[invite6754323456711]

Difficile d'être d'accord avec cela alors que tu utilises des symboles propres aux modèles, si tu veux vraiment faire du pur syntaxique, tu dois préciser dans quelle théorie tu te places, comme tu utilises le symbole d'appartenance, il me semble que la théorie des ensembles est un bon candidat, et remplacer les symboles et par des symboles de variables (en réfléchissant aux quantificateurs à utiliser (ou non)).

Oui c'est bien la ma difficulté.

Pour introduire le symbole on peut donc utiliser la signature de la théorie des ensembles :

- Aucun symbole de constante ni fonction
- Deux symboles de prédicat = et

Maintenant pour et je suis donc obligé à définir par une interprétation ? Le domaine étant

Ce n'est donc pas possible de démontrer sans passer par une interprétation pour vérifier la valididé ?


Patrick

[A voir en vidéo sur Futura]

[Médiat]

Maintenant pour et je suis donc obligé à définir par une interprétation ? Le domaine étant

Si par domaine tu entends l'univers du modèles, alors non, c'est un des ensembles du modèle, pas le modèle.

Ce n'est donc pas possible de démontrer sans passer par une interprétation pour vérifier la valididé ?

Si c'est possible, je t'ai dit comment faire dans mon message précédent.

[invite6754323456711]

Si par domaine tu entends l'univers du modèles, alors non, c'est un des ensembles du modèle, pas le modèle.

Si c'est possible, je t'ai dit comment faire dans mon message précédent.

Pour domaine j'ai pris la définition de http://www.dicosmo.org/CourseNotes/M.../Predicats.pdf lié à la notion d'interprétation

Pour modèle j'ai pris la définition d'une interprétation qui satisfait un ensemble de formules http://www.i3s.unice.fr/~fedou/OFI20...OFI-Cours5.pdf (P 28)

On se place donc dans la théorie des ensembles et la logique classique (pour avoir des règles de déductions) avec comme symbole de variable , symbole de fonction sqrt et symbole constante 2 (ou fonction d'aridité 0).

et deviennent des termes dans le langage des prédicats.

Une fois cela posé. Les formules restent pourtant correctes (syntaxiquement) ?





Patrick

[invite6754323456711]

Une fois cela posé. Les formules restent pourtant correctes (syntaxiquement) ?





Patrick

Peut être plus correct ?



Patrick

[Médiat]

et deviennent des termes dans le langage des prédicats.

Et tu trouves plus sain d'utiliser des symboles bien connus pour autre chose que leur définition habituelle, comme par exemple , plutôt que d'utiliser les symboles utilisés par tout le monde, par exemple .
De la même façon étant un symbole de constante que tu n'as pas défini, je choisi ce que je veux, par exemple l'ensemble vide, qui est aussi le 0 des ordinaux et donc d'après toi .

Voila encore une conversation qui se précipite dans le mur, qu'elle repose en paix !

[invite6754323456711]

Et tu trouves plus sain d'utiliser des symboles bien connus pour autre chose que leur définition habituelle, comme par exemple , plutôt que d'utiliser les symboles utilisés par tout le monde, par exemple .
De la même façon étant un symbole de constante que tu n'as pas défini, je choisi ce que je veux, par exemple l'ensemble vide, qui est aussi le 0 des ordinaux et donc d'après toi .

Voila encore une conversation qui se précipite dans le mur, qu'elle repose en paix !

Je n'affirme absolument rien. Ma démarche consiste juste à mieux comprendre la théorie formelle de la démonstration au travers d'un exemple.

Je ne suis absolument pas un expert du domaine (il me semble l'avoir déjà dit). C'est pour cela que faire un exercice de A à Z je pense m'aiderai à mieux comprendre tous ces concepts abstraits.


Patrick

[invite6754323456711]

De la même façon étant un symbole de constante que tu n'as pas défini, je choisi ce que je veux, par exemple l'ensemble vide, qui est aussi le 0 des ordinaux et donc d'après toi .

Pour définir un symbole de constante il suffit de l'énoncer ?

D'après ce que j'ai lu dans une signature il n'y a que des symboles de variables ou de fonctions. un symbole de constante est vue comme une fonction d'arité 0.

doit aussi être un ensemble !!

?

Patrick

[Médiat]

JMa démarche consiste juste à mieux comprendre la théorie formelle de la démonstration au travers d'un exemple.

Je te propose de commencer par ne pas utiliser des symboles de constante (, par exemple) pour des variables, et, soit de définir tes constantes correctement, soit d'utiliser un symbole sans signification pour une constante n'ayant pas de signification particulière (c, par exemple), mais je n'en vois pas l'utilité ici, une autre variable irait très bien.

[Médiat]

doit aussi être un ensemble !!

Oui, l'ensemble vide, par exemple ! Donc .
Déjà que certains méprisent les logiciens parce que trop abscons, qu'est-ce que cela va être avec ce genre d'écriture.

[invite6754323456711]

Oui, l'ensemble vide, par exemple ! Donc .

Cela me permet donc d'écrire l'énoncé sous cette forme ? :



Patrick

[Médiat]

Est-ce que ce que tu veux démontrer ce ne serait pas :

[invite6754323456711]

Est-ce que ce que tu veux démontrer ce ne serait pas :

Oui. Merci c'est plus clair

Patrick

[invite6754323456711]

Bonjour,

Pour démontrer


J'essai remonter le processus en arrière

3 Introductions du en arrière donne
(1)

Introduction du en arrière

(2)

Introduction du en arrière

(3)

Maintenant quel sont les axiomes de la théorie des ensembles ZF(C) qui pourraient induire à cette contradiction ?

Quelqu'un aurait-il une piste ?


Patrick

[invite6754323456711]

Bonjour,

Peut être l'axiome qui permet de retrouver les propriétés usuelles de l'égalité ?
http://fr.wikipedia.org/wiki/Axiome_...ionnalit%C3%A9

Patrick