Déduction naturelle

ù100fil · 07/02/2009 - 14h40

Bonjour,

Je cherche à démonter à partir des règles d'inférences de la déduction naturelle $\forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big) \vdash \neg $ \sqrt2\in\mathbb{Q} $$

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

(1) $\forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big), \sqrt2\in\mathbb{Q} \vdash \forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big)$

(2) utilisation de la règle d'élimination du $\forall$
$\forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big), \sqrt2\in\mathbb{Q} \vdash \sqrt2\in\mathbb{Q} \Rightarrow \neg(\sqrt 2=\sqrt 2)$

(3) $\forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big), \sqrt2\in\mathbb{Q} \vdash \sqrt2\in\mathbb{Q}$

(4) déduite de (3) et (2) élimination de l'implication
$\forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big), \sqrt2\in\mathbb{Q} \vdash \neg(\sqrt 2=\sqrt 2)$

(5) $\vdash (\sqrt 2=\sqrt 2)$

(6) déduit du (5) et (4) élimination du $\neg$
$\forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big), \sqrt2\in\mathbb{Q} \vdash \perp$

(7) déduit de 6 et introduction du $\neg$

$\forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big) \vdash \neg $ \sqrt2\in\mathbb{Q} $$

Est-ce complet ? Est-ce valide ?

Merci
Patrick

ù100fil · 08/02/2009 - 11h32

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 $\Phi = \forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big)$ .
La conclusion est $\varphi = \neg $ \sqrt2\in\mathbb{Q} $$ .

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

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** · 08/02/2009 - 14h52

Envoyé par ù100fil

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 $\mathbb{Q}$ et $\sqrt{2}$ par des symboles de variables (en réfléchissant aux quantificateurs à utiliser (ou non)).

ù100fil · 08/02/2009 - 18h59

Envoyé par Médiat

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 $\mathbb{Q}$ et $\sqrt{2}$ 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 $\in$ on peut donc utiliser la signature de la théorie des ensembles :

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

Maintenant pour $\mathbb{Q}$ et $\sqrt{2}$ je suis donc obligé à définir par une interprétation ? Le domaine étant $\mathbb{Q}$

Ce n'est donc pas possible de démontrer $\forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big) \vdash \neg $ \sqrt2\in\mathbb{Q} $$ sans passer par une interprétation pour vérifier la valididé $\forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big)\ \mid = \neg $ \sqrt2\in\mathbb{Q} $$ ?

Patrick

**Médiat** · 09/02/2009 - 04h23

Envoyé par ù100fil

Maintenant pour $\mathbb{Q}$ et $\sqrt{2}$ je suis donc obligé à définir par une interprétation ? Le domaine étant $\mathbb{Q}$

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

Envoyé par ù100fil

Ce n'est donc pas possible de démontrer $\forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big) \vdash \neg $ \sqrt2\in\mathbb{Q} $$ sans passer par une interprétation pour vérifier la valididé $\forall r, \ \Big(r\in\mathbb{Q} \Rightarrow \neg(r=\sqrt 2)\Big)\ \mid = \neg $ \sqrt2\in\mathbb{Q} $$ ?

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

ù100fil · 09/02/2009 - 07h12

Envoyé par Médiat

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 $\mathbb{Q}$ , symbole de fonction sqrt et symbole constante 2 (ou fonction d'aridité 0).

$\mathbb{Q}$ et $\sqrt 2$ deviennent des termes dans le langage des prédicats.

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

$\forall x, \ \Big(x\in\mathbb{Q} \Rightarrow \neg(x=\sqrt 2)\Big)$
$\neg $ \sqrt2\in\mathbb{Q} $$

Patrick

ù100fil · 09/02/2009 - 07h24

Envoyé par ù100fil

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

$\forall x, \ \Big(x\in\mathbb{Q} \Rightarrow \neg(x=\sqrt 2)\Big)$
$\neg $ \sqrt2\in\mathbb{Q} $$

Patrick

Peut être plus correct ?

$\exists \mathbb{Q} \forall x, \ \Big(x\in\mathbb{Q} \Rightarrow \neg(x=\sqrt 2)\Big)$

Patrick

**Médiat** · 09/02/2009 - 07h43

Envoyé par ù100fil

$\mathbb{Q}$ et $\sqrt 2$ 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 $\exists \mathbb{Q}$ , plutôt que d'utiliser les symboles utilisés par tout le monde, par exemple $\exists x$ .
De la même façon $\sqrt 2$ é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 $\sqrt 2 = 0$ .

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

ù100fil · 09/02/2009 - 08h58

Envoyé par Médiat

Et tu trouves plus sain d'utiliser des symboles bien connus pour autre chose que leur définition habituelle, comme par exemple $\exists \mathbb{Q}$ , plutôt que d'utiliser les symboles utilisés par tout le monde, par exemple $\exists x$ .
De la même façon $\sqrt 2$ é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 $\sqrt 2 = 0$ .

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

ù100fil · 09/02/2009 - 09h45

Envoyé par Médiat

De la même façon $\sqrt 2$ é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 $\sqrt 2 = 0$ .

Pour définir un symbole de constante $\sqrt 2$ 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.

$\sqrt 2$ doit aussi être un ensemble !!

$\exists y \forall x, \ \Big(x\subset y \Rightarrow \neg(x= \{\sqrt 2\})\Big)$ ?

Patrick

**Médiat** · 09/02/2009 - 09h47

Envoyé par ù100fil

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 ( $\mathbb{Q}$ , 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** · 09/02/2009 - 09h50

Envoyé par ù100fil

$\sqrt 2$ doit aussi être un ensemble !!

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

ù100fil · 09/02/2009 - 10h01

Envoyé par Médiat

Oui, l'ensemble vide, par exemple ! Donc $\sqrt 2 = 0$ .

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

$\exists y \forall x, \ \Big(x\in y \Rightarrow \neg(x=\sqrt 2)\Big)$

Patrick

**Médiat** · 09/02/2009 - 10h35

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

$<br /> \forall x \forall y \forall z (((z \in x) \Rightarrow \neg (z = y)) \Rightarrow \neg (y \in x))<br />$

ù100fil · 09/02/2009 - 11h52

Envoyé par Médiat

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

$<br /> \forall x \forall y \forall z (((z \in x) \Rightarrow \neg (z = y)) \Rightarrow \neg (y \in x))<br />$

Oui. Merci c'est plus clair

Patrick

Déduction naturelle

Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Re : Déduction naturelle

Sur le même sujet

Discussions similaires

Ventilation Naturelle - Naturelle Assistée

problème de déduction

Deduction logique

Déduction de pH

Deduction d'encadrement