Uma outra forma de lidar sintáticamente com o CPC é axiomáticamente. Como você deve saber, axiomas são proposições tomadas como verdadeiras a partir das quais os teoremas são derivados.
Funciona assim:
Seja
o conjunto dos axiomas e todas suas instâncias, se
, então
. Ou seja, se
é dedutível dos axiomas, então
é teorema.
E seja
um conjunto qualquer de fórmulas, se
então
. Ou seja, se
é dedutível de um conjunto
de fórmulas juntamente com os axiomas, então um raciocínio que tenha
como premissas e
como conclusão é válido.
A escolha adequada de axiomas e da regra de inferência primitiva confere ao sistema tanto a correção quanto a completude.
Gottlob Frege usava apenas a implicação e a negação como operadores primitivos, definindo as demais operações por meio destes, mas sem criar símbolos para expressá-las. Sua axiomática do CPC tem seis axiomas e uma regra de inferência.
Por questões de economia, demonstraremos algumas regras de inferência derivadas e as aplicaremos.
Nas tabelas onde as deduções são expressas, "wff" significa "well formed formula", ou seja, "fórmula bem formada".
THEN-1:
THEN-2:
THEN-3:
FRG-1:
FRG-2:
FRG-3:
MP:
Regra THEN-1*:
#
|
wff
|
razão
|
1. |
![{\displaystyle A\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b041434092d1f0042c2b4c7ab32ea84d462cb53e) |
premissa
|
2. |
![{\displaystyle A\to \left(B\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ff69c63930e2ccb82ab086bb7e20eec1a203fcc8) |
THEN-1
|
3. |
![{\displaystyle B\to A\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0118c2b9ccf1f2af9ebfbae13350aa277b222937) |
MP 1,2.
|
Regra THEN-2*:
#
|
wff
|
razão
|
1. |
![{\displaystyle A\to \left(B\to C\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f2aa8647bcf2814b403b8d32e4aa8bde7f8471a9) |
premissa
|
2. |
![{\displaystyle \left(A\to \left(B\to C\right)\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d75c7a1996d57b158070d39822b16a4140bba66a) |
THEN-2
|
3. |
![{\displaystyle \left(A\to B\right)\to \left(A\to C\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f899e89a14ec1e6c9158855adf4930ca91c307ac) |
MP 1,2.
|
Regra THEN-3*:
#
|
wff
|
razão
|
1. |
![{\displaystyle A\to \left(B\to C\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f2aa8647bcf2814b403b8d32e4aa8bde7f8471a9) |
premissa
|
2. |
![{\displaystyle \left(A\to \left(B\to C\right)\right)\to \left(B\to \left(A\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ab2cd8d64a808c445b96914cfd02ccdb9d5ce37b) |
THEN-3
|
3. |
![{\displaystyle B\to \left(A\to C\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ff82c7f1f53cca319d3b875743680937b58a1f62) |
MP 1,2.
|
Regra FRG-1*:
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(A\to B\right)\to \left(\neg B\to \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/322e5967500d5e5108e04a3dedeb2d57e22328cb) |
FRG-1
|
2. |
![{\displaystyle A\to B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d5b8dd84619daff17b52a08b77d15db2b9ad6c2a) |
premissa
|
3. |
![{\displaystyle \neg B\to \neg A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fed8b28f42f63937db9b96078fbbcf92a8fc1cd6) |
MP 2,1.
|
Regra TH1*:
#
|
wff
|
razão
|
1. |
![{\displaystyle B\to C}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a9febe2010e6933c5e384a066ef7d5f634b97a7e) |
premissa
|
2. |
![{\displaystyle \left(B\to C\right)\to \left(A\to \left(B\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/56eb9b1895d310b43b0db7b81768e308b9481e47) |
THEN-1
|
3. |
![{\displaystyle A\to \left(B\to C\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f2aa8647bcf2814b403b8d32e4aa8bde7f8471a9) |
MP 1,2
|
4. |
![{\displaystyle \left(A\to \left(B\to C\right)\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d75c7a1996d57b158070d39822b16a4140bba66a) |
THEN-2
|
5. |
![{\displaystyle \left(A\to B\right)\to \left(A\to C\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f899e89a14ec1e6c9158855adf4930ca91c307ac) |
MP 3,4
|
6. |
![{\displaystyle A\to B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d5b8dd84619daff17b52a08b77d15db2b9ad6c2a) |
premissa
|
7. |
![{\displaystyle A\to C}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dbb3ec243d54ee353c0664f2ac5a9c491e5d1312) |
MP 6,5.
|
Teorema TH1:
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(B\to C\right)\to \left(A\to \left(B\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/56eb9b1895d310b43b0db7b81768e308b9481e47) |
THEN-1
|
2. |
![{\displaystyle \left(A\to \left(B\to C\right)\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d75c7a1996d57b158070d39822b16a4140bba66a) |
THEN-2
|
3. |
![{\displaystyle \left(B\to C\right)\to \left(\left(A\to B\right)\to \left(A\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b36d1492bafcfb31937c272bc5e76cb53ea2b411) |
TH1* 1,2
|
4.
|
|
THEN-3
|
5. |
![{\displaystyle \left(A\to B\right)\to \left(\left(B\to C\right)\to \left(A\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7e928bb892c12416fde45f073367b16574408961) |
MP 3,4.
|
Teorema TH2:
#
|
wff
|
razão
|
1. |
![{\displaystyle A\to \left(B\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ff69c63930e2ccb82ab086bb7e20eec1a203fcc8) |
THEN-1
|
2. |
![{\displaystyle \left(B\to A\right)\to \left(\neg A\to \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a44e1e7be83897afd3bd90bf96a2e1b4c8070e21) |
FRG-1
|
3. |
![{\displaystyle A\to \left(\neg A\to \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/49dbbfa88f2f5db9f81a3552ee44341ef89ae4ef) |
TH1* 1,2.
|
Teorema TH3:
#
|
wff
|
razão
|
1. |
![{\displaystyle A\to \left(\neg A\to \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/49dbbfa88f2f5db9f81a3552ee44341ef89ae4ef) |
TH 2
|
2. |
![{\displaystyle \left(A\to \left(\neg A\to \neg B\right)\right)\to \left(\neg A\to \left(A\to \neg B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/951943849b5a8261ba59b112baabb2efa6daba66) |
THEN-3
|
3. |
![{\displaystyle \neg A\to \left(A\to \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e098c387174c84b69f5bc66215a67be8eb35087c) |
MP 1,2.
|
Teorema TH4:
#
|
wff
|
razão
|
1. |
![{\displaystyle \neg A\to \left(A\to \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e098c387174c84b69f5bc66215a67be8eb35087c) |
TH3
|
2. |
![{\displaystyle \left(\neg A\to \left(A\to \neg B\right)\right)\to \left(\neg \left(A\to \neg B\right)\to \neg \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0aaccbdc5dab886ab7b61e0e3c1ad990158e98c1) |
FRG-1
|
3. |
![{\displaystyle \neg \left(A\to \neg B\right)\to \neg \neg A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/28ad328f7e96a01d2ab97b8a8a8055b410621bbd) |
MP 1,2
|
4. |
![{\displaystyle \neg \neg A\to A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/84aaf1a07ba682fb0d3a84a80bc528871cd5bd78) |
FRG-2
|
5. |
![{\displaystyle \neg \left(A\to \neg B\right)\to A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b295ea261660a05d10668f88380082b3eb4b99d2) |
TH1* 3,4.
|
Teorema TH5:
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(A\to \neg B\right)\to \left(\neg \neg B\to \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e9154024c3682205bf75419d2cd02f7beff36713) |
FRG-1
|
2.
|
|
THEN-3
|
3. |
![{\displaystyle \neg \neg B\to \left(\left(A\to \neg B\right)\to \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2b1d9f8dc52f58ebde64e8b3f40ba34d69e6ca04) |
MP 1,2
|
4. |
![{\displaystyle B\to \neg \neg B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e0b4df56ed996f4b2b23a917f2f072739a2cfd35) |
FRG-3, with A := B
|
5. |
![{\displaystyle B\to \left(\left(A\to \neg B\right)\to \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b62d005a7108a3570226f17ca86e983ae58c63e3) |
TH1* 4,3
|
6.
|
|
FRG-1
|
7. |
![{\displaystyle \left(A\to \neg B\right)\to \left(B\to \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fdcc02bd5d23f1c60a8c3d164a586c2510eb209c) |
MP 5,6.
|
Teorema TH6:
#
|
wff
|
razão
|
1. |
![{\displaystyle \neg \left(B\to \neg A\right)\to B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ea5cd66124677c330043504bca2222c77bda0502) |
TH4, with A := B, B := A
|
2. |
![{\displaystyle \left(B\to \neg A\right)\to \left(A\to \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3b4cec5070b78e1e1ffe6e0dcfa5313ec36cf602) |
TH5, with A := B, B := A
|
3.
|
|
FRG-1
|
4. |
![{\displaystyle \neg \left(A\to \neg B\right)\to \neg \left(B\to \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/75ba3763f61af5c40b24fc120275716c22feeb79) |
MP 2,3
|
5. |
![{\displaystyle \neg \left(A\to \neg B\right)\to B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/49eaafa15691e6b1821e7f2a92906f95fdae0475) |
TH1* 4,1.
|
Teorema TH7:
#
|
wff
|
razão
|
1. |
![{\displaystyle A\to \neg \neg A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/40524c0074098b110e96fb57d534c5b414c4e2f4) |
FRG-3
|
2. |
![{\displaystyle \neg \neg A\to A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/84aaf1a07ba682fb0d3a84a80bc528871cd5bd78) |
FRG-2
|
3. |
![{\displaystyle A\to A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4fbf720da5a9387e23c628079fbc3e021399c911) |
TH1* 1,2.
|
Teorema TH8:
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(A\to B\right)\to \left(A\to B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ff9f71f303b018622ff18352c5fcdaf3e48ff17f) |
TH7, com A :=
|
2.
|
|
THEN-3
|
3. |
![{\displaystyle A\to \left(\left(A\to B\right)\to B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1a7ea0c96386d39a1a8109b5e5b57ec298b07dfc) |
MP 1,2.
|
Teorema TH9:
#
|
wff
|
razão
|
1. |
![{\displaystyle B\to \left(\left(A\to B\right)\to B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/31d917b770de6d625513aa4b418ecd60936ecce3) |
THEN-1, com A := B, B := .
|
Teorema TH10:
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(A\to \neg B\right)\to \left(A\to \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bcd8d5cda0bf2629040064702a5b6e99c45f33ac) |
TH7
|
2.
|
|
THEN-3
|
3. |
![{\displaystyle A\to \left(\left(A\to \neg B\right)\to \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ed3a1c4a82ca4f7a7a108ae055c0f640b2022466) |
MP 1,2
|
4. |
![{\displaystyle \left(\left(A\to \neg B\right)\to \neg B\right)\to \left(B\to \neg \left(A\to \neg B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a67dd197faf7f2c2d7392acd00ebe25c85fbb4b4) |
TH5
|
5. |
![{\displaystyle A\to \left(B\to \neg \left(A\to \neg B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/885be789f2baac88c02dd7b84ce5d8ec03ee93b8) |
TH1* 3,4.
|
Teorema TH11:
#
|
wff
|
razão
|
1. |
![{\displaystyle A\to \left(B\to \neg \left(A\to \neg B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/885be789f2baac88c02dd7b84ce5d8ec03ee93b8) |
TH10
|
2.
|
|
THEN-2
|
3. |
![{\displaystyle \left(A\to B\right)\to \left(A\to \neg \left(A\to \neg B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/058a99a699c12ad6e7e11da19537da57b91098ab) |
MP 1,2
|
4. |
![{\displaystyle \left(A\to \neg \left(A\to \neg B\right)\right)\to \left(\left(A\to \neg B\right)\to \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ec40e36e4e312a1b3976b453aef35b24e7b9a13e) |
TH5
|
5. |
![{\displaystyle \left(A\to B\right)\to \left(\left(A\to \neg B\right)\to \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/866d599c837172aebb8418fed6099e02fde80624) |
TH1* 3,4.
|
Teorema TH12:
#
|
wff
|
razão
|
1. |
![{\displaystyle B\to \left(A\to B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/be75c69748401b2dbe5e19b6a824bbca005f81e7) |
THEN-1
|
2.
|
|
TH1
|
3. |
![{\displaystyle \left(\left(A\to B\right)\to C\right)\to \left(B\to C\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/55d9a15e79315e2a54ce1ab2d64c654a19323df3) |
MP 1,2
|
4. |
![{\displaystyle \left(B\to C\right)\to \left(A\to \left(B\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/56eb9b1895d310b43b0db7b81768e308b9481e47) |
THEN-1
|
5. |
![{\displaystyle \left(\left(A\to B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/08fe561705a71ca4aefacc0883fcf801b929fe69) |
TH1* 3,4.
|
Teorema TH13:
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(B\to \left(B\to C\right)\right)\to \left(\left(B\to B\right)\to \left(B\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0fbc53a9c9e801fcc41a588ff7c1d0eff095d61c) |
THEN-2
|
2. |
![{\displaystyle \left(B\to B\right)\to \left(\left(B\to \left(B\to C\right)\right)\to \left(B\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f592f67562b7c876dbc00c23ae4a7fd6c43875c4) |
THEN-3* 1
|
3. |
![{\displaystyle B\to B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cc5c92411f29ae67df761f2d1500ce5e79e4517c) |
TH7
|
4. |
![{\displaystyle \left(B\to \left(B\to C\right)\right)\to \left(B\to C\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/917c009d41f243a9714f696e6f14f93e71e062be) |
MP 3,2.
|
Regra TH14*:
#
|
wff
|
razão
|
1. |
![{\displaystyle P\to Q\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/210079f4744e8c1b484cff80a5d772a1262d1d06) |
premissa
|
2. |
![{\displaystyle \left(P\to Q\right)\to \left(B\to \left(P\to Q\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b86ccd614c2209519de921e38c2999da1fc8a262) |
THEN-1
|
3. |
![{\displaystyle B\to \left(P\to Q\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0bea23ce4ef6df016f2d8da8f2517c7038d78550) |
MP 1,2
|
4. |
![{\displaystyle \left(B\to \left(P\to Q\right)\right)\to \left(\left(B\to P\right)\to \left(B\to Q\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/87f8deeec65da382470fc590ea2ecb120317ffaa) |
THEN-2
|
5. |
![{\displaystyle \left(B\to P\right)\to \left(B\to Q\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4bd3b15c5a318fca0ad833cea70d8a827c3e63ad) |
MP 3,4
|
6.
|
|
THEN-1
|
7. |
![{\displaystyle A\to \left(\left(B\to P\right)\to \left(B\to Q\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7562b54f591f52a38a21563f281dd57a0f11204f) |
MP 5,6
|
8. |
![{\displaystyle \left(A\to \left(B\to P\right)\right)\to \left(A\to \left(B\to Q\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3d31d451f4d8a81036d417e926ac416abe41d9e2) |
THEN-2* 7
|
9. |
![{\displaystyle A\to \left(B\to P\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a75425d14b95697f180570ef65b8099639d50091) |
premissa
|
10. |
![{\displaystyle A\to \left(B\to Q\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c4c2854888a53312aaa832d07888ebb5cb329ef9) |
MP 9,8.
|
Teorema TH15:
#
|
wff
|
razão
|
1.
|
|
THEN-2
|
2. |
![{\displaystyle \left(\left(A\to B\right)\to C\right)\to \left(A\to \left(B\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/08fe561705a71ca4aefacc0883fcf801b929fe69) |
TH12
|
3.
|
|
TH14* 1,2
|
4.
|
|
THEN-3* 3
|
5. |
![{\displaystyle A\to \left(\left(A\to B\right)\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c278ad370708cdd7651ea1f708ba9c836e6b4323) |
THEN-1
|
6.
|
|
TH1* 5,4
|
7.
|
|
THEN-3* 6
|
8. |
![{\displaystyle \left(A\to \left(A\to \left(B\to C\right)\right)\right)\to \left(A\to \left(B\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e2558bd428bf50c46a6735de4bd465f69f6a46e8) |
TH13
|
9. |
![{\displaystyle \left(\left(A\to B\right)\to \left(A\to C\right)\right)\to \left(A\to \left(B\to C\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6fa7528d0466b5820510a63474e6bd93253eb28c) |
TH1* 7,8.
|
Teorema TH16:
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(\neg A\to \neg B\right)\to \left(\neg \neg B\to \neg \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1dc03acfbd88d00a569e1052c70eb1d300d0394b) |
FRG-1
|
2. |
![{\displaystyle \neg \neg B\to \left(\left(\neg A\to \neg B\right)\to \neg \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5db8fc7425eb69acac250a4a55d24fea13cd839b) |
THEN-3* 1
|
3. |
![{\displaystyle B\to \neg \neg B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e0b4df56ed996f4b2b23a917f2f072739a2cfd35) |
FRG-3
|
4. |
![{\displaystyle B\to \left(\left(\neg A\to \neg B\right)\to \neg \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c07d003edff9623589151714c1ce4ad0e04b36cb) |
TH1* 3,2
|
5. |
![{\displaystyle \left(\neg A\to \neg B\right)\to \left(B\to \neg \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a494b0cacc9d094422cc4e81d2abf7123705e85c) |
THEN-3* 4
|
6. |
![{\displaystyle \neg \neg A\to A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/84aaf1a07ba682fb0d3a84a80bc528871cd5bd78) |
FRG-2
|
7. |
![{\displaystyle \left(\neg \neg A\to A\right)\to \left(B\to \left(\neg \neg A\to A\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ef51e9a148cb4dbfae669cc9770843abfb2b6cd2) |
THEN-1
|
8. |
![{\displaystyle B\to \left(\neg \neg A\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/815f07304c4f19a19e2a6c8b93fc42d22307a1e0) |
MP 6,7
|
9.
|
|
THEN-2
|
10. |
![{\displaystyle \left(B\to \neg \neg A\right)\to \left(B\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/741db5d1f8d14a7d4b5f5c05cb2d128b43d3e216) |
MP 8,9
|
11. |
![{\displaystyle \left(\neg A\to \neg B\right)\to \left(B\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ab6eab92e8fae2658ae252c2afffa2e8f314d7fc) |
TH1* 5,10.
|
Teorema TH17:
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(\neg A\to \neg \neg B\right)\to \left(\neg B\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/68fad5f59be0b8a73c95c81e5dc0482a16641dac) |
TH16, com B := \neg B
|
2. |
![{\displaystyle B\to \neg \neg B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e0b4df56ed996f4b2b23a917f2f072739a2cfd35) |
FRG-3
|
3. |
![{\displaystyle \left(B\to \neg \neg B\right)\to \left(\neg A\to \left(B\to \neg \neg B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a36ba8366278aa61b6f1dd811988ca8ccc797cc3) |
THEN-1
|
4. |
![{\displaystyle \neg A\to \left(B\to \neg \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/017c4c3fe70de2cb9f4f762a9251cc08f23a9e22) |
MP 2,3
|
5.
|
|
THEN-2
|
6. |
![{\displaystyle \left(\neg A\to B\right)\to \left(\neg A\to \neg \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/31fa39587ff65a83e25c76cf06ce991365b27d8c) |
MP 4,5
|
7. |
![{\displaystyle \left(\neg A\to B\right)\to \left(\neg B\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b86821acab95f6aebe8dd47b4850d3a221e5979f) |
TH1* 6,1.
|
Teorema TH18:
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(A\to B\right)\to \left(\neg B\to \left(A\to B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/99897673a0d254a521ad6a41d1d23f72367654a7) |
THEN-1
|
2. |
![{\displaystyle \left(\neg B\to \neg A\right)\to \left(A\to B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d9086e93e99a9480508488c853eccd0a8b45711e) |
TH16
|
3. |
![{\displaystyle \left(\neg B\to \neg A\right)\to \left(\neg B\to \left(A\to B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d54b35ef4b437c2a8ba08b5c81252c8d94600102) |
TH1* 2,1
|
4.
|
|
TH15
|
5. |
![{\displaystyle \neg B\to \left(\neg A\to \left(A\to B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d97cb2d00d47cfd252d9303dc919a137524302c1) |
MP 3,4
|
6. |
![{\displaystyle \left(\neg A\to \left(A\to B\right)\right)\to \left(\neg \left(A\to B\right)\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7279e0f15af4d9f1721aff9ecd4825bdc6af205f) |
TH17
|
7. |
![{\displaystyle \neg B\to \left(\neg \left(A\to B\right)\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c228794a81a2f2c495843301704a2186936bc448) |
TH1* 5,6
|
8.
|
|
THEN-2
|
9. |
![{\displaystyle \left(\neg B\to \neg \left(A\to B\right)\right)\to \left(\neg B\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cbf9585a13e8ded4745766c9e1a3cca7c4ecacaa) |
MP 7,8
|
10. |
![{\displaystyle \left(\left(A\to B\right)\to B\right)\to \left(\neg B\to \neg \left(A\to B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/34af49e6383a83dd7bdbdd6f65d14913db367946) |
FRG-1
|
11. |
![{\displaystyle \left(\left(A\to B\right)\to B\right)\to \left(\neg B\to A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/72a48b4321ef9376d74a89fb100488762a2d216d) |
TH1* 10,9
|
12. |
![{\displaystyle \left(\neg B\to A\right)\to \left(\neg A\to B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d9d2258b9d43f80e65876dd521614d26a6ddc66c) |
TH17
|
13. |
![{\displaystyle \left(\left(A\to B\right)\to B\right)\to \left(\neg A\to B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b9c0e1d7c74e1575c95cabca1bcbf92db3f9c3a1) |
TH1* 11,12.
|
Teorema TH19:
#
|
wff
|
razão
|
1. |
![{\displaystyle \neg A\to \left(\neg B\to \neg \left(\neg A\to \neg \neg B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7dd7f113b9dd71a2f3103a715530877dfb3cca83) |
TH10
|
2. |
![{\displaystyle B\to \neg \neg B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e0b4df56ed996f4b2b23a917f2f072739a2cfd35) |
FRG-3
|
3. |
![{\displaystyle \left(B\to \neg \neg B\right)\to \left(\neg A\to \left(B\to \neg \neg B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a36ba8366278aa61b6f1dd811988ca8ccc797cc3) |
THEN-1
|
4. |
![{\displaystyle \neg A\to \left(B\to \neg \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/017c4c3fe70de2cb9f4f762a9251cc08f23a9e22) |
MP 2,3
|
5.
|
|
THEN-2
|
6. |
![{\displaystyle \left(\neg A\to B\right)\to \left(\neg A\to \neg \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/31fa39587ff65a83e25c76cf06ce991365b27d8c) |
MP 4,5
|
7. |
![{\displaystyle \neg \left(\neg A\to \neg \neg B\right)\to \neg \left(\neg A\to B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/24ef61f457eb280db3775aba0d56b0b6a6235473) |
FRG-1* 6
|
8. |
![{\displaystyle \neg A\to \left(\neg B\to \neg \left(\neg A\to B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d69f42c9622fd4e4c2fd7818f50d36102375ca28) |
TH14* 1,7
|
9. |
![{\displaystyle \left(\left(A\to B\right)\to B\right)\to \left(\neg A\to B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b9c0e1d7c74e1575c95cabca1bcbf92db3f9c3a1) |
TH18
|
10. |
![{\displaystyle \neg \left(\neg A\to B\right)\to \neg \left(\left(A\to B\right)\to B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/507e2a28ea5e31e56f2ff5aa0779460f933c1370) |
FRG-1* 9
|
11. |
![{\displaystyle \neg A\to \left(\neg B\to \neg \left(\left(A\to B\right)\to B\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/20b0c3fc7a469963b32df8c879a00c394a1f5a6b) |
TH14* 8,10
|
12.
|
|
THEN-1* 11
|
13.
|
|
THEN-2* 12
|
14.
|
|
THEN-2
|
15.
|
|
TH1* 13,14
|
16. |
![{\displaystyle \left(A\to C\right)\to \left(\neg C\to \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4b84c5d9c7a951e22b5746628bce8cdcedb35a6a) |
FRG-1
|
17.
|
|
TH1* 16,15
|
18.
|
|
TH16
|
19.
|
|
TH14* 17,18
|
20. |
![{\displaystyle \left(B\to C\right)\to \left(\neg C\to \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d66068298ae5815eb2884f8051968b9a9135ac88) |
FRG-1
|
21.
|
|
TH1
|
22.
|
|
MP 20,21
|
23.
|
|
TH1* 19,22.
|
Teorema TH20:
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(A\to A\right)\to \left(\left(A\to \neg A\right)\to \neg A\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/47e98168292db9716ca79b6feb0400df5bbddbc4) |
TH11
|
2. |
![{\displaystyle A\to A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4fbf720da5a9387e23c628079fbc3e021399c911) |
TH7
|
3. |
![{\displaystyle \left(A\to \neg A\right)\to \neg A}](https://wikimedia.org/api/rest_v1/media/math/render/svg/db770753dfe47555be5b472d165fdbc8047f6839) |
MP 2,1.
|
Teorema TH21:
#
|
wff
|
razão
|
1. |
![{\displaystyle A\to \left(\neg A\to \neg \neg B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/00233f9a08ba334e17b5ff8cdd2ba62151e2cbca) |
TH2, com B := ~B
|
2. |
![{\displaystyle \neg \neg B\to B}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0e87655e86dcda07099f7911e61f00372187d2d0) |
FRG-2
|
3. |
![{\displaystyle A\to \left(\neg A\to B\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6002b32e08d96796e3bfa268b67176f1f5dcde5c) |
TH14* 1,2.
|
O lógico e filósofo polonês Jan Łukasiewicz, famoso por seus estudos em lógicas não-clássicas, provou que o THEN-3 é dedutível do THEN-1 e do THEN-2.
- THEN-1:
![{\displaystyle P\to \left(Q\to P\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/efd69e89a780004702cb03853ae204655dca67c1)
- THEN-2:
![{\displaystyle \left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c055e2fb4ae517bf11e89bb7c457f4b01403f2c7)
- Tese 1:
![{\displaystyle \left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a00e1b0742e52220970dd18c6a6af5c2ec33de1a)
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(\left(\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d2218d472055912bfced7ec2568517d0cb53bf7d) |
THEN-1*
|
2. |
![{\displaystyle \left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c055e2fb4ae517bf11e89bb7c457f4b01403f2c7) |
THEN-2
|
3. |
![{\displaystyle \left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a00e1b0742e52220970dd18c6a6af5c2ec33de1a) |
MP 1,2.
|
*
*
- Tese 2:
![{\displaystyle \left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c0884c56aea87da838d50c57f9b476c7a70d91ec)
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(\left(\left(Q\to R\right)\to \left(\left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\right)\to \left(\left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7ea9d5648a5b018a491a43a4e8a33ca3a61b2423) |
THEN-2*
|
2. |
![{\displaystyle \left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a00e1b0742e52220970dd18c6a6af5c2ec33de1a) |
Prop. 1
|
3. |
![{\displaystyle \left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c0884c56aea87da838d50c57f9b476c7a70d91ec) |
MP 1,2.
|
*
*
*
- Tese 3:
![{\displaystyle \left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3efb0196417b085d417c3ee91537448d9052fa67)
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(\left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)\right)\to \left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c0884c56aea87da838d50c57f9b476c7a70d91ec) |
Prop.2
|
2. |
![{\displaystyle \left(Q\to R\right)\to \left(P\to \left(Q\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1672a654e3e0b60e9d0da54696c8f6253fe66d8e) |
THEN-1*
|
3. |
![{\displaystyle \left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3efb0196417b085d417c3ee91537448d9052fa67) |
MP 1,2.
|
*
*
- Tese 4:
![{\displaystyle \left(\left(Q\to R\right)\to \left(P\to Q\right)\right)\to \left(\left(Q\to R\right)\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5ccdbd81b89cf4a8ca7b7d69afc4a92953d4e925)
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(\left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\to \left(\left(\left(Q\to R\right)\to \left(P\to Q\right)\right)\to \left(\left(Q\to R\right)\to \left(P\to R\right)\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/73bb94d88f341ba102317befb64940559065ee5d) |
THEN-2*
|
2. |
![{\displaystyle \left(Q\to R\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3efb0196417b085d417c3ee91537448d9052fa67) |
Prop.3
|
3. |
![{\displaystyle \left(\left(Q\to R\right)\to \left(P\to Q\right)\right)\to \left(\left(Q\to R\right)\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5ccdbd81b89cf4a8ca7b7d69afc4a92953d4e925) |
MP 1,2.
|
*
*
*
- Tese 5:
![{\displaystyle R\to \left(P\to \left(Q\to P\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fd8d78300353aadc62e19701ed6dfd302176c6c8)
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(P\to \left(Q\to P\right)\right)\to \left(R\to \left(P\to \left(Q\to P\right)\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9689f40a780ac5f94a40936e2b677d42265ea6fc) |
THEN-1*
|
2. |
![{\displaystyle P\to \left(Q\to P\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/efd69e89a780004702cb03853ae204655dca67c1) |
THEN-1
|
3. |
![{\displaystyle R\to \left(P\to \left(Q\to P\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fd8d78300353aadc62e19701ed6dfd302176c6c8) |
MP 1,2.
|
*
*
- Tese 6:
![{\displaystyle \left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b7ef57015a26d8c9cbe5ad4b1c7c15513240147c)
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(\left(\left(P\to Q\right)\to R\right)\to \left(Q\to \left(P\to Q\right)\right)\right)\to \left(\left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/83a1e7720252bac142640dee30e43d9f34607778) |
Prop.4*
|
2. |
![{\displaystyle \left(\left(P\to Q\right)\to R\right)\to \left(Q\to \left(P\to Q\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/805b056527428455af804582b0f11fe15f1e4aaa) |
Prop.5**
|
3. |
![{\displaystyle \left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b7ef57015a26d8c9cbe5ad4b1c7c15513240147c) |
MP 1,2.
|
*
*
**
**
**
- Tese 7:
![{\displaystyle \left(S\to \left(\left(P\to Q\right)\to R\right)\right)\to \left(S\to \left(Q\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f110e4932bc1590081d5581d6d74a59bb2d591e4)
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(\left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)\right)\to \left(\left(S\to \left(\left(P\to Q\right)\to R\right)\right)\to \left(S\to \left(Q\to R\right)\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/04c1c699ca7316e4b7c89c466a414ec8e84d687d) |
Prop.3*
|
2. |
![{\displaystyle \left(\left(P\to Q\right)\to R\right)\to \left(Q\to R\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b7ef57015a26d8c9cbe5ad4b1c7c15513240147c) |
Prop.6
|
3. |
![{\displaystyle \left(S\to \left(\left(P\to Q\right)\to R\right)\right)\to \left(S\to \left(Q\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f110e4932bc1590081d5581d6d74a59bb2d591e4) |
MP 1,2.
|
*
*
*
- THEN-3:
![{\displaystyle \left(P\to \left(Q\to R\right)\right)\to \left(Q\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5e779c7d0bfdf6cec6b723411af95e9abc25aa07)
#
|
wff
|
razão
|
1. |
![{\displaystyle \left(\left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)\right)\to \left(\left(P\to \left(Q\to R\right)\right)\to \left(Q\to \left(P\to R\right)\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6bc94d5ebb86f13c523f8b040487f6573f223914) |
Prop.7*
|
2. |
![{\displaystyle \left(P\to \left(Q\to R\right)\right)\to \left(\left(P\to Q\right)\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c055e2fb4ae517bf11e89bb7c457f4b01403f2c7) |
THEN-2
|
3. |
![{\displaystyle \left(P\to \left(Q\to R\right)\right)\to \left(Q\to \left(P\to R\right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5e779c7d0bfdf6cec6b723411af95e9abc25aa07) |
MP 1,2.
|
*
*
- THEN-1:
![{\displaystyle \varphi \to \left(\chi \to \varphi \right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/81b6f7786210ec897417ace4ece8575a86f9448a)
- THEN-2:
![{\displaystyle \left(\varphi \to \left(\chi \to \psi \right)\right)\to \left(\left(\varphi \to \chi \right)\to \left(\varphi \to \psi \right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7913b25384b898fcbb364f94bab819b4a755f179)
- AND-1:
![{\displaystyle \left(\varphi \land \chi \right)\to \varphi }](https://wikimedia.org/api/rest_v1/media/math/render/svg/cf1638e5542a3073fe833900674f0d604f8a7c09)
- AND-2:
![{\displaystyle \left(\varphi \land \chi \right)\to \chi }](https://wikimedia.org/api/rest_v1/media/math/render/svg/c3bb2ab7411a51c50c7c9854248132a0172b041d)
- AND-3:
![{\displaystyle \varphi \to \left(\chi \to \left(\varphi \land \chi \right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/619afcf12514cac06d0cbd9b48d7a11fc04fb366)
- OR-1:
![{\displaystyle \varphi \to \left(\varphi \lor \chi \right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/84b8a9a2e37893242a7c3b79e75dc921f06b280d)
- OR-2:
![{\displaystyle \chi \to \left(\varphi \lor \chi \right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2a2bd0c0df15f9143f452931470402eeab48520f)
- OR-3:
![{\displaystyle \left(\varphi \to \psi \right)\to \left(\left(\chi \to \psi \right)\to \left(\left(\varphi \lor \chi \right)\to \psi \right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e4ab8917f7ff3589c93ae2e1d947c22578837117)
- NOT-1:
![{\displaystyle \left(\varphi \to \chi \right)\to \left(\left(\varphi \to \neg \chi \right)\to \neg \varphi \right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/28b4342e8074b4195a2db025f5c2f4ad27362fdb)
- NOT-2:
![{\displaystyle \varphi \to \left(\neg \varphi \to \chi \right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9a5eac2396ae885aae824f614d3abfad19052875)
- NOT-3:
![{\displaystyle \varphi \lor \neg \varphi }](https://wikimedia.org/api/rest_v1/media/math/render/svg/e772af885ac1d37a565143123958ca1e75a55657)
- IFF-1:
![{\displaystyle \left(\varphi \leftrightarrow \chi \right)\to \left(\varphi \to \chi \right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0751de4d42bce2eb547e6a48d0fdcc35a5df197c)
- IFF-2:
![{\displaystyle \left(\varphi \leftrightarrow \chi \right)\to \left(\chi \to \varphi \right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3ce4eba2d9e7a080656ddad481585a3d0aada1a5)
- IFF-3:
![{\displaystyle \left(\varphi \to \chi \right)\to \left(\left(\chi \to \varphi \right)\to \left(\varphi \leftrightarrow \chi \right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4db2d93cd12f455eb33c1464e308520b8a9909ba)
![{\displaystyle \alpha \to \alpha \,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/56f54023222cbae2814fedec5262ad0b6c5215ef)
#
|
wff
|
razão
|
1. |
![{\displaystyle \alpha \to \left(\alpha \to \alpha \right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3dd65cf8e2cb1feaa79d37053a58ee624c0d426b) |
THEN-1*
|
2. |
![{\displaystyle \alpha \to \left(\left(\alpha \to \alpha \right)\to \alpha \right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ed0244668e5f15709112ad7c54a5a08bd9d4d667) |
THEN-1**
|
3. |
![{\displaystyle \left(\alpha \to \left(\left(\alpha \to \alpha \right)\to \alpha \right)\right)\to \left(\left(\alpha \to \left(\alpha \to \alpha \right)\right)\to \left(\alpha \to \alpha \right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8bed2f0105453decddf30e1bae9f17aa343e75a3) |
THEN-2***.
|
4. |
![{\displaystyle \left(\left(\alpha \to \left(\alpha \to \alpha \right)\right)\to \left(\alpha \to \alpha \right)\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f6ec13059f0a519081b85d8689ca6bc43880139e) |
2,3 MP.
|
5. |
![{\displaystyle \alpha \to \alpha \,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/56f54023222cbae2814fedec5262ad0b6c5215ef) |
1,4 MP.
|
*
,
**
,
***
,
,