← Florian Gatignon

Vérificateur de preuvesProof checker

Déduction naturelle, selon le système du cours d’introduction à la logique (Université de Genève). Rien n’est envoyé : la vérification se fait dans votre navigateur. Natural deduction, following the system of the introductory logic course (University of Geneva). Nothing is sent anywhere: the checking happens in your browser.

ExerciceExercise

PreuveProof

Colonne des hypothèses activesActive-hypotheses column

AideHelp

Écrire les formules
  • Lettres de proposition : p, q, r, s, t. Constantes : a, b, c… (après un prédicat ou autour de =, p à t sont aussi des constantes : Pp, Rpx). Variables : x, y, z, u, w. Prédicats : majuscules (Fa, Rab, Gxx ; P seul est un prédicat 0-adique). Identité : a = b, a ≠ b.
  • Biconditionnel : A ≡ B (raccourci <->) abrège (A ⊃ B) ∧ (B ⊃ A) ; il n’a pas de règles propres : on utilise celles de ∧ et de ⊃ (par exemple ∧E sur p ≡ q donne p ⊃ q).
  • Raccourcis clavier : ~ → ¬, & ou ^ → ∧, | ou « v » entre deux espaces → ∨, -> → ⊃, @ → ∀, # → ∃, != → ≠. Les symboles → et ↔ d’autres notations sont aussi acceptés, ainsi que pvq, &&, || et =>.
  • Parenthèses comme au cours : on peut omettre les parenthèses extérieures et celles d’une suite de ∧ (ou de ∨) seulement. Une suite comme p ∧ q ∧ r peut se lire avec n’importe quel regroupement : (p ∧ q) ∧ r ou p ∧ (q ∧ r). Mais dans une ligne de la preuve, elle se lit avec le regroupement que donne sa justification, et le garde ensuite : on ne peut pas regrouper autrement sans règle (R de p ∧ (q ∧ r) donne p ∧ (q ∧ r), pas (p ∧ q) ∧ r). ∀x et ∃x portent sur ce qui suit immédiatement : ∀x(Fx ⊃ Gx).
  • Les lignes d’une preuve doivent être des phrases (aucune variable libre).
  • « + » insère une ligne au-dessus, « × » supprime la ligne : les numéros cités dans les autres lignes sont mis à jour (« ? » signale une ligne citée qui a été supprimée).
  • Une formule, et une preuve, appartient à un seul langage : soit la logique des propositions (p, q, r…), soit celle des prédicats (Fa, a = b, ∀x…). On ne peut pas écrire p ∧ Fa.
Writing formulas
  • Sentence letters: p, q, r, s, t. Constants: a, b, c… (after a predicate or around =, p to t are constants too: Pp, Rpx). Variables: x, y, z, u, w. Predicates: capital letters (Fa, Rab, Gxx; P alone is a 0-place predicate). Identity: a = b, a ≠ b.
  • Biconditional: A ≡ B (shortcut <->) abbreviates (A ⊃ B) ∧ (B ⊃ A); it has no rules of its own: use those of ∧ and ⊃ (for instance ∧E on p ≡ q gives p ⊃ q).
  • Keyboard shortcuts: ~ → ¬, & or ^ → ∧, | or “v” between two spaces → ∨, -> → ⊃, @ → ∀, # → ∃, != → ≠. The symbols → and ↔ of other notations are accepted too, as well as pvq, &&, || and =>.
  • Parentheses as in the course: you can leave out the outer parentheses and those of a run of ∧ (or of ∨) only. A run such as p ∧ q ∧ r can be read with any grouping: (p ∧ q) ∧ r or p ∧ (q ∧ r). But in a line of the proof, it is read with the grouping its justification gives, and keeps it afterwards: you cannot regroup without a rule (R from p ∧ (q ∧ r) gives p ∧ (q ∧ r), not (p ∧ q) ∧ r). ∀x and ∃x apply to what immediately follows: ∀x(Fx ⊃ Gx).
  • The lines of a proof must be sentences (no free variable).
  • “+” inserts a line above, “×” deletes the line: the line numbers cited in other lines are updated (“?” marks a cited line that was deleted).
  • A formula, and a proof, belongs to a single language: either propositional logic (p, q, r…) or predicate logic (Fa, a = b, ∀x…). You cannot write p ∧ Fa.
