LaTeX962713 views
雑学1473717 views
英語614322 views
中学社会669002 views
教育149564 views
高校日本史190639 views
MathPython498072 views
高校生物551985 views
世界の国564972 views
高校物理160543 views
Help
Tools
NewsSpreadsheetCalendarBookkeepingMarkdown TablesLanguage Model NewsLinux CommandsSlidesTier ListPen ToolIllustrationCrayonWatercolorPixel ArtASCII ArtPerspectiveEndless StairsGraphMind MapER DiagramFamily TreeMemeCurved TextImage EditorMosaicRetro FilterPencil SketchSwirl EffectLine ArtOCR/HighlighterMakeup EditorFaviconVideo TrimmerScrolling VideoVideo TitleColor PickerColor ExtractorBonfireFireworksCherry BlossomWater RippleWater SplashBreaking GlassGlass TextureFabric TextureWood GrainMarble TextureBrick Wall TextureMetal TextureWashi Paper TextureCardboard TextureCSS ButtonIcon MakerBar ChartGrouped Bar ChartStacked Bar ChartPie ChartLine ChartArea ChartStacked Area ChartScatter Plot3D Bar Chart3D Pie ChartBar Chart RaceBubble ChartPopulation PyramidPictogramEarningsCandlestick ChartInvestment RiskMortgage SimulatorCalculatorMatrix CalculatorFunction GraphPolynomial ExpansionVenn DiagramField VisualizerRubik's Cube Group TheoryTraveling SalesmanVoronoi and DelaunayFractalUniversity Entrance Exam MathColumn ArithmeticDraw Math FiguresArithmetic AnimationArithmetic Word ProblemsCounting with Tree DiagramsCube NetsRolling DiceCross SectionsMotion PathMechanicsWavesUniversity Entrance Exam Physics解析力学Quantum MechanicsStatistical MechanicsRelativityCelestial MechanicsAstrophysicsCosmologyElectromagnetic WavesCapacitorsLight and LensesThermodynamicsHow Semiconductors WorkMolecular StructuresAtomic OrbitalsElectrochemical CellsChemical EquilibriumCrystal LatticesBuffer pHOrganic Reaction MapPeriodic TableComplex IonsDNA Double HelixCell DivisionMembrane ChannelsNerve ImpulseMuscle ContractionHormones and HomeostasisRock ClassificationWeatherConstellationsSolar and Lunar Eclipses3D ModelingFloor PlanSeismic StructuresIntersection TurnMaglevCooking AnimationOrigamiLive Viewer CountGeoJSON MapRailway MapPopulation MapCrime MapLand Price MapSchool MapShrine and Castle MapHouse of Representatives MapWord MapSolitaireReversiHakoiri MusumeChessHamburgerRippleSlide Puzzle MakerNeon PinballNovel MakerJapanese Typing PracticePiano Score EditorMusic TheoryShogi StrategyPiano Rhythm Game

English

命題論理を公理から構築する|記号論理学の公理系

自然演繹とは異なるアプローチとして、公理系(axiomatic system)があります。少数の公理と推論規則だけを使って、命題論理のすべての定理を導く体系です。ヒルベルト流と呼ばれることもあります。

公理系とは何か

公理系は、証明なしに正しいと認める命題(公理)と、公理から新しい命題を導く規則(推論規則)からなります。公理は体系の出発点であり、そこから推論規則を繰り返し適用して定理を導きます。

自然演繹

多くの推論規則を使う。仮定を立てて解消するスタイル。

公理系

少数の公理と最小限の推論規則。公理から演繹的に導くスタイル。

古典的な公理系の例

命題論理の代表的な公理系を紹介します。含意 → と否定 ¬ を基本結合子とし、他の結合子は定義で導入します。

公理は 3 つだけです。

公理 1

φ → (ψ → φ)

公理 2

(φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))

公理 3

(¬φ → ¬ψ) → (ψ → φ)

これらは公理スキーマと呼ばれ、φ, ψ, χ に任意の論理式を代入したものがすべて公理として認められます。

推論規則:モーダスポネンス

公理系で使う推論規則は、モーダスポネンスただ一つです。

$$

φ と φ → ψ から ψ を導きます。この一つの規則と 3 つの公理だけで、命題論理のすべての定理が証明できます。

公理系での証明の例

p → p を公理系で証明してみましょう。自然演繹では一瞬でしたが、公理系ではやや技巧が必要です。

まず公理 2 に φ = p, ψ = p → p, χ = p を代入すると、(p → ((p → p) → p)) → ((p → (p → p)) → (p → p)) を得ます。

公理 1 に φ = p, ψ = p → p を代入すると、p → ((p → p) → p) を得ます。

モーダスポネンスで (p → (p → p)) → (p → p) を得ます。

公理 1 に φ = p, ψ = p を代入すると、p → (p → p) を得ます。

最後にモーダスポネンスで p → p を得ます。

公理を適切に代入

モーダスポネンスで中間結果を導く

さらにモーダスポネンスで最終結果

なぜ公理系は複雑なのか

公理系での証明は、自然演繹と比べて人工的で複雑に見えます。p → p のような自明な命題でさえ、5 ステップもかかります。

しかし、公理系には理論的な利点があります。体系の構造が単純なので、メタ定理(体系に関する定理)を証明しやすいのです。たとえば「この体系で証明可能なすべての式はトートロジーである」といった性質を示すのに、規則が少ない方が扱いやすいです。

連言と選言の定義

公理系では、連言と選言を含意と否定で定義します。

p ∧ q は ¬(p → ¬q) と定義できます。「p ならば q でない」が成り立たない、つまり p と q が両方真ということです。

p ∨ q は ¬p → q と定義できます。「p でないならば q」は「p または q」と同値です。

連言の定義

p ∧ q ≡ ¬(p → ¬q)

選言の定義

p ∨ q ≡ ¬p → q

公理系のバリエーション

命題論理の公理系は一通りではありません。異なる公理の選び方があり、どれも同じ定理の集合を導きます。

たとえばウカシェヴィチの公理系、メンデルソンの公理系など、さまざまなバリエーションがあります。公理の数や形が異なっても、最終的に証明できる定理は同じです。

次回は、公理系と自然演繹の関係、特に健全性と完全性について学びます。