Axiomas de la lógica proposicional

Question

El libro en el que estoy estudiando lógica (Mendelson) utiliza los siguientes axiomas:

$$\begin{array} {rl} \text{A1)} & P \to (Q \to P) \\ \text{A2)} & [P \to (Q \to R)] \to [(P \to Q) \to (P \to R)] \\ \text{A3)} & (\lnot P \to \lnot Q) \to [(\lnot P \to Q) \to P] \\ \end{array}$$

Otras fuentes que he visto sustituyen A3) por uno de los axiomas:

$$\begin{array} {rl} \text{A3’) }& (\lnot P \to \lnot Q) \to (Q \to P) \\ \text{A3’’)}& \lnot \lnot P \to P \end{array}$$

¿Puede alguien dar una prueba de $A3$ en los sistemas $\{A1,A2,A3’\}$ y $\{A1,A2,A3’’\}$ ?

Answer 1

$\{A1, A2, A3''\}$ no puede establecer $A3$ . Basta con considerar cuando $\lnot$ se interpreta como la identidad.

$\{A1, A2, A3'\}$ puede establecer $A3$ porque es clásico Pero la derivación real puede ser larga y tediosa. Como referencia la respuesta de Bram a esta pregunta: ayuda con algunas pruebas de estilo Hilbert en un sistema de axiomas de lógica proposicional.

Answer 2

$\lnot$$ \no $P gets used only when $ \no $P abbreviates (P$ \flecha derecha $$\bot$ ). Así, cuando se utiliza, A3'': ( $\lnot$$ \no $P$ \flecha derecha $P) is not the axiom, but rather (((P$ \flecha derecha $$\bot$ ) $\rightarrow$$ \bot $)$ \flecha derecha $P) is the axiom, which is a special case of the tautology (((P$ \flecha derecha $Q)$ \flecha derecha $$\bot$ ) $\rightarrow$ P). Es un sistema completo, pero hay que empezar con (((P $\rightarrow$$ \bot $)$ \flecha derecha $$\bot$ ) $\rightarrow$ P). No ocurre en el primer sistema que mencionas, ya que $\lnot$ es una conectiva primitiva, ni $\bot$ bien formados para ese sistema.

Del teorema Prover9 desarrollado por William McCune en el Laboratorio Nacional Argonne; si interpretas "P" como $\vdash$ , lo siguiente corresponde a una prueba condensada de desprendimiento de A3 (al menos si es correcta, no la he comprobado a mano). Nótese que un correlato de $\lnot$$ \lnot$P en la fórmula 4594 se demuestra aquí también.

% -------- Comments from original proof --------
% Proof 1 at 14.73 (+ 4.26) seconds.
% Length of proof is 46.
% Level of proof is 17.
% Maximum clause weight is 24.
% Given clauses 1864.

1 P((-x -> -y) -> ((-x -> y) -> x)) # label(non_clause) # label(goal).  [goal].
2 -P(x -> y) | -P(x) | P(y).  [assumption].
3 P(x -> (y -> x)).  [assumption].
4 P((x -> (y -> z)) -> ((x -> y) -> (x -> z))).  [assumption].
5 P((-x -> -y) -> (y -> x)).  [assumption].
6 -P((-c1 -> -c2) -> ((-c1 -> c2) -> c1)).  [deny(1)].
7 P(x -> (y -> (z -> y))).  [hyper(2,a,3,a,b,3,a)].
8 P(((x -> (y -> z)) -> (x -> y)) -> ((x -> (y -> z)) -> (x -> z))).  [hyper(2,a,4,a,b,4,a)].
9 P(x -> ((y -> (z -> u)) -> ((y -> z) -> (y -> u)))).  [hyper(2,a,3,a,b,4,a)].
10 P((x -> y) -> (x -> x)).  [hyper(2,a,4,a,b,3,a)].
11 P(((-x -> -y) -> y) -> ((-x -> -y) -> x)).  [hyper(2,a,4,a,b,5,a)].
12 P(x -> ((-y -> -z) -> (z -> y))).  [hyper(2,a,3,a,b,5,a)].
14 P(x -> (y -> (z -> (u -> z)))).  [hyper(2,a,3,a,b,7,a)].
17 P(x -> x).  [hyper(2,a,10,a,b,7,a)].
18 P(((x -> y) -> x) -> ((x -> y) -> y)).  [hyper(2,a,4,a,b,17,a)].
26 P((x -> ((y -> x) -> z)) -> (x -> z)).  [hyper(2,a,8,a,b,7,a)].
44 P((x -> ((y -> (z -> y)) -> u)) -> (x -> u)).  [hyper(2,a,8,a,b,14,a)].
48 P(((x -> (y -> z)) -> (((x -> y) -> (x -> z)) -> u)) -> ((x -> (y -> z)) -> u)).  [hyper(2,a,8,a,b,9,a)].
71 P((x -> (-y -> -z)) -> (x -> (z -> y))).  [hyper(2,a,4,a,b,12,a)].
159 P(-x -> (x -> y)).  [hyper(2,a,26,a,b,12,a)].
160 P((x -> y) -> ((z -> x) -> (z -> y))).  [hyper(2,a,26,a,b,9,a)].
166 P(x -> (-y -> (y -> z))).  [hyper(2,a,3,a,b,159,a)].
197 P(((-x -> (x -> y)) -> z) -> z).  [hyper(2,a,18,a,b,166,a)].
815 P(((x -> y) -> z) -> (y -> z)).  [hyper(2,a,44,a,b,160,a)].
835 P(x -> (((y -> z) -> u) -> (z -> u))).  [hyper(2,a,3,a,b,815,a)].
841 P(x -> ((x -> y) -> y)).  [hyper(2,a,815,a,b,18,a)].
842 P(x -> ((-y -> -x) -> y)).  [hyper(2,a,815,a,b,11,a)].
915 P(((x -> ((x -> y) -> y)) -> z) -> z).  [hyper(2,a,841,a,b,841,a)].
918 P((x -> y) -> (x -> ((y -> z) -> z))).  [hyper(2,a,160,a,b,841,a)].
1299 P((x -> (-y -> -x)) -> (x -> y)).  [hyper(2,a,4,a,b,842,a)].
3180 P((x -> (y -> z)) -> (y -> (x -> z))).  [hyper(2,a,48,a,b,835,a)].
3224 P(x -> ((((x -> y) -> y) -> z) -> z)).  [hyper(2,a,915,a,b,918,a)].
4594 P(--x -> x).  [hyper(2,a,197,a,b,1299,a)].
4644 P(--x -> ((x -> y) -> y)).  [hyper(2,a,918,a,b,4594,a)].
4672 P(x -> --x).  [hyper(2,a,5,a,b,4594,a)].
4728 P((x -> y) -> (x -> --y)).  [hyper(2,a,160,a,b,4672,a)].
19603 P(x -> ((x -> y) -> --y)).  [hyper(2,a,3180,a,b,4728,a)].
19609 P((x -> y) -> (--x -> y)).  [hyper(2,a,3180,a,b,4644,a)].
20528 P(--x -> ((x -> y) -> --y)).  [hyper(2,a,19609,a,b,19603,a)].
23007 P((((x -> y) -> y) -> z) -> (x -> z)).  [hyper(2,a,3180,a,b,3224,a)].
26321 P((x -> y) -> (--x -> --y)).  [hyper(2,a,3180,a,b,20528,a)].
27746 P((x -> y) -> (-y -> -x)).  [hyper(2,a,71,a,b,26321,a)].
27754 P(x -> (-y -> -(x -> y))).  [hyper(2,a,23007,a,b,27746,a)].
28044 P((x -> -y) -> (x -> -(x -> y))).  [hyper(2,a,4,a,b,27754,a)].
28694 P((-x -> -y) -> ((-x -> y) -> x)).  [hyper(2,a,71,a,b,28044,a)].
28695 $F.  [resolve(28694,a,6,a)].