Dedvctio: introdvctio · Topos Uranos

Svmmarivm

Haec lectio secvndam cvrsvs vnitatem aperit, dedvctioni dicatam. Qvinqve eivs lectiones exhibet et filvm qvo connectvntvr, a definitione systematis dedvctivi formalis vsqve ad leges De Morgani et leges distribvtivas; vnitatem in itinere cvrsvs collocat, inter lingvam, iam constrvctam, et semanticam et metatheoriam, qvae venient, et praenvntiat qvid hae de ea dictvrae sint; electionem systematis axiomatici ivstificat, qvod dvabvs partibvs constrvitvr (systemate Łvkasiewiczii, cvm tribvs schematibvs axiomatvm et modo ponente, et systemate cvrsvs, qvod ei regvlam svbstitvtionis dvplicis negationis addit), et exponit cvr haec secvnda regvla necessaria sit et cvr postvletvr potivs qvam demonstretvr; brevi dedvctione ostendit qvantvm laboris ratiocinatio elementaris celet; definit qvid ex vnitate svperiore svmatvr, scilicet legibilitas vnica, indvctio (fortis in nvmeris natvralibvs et strvctvralis) et explicatio abbreviationvm, et consilia dat ad eam discendam.

Proposita discendi

Seriem qvinqve lectionvm vnitatis describere et exponere qvae cvivsqve effecta seqvens adhibeat.
Dedvctionem in itinere cvrsvs collocare, dedvcibilitatem $\Gamma \vdash \varphi$ a conseqventia semantica $\Gamma \models \varphi$ distingvere et exponere qvid firmitas et completvdo affirmatvrae sint.
Explicare cvr systema cvrsvs systemati Łvkasiewiczii secvndam regvlam primitivam addat, svbstitvtionem dvplicis negationis, ab eo profectvm qvod tria schemata in negatione conivncta videre possvnt et non possvnt.
Dedvctionem brevem per versvs nvmeratos legere, dedvctionem formvlarvm a dedvctione de dedvctionibvs distingvere, agnoscere qvid vnitas ex svperiore svmat et stvdivm eivs a probatione initiali profectvm ordinare.

Probatio initialis

Anteqvam vnitas percvrritvr, initivm ipsvm metiri expedit. Haec probatio est svi ipsivs exploratio: nvlli censvrae svbicitvr, et solvm eivs propositvm est stvdivm dirigere. Tredecim eivs qvaestiones dvorvm genervm svnt. Tres primae attingvnt qvae vnitas ex svperiore pro cognitis habet: legibilitatem vnicam, indvctionem fortem et explicationem abbreviationvm; qvi in aliqva errat, anteqvam pergat, lectionem qvam qvaestio nominat repetere debet. Decem reliqvae ordine qvinqve hvivs vnitatis lectiones attingvnt: tres primam, tres secvndam, dvae tertiam, vna qvartam et vna qvintam. Qvi nvmqvam systema dedvctivvm didicit eas recte solvere non debet exspectare, neqve id refert: qvodqve responsvm, rectvm necne, rem exponit et lectionem nominat qvae eam tractat. Eaedem facvltates in fine, in lectione synthesis, itervm metivntvr.

Probatio initialis

Antequam vnitatem incipias, pvnctvm vnde proficisceris metire. Brevis est sui ipsivs probatio: non aestimatvr, et eivs exitvs in solo tvo navigatro servatvr.

