meta-theorems-of-predicate-logic.html (2939B)
1 <html> 2 <head> 3 <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> 4 <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> 5 <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> 6 <link rel="Stylesheet" type="text/css" href="style.css" /> 7 <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> 8 <script> 9 document.addEventListener('DOMContentLoaded', function() { 10 document.querySelectorAll('pre.code').forEach(function(item) { 11 hljs.highlightBlock(item) 12 }) 13 }); 14 </script> 15 <title>meta-theorems-of-predicate-logic</title> 16 </head> 17 <body> 18 <style type="text/css"> 19 nav a { 20 text-align: left; 21 } 22 nav #name { 23 text-align: right; 24 float: right; 25 font-style: italic; 26 } 27 </style> 28 <nav> 29 <a href="index.html">Index</a> 30 <span id="name">Alex Balgavy</span> 31 </nav> 32 <hr> 33 <div class="content"> 34 35 <div id="Meta-Theorems of Predicate Logic"><h2 id="Meta-Theorems of Predicate Logic" class="header"><a href="#Meta-Theorems of Predicate Logic">Meta-Theorems of Predicate Logic</a></h2></div> 36 <p> 37 Entailment syntactically (⊢) and semantically (⊨) 38 </p> 39 <ul> 40 <li> 41 Γ ⊢ ψ: there is natural deduction derivation of ψ that only uses premises in Γ 42 43 <li> 44 Γ ⊨ ψ: for all M and l, if M ⊨l Φ for every Φ ∈ Γ, then M ⊨ ψ 45 46 </ul> 47 48 <p> 49 Soundness and completeness: 50 </p> 51 <ul> 52 <li> 53 Γ ⊢ Φ ⇔ Γ ⊨ Φ 54 55 <li> 56 for all formulas Φ, every set Γ of formulas 57 58 <li> 59 soundness (correctness): left-to-right (⇒) 60 61 <li> 62 completeness: right-to-left (⇐) 63 64 </ul> 65 66 <p> 67 soundness theorem: 68 </p> 69 <ul> 70 <li> 71 Γ ⊢ Φ ⇒ Γ ⊨ Φ 72 73 <li> 74 if there is natural deduction derivation of Φ from Γ, then there's no model M in which all formulas of Γ are true, but Φ is false 75 76 <li> 77 "correct" means not possible to derive false conclusion Φ from true premises Γ 78 79 <li> 80 prove by induction on derivation lengths 81 82 </ul> 83 84 <p> 85 completeness theorem: 86 </p> 87 <ul> 88 <li> 89 Γ ⊨ Φ ⇒ Γ ⊢ Φ 90 91 <li> 92 derivations are strong enough to derive all valid semantic entailment statements 93 94 <li> 95 "complete" means more derivation rules are not necessary 96 97 <li> 98 proof is non-trivial 99 100 </ul> 101 102 <p> 103 consistency and syntactical consistency 104 </p> 105 <ul> 106 <li> 107 Γ is consistent ⇔ Γ is syntactically consistent 108 109 <li> 110 Γ has a model ⇔ there is no derivation of ⊥ from Γ 111 112 </ul> 113 114 <p> 115 semantical consistency: 116 </p> 117 <ul> 118 <li> 119 set Γ of formulas is consistent if there is model M and environment l such that M ⊨ Φ for all Φ ∈ Γ 120 121 </ul> 122 123 <p> 124 syntactical consistency: 125 </p> 126 <ul> 127 <li> 128 set Γ of formulas is syntactically consistent if Γ ⊬ ⊥ 129 130 </ul> 131 132 <p> 133 compactness theorem: 134 </p> 135 <ul> 136 <li> 137 Γ is consistent ⇔ every finite subset Γ₀ ⊆ Γ si consistent 138 139 </ul> 140 141 </div> 142 </body> 143 </html>