> Alguna sugerencia para encontrar una derivacion de (φ v ¬φ)??
Se puede construir usando RAA
Posiblemente tu idea es construir una prueba así:
[φ]₁ [¬φ]₁
⋮ ⋮ ⋮
ϕ∨¬ϕ α α
-------------------------- ∨-E (1)
α
Donde α es lo que quiero probar y se supone que conozco como probarlo a partir de φ y también a partir de ¬φ.
La derivación anterior es correcta, pero podemos hacer una derivación más simple y evitar construir la prueba de (ϕ∨¬ϕ) de esta manera:
[φ]₁
⋮
[¬α]₂ α
---------- ¬-E
⊥
-------- ¬-I (1)
¬φ
⋮
[¬α]₂ α
-------- ¬-E
⊥
----- RAA (2)
α
Este mismo esquema te puede servir para probar (ϕ∨¬ϕ).