Logic | Compsci Compsci

<h1>Lecture 1</h1><h2>What is logic</h2><ul><li>A proof system where deductions can be made</li><li>The semantics of things and how the truth/false value of an entity can be determined</li></ul><h3>Logic requirements</h3><ul><li>Syntax</li><li>Semantics</li><li>Proof system</li></ul><p>Logic syntax should be complete an the semantics should be sound.</p><h2>Logic in action</h2><h3>Programming languages</h3><ul><li>Syntax tells you what is allowed in a legitimate program</li><li>Semantics tell you what the program will do</li></ul><h3>Databases</h3><p>Database is a structured collection of logical records.</p><ul><li><strong>Database query language: </strong>Language for asking questions about the logically structured data. E.g SQL</li></ul><h3>Formal methods</h3><p>Thi is use of mathematically based methods to prove that programs have certain properties so that we don't have to rely on testing.</p><p><strong>Model checking: </strong>Computer system modelled as a mathematical structure and then proving a property using the power of logic.</p><ul><li>Microprocessor design - Major microprocessor manufacturers still use model checking methods as part of their design process.</li><li>Data communications protocol software - rapid prototyping systems use it to validate new data-communications</li><li>Critical software - NASA uses model checking to make sure there aren't bugs in the space program code.</li><li>Operating systems - Microsoft uses it to verify the correct functioning of new </li></ul><h2>Hilbert's Programme</h2><p>Hilbert at a quest to formalize Mathematics by saying that all mathematical statements could be written with a formal language and by manipulating things accoruding to formal rules. Then things could be proved with formalism.</p><p>The idea was to create an algorithm to prove things.</p><h3>Gödel’s Incompleteness Theorems</h3><p>He proved that in any logical system powerful enough to describe the arithmetic of the natural numbers then there are things which cannot be proved within the system. This was a devastating blow to hilbert.</p><h3>Entscheidungsproblem</h3><p> </p>