TP 7 : Systèmes de preuve

Donnez les variables libres et mettre sous forme prénexe.

1. ∀x(P(x)) ⇒ (∃t(Q(t))∨∃t(C(t,x)))
2. ∀x(∀y(P(x,y))⇒∃z(R(x,z)))
3. ∀x∀y∃z(P(x,y,z)∧(∃u(Q(x,u))⇒∃v(Q(y,v,u))))
4. (∃xP(x)⇒∃xR(x)∨∀yP(y)) ∧ ∀x∃y(R(y)⇒P(x))

Proposez une Skolemisation des formules précédentes.

Montrez en utilisant le calcul des séquents que les formules suivantes sont des théorèmes de la logique propositionnelle :

1. ¬P ∨ P
2. (¬P∧P) ⇒ ∀y.Q(y)
3. (¬¬P⇒P) ∧ (P⇒¬¬P)
4. ∀x(P(x)) ⇒ ∃x(P(x))
5. ∃x(P(x)) ⇒ ¬∀x(¬P(x))
6. ∃x∀y(R(x)⇒R(y)). (difficile)