PROPOSITUM DISCENDI:
Post hanc lectionem, discipulus poterit:

1. Intelligere notionem inductionis de complexitate expressionum.
2. Applicare inductionem mathematicam de complexitate formularum in logica propositionali.
3. Intelligere demonstrationem per inductionem de complexitate et eius applicationem in logica propositionali.

INDEX
INDUCTIO DE COMPLEXITATE
EXEMPLUM SIMPLEX: THEOREMA SUBSTITUTIONIS

Inductio de complexitate

Supponamus nos velle demonstrare proprietatem \mathcal{P} valere pro qualibet expressione F. Hoc demonstrari potest per variationem inductionis mathematicae, quae “inductio de complexitate expressionum” vocatur. Haec per hos gradus exsequitur:

• Primum ostendimus omnes expressiones atomicas hanc proprietatem implere (hoc respondet casui n=1 in inductione classica).
• Deinde, assumendo eam valere pro quibuslibet expressionibus F et G, demonstramus ex hoc sequi eam quoque valere pro expressionibus formae F\downarrow G; seu equivalenter, pro \neg F et aliqua ex sequentibus: F\wedge G, F\vee G, F\rightarrow G.

Si hoc perficere possumus, concludimus proprietatem \mathcal{P} valere pro omnibus expressionibus logicae propositionalis. Hoc est quod dicimus “inductionem mathematicam de complexitate expressionum”.

Exemplum Simplex: Theorema Substitutionis

Ut clarius intellegamus quomodo fiat inductio de complexitate formularum, consideremus (meta)theorema substitutionis.

Supponamus F\equiv G. Sit H expressio quae F tamquam subexpressionem continet, et sit H^\prime expressio quae fit substituendo omnes occurrentias F per G; tum H\equiv H^\prime.

Demonstratio per Inductionem de Complexitate Formularum

Demonstratio per inductionem de complexitate constat ostensione duarum rerum: 1) casus initialis (pro formulis atomicis) et 2) passus inductivus (si valet pro quibuslibet expressionibus F et G, tum valet etiam pro F\downarrow G, vel simplicius: valet pro \neg F et saltem uno ex sequentibus: F\vee G, F\wedge G, F\rightarrow G, F\leftrightarrow G.)

Supponamus H esse expressionem atomicam, F subexpressionem H, et F\equiv G. Si H^\prime est expressio quae fit substituendo omnes subexpressiones F in H, cum H sit atomica, erit H^\prime \equiv G. Praeterea, cum H sit atomica et F eius subexpressio, tunc H\equiv F. Denique sequetur:

H\equiv F \equiv G \equiv H^\prime

Ita demonstratur casus initialis pro expressionibus atomicis.

Videamus nunc casum inductivum.

Hypothesis Inductionis

Supponamus theorema valere pro duabus quibuslibet expressionibus H_1 et H_2, quarum utraque F tamquam subexpressionem continet et F \equiv G. Tum si H_1^\prime est expressio ex H_1 orta per substitutionem omnium F per G, et H_2^\prime similter ex H_2, sequitur H_1\equiv H_1^\prime et H_2\equiv H_2^\prime.

Passus Inductivus

Hic examinamus an, ex hypothesi inductionis, theorema quoque valeat pro \neg H_1 (vel \neg H_2, alterutro) et saltem uno ex sequentibus: H_1 \wedge H_2, H_1 \vee H_2, H_1 \rightarrow H_2.

Si H:= \neg H_1, tum ex hypothesi inductionis sequetur H\equiv \neg H_1^\prime=: H^\prime , ubi H^\prime est expressio quae fit ex H substituendo omnes occurrentias F per G. Ergo H\equiv H^\prime.

Similiter, si H:= H_1 \wedge H_2, tum ex hypothesi inductionis habebitur H\equiv H_1^\prime \wedge H_2 \equiv H_1^\prime \wedge H_2^\prime =: H^\prime , ubi H^\prime est expressio quae fit ex H substituendo omnes occurrentias F per G. Ergo H\equiv H^\prime.

Ergo inductio completa est et theorema substitutionis valet pro omnibus expressionibus logicae propositionalis.

Applicando hanc formam inductionis, potest demonstrari proprietatem manere pro omnibus expressionibus systematis logici, quod est praecipue utile in logica propositionali ad structuras demonstrationum rigorosas instituendas. Praeterea eius utilitas ad disciplinas extenditur sicut intelligentia artificialis et progressus programmatum computatoriorum, ubi verificatio systematum logicorum est fundamentalis. Per hanc technicam, demonstrationes automatice perfici possunt et consistentia expressionum complexarum corroborari, quod periculum errorum minuit et praecisionem auget in mediis quae ex firmitate mathematica et logica pendent.