Règles et ordre des lignes citéesRules and order of the cited lines

Les lignes citées s’écrivent dans l’ordre indiqué sous chaque règle. Si elles sont dans un autre ordre mais qu’on ne peut les lire que d’une seule façon, le vérificateur l’accepte avec une remarque. Sinon, c’est une erreur.

The cited lines are written in the order given under each rule. If they are in another order but can be read in only one way, the checker accepts them with a note. Otherwise, it is an error.

H, [H] hypothèse, hypothèse transitoirehypothesis, temporary hypothesis

Aucune ligne citée. Une confusion entre H et [H] donne seulement une remarque ; à la fin, toute hypothèse qui n’est pas une prémisse doit avoir été libérée.No line cited. Mixing up H and [H] only gives a note; at the end, every hypothesis that is not a premise must have been discharged.

R répétitionrepetition
A
A

Ligne citée : la ligne répétée.Cited line: the repeated line.

∧I introduction de la conjonctionconjunction introduction
A
B
A ∧ B

Lignes citées : A, B.Cited lines: A, B.

∧E élimination de la conjonctionconjunction elimination
A ∧ B
A
A ∧ B
B

Ligne citée : la conjonction.Cited line: the conjunction.

∨I introduction de la disjonctiondisjunction introduction
A
A ∨ B
B
A ∨ B

Ligne citée : le disjoint.Cited line: the disjunct.

∨E élimination de la disjonctiondisjunction elimination
A ∨ B
[A]
⋮
C
[B]
⋮
C
C

Lignes citées : A ∨ B, [A], C, [B], C.Cited lines: A ∨ B, [A], C, [B], C.

⊃I introduction de l’implicationconditional introduction
[A]
⋮
B
A ⊃ B

Lignes citées : l’hypothèse [A], puis B.Cited lines: the hypothesis [A], then B.

⊃E élimination de l’implicationconditional elimination
A
A ⊃ B
B

Lignes citées : A, puis A ⊃ B.Cited lines: A, then A ⊃ B.

¬I introduction de la négationnegation introduction
[A]
⋮
B
⋮
¬B
¬A

Lignes citées : l’hypothèse [A], puis B et ¬B.Cited lines: the hypothesis [A], then B and ¬B.

¬E élimination de la négationnegation elimination
[¬A]
⋮
B
⋮
¬B
A

Lignes citées : l’hypothèse [¬A], puis B et ¬B.Cited lines: the hypothesis [¬A], then B and ¬B.

∀I introduction de ∀∀ introduction
φ[a/x]
∀xφ

Ligne citée : φ[a/x]. Condition : a n’apparaît ni dans ∀xφ ni dans une hypothèse dont φ[a/x] dépend.Cited line: φ[a/x]. Condition: a occurs neither in ∀xφ nor in a hypothesis on which φ[a/x] depends.

∀E élimination de ∀∀ elimination
∀xφ
φ[a/x]

Ligne citée : ∀xφ.Cited line: ∀xφ.

∃I introduction de ∃∃ introduction
φ[a/x]
∃xφ

Ligne citée : φ[a/x].Cited line: φ[a/x].

∃E élimination de ∃∃ elimination
∃xφ
[φ[a/x]]
⋮
ψ
ψ

Lignes citées : ∃xφ, [φ[a/x]], ψ. Condition : a n’apparaît ni dans ψ, ni dans ∃xφ, ni dans une autre hypothèse dont dépend ψ.Cited lines: ∃xφ, [φ[a/x]], ψ. Condition: a occurs neither in ψ, nor in ∃xφ, nor in another hypothesis on which ψ depends.

=I introduction de == introduction
 
a = a

Aucune ligne citée.No line cited.

=E élimination de == elimination
a = b
φ
φ[b//a]

Lignes citées : a = b et φ. φ[b//a] remplace une ou plusieurs occurrences de a dans φ par b.Cited lines: a = b and φ. φ[b//a] replaces one or more occurrences of a in φ by b.