Qvaestio 1Ex vnitatibvs prioribvsCatena $\sigI\sigI\sigO\sigI\sigO\sigO\sigI\sigO\sigI$ est formvla composita, formae $\sigI\varphi\psi$ . Qvae svnt eivs partes $\varphi$ et $\psi$ ?
$\varphi = \sigI\sigO\sigI\sigO\sigO\sigI$ et $\psi = \sigO\sigI$ .
$\varphi = \sigI\sigO\sigI$ et $\psi = \sigO\sigO\sigI\sigO\sigI$ .
Dvas partitiones admittit, provt catena post discvm initialem alio loco secatvr.
$\varphi$ est tota catena qvae discvm initialem seqvitvr, et $\psi$ est catena vacva.
Qvaestio 2Ex vnitatibvs prioribvsIn demonstratione per indvctionem fortem omnem nvmervm natvralem $n$ proprietatem $P(n)$ habere, qvid svpponi potest cvm $P(n)$ demonstratvr?
Valere $P(m)$ pro omni nvmero natvrali $m$ minore qvam $n$ .
Solvm valere $P(n - 1)$ .
Valere $P(m)$ pro omni nvmero natvrali $m$ minore qvam $n$ vel aeqvali.
Nihil, donec $P(1)$ et $P(2)$ separatim demonstrata sint.
Qvaestio 3Ex vnitatibvs prioribvsAbbreviationibvs statvtis cvrsvs, qvam formvlam designat $(\varphi \rightarrow \psi)$ , negatione conivncta et negatione scriptam?
$\neg(\neg\varphi \downarrow \psi)$ .
$(\neg\varphi \downarrow \psi)$ .
$\neg(\varphi \downarrow \neg\psi)$ .
Nvlla certa: pendet ex eo qvomodo eam legere decernatvr.
Qvaestio 4Schema A1 est $(\varphi \rightarrow (\psi \rightarrow \varphi))$ . Estne formvla $(v_{1} \rightarrow (v_{2} \rightarrow v_{3}))$ instantia schematis A1?
Non: prima et vltima occvrrentia ipsivs $\varphi$ in eandem formvlam mvtari deberent, et hic svnt $v_{1}$ et $v_{3}$ .
Ita, cvm $\varphi := v_{1}$ et $\psi := v_{2}$ .
Ita, qvia omnis implicatio cvivs conseqvens est alia implicatio instantia est schematis A1.
Non, qvia instantiae schematis variabiles continere non possvnt.
Qvaestio 5In dedvctione iam invenivntvr versvs $\psi$ et $(\varphi \rightarrow \psi)$ , vbi $\varphi$ et $\psi$ formvlae distinctae svnt. Qvam formvlam scribere sinit modvs ponens ad hos dvos versvs adhibitvs?
Nvllam: modvs ponens antecedens $\varphi$ postvlat, et qvod habetvr est conseqvens.
$\varphi$ .
$(\psi \rightarrow \varphi)$ .
$\neg\varphi$ .
Qvaestio 6Notvm est $\{\varphi\} \vdash \psi$ , id est esse dedvctionem formvlae $\psi$ cvivs vnica praemissa est $\varphi$ . Qvid tvm affirmat theorema dedvctionis?
$\vdash (\varphi \rightarrow \psi)$ : implicatio est theorema.
$\vdash \psi$ : praemissa sine vlla mora tolli potest.
$\vdash (\psi \rightarrow \varphi)$ .
$\{\psi\} \vdash \varphi$ .
Qvaestio 7Qvid dedvcitvr, nvllis aliis praemissis, ex classe $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\}$ ?
$(\varphi \rightarrow \chi)$ .
$\chi$ , modo ponente bis adhibito.
$(\chi \rightarrow \varphi)$ .
$(\varphi \wedge \chi)$ .
Qvaestio 8Regvla svbstitvtionis dvplicis negationis (SDN) in versv vnam solam occvrrentiam svbformvlae mvtat, et in catenam lingvae fvndamentalis agit. Qvot occvrrentias svbformvlae $\neg v_{1}$ continet catena qvam designat $(v_{1} \rightarrow v_{2})$ ?
Dvas.
Vnam, eam qvae antecedenti respondet.
Nvllam: formvla negationes non continet.
Qvattvor.
Qvaestio 9Qvae formvla ex $(\neg\varphi \rightarrow \psi)$ per contrapositionem obtinetvr, nvllis dvplicibvs negationibvs additis?
$(\neg\psi \rightarrow \varphi)$ .
$(\psi \rightarrow \neg\varphi)$ .
$(\varphi \rightarrow \neg\psi)$ .
$(\neg\psi \rightarrow \neg\varphi)$ .
Qvaestio 10Designantne $(\varphi \vee \psi)$ et $(\neg\varphi \rightarrow \psi)$ eandem formvlam?
Non: prima est $\neg(\varphi \downarrow \psi)$ et secvnda $\neg(\neg\neg\varphi \downarrow \psi)$ ; formvlae distinctae svnt, per dedvctionem aeqvivalentes.
Ita, per definitionem implicationis.
Ita, qvia vtraqve « $\varphi$ vel $\psi$ » legitvr.
Non, neqve altera ex altera dedvcitvr.
Qvaestio 11Notvm est $\varphi \dashv\vdash \varphi'$ , id est vtramqve ex altera dedvci. Qvid ivstificat etiam $\neg\varphi \dashv\vdash \neg\varphi'$ ?
Theorema, svbstitvtio aeqvivalentivm, qvod theoremate dedvctionis et contrapositione demonstratvr.
Nvlla ivstificatio pecvliaris: satis est «vtrvmqve latvs negare» aeqvivalentiae.
Definitio negationis, qvia $\neg\varphi$ est $(\varphi \downarrow \varphi)$ .
Nihil, qvia vervm non est: negatio formvlas aeqvivalentes separare potest.
Qvaestio 12Ex classe praemissarvm $\Gamma \cup \{\neg\varphi\}$ dedvcvntvr formvla $\chi$ eivsqve negatio $\neg\chi$ . Qvid conclvdi potest?
$\Gamma \vdash \varphi$ .
$\Gamma \vdash \neg\varphi$ .
Ex $\Gamma$ qvamlibet formvlam dedvci.
Nihil: dedvctio qvae ad contradictionem pervenit nihil probat.
Qvaestio 13Cvi formvlae aeqvivalet negatio implicationis, $\neg(\varphi \rightarrow \psi)$ ?
Formvlae $(\varphi \wedge \neg\psi)$ .
Formvlae $(\neg\varphi \rightarrow \neg\psi)$ .
Formvlae $(\varphi \rightarrow \neg\psi)$ .
Formvlae $(\neg\varphi \wedge \psi)$ .