Флашкарти: Introduction aux règles de déduction logique — 22 карти

Démonstration — définition ?

Organisation logique par règles d’introduction et d’élimination.

H ⊢ P — signification ?

P est démontrable à partir du contexte H.

Modus ponens — mécanisme ?

De P ⇒ Q et P, on déduit Q.

Conjonction — introduction ?

Utiliser And.intro pour prouver P ∧ Q.

Disjonction — élimination ?

Raisonnement par cas sur P ∨ Q.

Équivalence — double implication ?

P ⇔ Q signifie (P⇒Q) ∧ (Q⇒P).

Négation — introduction ?

Supposer P, dériver contradiction pour conclure ¬P.

Quantificateur universel — démonstration ?

Prouver P(x) pour tout x, sans x libre dans H.

Quantificateur existentiel — introduction ?

Fournir un témoin a tel que P(a) soit vrai.

Règles Lean — tactiques ?

Méthodes comme intro, apply, specialize, etc., pour prouver.

Implication en Lean — intro ?

Utiliser tactic 'intro' pour supposer P et prouver Q.

Conjonction en Lean — constructor ?

Utiliser 'constructor' ou And.left pour prouver P ∧ Q.

Turnstile — rôle ?

Sépare hypothèses et but dans une preuve.

H — rôle ?

Liste des hypothèses disponibles.

P — rôle ?

Énoncé à démontrer.

H ` P — signification ?

P est démontrable à partir de H.

Récurrence — principe ?

Prouver Q(n+1) à partir de Q(n) pour tout n.

Double implication — rôle ?

Exprime l’équivalence entre deux propositions.

Négation — rôle ?

Exprime que P ne peut pas être vrai.

Existential — introduction ?

Fournir un témoin a tel que P(a) soit vrai.

Lean apply — rôle ?

Utiliser une hypothèse ou théorème pour transformer le but.

And.left — rôle ?

Extraire la partie gauche d’une conjonction.