The Peano axioms๏
This package formalizes [Tao06, chapter 2.1 - The Peano axioms] .
The report content.
๐๐๐พ ๐ฏ๐พ๐บ๐๐ ๐บ๐๐๐๐๐ # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฝ๐ฟ๐ผ๐ฝ๐ฒ๐ฟ๐๐ถ๐ฒ๐ ๐๐ผ๐ป๐๐ถ๐๐๐ฒ๐ป๐ฐ๐: undetermined ๐ฆ๐๐ฎ๐ฏ๐ถ๐น๐ถ๐๐ฒ๐ฑ: False ๐๐ ๐๐ฒ๐ป๐ฑ๐ฒ๐ฑ ๐๐ต๐ฒ๐ผ๐ฟ๐: N/A # ๐ฆ๐ถ๐บ๐ฝ๐น๐ฒ-๐ผ๐ฏ๐ท๐ฒ๐ฐ๐๐ ๐ฑ๐ฒ๐ฐ๐น๐ฎ๐ฟ๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ โ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐โ, โ0โ, โ1โ, โ2โ, โ3โ, โ4โ, โ5โ, โ6โ ๐ป๐พ ๐ ๐๐๐๐๐-๐๐๐๐๐๐ก๐ ๐๐ ๐ฐโ. # ๐ฅ๐ฒ๐น๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ โ++โ, โ๐ผ๐๐โ ๐ป๐พ ๐ข๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐๐ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โโนโ, โโ โ, โโงโ, โ๐๐ -๐โ, โ=โ ๐ป๐พ ๐๐๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐๐ ๐๐ ๐ฐโ. # ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ๐ ๐ณ๐๐พ ๐ฟ๐๐ ๐ ๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ๐ ๐บ๐๐พ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐๐ฝ๐พ๐ ๐๐๐๐ ๐๐๐พ๐๐๐: ๐ซ๐พ๐ โ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐๐ข๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข (๐โ โง ๐โ ))โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ฑ, ๐ฒ โข (๐ฑ = ๐ฒ))โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ)โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆโ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ))โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐๐๐ ๐๐ ๐ก๐๐๐๐ฆ-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐-2โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ = ๐โ), (๐โ โ ๐โ) โข ๐ผ๐๐(๐ฏโ))โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐ข๐ -๐๐๐๐๐๐ โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ โน ๐โ), ๐โ โข ๐โ)โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐๐-๐๐ฆ-๐๐๐๐ข๐ก๐๐ก๐๐๐-2โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ ๐๐๐๐๐ข๐๐๐ก๐ (๐ฑโ = ๐ฒโ)), ๐ผ๐๐(๐โ) โข (๐ฑโ โ ๐ฒโ))โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข ๐โ)โ ๐๐ ๐ฐโ. # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฒ๐น๐ฎ๐ฏ๐ผ๐ฟ๐ฎ๐๐ถ๐ผ๐ป ๐๐ฒ๐พ๐๐ฒ๐ป๐ฐ๐ฒ # ๐ฎ: ๐ง๐ต๐ฒ ๐ป๐ฎ๐๐๐ฟ๐ฎ๐น ๐ป๐๐บ๐ฏ๐ฒ๐ฟ๐ ## ๐ฎ.๐ญ: ๐ง๐ต๐ฒ ๐ฝ๐ฒ๐ฎ๐ป๐ผ ๐ฎ๐ ๐ถ๐ผ๐บ๐ ### ๐๐ป๐ณ๐ผ๐ฟ๐บ๐ฎ๐น ๐ฑ๐ฒ๐ณ๐ถ๐ป๐ถ๐๐ถ๐ผ๐ป ๐ผ๐ณ ๐ป๐ฎ๐๐๐ฟ๐ฎ๐น ๐ป๐๐บ๐ฏ๐ฒ๐ฟ ### ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ญ ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ญ (๐ฏโ.๐ดโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐โ โ๐ข ๐ช๐ด ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ.โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ### ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฎ ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฎ (๐ฏโ.๐ดโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐โ โ๐๐ง ๐ฏ ๐ช๐ด ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ, ๐ต๐ฉ๐ฆ๐ฏ ๐ฏ++ ๐ช๐ด ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ.โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข ๐โ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): ((0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐ข๐ -๐๐๐๐๐๐ ): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ โน ๐โ), ๐โ โข ๐โ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฎ.๐ฎ.๐ฏ (๐ฏโ.๐โ): ((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐๐ฒ๐ณ๐ถ๐ป๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐ทโ): ๐ซ๐พ๐ ๐๐๐๐๐๐๐ก๐๐๐ ๐โ โ๐๐ฆ ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ ๐ฃ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ข++, ๐ค ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ (๐ข++)++, ๐ฅ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ((๐ข++)++)++,๐ฆ๐ต๐ค. (๐๐ฏ ๐ฐ๐ต๐ฉ๐ฆ๐ณ ๐ธ๐ฐ๐ณ๐ฅ๐ด, ๐ฃ := ๐ข++, ๐ค := ๐ฃ++, ๐ฅ := ๐ค++, ๐ฆ๐ต๐ค. ๐๐ฏ ๐ต๐ฉ๐ช๐ด ๐ต๐ฆ๐น๐ต ๐ ๐ถ๐ด๐ฆ "๐น := ๐บ" ๐ต๐ฐ ๐ฅ๐ฆ๐ฏ๐ฐ๐ต๐ฆ ๐ต๐ฉ๐ฆ ๐ด๐ต๐ข๐ต๐ฆ๐ฎ๐ฆ๐ฏ๐ต ๐ต๐ฉ๐ข๐ต ๐น ๐ช๐ด ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ๐ฅ ๐ต๐ฐ ๐ฆ๐ฒ๐ถ๐ข๐ญ ๐บ.)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ฑ, ๐ฒ โข (๐ฑ = ๐ฒ))โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ ): (1 = (0)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): (2 = ((0)++)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): (3 = (((0)++)++)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): (4 = ((((0)++)++)++)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): (((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ))โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ ): ((0)++ = 1). ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (2 = (1)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((0)++)++ = 2). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (3 = (2)++). ### ๐ฏ ๐ถ๐ ๐ฎ ๐ป๐ฎ๐๐๐ฟ๐ฎ๐น ๐ป๐๐บ๐ฏ๐ฒ๐ฟ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((0)++)++)++ = 3). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((2)++ = 3). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฎ.๐ญ.๐ฐ (๐ฏโ.๐โโ): (3 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (4 = ((((0)++)++)++)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((((0)++)++)++)++ = 4). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((3)++ = 4). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ ): (((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ### ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฏ ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฏ (๐ฏโ.๐ดโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐โ โ๐ข ๐ช๐ด ๐ฏ๐ฐ๐ต ๐ต๐ฉ๐ฆ ๐ด๐ถ๐ค๐ค๐ฆ๐ด๐ด๐ฐ๐ณ ๐ฐ๐ง ๐ข๐ฏ๐บ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ; ๐ช.๐ฆ., ๐ธ๐ฆ ๐ฉ๐ข๐ท๐ฆ ๐ฏ++ โ ๐ข ๐ง๐ฐ๐ณ ๐ฆ๐ท๐ฆ๐ณ๐บ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ฏ.โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ โ 0)). ### ๐ฐ ๐ถ๐ ๐ป๐ผ๐ ๐ฒ๐พ๐๐ฎ๐น ๐๐ผ ๐ฌ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((3 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((3)++ โ 0)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((3)++ โ 0). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฎ.๐ญ.๐ฒ (๐ฏโ.๐โโ): (4 โ 0). ### ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฐ ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฐ (๐ฏโ.๐ดโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐โ โ๐๐ช๐ง๐ง๐ฆ๐ณ๐ฆ๐ฏ๐ต ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ๐ด ๐ฎ๐ถ๐ด๐ต ๐ฉ๐ข๐ท๐ฆ ๐ฅ๐ช๐ง๐ง๐ฆ๐ณ๐ฆ๐ฏ๐ต ๐ด๐ถ๐ค๐ค๐ฆ๐ด๐ด๐ฐ๐ณ๐ด; ๐ช.๐ฆ., ๐ช๐ง ๐ฏ, ๐ฎ ๐ข๐ณ๐ฆ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ๐ด ๐ข๐ฏ๐ฅ ๐ฏ โ ๐ฎ, ๐ต๐ฉ๐ฆ๐ฏ ๐ฏ++ โ ๐ฎ++. ๐๐ฒ๐ถ๐ช๐ท๐ข๐ญ๐ฆ๐ฏ๐ต๐ญ๐บ, ๐ช๐ง ๐ฏ++ = ๐ฎ++, ๐ต๐ฉ๐ฆ๐ฏ ๐ธ๐ฆ ๐ฎ๐ถ๐ด๐ต ๐ฉ๐ข๐ท๐ฆ ๐ฏ = ๐ฎ.โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (๐งโ โ ๐ฆโ)) โน ((๐งโ)++ โ (๐ฆโ)++)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง ((๐งโ)++ = (๐ฆโ)++)) โน (๐งโ = ๐ฆโ)). ### ๐ฒ ๐ถ๐ ๐ป๐ผ๐ ๐ฒ๐พ๐๐ฎ๐น ๐๐ผ ๐ฎ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (4 โ 0)) โน ((4)++ โ (0)++)). ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐๐ข๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐๐ข๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข (๐โ โง ๐โ ))โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ ): (((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (4 โ 0)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4)++ โ (0)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (5 = (((((0)++)++)++)++)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((((0)++)++)++)++)++ = 5). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4)++ = 5). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (5 = (4)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน ((5)++ โ (1)++)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((4)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ ): ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน ((5)++ โ (1)++)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4)++ โ (0)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (5 โ (0)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (6 = ((((((0)++)++)++)++)++)++). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((((((0)++)++)++)++)++)++ = 6). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ โ): (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ โ): ((5)++ = 6). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ โ): (6 = (5)++). #### ๐ฃ๐ฟ๐ผ๐ผ๐ณ ๐ฏ๐ ๐ฐ๐ผ๐ป๐๐ฟ๐ฎ๐ฑ๐ถ๐ฐ๐๐ถ๐ผ๐ป ๐๐๐ฝ๐ผ๐๐ต๐ฒ๐๐ถ๐ (๐ฏโ.๐ปโ): (6 = 2). ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐๐๐ ๐๐ ๐ก๐๐๐๐ฆ-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐-2): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐๐๐ ๐๐ ๐ก๐๐๐๐ฆ-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐-2 ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ = ๐โ), (๐โ โ ๐โ) โข ๐ผ๐๐(๐ฏโ))โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ๐ผ๐๐(โโ). ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐๐-๐๐ฆ-๐๐๐๐ข๐ก๐๐ก๐๐๐-2): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐๐-๐๐ฆ-๐๐๐๐ข๐ก๐๐ก๐๐๐-2 ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ ๐๐๐๐๐ข๐๐๐ก๐ (๐ฑโ = ๐ฒโ)), ๐ผ๐๐(๐โ) โข (๐ฑโ โ ๐ฒโ))โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฎ.๐ญ.๐ด (๐ฏโ.๐โโ): (6 โ 2). #### ๐๐ถ๐ฟ๐ฒ๐ฐ๐ ๐ฝ๐ฟ๐ผ๐ผ๐ณ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((1)++ = 2). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (5 โ 1). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน (6 โ (1)++)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน (6 โ 2)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)). ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (6 โ 2). ### ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฑ: ๐๐ต๐ฒ ๐ฝ๐ฟ๐ถ๐ป๐ฐ๐ถ๐ฝ๐น๐ฒ ๐ผ๐ณ ๐บ๐ฎ๐๐ต๐ฒ๐บ๐ฎ๐๐ถ๐ฐ๐ฎ๐น ๐ถ๐ป๐ฑ๐๐ฐ๐๐ถ๐ผ๐ป ๐๐ ๐ถ๐ผ๐บ ๐๐ฐ๐ต๐ฒ๐บ๐ฎ (๐ฏโ.๐ดโ) - Principle of mathematical induction: ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐โ โ๐๐ฆ๐ต ๐(๐ฏ) ๐ฃ๐ฆ ๐ข๐ฏ๐บ ๐ฑ๐ณ๐ฐ๐ฑ๐ฆ๐ณ๐ต๐บ ๐ฑ๐ฆ๐ณ๐ต๐ข๐ช๐ฏ๐ช๐ฏ๐จ ๐ต๐ฐ ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ฏ. ๐๐ถ๐ฑ๐ฑ๐ฐ๐ด๐ฆ ๐ต๐ฉ๐ข๐ต ๐(๐) ๐ช๐ด ๐ต๐ณ๐ถ๐ฆ, ๐ข๐ฏ๐ฅ ๐ด๐ถ๐ฑ๐ฑ๐ฐ๐ด๐ฆ ๐ต๐ฉ๐ข๐ต ๐ธ๐ฉ๐ฆ๐ฏ๐ฆ๐ท๐ฆ๐ณ ๐(๐ฏ) ๐ช๐ด ๐ต๐ณ๐ถ๐ฆ, ๐(๐ฏ++) ๐ช๐ด ๐ข๐ญ๐ด๐ฐ ๐ต๐ณ๐ถ๐ฆ. ๐๐ฉ๐ฆ๐ฏ ๐(๐ฏ) ๐ช๐ด ๐ต๐ณ๐ถ๐ฆ ๐ง๐ฐ๐ณ ๐ฆ๐ท๐ฆ๐ณ๐บ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ฏ.โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ ): (((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐โโ(0) โง (๐โโ(๐งโ ) โน ๐โโ((๐งโ )++)))) โน ((๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ๐โโ(๐ฆโ))). ### ๐ง๐ต๐ฒ ๐ป๐๐บ๐ฏ๐ฒ๐ฟ ๐๐๐๐๐ฒ๐บ ๐ป ### ๐ฅ๐ฒ๐ฐ๐๐ฟ๐๐ถ๐๐ฒ ๐ฑ๐ฒ๐ณ๐ถ๐ป๐ถ๐๐ถ๐ผ๐ป๐
The report content.
๐๐๐พ ๐ฏ๐พ๐บ๐๐ ๐บ๐๐๐๐๐ # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฝ๐ฟ๐ผ๐ฝ๐ฒ๐ฟ๐๐ถ๐ฒ๐ ๐๐ผ๐ป๐๐ถ๐๐๐ฒ๐ป๐ฐ๐: undetermined ๐ฆ๐๐ฎ๐ฏ๐ถ๐น๐ถ๐๐ฒ๐ฑ: False ๐๐ ๐๐ฒ๐ป๐ฑ๐ฒ๐ฑ ๐๐ต๐ฒ๐ผ๐ฟ๐: N/A # ๐ฆ๐ถ๐บ๐ฝ๐น๐ฒ-๐ผ๐ฏ๐ท๐ฒ๐ฐ๐๐ ๐ฑ๐ฒ๐ฐ๐น๐ฎ๐ฟ๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ โ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐โ, โ0โ, โ1โ, โ2โ, โ3โ, โ4โ, โ5โ, โ6โ ๐ป๐พ ๐ ๐๐๐๐๐-๐๐๐๐๐๐ก๐ ๐๐ ๐ฐโ. # ๐ฅ๐ฒ๐น๐ฎ๐๐ถ๐ผ๐ป๐ ๐ซ๐พ๐ โ++โ, โ๐ผ๐๐โ ๐ป๐พ ๐ข๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐๐ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โโนโ, โโ โ, โโงโ, โ๐๐ -๐โ, โ=โ ๐ป๐พ ๐๐๐๐๐๐ฆ-๐๐๐๐๐ก๐๐๐๐ ๐๐ ๐ฐโ. # ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ๐ ๐ณ๐๐พ ๐ฟ๐๐ ๐ ๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ๐ ๐บ๐๐พ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐๐ฝ๐พ๐ ๐๐๐๐ ๐๐๐พ๐๐๐: ๐ซ๐พ๐ โ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐๐ข๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข (๐โ โง ๐โ ))โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ฑ, ๐ฒ โข (๐ฑ = ๐ฒ))โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ)โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆโ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ))โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐๐๐ ๐๐ ๐ก๐๐๐๐ฆ-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐-2โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ = ๐โ), (๐โ โ ๐โ) โข ๐ผ๐๐(๐ฏโ))โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐ข๐ -๐๐๐๐๐๐ โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ โน ๐โ), ๐โ โข ๐โ)โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐๐๐๐๐-๐๐ฆ-๐๐๐๐ข๐ก๐๐ก๐๐๐-2โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ ๐๐๐๐๐ข๐๐๐ก๐ (๐ฑโ = ๐ฒโ)), ๐ผ๐๐(๐โ) โข (๐ฑโ โ ๐ฒโ))โ ๐๐ ๐ฐโ. ๐ซ๐พ๐ โ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐โ ๐ป๐พ ๐บ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข ๐โ)โ ๐๐ ๐ฐโ. # ๐ง๐ต๐ฒ๐ผ๐ฟ๐ ๐ฒ๐น๐ฎ๐ฏ๐ผ๐ฟ๐ฎ๐๐ถ๐ผ๐ป ๐๐ฒ๐พ๐๐ฒ๐ป๐ฐ๐ฒ # ๐ฎ: ๐ง๐ต๐ฒ ๐ป๐ฎ๐๐๐ฟ๐ฎ๐น ๐ป๐๐บ๐ฏ๐ฒ๐ฟ๐ ## ๐ฎ.๐ญ: ๐ง๐ต๐ฒ ๐ฝ๐ฒ๐ฎ๐ป๐ผ ๐ฎ๐ ๐ถ๐ผ๐บ๐ ### ๐๐ป๐ณ๐ผ๐ฟ๐บ๐ฎ๐น ๐ฑ๐ฒ๐ณ๐ถ๐ป๐ถ๐๐ถ๐ผ๐ป ๐ผ๐ณ ๐ป๐ฎ๐๐๐ฟ๐ฎ๐น ๐ป๐๐บ๐ฏ๐ฒ๐ฟ ### ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ญ ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ญ (๐ฏโ.๐ดโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐โ โ๐ข ๐ช๐ด ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ.โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ โข ๐)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐ข ๐ช๐ด ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ.โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฎ.๐ญ (๐ดโ). (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). โ ### ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฎ ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฎ (๐ฏโ.๐ดโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐โ โ๐๐ง ๐ฏ ๐ช๐ด ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ, ๐ต๐ฉ๐ฆ๐ฏ ๐ฏ++ ๐ช๐ด ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ.โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐๐ง ๐ฏ ๐ช๐ด ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ, ๐ต๐ฉ๐ฆ๐ฏ ๐ฏ++ ๐ช๐ด ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ.โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฎ (๐ดโ). ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). โ ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข ๐โ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): ((0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ซ๐พ๐ ๐งโ = 0. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). โ ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐ข๐ -๐๐๐๐๐๐ ): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ โน ๐โ), ๐โ โข ๐โ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฎ.๐ฎ.๐ฏ (๐ฏโ.๐โ): ((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ).(0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). โ ๐๐ฒ๐ณ๐ถ๐ป๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐ทโ): ๐ซ๐พ๐ ๐๐๐๐๐๐๐ก๐๐๐ ๐โ โ๐๐ฆ ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ ๐ฃ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ข++, ๐ค ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ (๐ข++)++, ๐ฅ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ((๐ข++)++)++,๐ฆ๐ต๐ค. (๐๐ฏ ๐ฐ๐ต๐ฉ๐ฆ๐ณ ๐ธ๐ฐ๐ณ๐ฅ๐ด, ๐ฃ := ๐ข++, ๐ค := ๐ฃ++, ๐ฅ := ๐ค++, ๐ฆ๐ต๐ค. ๐๐ฏ ๐ต๐ฉ๐ช๐ด ๐ต๐ฆ๐น๐ต ๐ ๐ถ๐ด๐ฆ "๐น := ๐บ" ๐ต๐ฐ ๐ฅ๐ฆ๐ฏ๐ฐ๐ต๐ฆ ๐ต๐ฉ๐ฆ ๐ด๐ต๐ข๐ต๐ฆ๐ฎ๐ฆ๐ฏ๐ต ๐ต๐ฉ๐ข๐ต ๐น ๐ช๐ด ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ๐ฅ ๐ต๐ฐ ๐ฆ๐ฒ๐ถ๐ข๐ญ ๐บ.)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐, ๐ฑ, ๐ฒ โข (๐ฑ = ๐ฒ))โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ ): (1 = (0)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐๐ฆ ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ ๐ฃ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ข++, ๐ค ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ (๐ข++)++, ๐ฅ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ((๐ข++)++)++,๐ฆ๐ต๐ค. (๐๐ฏ ๐ฐ๐ต๐ฉ๐ฆ๐ณ ๐ธ๐ฐ๐ณ๐ฅ๐ด, ๐ฃ := ๐ข++, ๐ค := ๐ฃ++, ๐ฅ := ๐ค++, ๐ฆ๐ต๐ค. ๐๐ฏ ๐ต๐ฉ๐ช๐ด ๐ต๐ฆ๐น๐ต ๐ ๐ถ๐ด๐ฆ "๐น := ๐บ" ๐ต๐ฐ ๐ฅ๐ฆ๐ฏ๐ฐ๐ต๐ฆ ๐ต๐ฉ๐ฆ ๐ด๐ต๐ข๐ต๐ฆ๐ฎ๐ฆ๐ฏ๐ต ๐ต๐ฉ๐ข๐ต ๐น ๐ช๐ด ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ๐ฅ ๐ต๐ฐ ๐ฆ๐ฒ๐ถ๐ข๐ญ ๐บ.)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฑ๐ฒ๐ณ. (๐ทโ). 1 ๐๐ ๐บ๐ ๐๐๐๐พ๐๐๐๐พ๐๐บ๐๐๐๐ ๐๐ฟ ๐๐๐บ๐ ๐ฝ๐พ๐ฟ๐๐๐๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ฑ, ๐ฒ โข (๐ฑ = ๐ฒ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (1 = (0)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): (2 = ((0)++)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐๐ฆ ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ ๐ฃ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ข++, ๐ค ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ (๐ข++)++, ๐ฅ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ((๐ข++)++)++,๐ฆ๐ต๐ค. (๐๐ฏ ๐ฐ๐ต๐ฉ๐ฆ๐ณ ๐ธ๐ฐ๐ณ๐ฅ๐ด, ๐ฃ := ๐ข++, ๐ค := ๐ฃ++, ๐ฅ := ๐ค++, ๐ฆ๐ต๐ค. ๐๐ฏ ๐ต๐ฉ๐ช๐ด ๐ต๐ฆ๐น๐ต ๐ ๐ถ๐ด๐ฆ "๐น := ๐บ" ๐ต๐ฐ ๐ฅ๐ฆ๐ฏ๐ฐ๐ต๐ฆ ๐ต๐ฉ๐ฆ ๐ด๐ต๐ข๐ต๐ฆ๐ฎ๐ฆ๐ฏ๐ต ๐ต๐ฉ๐ข๐ต ๐น ๐ช๐ด ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ๐ฅ ๐ต๐ฐ ๐ฆ๐ฒ๐ถ๐ข๐ญ ๐บ.)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฑ๐ฒ๐ณ. (๐ทโ). 2 ๐๐ ๐บ๐ ๐๐๐๐พ๐๐๐๐พ๐๐บ๐๐๐๐ ๐๐ฟ ๐๐๐บ๐ ๐ฝ๐พ๐ฟ๐๐๐๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ฑ, ๐ฒ โข (๐ฑ = ๐ฒ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (2 = ((0)++)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): (3 = (((0)++)++)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐๐ฆ ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ ๐ฃ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ข++, ๐ค ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ (๐ข++)++, ๐ฅ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ((๐ข++)++)++,๐ฆ๐ต๐ค. (๐๐ฏ ๐ฐ๐ต๐ฉ๐ฆ๐ณ ๐ธ๐ฐ๐ณ๐ฅ๐ด, ๐ฃ := ๐ข++, ๐ค := ๐ฃ++, ๐ฅ := ๐ค++, ๐ฆ๐ต๐ค. ๐๐ฏ ๐ต๐ฉ๐ช๐ด ๐ต๐ฆ๐น๐ต ๐ ๐ถ๐ด๐ฆ "๐น := ๐บ" ๐ต๐ฐ ๐ฅ๐ฆ๐ฏ๐ฐ๐ต๐ฆ ๐ต๐ฉ๐ฆ ๐ด๐ต๐ข๐ต๐ฆ๐ฎ๐ฆ๐ฏ๐ต ๐ต๐ฉ๐ข๐ต ๐น ๐ช๐ด ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ๐ฅ ๐ต๐ฐ ๐ฆ๐ฒ๐ถ๐ข๐ญ ๐บ.)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฑ๐ฒ๐ณ. (๐ทโ). 3 ๐๐ ๐บ๐ ๐๐๐๐พ๐๐๐๐พ๐๐บ๐๐๐๐ ๐๐ฟ ๐๐๐บ๐ ๐ฝ๐พ๐ฟ๐๐๐๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ฑ, ๐ฒ โข (๐ฑ = ๐ฒ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (3 = (((0)++)++)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): (4 = ((((0)++)++)++)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐๐ฆ ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ ๐ฃ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ข++, ๐ค ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ (๐ข++)++, ๐ฅ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ((๐ข++)++)++,๐ฆ๐ต๐ค. (๐๐ฏ ๐ฐ๐ต๐ฉ๐ฆ๐ณ ๐ธ๐ฐ๐ณ๐ฅ๐ด, ๐ฃ := ๐ข++, ๐ค := ๐ฃ++, ๐ฅ := ๐ค++, ๐ฆ๐ต๐ค. ๐๐ฏ ๐ต๐ฉ๐ช๐ด ๐ต๐ฆ๐น๐ต ๐ ๐ถ๐ด๐ฆ "๐น := ๐บ" ๐ต๐ฐ ๐ฅ๐ฆ๐ฏ๐ฐ๐ต๐ฆ ๐ต๐ฉ๐ฆ ๐ด๐ต๐ข๐ต๐ฆ๐ฎ๐ฆ๐ฏ๐ต ๐ต๐ฉ๐ข๐ต ๐น ๐ช๐ด ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ๐ฅ ๐ต๐ฐ ๐ฆ๐ฒ๐ถ๐ข๐ญ ๐บ.)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฑ๐ฒ๐ณ. (๐ทโ). 4 ๐๐ ๐บ๐ ๐๐๐๐พ๐๐๐๐พ๐๐บ๐๐๐๐ ๐๐ฟ ๐๐๐บ๐ ๐ฝ๐พ๐ฟ๐๐๐๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ฑ, ๐ฒ โข (๐ฑ = ๐ฒ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (4 = ((((0)++)++)++)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ): (((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ซ๐พ๐ ๐งโ = (0)++. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ).((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ฎ.๐ฎ.๐ฏ (๐โ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ซ๐พ๐ ๐งโ = ((0)++)++. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ).(((0)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ซ๐พ๐ ๐งโ = (((0)++)++)++. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ).((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). โ ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ))โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ ): ((0)++ = 1). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (1 = (0)++) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((0)++ = 1). โ ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ)โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (2 = (1)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (2 = ((0)++)++) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ((0)++ = 1) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (2 = (1)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((0)++)++ = 2). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (2 = ((0)++)++) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((0)++)++ = 2). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (3 = (2)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (3 = (((0)++)++)++) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). (((0)++)++ = 2) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (3 = (2)++). โ ### ๐ฏ ๐ถ๐ ๐ฎ ๐ป๐ฎ๐๐๐ฟ๐ฎ๐น ๐ป๐๐บ๐ฏ๐ฒ๐ฟ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((0)++)++)++ = 3). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (3 = (((0)++)++)++) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((0)++)++)++ = 3). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((2)++ = 3). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((0)++)++)++ = 3) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). (((0)++)++ = 2) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((2)++ = 3). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฎ.๐ญ.๐ฐ (๐ฏโ.๐โโ): (3 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ((((0)++)++)++ = 3) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (3 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (4 = ((((0)++)++)++)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐๐ฆ ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ ๐ฃ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ข++, ๐ค ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ (๐ข++)++, ๐ฅ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ((๐ข++)++)++,๐ฆ๐ต๐ค. (๐๐ฏ ๐ฐ๐ต๐ฉ๐ฆ๐ณ ๐ธ๐ฐ๐ณ๐ฅ๐ด, ๐ฃ := ๐ข++, ๐ค := ๐ฃ++, ๐ฅ := ๐ค++, ๐ฆ๐ต๐ค. ๐๐ฏ ๐ต๐ฉ๐ช๐ด ๐ต๐ฆ๐น๐ต ๐ ๐ถ๐ด๐ฆ "๐น := ๐บ" ๐ต๐ฐ ๐ฅ๐ฆ๐ฏ๐ฐ๐ต๐ฆ ๐ต๐ฉ๐ฆ ๐ด๐ต๐ข๐ต๐ฆ๐ฎ๐ฆ๐ฏ๐ต ๐ต๐ฉ๐ข๐ต ๐น ๐ช๐ด ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ๐ฅ ๐ต๐ฐ ๐ฆ๐ฒ๐ถ๐ข๐ญ ๐บ.)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฑ๐ฒ๐ณ. (๐ทโ). 4 ๐๐ ๐บ๐ ๐๐๐๐พ๐๐๐๐พ๐๐บ๐๐๐๐ ๐๐ฟ ๐๐๐บ๐ ๐ฝ๐พ๐ฟ๐๐๐๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ฑ, ๐ฒ โข (๐ฑ = ๐ฒ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (4 = ((((0)++)++)++)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((((0)++)++)++)++ = 4). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (4 = ((((0)++)++)++)++) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((((0)++)++)++)++ = 4). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((3)++ = 4). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (((((0)++)++)++)++ = 4) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ((((0)++)++)++ = 3) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((3)++ = 4). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ ): (((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ((3)++ = 4) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((((0)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (((((0)++)++)++)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). (((((0)++)++)++)++ = 4) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). โ ### ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฏ ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฏ (๐ฏโ.๐ดโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐โ โ๐ข ๐ช๐ด ๐ฏ๐ฐ๐ต ๐ต๐ฉ๐ฆ ๐ด๐ถ๐ค๐ค๐ฆ๐ด๐ด๐ฐ๐ณ ๐ฐ๐ง ๐ข๐ฏ๐บ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ; ๐ช.๐ฆ., ๐ธ๐ฆ ๐ฉ๐ข๐ท๐ฆ ๐ฏ++ โ ๐ข ๐ง๐ฐ๐ณ ๐ฆ๐ท๐ฆ๐ณ๐บ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ฏ.โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ โ 0)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐ข ๐ช๐ด ๐ฏ๐ฐ๐ต ๐ต๐ฉ๐ฆ ๐ด๐ถ๐ค๐ค๐ฆ๐ด๐ด๐ฐ๐ณ ๐ฐ๐ง ๐ข๐ฏ๐บ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ; ๐ช.๐ฆ., ๐ธ๐ฆ ๐ฉ๐ข๐ท๐ฆ ๐ฏ++ โ ๐ข ๐ง๐ฐ๐ณ ๐ฆ๐ท๐ฆ๐ณ๐บ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ฏ.โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฏ (๐ดโ). ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ โ 0)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ โ 0)). โ ### ๐ฐ ๐ถ๐ ๐ป๐ผ๐ ๐ฒ๐พ๐๐ฎ๐น ๐๐ผ ๐ฌ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((3 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((3)++ โ 0)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ โ 0)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ซ๐พ๐ ๐งโ = 3. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((3 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((3)++ โ 0)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((3)++ โ 0). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((3 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((3)++ โ 0)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ).(3 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ฎ.๐ญ.๐ฐ (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((3)++ โ 0). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฎ.๐ญ.๐ฒ (๐ฏโ.๐โโ): (4 โ 0). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((3)++ โ 0) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ((3)++ = 4) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (4 โ 0). โ ### ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฐ ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฐ (๐ฏโ.๐ดโ): ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐โ โ๐๐ช๐ง๐ง๐ฆ๐ณ๐ฆ๐ฏ๐ต ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ๐ด ๐ฎ๐ถ๐ด๐ต ๐ฉ๐ข๐ท๐ฆ ๐ฅ๐ช๐ง๐ง๐ฆ๐ณ๐ฆ๐ฏ๐ต ๐ด๐ถ๐ค๐ค๐ฆ๐ด๐ด๐ฐ๐ณ๐ด; ๐ช.๐ฆ., ๐ช๐ง ๐ฏ, ๐ฎ ๐ข๐ณ๐ฆ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ๐ด ๐ข๐ฏ๐ฅ ๐ฏ โ ๐ฎ, ๐ต๐ฉ๐ฆ๐ฏ ๐ฏ++ โ ๐ฎ++. ๐๐ฒ๐ถ๐ช๐ท๐ข๐ญ๐ฆ๐ฏ๐ต๐ญ๐บ, ๐ช๐ง ๐ฏ++ = ๐ฎ++, ๐ต๐ฉ๐ฆ๐ฏ ๐ธ๐ฆ ๐ฎ๐ถ๐ด๐ต ๐ฉ๐ข๐ท๐ฆ ๐ฏ = ๐ฎ.โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (๐งโ โ ๐ฆโ)) โน ((๐งโ)++ โ (๐ฆโ)++)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐๐ช๐ง๐ง๐ฆ๐ณ๐ฆ๐ฏ๐ต ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ๐ด ๐ฎ๐ถ๐ด๐ต ๐ฉ๐ข๐ท๐ฆ ๐ฅ๐ช๐ง๐ง๐ฆ๐ณ๐ฆ๐ฏ๐ต ๐ด๐ถ๐ค๐ค๐ฆ๐ด๐ด๐ฐ๐ณ๐ด; ๐ช.๐ฆ., ๐ช๐ง ๐ฏ, ๐ฎ ๐ข๐ณ๐ฆ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ๐ด ๐ข๐ฏ๐ฅ ๐ฏ โ ๐ฎ, ๐ต๐ฉ๐ฆ๐ฏ ๐ฏ++ โ ๐ฎ++. ๐๐ฒ๐ถ๐ช๐ท๐ข๐ญ๐ฆ๐ฏ๐ต๐ญ๐บ, ๐ช๐ง ๐ฏ++ = ๐ฎ++, ๐ต๐ฉ๐ฆ๐ฏ ๐ธ๐ฆ ๐ฎ๐ถ๐ด๐ต ๐ฉ๐ข๐ท๐ฆ ๐ฏ = ๐ฎ.โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฐ (๐ดโ). ((((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (๐งโ โ ๐ฆโ)) โน ((๐งโ)++ โ (๐ฆโ)++)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (๐งโ โ ๐ฆโ)) โน ((๐งโ)++ โ (๐ฆโ)++)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง ((๐งโ)++ = (๐ฆโ)++)) โน (๐งโ = ๐ฆโ)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐๐ช๐ง๐ง๐ฆ๐ณ๐ฆ๐ฏ๐ต ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ๐ด ๐ฎ๐ถ๐ด๐ต ๐ฉ๐ข๐ท๐ฆ ๐ฅ๐ช๐ง๐ง๐ฆ๐ณ๐ฆ๐ฏ๐ต ๐ด๐ถ๐ค๐ค๐ฆ๐ด๐ด๐ฐ๐ณ๐ด; ๐ช.๐ฆ., ๐ช๐ง ๐ฏ, ๐ฎ ๐ข๐ณ๐ฆ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ๐ด ๐ข๐ฏ๐ฅ ๐ฏ โ ๐ฎ, ๐ต๐ฉ๐ฆ๐ฏ ๐ฏ++ โ ๐ฎ++. ๐๐ฒ๐ถ๐ช๐ท๐ข๐ญ๐ฆ๐ฏ๐ต๐ญ๐บ, ๐ช๐ง ๐ฏ++ = ๐ฎ++, ๐ต๐ฉ๐ฆ๐ฏ ๐ธ๐ฆ ๐ฎ๐ถ๐ด๐ต ๐ฉ๐ข๐ท๐ฆ ๐ฏ = ๐ฎ.โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฐ (๐ดโ). ((((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง ((๐งโ)++ = (๐ฆโ)++)) โน (๐งโ = ๐ฆโ)) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง ((๐งโ)++ = (๐ฆโ)++)) โน (๐งโ = ๐ฆโ)). โ ### ๐ฒ ๐ถ๐ ๐ป๐ผ๐ ๐ฒ๐พ๐๐ฎ๐น ๐๐ผ ๐ฎ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (4 โ 0)) โน ((4)++ โ (0)++)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (๐งโ โ ๐ฆโ)) โน ((๐งโ)++ โ (๐ฆโ)++)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ซ๐พ๐ ๐งโ = 4, ๐ฆโ = 0. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (4 โ 0)) โน ((4)++ โ (0)++)). โ ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐๐ข๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐๐ข๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐ ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ(๐โ, ๐โ โข (๐โ โง ๐โ ))โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐), ๐๐ฟ ๐๐๐พ ๐ฟ๐๐๐ ๐โ, ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐), ๐๐ฟ ๐๐๐พ ๐ฟ๐๐๐ ๐โ , ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐ข๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข (๐โ โง ๐โ )), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ ): (((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (4 โ 0)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)), ๐๐ฟ ๐๐๐พ ๐ฟ๐๐๐ ๐โ, ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). (4 โ 0), ๐๐ฟ ๐๐๐พ ๐ฟ๐๐๐ ๐โ , ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ฎ.๐ญ.๐ฒ (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐ข๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข (๐โ โง ๐โ )), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (4 โ 0)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4)++ โ (0)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (4 โ 0)) โน ((4)++ โ (0)++)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ).(((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (4 โ 0)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((4)++ โ (0)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (5 = (((((0)++)++)++)++)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐๐ฆ ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ ๐ฃ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ข++, ๐ค ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ (๐ข++)++, ๐ฅ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ((๐ข++)++)++,๐ฆ๐ต๐ค. (๐๐ฏ ๐ฐ๐ต๐ฉ๐ฆ๐ณ ๐ธ๐ฐ๐ณ๐ฅ๐ด, ๐ฃ := ๐ข++, ๐ค := ๐ฃ++, ๐ฅ := ๐ค++, ๐ฆ๐ต๐ค. ๐๐ฏ ๐ต๐ฉ๐ช๐ด ๐ต๐ฆ๐น๐ต ๐ ๐ถ๐ด๐ฆ "๐น := ๐บ" ๐ต๐ฐ ๐ฅ๐ฆ๐ฏ๐ฐ๐ต๐ฆ ๐ต๐ฉ๐ฆ ๐ด๐ต๐ข๐ต๐ฆ๐ฎ๐ฆ๐ฏ๐ต ๐ต๐ฉ๐ข๐ต ๐น ๐ช๐ด ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ๐ฅ ๐ต๐ฐ ๐ฆ๐ฒ๐ถ๐ข๐ญ ๐บ.)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฑ๐ฒ๐ณ. (๐ทโ). 5 ๐๐ ๐บ๐ ๐๐๐๐พ๐๐๐๐พ๐๐บ๐๐๐๐ ๐๐ฟ ๐๐๐บ๐ ๐ฝ๐พ๐ฟ๐๐๐๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ฑ, ๐ฒ โข (๐ฑ = ๐ฒ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (5 = (((((0)++)++)++)++)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((((0)++)++)++)++)++ = 5). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (5 = (((((0)++)++)++)++)++) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((((0)++)++)++)++)++ = 5). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4)++ = 5). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((((0)++)++)++)++)++ = 5) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). (((((0)++)++)++)++ = 4) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((4)++ = 5). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (5 = (4)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((4)++ = 5) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (5 = (4)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน ((5)++ โ (1)++)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (๐งโ โ ๐ฆโ)) โน ((๐งโ)++ โ (๐ฆโ)++)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ซ๐พ๐ ๐งโ = 5, ๐ฆโ = 1. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน ((5)++ โ (1)++)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((4)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((๐งโ)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ). ๐ซ๐พ๐ ๐งโ = 4. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((4)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ((4)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ((4)++ = 5) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน (5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ).(4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ ): ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน ((5)++ โ (1)++)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (๐งโ โ ๐ฆโ)) โน ((๐งโ)++ โ (๐ฆโ)++)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ซ๐พ๐ ๐งโ = 5, ๐ฆโ = 1. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐ฃ๐๐๐๐๐๐๐-๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน ((5)++ โ (1)++)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((4)++ โ (0)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (4 โ 0)) โน ((4)++ โ (0)++)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ).(((4 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (0 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (4 โ 0)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((4)++ โ (0)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (5 โ (0)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((4)++ โ (0)++) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ((4)++ = 5) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (5 โ (0)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (6 = ((((((0)++)++)++)++)++)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐๐ฆ ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ ๐ฃ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ข++, ๐ค ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ (๐ข++)++, ๐ฅ ๐ต๐ฐ ๐ฃ๐ฆ ๐ต๐ฉ๐ฆ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ((๐ข++)++)++,๐ฆ๐ต๐ค. (๐๐ฏ ๐ฐ๐ต๐ฉ๐ฆ๐ณ ๐ธ๐ฐ๐ณ๐ฅ๐ด, ๐ฃ := ๐ข++, ๐ค := ๐ฃ++, ๐ฅ := ๐ค++, ๐ฆ๐ต๐ค. ๐๐ฏ ๐ต๐ฉ๐ช๐ด ๐ต๐ฆ๐น๐ต ๐ ๐ถ๐ด๐ฆ "๐น := ๐บ" ๐ต๐ฐ ๐ฅ๐ฆ๐ฏ๐ฐ๐ต๐ฆ ๐ต๐ฉ๐ฆ ๐ด๐ต๐ข๐ต๐ฆ๐ฎ๐ฆ๐ฏ๐ต ๐ต๐ฉ๐ข๐ต ๐น ๐ช๐ด ๐ฅ๐ฆ๐ง๐ช๐ฏ๐ฆ๐ฅ ๐ต๐ฐ ๐ฆ๐ฒ๐ถ๐ข๐ญ ๐บ.)โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฑ๐ฒ๐ณ. (๐ทโ). 6 ๐๐ ๐บ๐ ๐๐๐๐พ๐๐๐๐พ๐๐บ๐๐๐๐ ๐๐ฟ ๐๐๐บ๐ ๐ฝ๐พ๐ฟ๐๐๐๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ฑ, ๐ฒ โข (๐ฑ = ๐ฒ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (6 = ((((((0)++)++)++)++)++)++). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((((((0)++)++)++)++)++)++ = 6). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (6 = ((((((0)++)++)++)++)++)++) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((((((0)++)++)++)++)++)++ = 6). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ โ): (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((0)++ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ฎ.๐ฎ.๐ฏ (๐โ). ((0)++ = 1) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ โ): ((5)++ = 6). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (((((((0)++)++)++)++)++)++ = 6) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ((((((0)++)++)++)++)++ = 5) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((5)++ = 6). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โ โ): (6 = (5)++). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((5)++ = 6) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ โ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐๐๐ก๐ฆ-๐๐๐๐๐ข๐ก๐๐ก๐๐ฃ๐๐ก๐ฆ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐ฑโ = ๐ฒโ) โข (๐ฒโ = ๐ฑโ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (6 = (5)++). โ #### ๐ฃ๐ฟ๐ผ๐ผ๐ณ ๐ฏ๐ ๐ฐ๐ผ๐ป๐๐ฟ๐ฎ๐ฑ๐ถ๐ฐ๐๐ถ๐ผ๐ป ๐๐๐ฝ๐ผ๐๐ต๐ฒ๐๐ถ๐ (๐ฏโ.๐ปโ): (6 = 2). ๐ณ๐๐๐ ๐๐๐๐๐๐๐พ๐๐๐ ๐๐ ๐พ๐ ๐บ๐ป๐๐๐บ๐๐พ๐ฝ ๐๐ ๐๐๐พ๐๐๐ โโ. ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐๐๐ ๐๐ ๐ก๐๐๐๐ฆ-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐-2): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐๐๐ ๐๐ ๐ก๐๐๐๐ฆ-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐-2 ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ = ๐โ), (๐โ โ ๐โ) โข ๐ผ๐๐(๐ฏโ))โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ๐ผ๐๐(โโ). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ๐ซ๐พ๐ (๐ท = ๐ธ) := (4 = 0) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ ). ๐ซ๐พ๐ (๐ท โ ๐ธ) := (4 โ 0) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. ๐ฎ.๐ญ.๐ฒ (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐๐ ๐๐ ๐ก๐๐๐๐ฆ-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐-2 ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ = ๐โ), (๐โ โ ๐โ) โข ๐ผ๐๐(๐ฏโ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ๐ผ๐๐(โโ). โ ๐๐ป๐ณ๐ฒ๐ฟ๐ฒ๐ป๐ฐ๐ฒ ๐ฟ๐๐น๐ฒ (๐๐๐๐๐-๐๐ฆ-๐๐๐๐ข๐ก๐๐ก๐๐๐-2): ๐ซ๐พ๐ ๐๐๐๐๐๐๐๐๐-๐๐ข๐๐ ๐๐๐๐๐-๐๐ฆ-๐๐๐๐ข๐ก๐๐ก๐๐๐-2 ๐ฝ๐พ๐ฟ๐๐๐พ๐ฝ ๐บ๐ โ((๐โ ๐๐๐๐๐ข๐๐๐ก๐ (๐ฑโ = ๐ฒโ)), ๐ผ๐๐(๐โ) โข (๐ฑโ โ ๐ฒโ))โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ ๐บ๐๐ฝ ๐ผ๐๐๐๐๐ฝ๐พ๐๐พ๐ฝ ๐๐บ๐ ๐๐ฝ ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป ๐ฎ.๐ญ.๐ด (๐ฏโ.๐โโ): (6 โ 2). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ๐ซ๐พ๐ ๐ต๐๐ฝ. (๐ปโ) ๐ป๐พ ๐๐๐พ ๐๐๐๐๐๐๐พ๐๐๐ (6 = 2). ๐ผ๐๐(โโ) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐-๐๐ฆ-๐๐๐๐ข๐ก๐๐ก๐๐๐-2 ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ ๐๐๐๐๐ข๐๐๐ก๐ (๐ฑโ = ๐ฒโ)), ๐ผ๐๐(๐โ) โข (๐ฑโ โ ๐ฒโ)), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (6 โ 2). โ #### ๐๐ถ๐ฟ๐ฒ๐ฐ๐ ๐ฝ๐ฟ๐ผ๐ผ๐ณ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((1)++ = 2). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (((0)++)++ = 2) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ((0)++ = 1) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((1)++ = 2). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (5 โ 1). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (5 โ (0)++) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ((0)++ = 1) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (5 โ 1). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน (6 โ (1)++)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน ((5)++ โ (1)++)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ ). ((5)++ = 6) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ โ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน (6 โ (1)++)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน (6 โ 2)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน (6 โ (1)++)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ((1)++ = 2) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐ข๐๐-๐ก๐๐๐๐ -๐ ๐ข๐๐ ๐ก๐๐ก๐ข๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, (๐ฑโ = ๐ฒโ) โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน (6 โ 2)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): ((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: (5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐), ๐๐ฟ ๐๐๐พ ๐ฟ๐๐๐ ๐โ, ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐), ๐๐ฟ ๐๐๐พ ๐ฟ๐๐๐ ๐โ , ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โ โ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐ข๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข (๐โ โง ๐โ )), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ ((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)), ๐๐ฟ ๐๐๐พ ๐ฟ๐๐๐ ๐โ, ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). (5 โ 1), ๐๐ฟ ๐๐๐พ ๐ฟ๐๐๐ ๐โ , ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐๐ข๐๐๐ก๐๐๐-๐๐๐ก๐๐๐๐ข๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐โ, ๐โ โข (๐โ โง ๐โ )), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)). โ ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ): (6 โ 2). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: ((((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) โน (6 โ 2)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ).(((5 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (1 ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐)) โง (5 โ 1)) ๐ฟ๐๐ ๐ ๐๐๐ ๐ฟ๐๐๐ ๐ฝ๐ฟ๐ผ๐ฝ. (๐โโ). ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐๐๐ข๐ -๐๐๐๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: ((๐โ โน ๐โ), ๐โ โข ๐โ), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (6 โ 2). โ ### ๐๐ ๐ถ๐ผ๐บ ๐ฎ.๐ฑ: ๐๐ต๐ฒ ๐ฝ๐ฟ๐ถ๐ป๐ฐ๐ถ๐ฝ๐น๐ฒ ๐ผ๐ณ ๐บ๐ฎ๐๐ต๐ฒ๐บ๐ฎ๐๐ถ๐ฐ๐ฎ๐น ๐ถ๐ป๐ฑ๐๐ฐ๐๐ถ๐ผ๐ป ๐๐ ๐ถ๐ผ๐บ ๐๐ฐ๐ต๐ฒ๐บ๐ฎ (๐ฏโ.๐ดโ) - Principle of mathematical induction: ๐ซ๐พ๐ ๐๐ฅ๐๐๐ ๐โ โ๐๐ฆ๐ต ๐(๐ฏ) ๐ฃ๐ฆ ๐ข๐ฏ๐บ ๐ฑ๐ณ๐ฐ๐ฑ๐ฆ๐ณ๐ต๐บ ๐ฑ๐ฆ๐ณ๐ต๐ข๐ช๐ฏ๐ช๐ฏ๐จ ๐ต๐ฐ ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ฏ. ๐๐ถ๐ฑ๐ฑ๐ฐ๐ด๐ฆ ๐ต๐ฉ๐ข๐ต ๐(๐) ๐ช๐ด ๐ต๐ณ๐ถ๐ฆ, ๐ข๐ฏ๐ฅ ๐ด๐ถ๐ฑ๐ฑ๐ฐ๐ด๐ฆ ๐ต๐ฉ๐ข๐ต ๐ธ๐ฉ๐ฆ๐ฏ๐ฆ๐ท๐ฆ๐ณ ๐(๐ฏ) ๐ช๐ด ๐ต๐ณ๐ถ๐ฆ, ๐(๐ฏ++) ๐ช๐ด ๐ข๐ญ๐ด๐ฐ ๐ต๐ณ๐ถ๐ฆ. ๐๐ฉ๐ฆ๐ฏ ๐(๐ฏ) ๐ช๐ด ๐ต๐ณ๐ถ๐ฆ ๐ง๐ฐ๐ณ ๐ฆ๐ท๐ฆ๐ณ๐บ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ฏ.โ ๐ป๐พ ๐๐๐ผ๐ ๐๐ฝ๐พ๐ฝ (๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ) ๐๐ ๐ฏโ. ๐ฃ๐ฟ๐ผ๐ฝ๐ผ๐๐ถ๐๐ถ๐ผ๐ป (๐ฏโ.๐โโ ): (((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐โโ(0) โง (๐โโ(๐งโ ) โน ๐โโ((๐งโ )++)))) โน ((๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ๐โโ(๐ฆโ))). ๐ฃ๐ฟ๐ผ๐ผ๐ณ: โ๐๐ฆ๐ต ๐(๐ฏ) ๐ฃ๐ฆ ๐ข๐ฏ๐บ ๐ฑ๐ณ๐ฐ๐ฑ๐ฆ๐ณ๐ต๐บ ๐ฑ๐ฆ๐ณ๐ต๐ข๐ช๐ฏ๐ช๐ฏ๐จ ๐ต๐ฐ ๐ข ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ฏ. ๐๐ถ๐ฑ๐ฑ๐ฐ๐ด๐ฆ ๐ต๐ฉ๐ข๐ต ๐(๐) ๐ช๐ด ๐ต๐ณ๐ถ๐ฆ, ๐ข๐ฏ๐ฅ ๐ด๐ถ๐ฑ๐ฑ๐ฐ๐ด๐ฆ ๐ต๐ฉ๐ข๐ต ๐ธ๐ฉ๐ฆ๐ฏ๐ฆ๐ท๐ฆ๐ณ ๐(๐ฏ) ๐ช๐ด ๐ต๐ณ๐ถ๐ฆ, ๐(๐ฏ++) ๐ช๐ด ๐ข๐ญ๐ด๐ฐ ๐ต๐ณ๐ถ๐ฆ. ๐๐ฉ๐ฆ๐ฏ ๐(๐ฏ) ๐ช๐ด ๐ต๐ณ๐ถ๐ฆ ๐ง๐ฐ๐ณ ๐ฆ๐ท๐ฆ๐ณ๐บ ๐ฏ๐ข๐ต๐ถ๐ณ๐ข๐ญ ๐ฏ๐ถ๐ฎ๐ฃ๐ฆ๐ณ ๐ฏ.โ ๐๐ ๐๐๐๐๐๐ ๐บ๐๐พ๐ฝ ๐ป๐ ๐ฎ๐ ๐ถ๐ผ๐บ ๐๐ฐ๐ต๐ฒ๐บ๐ฎ (๐ดโ). (((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐โโ(0) โง (๐โโ(๐งโ ) โน ๐โโ((๐งโ )++)))) โน ((๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ๐โโ(๐ฆโ))) ๐๐ ๐บ ๐๐๐๐๐๐๐๐๐๐๐๐บ๐ ๐ฟ๐๐๐๐๐ ๐บ ๐๐๐๐พ๐๐๐๐พ๐๐พ๐ฝ ๐ฟ๐๐๐ ๐๐๐บ๐ ๐บ๐๐๐๐. ๐ณ๐๐พ๐๐พ๐ฟ๐๐๐พ, ๐ป๐ ๐๐๐พ ๐๐ฅ๐๐๐-๐๐๐ก๐๐๐๐๐๐ก๐๐ก๐๐๐ ๐๐๐ฟ๐พ๐๐พ๐๐ผ๐พ ๐๐๐ ๐พ: (๐, ๐ โข ๐), ๐๐ ๐ฟ๐๐ ๐ ๐๐๐ ๐๐๐บ๐ (((๐งโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โง (๐โโ(0) โง (๐โโ(๐งโ ) โน ๐โโ((๐งโ )++)))) โน ((๐ฆโ ๐๐ -๐ ๐๐๐ก๐ข๐๐๐-๐๐ข๐๐๐๐) โน ๐โโ(๐ฆโ))). โ ### ๐ง๐ต๐ฒ ๐ป๐๐บ๐ฏ๐ฒ๐ฟ ๐๐๐๐๐ฒ๐บ ๐ป ### ๐ฅ๐ฒ๐ฐ๐๐ฟ๐๐ถ๐๐ฒ ๐ฑ๐ฒ๐ณ๐ถ๐ป๐ถ๐๐ถ๐ผ๐ป๐
The report content.
๐๐๐พ ๐ฏ๐พ๐บ๐๐ ๐บ๐๐๐๐๐ # Theory properties Consistency: undetermined Stabilized: False Extended theory: N/A # Simple-objects declarations Let "natural-number", "0", "1", "2", "3", "4", "5", "6" be simple-objects in U4. # Connectives Let "++", "Inc" be unary-connectives in U4. Let "==>", "neq", "and", "is-a", "=" be binary-connectives in U4. # Inference rules The following inference rules are considered valid under this theory: Let "axiom-interpretation" be an inference-rule defined as "(A, P |- P)" in U4. Let "conjunction-introduction" be an inference-rule defined as "(P8, Q5 |- (P8 and Q5))" in U4. Let "definition-interpretation" be an inference-rule defined as "(D, x, y |- (x = y))" in U4. Let "equal-terms-substitution" be an inference-rule defined as "(P6, (x3 = y3) |- Q4)" in U4. Let "equality-commutativity" be an inference-rule defined as "((x1 = y1) |- (y1 = x1))" in U4. Let "inconsistency-introduction-2" be an inference-rule defined as "((P9 = Q6), (P9 neq Q6) |- Inc(T1))" in U4. Let "modus-ponens" be an inference-rule defined as "((P3 ==> Q2), P3 |- Q2)" in U4. Let "proof-by-refutation-2" be an inference-rule defined as "((H1 formulate (x7 = y7)), Inc(H1) |- (x7 neq y7))" in U4. Let "variable-substitution" be an inference-rule defined as "(P1, O1 |- Q1)" in U4. # Theory elaboration sequence # 2: The natural numbers ## 2.1: The peano axioms ### Informal definition of natural number ### Axiom 2.1 Axiom 2.1 (T1.A1): Let axiom A1 "0 is a natural number." be included (postulated) in T1. Inference rule (axiom-interpretation): Let inference-rule axiom-interpretation defined as "(A, P |- P)" be included and considered valid in T1. Proposition (T1.P1): (0 is-a natural-number). ### Axiom 2.2 Axiom 2.2 (T1.A2): Let axiom A2 "If n is a natural number, then n++ is a natural number." be included (postulated) in T1. Proposition (T1.P2): ((n1 is-a natural-number) ==> ((n1)++ is-a natural-number)). Inference rule (variable-substitution): Let inference-rule variable-substitution defined as "(P1, O1 |- Q1)" be included and considered valid in T1. Proposition (T1.P3): ((0 is-a natural-number) ==> ((0)++ is-a natural-number)). Inference rule (modus-ponens): Let inference-rule modus-ponens defined as "((P3 ==> Q2), P3 |- Q2)" be included and considered valid in T1. Proposition 2.2.3 (T1.P4): ((0)++ is-a natural-number). Definition (T1.D1): Let definition D1 "We define 1 to be the number 0++, 2 to be the number (0++)++, 3 to be the number ((0++)++)++,etc. (In other words, 1 := 0++, 2 := 1++, 3 := 2++, etc. In this text I use "x := y" to denote the statement that x is defined to equal y.)" be included (postulated) in T1. Inference rule (definition-interpretation): Let inference-rule definition-interpretation defined as "(D, x, y |- (x = y))" be included and considered valid in T1. Proposition (T1.P5): (1 = (0)++). Proposition (T1.P6): (2 = ((0)++)++). Proposition (T1.P7): (3 = (((0)++)++)++). Proposition (T1.P8): (4 = ((((0)++)++)++)++). Proposition (T1.P9): (((0)++ is-a natural-number) ==> (((0)++)++ is-a natural-number)). Proposition (T1.P10): (((0)++)++ is-a natural-number). Proposition (T1.P11): ((((0)++)++ is-a natural-number) ==> ((((0)++)++)++ is-a natural-number)). Proposition (T1.P12): ((((0)++)++)++ is-a natural-number). Proposition (T1.P13): (((((0)++)++)++ is-a natural-number) ==> (((((0)++)++)++)++ is-a natural-number)). Proposition (T1.P14): (((((0)++)++)++)++ is-a natural-number). Inference rule (equality-commutativity): Let inference-rule equality-commutativity defined as "((x1 = y1) |- (y1 = x1))" be included and considered valid in T1. Proposition (T1.P15): ((0)++ = 1). Inference rule (equal-terms-substitution): Let inference-rule equal-terms-substitution defined as "(P6, (x3 = y3) |- Q4)" be included and considered valid in T1. Proposition (T1.P16): (2 = (1)++). Proposition (T1.P17): (((0)++)++ = 2). Proposition (T1.P18): (3 = (2)++). ### 3 is a natural number Proposition (T1.P19): ((((0)++)++)++ = 3). Proposition (T1.P20): ((2)++ = 3). Proposition 2.1.4 (T1.P21): (3 is-a natural-number). Proposition (T1.P22): (4 = ((((0)++)++)++)++). Proposition (T1.P23): (((((0)++)++)++)++ = 4). Proposition (T1.P24): ((3)++ = 4). Proposition (T1.P25): (((((0)++)++)++ is-a natural-number) ==> (((((0)++)++)++)++ is-a natural-number)). Proposition (T1.P26): (4 is-a natural-number). ### Axiom 2.3 Axiom 2.3 (T1.A3): Let axiom A3 "0 is not the successor of any natural number; i.e., we have n++ 0 for every natural number n." be included (postulated) in T1. Proposition (T1.P27): ((n2 is-a natural-number) ==> ((n2)++ neq 0)). ### 4 is not equal to 0. Proposition (T1.P28): ((3 is-a natural-number) ==> ((3)++ neq 0)). Proposition (T1.P29): ((3)++ neq 0). Proposition 2.1.6 (T1.P30): (4 neq 0). ### Axiom 2.4 Axiom 2.4 (T1.A4): Let axiom A4 "Different natural numbers must have different successors; i.e., if n, m are natural numbers and n m, then n++ m++. Equivalently, if n++ = m++, then we must have n = m." be included (postulated) in T1. Proposition (T1.P31): ((((n3 is-a natural-number) and (m1 is-a natural-number)) and (n3 neq m1)) ==> ((n3)++ neq (m1)++)). Proposition (T1.P32): ((((n4 is-a natural-number) and (m2 is-a natural-number)) and ((n4)++ = (m2)++)) ==> (n4 = m2)). ### 6 is not equal to 2. Proposition (T1.P33): ((((4 is-a natural-number) and (0 is-a natural-number)) and (4 neq 0)) ==> ((4)++ neq (0)++)). Inference rule (conjunction-introduction): Let inference-rule conjunction-introduction defined as "(P8, Q5 |- (P8 and Q5))" be included and considered valid in T1. Proposition (T1.P34): ((4 is-a natural-number) and (0 is-a natural-number)). Proposition (T1.P35): (((4 is-a natural-number) and (0 is-a natural-number)) and (4 neq 0)). Proposition (T1.P36): ((4)++ neq (0)++). Proposition (T1.P37): (5 = (((((0)++)++)++)++)++). Proposition (T1.P38): ((((((0)++)++)++)++)++ = 5). Proposition (T1.P39): ((4)++ = 5). Proposition (T1.P40): (5 = (4)++). Proposition (T1.P41): ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> ((5)++ neq (1)++)). Proposition (T1.P42): ((4 is-a natural-number) ==> ((4)++ is-a natural-number)). Proposition (T1.P43): ((4 is-a natural-number) ==> (5 is-a natural-number)). Proposition (T1.P44): (5 is-a natural-number). Proposition (T1.P45): ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> ((5)++ neq (1)++)). Proposition (T1.P46): ((4)++ neq (0)++). Proposition (T1.P47): (5 neq (0)++). Proposition (T1.P48): (6 = ((((((0)++)++)++)++)++)++). Proposition (T1.P49): (((((((0)++)++)++)++)++)++ = 6). Proposition (T1.P50): (1 is-a natural-number). Proposition (T1.P51): ((5)++ = 6). Proposition (T1.P52): (6 = (5)++). #### Proof by contradiction Hypothesis (T1.H1): (6 = 2). Inference rule (inconsistency-introduction-2): Let inference-rule inconsistency-introduction-2 defined as "((P9 = Q6), (P9 neq Q6) |- Inc(T1))" be included and considered valid in T1. Proposition (T1.P66): Inc(H1). Inference rule (proof-by-refutation-2): Let inference-rule proof-by-refutation-2 defined as "((H1 formulate (x7 = y7)), Inc(H1) |- (x7 neq y7))" be included and considered valid in T1. Proposition 2.1.8 (T1.P67): (6 neq 2). #### Direct proof Proposition (T1.P68): ((1)++ = 2). Proposition (T1.P69): (5 neq 1). Proposition (T1.P70): ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> (6 neq (1)++)). Proposition (T1.P71): ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> (6 neq 2)). Proposition (T1.P72): ((5 is-a natural-number) and (1 is-a natural-number)). Proposition (T1.P73): (((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)). Proposition (T1.P74): (6 neq 2). ### Axiom 2.5: the principle of mathematical induction Axiom schema (T1.A6) - Principle of mathematical induction: Let axiom A6 "Let P(n) be any property pertaining to a natural number n. Suppose that P(O) is true, and suppose that whenever P(n) is true, P(n++) is also true. Then P(n) is true for every natural number n." be included (postulated) in T1. Proposition (T1.P75): (((n5 is-a natural-number) and (P10(0) and (P10(n5) ==> P10((n5)++)))) ==> ((m3 is-a natural-number) ==> P10(m3))). ### The number system n ### Recursive definitions
The report content.
๐๐๐พ ๐ฏ๐พ๐บ๐๐ ๐บ๐๐๐๐๐ # Theory properties Consistency: undetermined Stabilized: False Extended theory: N/A # Simple-objects declarations Let "natural-number", "0", "1", "2", "3", "4", "5", "6" be simple-objects in U4. # Connectives Let "++", "Inc" be unary-connectives in U4. Let "==>", "neq", "and", "is-a", "=" be binary-connectives in U4. # Inference rules The following inference rules are considered valid under this theory: Let "axiom-interpretation" be an inference-rule defined as "(A, P |- P)" in U4. Let "conjunction-introduction" be an inference-rule defined as "(P8, Q5 |- (P8 and Q5))" in U4. Let "definition-interpretation" be an inference-rule defined as "(D, x, y |- (x = y))" in U4. Let "equal-terms-substitution" be an inference-rule defined as "(P6, (x3 = y3) |- Q4)" in U4. Let "equality-commutativity" be an inference-rule defined as "((x1 = y1) |- (y1 = x1))" in U4. Let "inconsistency-introduction-2" be an inference-rule defined as "((P9 = Q6), (P9 neq Q6) |- Inc(T1))" in U4. Let "modus-ponens" be an inference-rule defined as "((P3 ==> Q2), P3 |- Q2)" in U4. Let "proof-by-refutation-2" be an inference-rule defined as "((H1 formulate (x7 = y7)), Inc(H1) |- (x7 neq y7))" in U4. Let "variable-substitution" be an inference-rule defined as "(P1, O1 |- Q1)" in U4. # Theory elaboration sequence # 2: The natural numbers ## 2.1: The peano axioms ### Informal definition of natural number ### Axiom 2.1 Axiom 2.1 (T1.A1): Let axiom A1 "0 is a natural number." be included (postulated) in T1. Inference rule (axiom-interpretation): Let inference-rule axiom-interpretation defined as "(A, P |- P)" be included and considered valid in T1. Proposition (T1.P1): (0 is-a natural-number). Proof: "0 is a natural number." is postulated by axiom 2.1 (A1). (0 is-a natural-number) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (0 is-a natural-number). QED ### Axiom 2.2 Axiom 2.2 (T1.A2): Let axiom A2 "If n is a natural number, then n++ is a natural number." be included (postulated) in T1. Proposition (T1.P2): ((n1 is-a natural-number) ==> ((n1)++ is-a natural-number)). Proof: "If n is a natural number, then n++ is a natural number." is postulated by axiom 2.2 (A2). ((n1 is-a natural-number) ==> ((n1)++ is-a natural-number)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that ((n1 is-a natural-number) ==> ((n1)++ is-a natural-number)). QED Inference rule (variable-substitution): Let inference-rule variable-substitution defined as "(P1, O1 |- Q1)" be included and considered valid in T1. Proposition (T1.P3): ((0 is-a natural-number) ==> ((0)++ is-a natural-number)). Proof: ((n1 is-a natural-number) ==> ((n1)++ is-a natural-number)) follows from prop. (P2). Let n1 = 0. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that ((0 is-a natural-number) ==> ((0)++ is-a natural-number)). QED Inference rule (modus-ponens): Let inference-rule modus-ponens defined as "((P3 ==> Q2), P3 |- Q2)" be included and considered valid in T1. Proposition 2.2.3 (T1.P4): ((0)++ is-a natural-number). Proof: ((0 is-a natural-number) ==> ((0)++ is-a natural-number)) follows from prop. (P3).(0 is-a natural-number) follows from prop. (P1). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that ((0)++ is-a natural-number). QED Definition (T1.D1): Let definition D1 "We define 1 to be the number 0++, 2 to be the number (0++)++, 3 to be the number ((0++)++)++,etc. (In other words, 1 := 0++, 2 := 1++, 3 := 2++, etc. In this text I use "x := y" to denote the statement that x is defined to equal y.)" be included (postulated) in T1. Inference rule (definition-interpretation): Let inference-rule definition-interpretation defined as "(D, x, y |- (x = y))" be included and considered valid in T1. Proposition (T1.P5): (1 = (0)++). Proof: "We define 1 to be the number 0++, 2 to be the number (0++)++, 3 to be the number ((0++)++)++,etc. (In other words, 1 := 0++, 2 := 1++, 3 := 2++, etc. In this text I use "x := y" to denote the statement that x is defined to equal y.)" is postulated by def. (D1). 1 is an interpretation of that definition. Therefore, by the definition-interpretation inference rule: (D, x, y |- (x = y)), it follows that (1 = (0)++). QED Proposition (T1.P6): (2 = ((0)++)++). Proof: "We define 1 to be the number 0++, 2 to be the number (0++)++, 3 to be the number ((0++)++)++,etc. (In other words, 1 := 0++, 2 := 1++, 3 := 2++, etc. In this text I use "x := y" to denote the statement that x is defined to equal y.)" is postulated by def. (D1). 2 is an interpretation of that definition. Therefore, by the definition-interpretation inference rule: (D, x, y |- (x = y)), it follows that (2 = ((0)++)++). QED Proposition (T1.P7): (3 = (((0)++)++)++). Proof: "We define 1 to be the number 0++, 2 to be the number (0++)++, 3 to be the number ((0++)++)++,etc. (In other words, 1 := 0++, 2 := 1++, 3 := 2++, etc. In this text I use "x := y" to denote the statement that x is defined to equal y.)" is postulated by def. (D1). 3 is an interpretation of that definition. Therefore, by the definition-interpretation inference rule: (D, x, y |- (x = y)), it follows that (3 = (((0)++)++)++). QED Proposition (T1.P8): (4 = ((((0)++)++)++)++). Proof: "We define 1 to be the number 0++, 2 to be the number (0++)++, 3 to be the number ((0++)++)++,etc. (In other words, 1 := 0++, 2 := 1++, 3 := 2++, etc. In this text I use "x := y" to denote the statement that x is defined to equal y.)" is postulated by def. (D1). 4 is an interpretation of that definition. Therefore, by the definition-interpretation inference rule: (D, x, y |- (x = y)), it follows that (4 = ((((0)++)++)++)++). QED Proposition (T1.P9): (((0)++ is-a natural-number) ==> (((0)++)++ is-a natural-number)). Proof: ((n1 is-a natural-number) ==> ((n1)++ is-a natural-number)) follows from prop. (P2). Let n1 = (0)++. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that (((0)++ is-a natural-number) ==> (((0)++)++ is-a natural-number)). QED Proposition (T1.P10): (((0)++)++ is-a natural-number). Proof: (((0)++ is-a natural-number) ==> (((0)++)++ is-a natural-number)) follows from prop. (P9).((0)++ is-a natural-number) follows from prop. 2.2.3 (P4). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that (((0)++)++ is-a natural-number). QED Proposition (T1.P11): ((((0)++)++ is-a natural-number) ==> ((((0)++)++)++ is-a natural-number)). Proof: ((n1 is-a natural-number) ==> ((n1)++ is-a natural-number)) follows from prop. (P2). Let n1 = ((0)++)++. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that ((((0)++)++ is-a natural-number) ==> ((((0)++)++)++ is-a natural-number)). QED Proposition (T1.P12): ((((0)++)++)++ is-a natural-number). Proof: ((((0)++)++ is-a natural-number) ==> ((((0)++)++)++ is-a natural-number)) follows from prop. (P11).(((0)++)++ is-a natural-number) follows from prop. (P10). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that ((((0)++)++)++ is-a natural-number). QED Proposition (T1.P13): (((((0)++)++)++ is-a natural-number) ==> (((((0)++)++)++)++ is-a natural-number)). Proof: ((n1 is-a natural-number) ==> ((n1)++ is-a natural-number)) follows from prop. (P2). Let n1 = (((0)++)++)++. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that (((((0)++)++)++ is-a natural-number) ==> (((((0)++)++)++)++ is-a natural-number)). QED Proposition (T1.P14): (((((0)++)++)++)++ is-a natural-number). Proof: (((((0)++)++)++ is-a natural-number) ==> (((((0)++)++)++)++ is-a natural-number)) follows from prop. (P13).((((0)++)++)++ is-a natural-number) follows from prop. (P12). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that (((((0)++)++)++)++ is-a natural-number). QED Inference rule (equality-commutativity): Let inference-rule equality-commutativity defined as "((x1 = y1) |- (y1 = x1))" be included and considered valid in T1. Proposition (T1.P15): ((0)++ = 1). Proof: (1 = (0)++) follows from prop. (P5). Therefore, by the equality-commutativity inference rule: ((x1 = y1) |- (y1 = x1)), it follows that ((0)++ = 1). QED Inference rule (equal-terms-substitution): Let inference-rule equal-terms-substitution defined as "(P6, (x3 = y3) |- Q4)" be included and considered valid in T1. Proposition (T1.P16): (2 = (1)++). Proof: (2 = ((0)++)++) follows from prop. (P6). ((0)++ = 1) follows from prop. (P15). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that (2 = (1)++). QED Proposition (T1.P17): (((0)++)++ = 2). Proof: (2 = ((0)++)++) follows from prop. (P6). Therefore, by the equality-commutativity inference rule: ((x1 = y1) |- (y1 = x1)), it follows that (((0)++)++ = 2). QED Proposition (T1.P18): (3 = (2)++). Proof: (3 = (((0)++)++)++) follows from prop. (P7). (((0)++)++ = 2) follows from prop. (P17). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that (3 = (2)++). QED ### 3 is a natural number Proposition (T1.P19): ((((0)++)++)++ = 3). Proof: (3 = (((0)++)++)++) follows from prop. (P7). Therefore, by the equality-commutativity inference rule: ((x1 = y1) |- (y1 = x1)), it follows that ((((0)++)++)++ = 3). QED Proposition (T1.P20): ((2)++ = 3). Proof: ((((0)++)++)++ = 3) follows from prop. (P19). (((0)++)++ = 2) follows from prop. (P17). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that ((2)++ = 3). QED Proposition 2.1.4 (T1.P21): (3 is-a natural-number). Proof: ((((0)++)++)++ is-a natural-number) follows from prop. (P12). ((((0)++)++)++ = 3) follows from prop. (P19). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that (3 is-a natural-number). QED Proposition (T1.P22): (4 = ((((0)++)++)++)++). Proof: "We define 1 to be the number 0++, 2 to be the number (0++)++, 3 to be the number ((0++)++)++,etc. (In other words, 1 := 0++, 2 := 1++, 3 := 2++, etc. In this text I use "x := y" to denote the statement that x is defined to equal y.)" is postulated by def. (D1). 4 is an interpretation of that definition. Therefore, by the definition-interpretation inference rule: (D, x, y |- (x = y)), it follows that (4 = ((((0)++)++)++)++). QED Proposition (T1.P23): (((((0)++)++)++)++ = 4). Proof: (4 = ((((0)++)++)++)++) follows from prop. (P8). Therefore, by the equality-commutativity inference rule: ((x1 = y1) |- (y1 = x1)), it follows that (((((0)++)++)++)++ = 4). QED Proposition (T1.P24): ((3)++ = 4). Proof: (((((0)++)++)++)++ = 4) follows from prop. (P23). ((((0)++)++)++ = 3) follows from prop. (P19). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that ((3)++ = 4). QED Proposition (T1.P25): (((((0)++)++)++ is-a natural-number) ==> (((((0)++)++)++)++ is-a natural-number)). Proof: (((((0)++)++)++ is-a natural-number) ==> (((((0)++)++)++)++ is-a natural-number)) follows from prop. (P13). ((3)++ = 4) follows from prop. (P24). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that (((((0)++)++)++ is-a natural-number) ==> (((((0)++)++)++)++ is-a natural-number)). QED Proposition (T1.P26): (4 is-a natural-number). Proof: (((((0)++)++)++)++ is-a natural-number) follows from prop. (P14). (((((0)++)++)++)++ = 4) follows from prop. (P23). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that (4 is-a natural-number). QED ### Axiom 2.3 Axiom 2.3 (T1.A3): Let axiom A3 "0 is not the successor of any natural number; i.e., we have n++ 0 for every natural number n." be included (postulated) in T1. Proposition (T1.P27): ((n2 is-a natural-number) ==> ((n2)++ neq 0)). Proof: "0 is not the successor of any natural number; i.e., we have n++ 0 for every natural number n." is postulated by axiom 2.3 (A3). ((n2 is-a natural-number) ==> ((n2)++ neq 0)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that ((n2 is-a natural-number) ==> ((n2)++ neq 0)). QED ### 4 is not equal to 0. Proposition (T1.P28): ((3 is-a natural-number) ==> ((3)++ neq 0)). Proof: ((n2 is-a natural-number) ==> ((n2)++ neq 0)) follows from prop. (P27). Let n2 = 3. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that ((3 is-a natural-number) ==> ((3)++ neq 0)). QED Proposition (T1.P29): ((3)++ neq 0). Proof: ((3 is-a natural-number) ==> ((3)++ neq 0)) follows from prop. (P28).(3 is-a natural-number) follows from prop. 2.1.4 (P21). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that ((3)++ neq 0). QED Proposition 2.1.6 (T1.P30): (4 neq 0). Proof: ((3)++ neq 0) follows from prop. (P29). ((3)++ = 4) follows from prop. (P24). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that (4 neq 0). QED ### Axiom 2.4 Axiom 2.4 (T1.A4): Let axiom A4 "Different natural numbers must have different successors; i.e., if n, m are natural numbers and n m, then n++ m++. Equivalently, if n++ = m++, then we must have n = m." be included (postulated) in T1. Proposition (T1.P31): ((((n3 is-a natural-number) and (m1 is-a natural-number)) and (n3 neq m1)) ==> ((n3)++ neq (m1)++)). Proof: "Different natural numbers must have different successors; i.e., if n, m are natural numbers and n m, then n++ m++. Equivalently, if n++ = m++, then we must have n = m." is postulated by axiom 2.4 (A4). ((((n3 is-a natural-number) and (m1 is-a natural-number)) and (n3 neq m1)) ==> ((n3)++ neq (m1)++)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that ((((n3 is-a natural-number) and (m1 is-a natural-number)) and (n3 neq m1)) ==> ((n3)++ neq (m1)++)). QED Proposition (T1.P32): ((((n4 is-a natural-number) and (m2 is-a natural-number)) and ((n4)++ = (m2)++)) ==> (n4 = m2)). Proof: "Different natural numbers must have different successors; i.e., if n, m are natural numbers and n m, then n++ m++. Equivalently, if n++ = m++, then we must have n = m." is postulated by axiom 2.4 (A4). ((((n4 is-a natural-number) and (m2 is-a natural-number)) and ((n4)++ = (m2)++)) ==> (n4 = m2)) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that ((((n4 is-a natural-number) and (m2 is-a natural-number)) and ((n4)++ = (m2)++)) ==> (n4 = m2)). QED ### 6 is not equal to 2. Proposition (T1.P33): ((((4 is-a natural-number) and (0 is-a natural-number)) and (4 neq 0)) ==> ((4)++ neq (0)++)). Proof: ((((n3 is-a natural-number) and (m1 is-a natural-number)) and (n3 neq m1)) ==> ((n3)++ neq (m1)++)) follows from prop. (P31). Let n3 = 4, m1 = 0. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that ((((4 is-a natural-number) and (0 is-a natural-number)) and (4 neq 0)) ==> ((4)++ neq (0)++)). QED Inference rule (conjunction-introduction): Let inference-rule conjunction-introduction defined as "(P8, Q5 |- (P8 and Q5))" be included and considered valid in T1. Proposition (T1.P34): ((4 is-a natural-number) and (0 is-a natural-number)). Proof: (4 is-a natural-number), of the form P8, follows from prop. (P26). (0 is-a natural-number), of the form Q5, follows from prop. (P1). Therefore, by the conjunction-introduction inference rule: (P8, Q5 |- (P8 and Q5)), it follows that ((4 is-a natural-number) and (0 is-a natural-number)). QED Proposition (T1.P35): (((4 is-a natural-number) and (0 is-a natural-number)) and (4 neq 0)). Proof: ((4 is-a natural-number) and (0 is-a natural-number)), of the form P8, follows from prop. (P34). (4 neq 0), of the form Q5, follows from prop. 2.1.6 (P30). Therefore, by the conjunction-introduction inference rule: (P8, Q5 |- (P8 and Q5)), it follows that (((4 is-a natural-number) and (0 is-a natural-number)) and (4 neq 0)). QED Proposition (T1.P36): ((4)++ neq (0)++). Proof: ((((4 is-a natural-number) and (0 is-a natural-number)) and (4 neq 0)) ==> ((4)++ neq (0)++)) follows from prop. (P33).(((4 is-a natural-number) and (0 is-a natural-number)) and (4 neq 0)) follows from prop. (P35). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that ((4)++ neq (0)++). QED Proposition (T1.P37): (5 = (((((0)++)++)++)++)++). Proof: "We define 1 to be the number 0++, 2 to be the number (0++)++, 3 to be the number ((0++)++)++,etc. (In other words, 1 := 0++, 2 := 1++, 3 := 2++, etc. In this text I use "x := y" to denote the statement that x is defined to equal y.)" is postulated by def. (D1). 5 is an interpretation of that definition. Therefore, by the definition-interpretation inference rule: (D, x, y |- (x = y)), it follows that (5 = (((((0)++)++)++)++)++). QED Proposition (T1.P38): ((((((0)++)++)++)++)++ = 5). Proof: (5 = (((((0)++)++)++)++)++) follows from prop. (P37). Therefore, by the equality-commutativity inference rule: ((x1 = y1) |- (y1 = x1)), it follows that ((((((0)++)++)++)++)++ = 5). QED Proposition (T1.P39): ((4)++ = 5). Proof: ((((((0)++)++)++)++)++ = 5) follows from prop. (P38). (((((0)++)++)++)++ = 4) follows from prop. (P23). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that ((4)++ = 5). QED Proposition (T1.P40): (5 = (4)++). Proof: ((4)++ = 5) follows from prop. (P39). Therefore, by the equality-commutativity inference rule: ((x1 = y1) |- (y1 = x1)), it follows that (5 = (4)++). QED Proposition (T1.P41): ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> ((5)++ neq (1)++)). Proof: ((((n3 is-a natural-number) and (m1 is-a natural-number)) and (n3 neq m1)) ==> ((n3)++ neq (m1)++)) follows from prop. (P31). Let n3 = 5, m1 = 1. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> ((5)++ neq (1)++)). QED Proposition (T1.P42): ((4 is-a natural-number) ==> ((4)++ is-a natural-number)). Proof: ((n1 is-a natural-number) ==> ((n1)++ is-a natural-number)) follows from prop. (P2). Let n1 = 4. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that ((4 is-a natural-number) ==> ((4)++ is-a natural-number)). QED Proposition (T1.P43): ((4 is-a natural-number) ==> (5 is-a natural-number)). Proof: ((4 is-a natural-number) ==> ((4)++ is-a natural-number)) follows from prop. (P42). ((4)++ = 5) follows from prop. (P39). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that ((4 is-a natural-number) ==> (5 is-a natural-number)). QED Proposition (T1.P44): (5 is-a natural-number). Proof: ((4 is-a natural-number) ==> (5 is-a natural-number)) follows from prop. (P43).(4 is-a natural-number) follows from prop. (P26). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that (5 is-a natural-number). QED Proposition (T1.P45): ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> ((5)++ neq (1)++)). Proof: ((((n3 is-a natural-number) and (m1 is-a natural-number)) and (n3 neq m1)) ==> ((n3)++ neq (m1)++)) follows from prop. (P31). Let n3 = 5, m1 = 1. Therefore, by the variable-substitution inference rule: (P1, O1 |- Q1), it follows that ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> ((5)++ neq (1)++)). QED Proposition (T1.P46): ((4)++ neq (0)++). Proof: ((((4 is-a natural-number) and (0 is-a natural-number)) and (4 neq 0)) ==> ((4)++ neq (0)++)) follows from prop. (P33).(((4 is-a natural-number) and (0 is-a natural-number)) and (4 neq 0)) follows from prop. (P35). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that ((4)++ neq (0)++). QED Proposition (T1.P47): (5 neq (0)++). Proof: ((4)++ neq (0)++) follows from prop. (P46). ((4)++ = 5) follows from prop. (P39). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that (5 neq (0)++). QED Proposition (T1.P48): (6 = ((((((0)++)++)++)++)++)++). Proof: "We define 1 to be the number 0++, 2 to be the number (0++)++, 3 to be the number ((0++)++)++,etc. (In other words, 1 := 0++, 2 := 1++, 3 := 2++, etc. In this text I use "x := y" to denote the statement that x is defined to equal y.)" is postulated by def. (D1). 6 is an interpretation of that definition. Therefore, by the definition-interpretation inference rule: (D, x, y |- (x = y)), it follows that (6 = ((((((0)++)++)++)++)++)++). QED Proposition (T1.P49): (((((((0)++)++)++)++)++)++ = 6). Proof: (6 = ((((((0)++)++)++)++)++)++) follows from prop. (P48). Therefore, by the equality-commutativity inference rule: ((x1 = y1) |- (y1 = x1)), it follows that (((((((0)++)++)++)++)++)++ = 6). QED Proposition (T1.P50): (1 is-a natural-number). Proof: ((0)++ is-a natural-number) follows from prop. 2.2.3 (P4). ((0)++ = 1) follows from prop. (P15). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that (1 is-a natural-number). QED Proposition (T1.P51): ((5)++ = 6). Proof: (((((((0)++)++)++)++)++)++ = 6) follows from prop. (P49). ((((((0)++)++)++)++)++ = 5) follows from prop. (P38). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that ((5)++ = 6). QED Proposition (T1.P52): (6 = (5)++). Proof: ((5)++ = 6) follows from prop. (P51). Therefore, by the equality-commutativity inference rule: ((x1 = y1) |- (y1 = x1)), it follows that (6 = (5)++). QED #### Proof by contradiction Hypothesis (T1.H1): (6 = 2). This hypothesis is elaborated in theory H1. Inference rule (inconsistency-introduction-2): Let inference-rule inconsistency-introduction-2 defined as "((P9 = Q6), (P9 neq Q6) |- Inc(T1))" be included and considered valid in T1. Proposition (T1.P66): Inc(H1). Proof: Let (P = Q) := (4 = 0) follows from prop. (P65). Let (P neq Q)) := (4 neq 0) follows from prop. 2.1.6 (P30). Therefore, by the inconsistency-introduction-2 inference rule: ((P9 = Q6), (P9 neq Q6) |- Inc(T1)), it follows that Inc(H1). QED Inference rule (proof-by-refutation-2): Let inference-rule proof-by-refutation-2 defined as "((H1 formulate (x7 = y7)), Inc(H1) |- (x7 neq y7))" be included and considered valid in T1. Proposition 2.1.8 (T1.P67): (6 neq 2). Proof: Let hyp. (H1) be the hypothesis (6 = 2). Inc(H1) follows from prop. (P66). Therefore, by the proof-by-refutation-2 inference rule: ((H1 formulate (x7 = y7)), Inc(H1) |- (x7 neq y7)), it follows that (6 neq 2). QED #### Direct proof Proposition (T1.P68): ((1)++ = 2). Proof: (((0)++)++ = 2) follows from prop. (P17). ((0)++ = 1) follows from prop. (P15). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that ((1)++ = 2). QED Proposition (T1.P69): (5 neq 1). Proof: (5 neq (0)++) follows from prop. (P47). ((0)++ = 1) follows from prop. (P15). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that (5 neq 1). QED Proposition (T1.P70): ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> (6 neq (1)++)). Proof: ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> ((5)++ neq (1)++)) follows from prop. (P45). ((5)++ = 6) follows from prop. (P51). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> (6 neq (1)++)). QED Proposition (T1.P71): ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> (6 neq 2)). Proof: ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> (6 neq (1)++)) follows from prop. (P70). ((1)++ = 2) follows from prop. (P68). Therefore, by the equal-terms-substitution inference rule: (P6, (x3 = y3) |- Q4), it follows that ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> (6 neq 2)). QED Proposition (T1.P72): ((5 is-a natural-number) and (1 is-a natural-number)). Proof: (5 is-a natural-number), of the form P8, follows from prop. (P44). (1 is-a natural-number), of the form Q5, follows from prop. (P50). Therefore, by the conjunction-introduction inference rule: (P8, Q5 |- (P8 and Q5)), it follows that ((5 is-a natural-number) and (1 is-a natural-number)). QED Proposition (T1.P73): (((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)). Proof: ((5 is-a natural-number) and (1 is-a natural-number)), of the form P8, follows from prop. (P72). (5 neq 1), of the form Q5, follows from prop. (P69). Therefore, by the conjunction-introduction inference rule: (P8, Q5 |- (P8 and Q5)), it follows that (((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)). QED Proposition (T1.P74): (6 neq 2). Proof: ((((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) ==> (6 neq 2)) follows from prop. (P71).(((5 is-a natural-number) and (1 is-a natural-number)) and (5 neq 1)) follows from prop. (P73). Therefore, by the modus-ponens inference rule: ((P3 ==> Q2), P3 |- Q2), it follows that (6 neq 2). QED ### Axiom 2.5: the principle of mathematical induction Axiom schema (T1.A6) - Principle of mathematical induction: Let axiom A6 "Let P(n) be any property pertaining to a natural number n. Suppose that P(O) is true, and suppose that whenever P(n) is true, P(n++) is also true. Then P(n) is true for every natural number n." be included (postulated) in T1. Proposition (T1.P75): (((n5 is-a natural-number) and (P10(0) and (P10(n5) ==> P10((n5)++)))) ==> ((m3 is-a natural-number) ==> P10(m3))). Proof: "Let P(n) be any property pertaining to a natural number n. Suppose that P(O) is true, and suppose that whenever P(n) is true, P(n++) is also true. Then P(n) is true for every natural number n." is postulated by axiom schema (A6). (((n5 is-a natural-number) and (P10(0) and (P10(n5) ==> P10((n5)++)))) ==> ((m3 is-a natural-number) ==> P10(m3))) is a propositional formula interpreted from that axiom. Therefore, by the axiom-interpretation inference rule: (A, P |- P), it follows that (((n5 is-a natural-number) and (P10(0) and (P10(n5) ==> P10((n5)++)))) ==> ((m3 is-a natural-number) ==> P10(m3))). QED ### The number system n ### Recursive definitions