Regulile lui \( P_1 \):
00. Din \( [A\supset B] \) si \( A \) rezulta \( B \). (regula modus ponens)
01. Daca \( b \) este variabila, atunci din \( A \) rezulta \( S_{_B}^{b}A\mid \). (regula substitutiei)
Axiomele lui \( P_1 \):
02. \( [p\supset[q\supset p]] \).
03. \( [[s\supset[p\supset q]]\supset[[s\supset p]\supset[s\supset q]]] \).
04. \( [[[p\supset f]\supset f]\supset p] \).
Demonstrati in \( P_1 \) teorema \( [[q\supset r]\supset[[p\supset q]\supset[p\supset r]]] \).
Sistemul P1 (Church)
Moderator: Liviu Paunescu
Sistemul P1 (Church)
Last edited by gefest on Mon Mar 16, 2009 1:11 am, edited 1 time in total.
Pentru a scurta demonstratia voi aplica metateorema despre substitutia simultana:
Daca \( \vdash A \), atunci \( \vdash S^{b_1,\ldots,b_n}_{B_1,\ldots,B_n}A \), care este o regula derivata
si voi scoate parantezele exterioare ale formulei.
(1) \( [q\supset r]\supset[p\supset [q\supset r]]\\ \) - substitutia simultana in 02.
(2) \( [p\supset[q\supset r]]\supset[[p\supset q]\supset[p\supset r]]\\ \) - substitutia simultana in 03.
(3) \( [[p\supset[q\supset r]]\supset[[p\supset q]\supset[p\supset r]]]\supset[[q\supset r]\supset[[p\supset[q\supset r]]\supset[[p\supset q]\supset[p\supset r]]]]\\ \) - substitutia simultana in 02.
(4) \( [q\supset r]\supset[[p\supset[q\supset r]]\supset[[p\supset q]\supset[p\supset r]]]\\ \) - regula 00, (2), (3).
(5) \( [[q\supset r]\supset[[p\supset[q\supset r]]\supset[[p\supset q]\supset[p\supset r]]]]\supset[[[q\supset r]\supset[p\supset[q\supset r]]]\supset[[q\supset r]\supset[[p\supset q]\supset[p\supset r]]]] \) - substitutia simultana in 03.
(6) \( [[q\supset r]\supset[p\supset[q\supset r]]]\supset[[q\supset r]\supset[[p\supset q]\supset[p\supset r]]] \) - regula 00, (4), (5).
(7) \( [q\supset r]\supset[[p\supset q]\supset[p\supset r]] \) - regula 00, (1), (6).
Folosind acest rezultat voi demonstra \( [p\supset q]\supset[[q\supset r]\supset[p\supset r]] \) ca teorema in \( P_1 \).
Substitutie simultana in 03:
\( \vdash[[q\supset r]\supset[[p\supset q]\supset[p\supset r]]]\supset\\
\quad\supset[[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]]].
\)
Rezultatul precedent:
\( \vdash[q\supset r]\supset[[p\supset q]\supset[p\supset r]].
\)
Modus ponens:
\(
\vdash[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]].
\)
Substitutie simultana in 02:
\(
\vdash[[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]]]\supset\\
\quad\supset[[p\supset q]\supset[[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]]]].
\)
Modus ponens:
\(
\vdash[p\supset q]\supset[[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]]].
\)
Substitutie simultana in 03:
\(
\vdash[[p\supset q]\supset[[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]]]]\supset\\
\quad\supset[[[p\supset q]\supset[[q\supset r]\supset[p\supset q]]]\supset[[p\supset q]\supset[[q\supset r]\supset[p\supset r]]]].
\)
Modus ponens:
\(
\vdash[[p\supset q]\supset[[q\supset r]\supset[p\supset q]]]\supset[[p\supset q]\supset[[q\supset r]\supset[p\supset r]]].
\)
Substitutie simultana in 02:
\(
\vdash[p\supset q]\supset[[q\supset r]\supset[p\supset q]].
\)
Modus ponens:
\(
\vdash[p\supset q]\supset[[q\supset r]\supset[p\supset r]].
\)
Daca \( \vdash A \), atunci \( \vdash S^{b_1,\ldots,b_n}_{B_1,\ldots,B_n}A \), care este o regula derivata
si voi scoate parantezele exterioare ale formulei.
(1) \( [q\supset r]\supset[p\supset [q\supset r]]\\ \) - substitutia simultana in 02.
(2) \( [p\supset[q\supset r]]\supset[[p\supset q]\supset[p\supset r]]\\ \) - substitutia simultana in 03.
(3) \( [[p\supset[q\supset r]]\supset[[p\supset q]\supset[p\supset r]]]\supset[[q\supset r]\supset[[p\supset[q\supset r]]\supset[[p\supset q]\supset[p\supset r]]]]\\ \) - substitutia simultana in 02.
(4) \( [q\supset r]\supset[[p\supset[q\supset r]]\supset[[p\supset q]\supset[p\supset r]]]\\ \) - regula 00, (2), (3).
(5) \( [[q\supset r]\supset[[p\supset[q\supset r]]\supset[[p\supset q]\supset[p\supset r]]]]\supset[[[q\supset r]\supset[p\supset[q\supset r]]]\supset[[q\supset r]\supset[[p\supset q]\supset[p\supset r]]]] \) - substitutia simultana in 03.
(6) \( [[q\supset r]\supset[p\supset[q\supset r]]]\supset[[q\supset r]\supset[[p\supset q]\supset[p\supset r]]] \) - regula 00, (4), (5).
(7) \( [q\supset r]\supset[[p\supset q]\supset[p\supset r]] \) - regula 00, (1), (6).
Folosind acest rezultat voi demonstra \( [p\supset q]\supset[[q\supset r]\supset[p\supset r]] \) ca teorema in \( P_1 \).
Substitutie simultana in 03:
\( \vdash[[q\supset r]\supset[[p\supset q]\supset[p\supset r]]]\supset\\
\quad\supset[[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]]].
\)
Rezultatul precedent:
\( \vdash[q\supset r]\supset[[p\supset q]\supset[p\supset r]].
\)
Modus ponens:
\(
\vdash[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]].
\)
Substitutie simultana in 02:
\(
\vdash[[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]]]\supset\\
\quad\supset[[p\supset q]\supset[[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]]]].
\)
Modus ponens:
\(
\vdash[p\supset q]\supset[[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]]].
\)
Substitutie simultana in 03:
\(
\vdash[[p\supset q]\supset[[[q\supset r]\supset[p\supset q]]\supset[[q\supset r]\supset[p\supset r]]]]\supset\\
\quad\supset[[[p\supset q]\supset[[q\supset r]\supset[p\supset q]]]\supset[[p\supset q]\supset[[q\supset r]\supset[p\supset r]]]].
\)
Modus ponens:
\(
\vdash[[p\supset q]\supset[[q\supset r]\supset[p\supset q]]]\supset[[p\supset q]\supset[[q\supset r]\supset[p\supset r]]].
\)
Substitutie simultana in 02:
\(
\vdash[p\supset q]\supset[[q\supset r]\supset[p\supset q]].
\)
Modus ponens:
\(
\vdash[p\supset q]\supset[[q\supset r]\supset[p\supset r]].
\)
Last edited by gefest on Fri Jul 31, 2009 2:12 pm, edited 1 time in total.