¿Se puede probar la Ley de Peirce sin contradicción?

Question

Buenas tardes, he escuchado la prueba por contradicción es necesaria para Peirce la ley. AFAIK, las tablas de verdad no están relacionados directamente a las pruebas por la contradicción, y si de una operación $\text {op}$ tenemos una tabla de verdad

P(p) P(q)   P(p op q)
  0    0        1
  0    1        1
  1    0        1
  1    1        1

tal que $P$ es el predicado, o lógico/valor de verdad de una proposición, entonces

$$ \forall p\forall q, P(p\ \text{op}\ q)=1\Leftrightarrow\forall p\forall q, p\ \text{op}\ p $$

Entonces, ¿no

(p    q   if p, then q  if p, q; and then p    modus ponens           Peirce's Law)
P(p) P(q)    P(p → q)     P((p → q) → p)   P(((p → q) → p) → q)   P(((p → q) → p) → p)
  0    0         1              0                   1                      1       
  0    1         1              0                   1                      1       
  1    0         0              1                   1                      1       
  1    1         1              1                   1                      1       

una prueba de Peirce de la ley?
(se puede hacer la matemáticas a sí mismo, tomando nota de esto es la lógica clásica y que $p \to q \Leftrightarrow \lnot p\lor q$; y todas las obras sin admiting cualquier prueba por contradicción)

Answer 1

Lo que he dicho en el vinculado respuesta fue que de Peirce, la ley exige la prueba por contradicción o algo esencialmente equivalente. Para este propósito el razonamiento de la tabla de verdad cuenta como "esencialmente equivalente a la prueba por contradicción".

Sí, eso suena como un tramo, pero en realidad la base para la aceptación de la tabla de verdad completa como es que nosotros sabemos que en cada relevantes del mundo, $p$ será verdadero o falso (y también para $q$). Y que es la misma cosa que está en la raíz de la prueba por contradicción: Si se puede probar que algo no puede ser falsa, entonces debe ser cierto, porque de ser cierto y de ser falsas son las únicas opciones.

Intuitionistic lógica rechaza la prueba por la tabla de verdad, así como la prueba por contradicción y el principio de la $P\lor \neg P$ siempre es cierto. Yo estaba usando "esencialmente equivalente a la prueba por contradicción" como (posiblemente) de fantasía abreviatura de "un razonamiento principio de que, cuando se añade a intuitionistic lógica, produce los clásicos de la lógica".

Answer 2

Yo uso la notación polaca. C representa el material condicional y se va antes de argumentos. Por lo tanto, estas las reglas de formación será suficiente aquí:

1. Todas las letras en minúscula del alfabeto latino, bien formados fórmulas (wffs).
2. Si $\alpha$ $\beta$ son wffs, entonces también lo es C$\alpha$$\beta$.

Por lo tanto, de Peirce, la Ley se convierte en CCCpqpp. Arthur Antes de el libro de la Lógica Formal indica que un único axioma por el puro implicational cálculo de proposiciones (las únicas reglas de inferencia es el desprendimiento y uniforme de la sustitución de las variables) dada por Lukasiewicz en 1936 es

3 CCCpqrCCrpCsp.

He utilizado prover9 para encontrar la siguiente prueba (incluso si soy lo suficientemente inteligente como para encontrar una prueba, es casi siempre más rápido que yo... cuando me puede llegar a encontrar en mí una prueba). La notación de 3 p/Crs indica que p presenta sustituido con Crs en wff 3. La notación de 3 p/Crt * C4-5 indica que vamos a sustituir p con la Crt en wff 4, tiene la misma forma como la wff que comienza con C, entonces ha wff 4, y termina con wff 5. 4 ya está en nuestro conjunto de teoremas lógicos o axiomas, y por lo tanto vamos a separar 5 como theoerem por la regla de la separación.

3 CCCpqrCCrpCsp.

 3 p/Cpq, q/r, r/CCrpCsp, s/t * C3-5

5 CCCCrpCspCpqCtCpq.

 5 r/Crp, p/Csp, s/p, q/CpCsp * C5 q/Csp, t/Csp-6

6 CtCCspCpCsp.

 3 p/CCrpCsp, q/Cpq, r/CtCpq, s/u * C5-7

7 CCCtCpqCCrpCspCuCCrpCsp.

 6 t/CtCCpqCqCpq, s/p, p/q * C6-8

8 CCpqCqCpq.

 3 r/CqCpq, s/r *C8-9

9 CCCqCpqpCrp.

 7 t/CqCCppq, q/p, s/p * C9 p/Cpp, r/Crp-10

10 CuCCrpCpp.

 10 u/CuCCpqCqq, r/p, p/q * C10 r/p, p/q-11

11 CCpqCqq.

 11 p/CCqCpqp,q/Crp * C9-12

12 CCrpCrp.

 3 p/r, q/p, r/Crp * C12-13

13 CCCrprCsr.

 3 p/Crp, q/r, r/Csr, s/t * C13-14

14 CCCsrCrpCtCrp.

 3 p/Csr, q/Crp, r/CtCrp, s/u * C14-15 

15 CCCtCrpCsrCuCsr.

 15 t/Cpq, s/CCCspqp, r/Csp, p/q * C3 r/CCspq -16

16 CuCCCCspqpCsp.

 16 u/CuCCCpqrqCpr, s/p, p/q, q/r * C16 s/p, p/q, q/r-17

17 CCCCpqrqCpq.

 3 p/CCpqr, r/Cpq * C17-18

18 CCCpqCCpqrCsCCpqr.

 18 p/Crp, q/r * C13 s/Cpq-19

19 CsCCCrprr.

 19 s/CsCCpqpp, r/p, p/q * C19 r/p, p/q-20

20 CCCpqpp.

Hay un montón de otras ya conocido axioma establece por el puro implicational cálculo de proposiciones... Antes de listas de libros 3-axioma, un 4-axioma establece, 12 2-axioma establece, y 4 único axioma establece. Todos estos sistemas sólo han desprendimiento y la sustitución como reglas de inferencia. Ninguno de ellos utilizar o permitir la prueba por contradicción.

Answer 3

Creo que la declaración de que "la prueba por contradicción es necesaria para Peirce la ley" debe ser interpretado de una manera diferente.

Me refiero a estos post anterior acerca de Implicational cálculo.

Mi punto de partida es la respuesta por @Doug Spoonwood : de acuerdo a Lukasiewicz' axiomatisation, un axioma es suficiente para derivar todos los "implicational" tautologías.

El problema es que de esta manera no hay lugar para la negación ($\lnot$) en el sistema.

La forma más fácil es introducir el falsum ($\bot$); con ello podemos usar $\lnot A$ como una abreviatura de $A \rightarrow \bot$.

En el post anterior, he argumentado que, con el fin de derivar las clásicas leyes de la negación, como Doble Negación, necesitamos de Peirce de la ley , más el Ex Falso Quodlibet axioma :

$\vdash \bot \rightarrow A$.

También en el fin de demostrar la equivalencia entre Peirce de la ley y la Ley de Medio Excluido, tenemos el símbolo $\bot$ como primitivo y el EFQ axioma.