Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
3 changed files
with
141 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,128 @@ | ||
| <!DOCTYPE html> | ||
| <html> | ||
|
|
||
| <head> | ||
| <meta http-equiv="content-type" content="text/html; charset=utf-8" /> | ||
| <title>Philippe Desjardins-Proulx</title> | ||
| <link rel="stylesheet" media="screen" href="../css/style.css" type="text/css" /> | ||
| <link rel="stylesheet" media="screen" href="../css/code.css" /> | ||
| <!-- <link href='http://fonts.googleapis.com/css?family=Questrial' rel='stylesheet' type='text/css'> --> | ||
| <!-- <link href='http://fonts.googleapis.com/css?family=Inconsolata:400,700' rel='stylesheet' type='text/css'> --> | ||
| <link href="http://fonts.googleapis.com/css?family=Montserrat:400,700" rel="stylesheet" type="text/css"> | ||
| <link href="http://fonts.googleapis.com/css?family=Source+Sans+Pro:400,400italic" rel="stylesheet" type="text/css" /> | ||
| <link href="http://fonts.googleapis.com/css?family=Ubuntu+Mono" rel="stylesheet" type="text/css" /> | ||
| <link href="//maxcdn.bootstrapcdn.com/font-awesome/4.2.0/css/font-awesome.min.css" rel="stylesheet" type="text/css" /> | ||
| </head> | ||
|
|
||
| <body> | ||
|
|
||
| <!-- <a href='https://github.com/PhDP/'> | ||
| <img style='position: absolute; top: 0; left: 0; border: 0;' src='/images/forkme.png' alt='Fork me on GitHub'> | ||
| </a> --> | ||
|
|
||
| <div id="header"> | ||
| <!-- <h1><a href='mailto:philippe.d.proulx@gmail.com'>Philippe Desjardins-Proulx</a></h1> --> | ||
| <nav> | ||
| <ul> | ||
| <li>( Philippe Desjardins-Proulx</li> | ||
| <li><a href="../index.html">about</a></li> | ||
| <li><a href="../blog.html">blog</a></li> | ||
| <li><a href="https://ca.linkedin.com/in/philippedp"><i class="fa fa-linkedin-square"></i></a></li> | ||
| <li><a href="https://github.com/PhDP"><i class="fa fa-github"></i></a></li> | ||
| <li><a href="https://twitter.com/phdpqc"><i class="fa fa-twitter"></i></a></li> | ||
| <li><a href="mailto:philippe.d.proulx@gmail.com"><i class="fa fa-envelope"></i></a>)</li> | ||
| </ul> | ||
| </nav> | ||
| </div> | ||
|
|
||
| <div id="content"> | ||
| <h1>A crash course in second-order logic</h1> | ||
|
|
||
| <a href="https://twitter.com/share" class="twitter-share-button" data-text="A crash course in second-order logic" data-via="phdpqc">Tweet</a> | ||
| <p id="dt"><script>!function(d,s,id){var js,fjs=d.getElementsByTagName(s)[0],p=/^http:/.test(d.location)?'http':'https';if(!d.getElementById(id)){js=d.createElement(s);js.id=id;js.src=p+'://platform.twitter.com/widgets.js';fjs.parentNode.insertBefore(js,fjs);}}(document, 'script', 'twitter-wjs');</script> | ||
| 2018.04.16 | ||
| </p> | ||
|
|
||
| <p><a href="2015-07-13-fol.html">I previously wrote a very short introduction | ||
| to first-order logic.</a> That introduction ignored many important questions, | ||
| like how to perform inference, and focused only on defining first-order logic | ||
| and providing some examples of what it could express. I wrote this intro | ||
| because first-order logic is a central player in researchers' effort to combine | ||
| symbolic with probabilistic representations, but a natural question arise: why | ||
| <b>first</b> order? Is there zeroth-order, second-order, higher-order? The | ||
| answers are: yes, yes, and yes, and here I'll briefly explain what second-order | ||
| and zeroth-order logics are.</p> | ||
|
|
||
| <p>First-order logic is a powerful symbolic representation for mathematical | ||
| ideas. Take Catalan's conjecture, explained in detail by <a href="https://www.youtube.com/watch?v=Us-__MukH9I">Holly Krieger in this | ||
| numberphile video</a>. In 1842, Eugène Charles Catalan wondered whether (2^3 = | ||
| 8\) and \(3^2 = 9\) was the only pair of consecutive perfect powers, i.e. the | ||
| power of a natural number greater than one such as \(2^3\), \(5^2\), | ||
| \(9^{15}\), ... We can formalize this conjecture in first-order logic:</p> | ||
|
|
||
| \[\exists! x, y, a, b \in \mathbb{N}: x > 0 \land y > 0 \land a > 1 \land b > 1 \land y^b = x^a + 1.\] | ||
|
|
||
| <p>\(\exists!\) is the unique quantifier ("there exists only one"), and \(x \in | ||
| \mathbb{N}\) reads "x belongs to the natural numbers". Preda Mihăilescu proved | ||
| it in 2002.</p> | ||
|
|
||
| <p>So what makes this formula <b>first</b> order? It means the formula only | ||
| quantifies over individual elements. In the previous formula, the variables | ||
| \(x, y, a, b\) ranged over individual elements (natural numbers). We call these | ||
| individual variables. They could also range over cities, presidential | ||
| candidates, species, complex numbers, vectors, etc etc, but they cannot, say, | ||
| range over functions or sets of elements. In a nutshell: second-order logic is | ||
| exactly like first-order logic in every way (same connectives, same predicates, | ||
| same quantifiers), but it allows quantification over sets, predicates, and | ||
| functions. It adds function variables and predicate variables (with sets being | ||
| in essence, predicates). And that's it. Take the principle of bivalence, that | ||
| something is or isn't in a set. It can be written in second-order logic as:</p> | ||
|
|
||
| \[\forall x, S: x \in S \veebar x \not \in S.\] | ||
|
|
||
| <p>with \(\veebar\) <a href="2015-07-13-fol.html">being the exlusive or | ||
| symbolc</a> and \(\in\) being the "belongs to" predicate. Here, \(x\) is an | ||
| individual variable, but \(S\) is a predicate variable, it represents sets, not | ||
| individual elements. Graph theory is famous for second-order logic | ||
| applications, with simple ideas like reachability being difficult to define | ||
| without second-order quantificiation. Another example is a fairly important | ||
| concept in optimization: convexity of functions.</p> | ||
|
|
||
| \[\forall f, x, y, \alpha: Convex(f) \iff f(\alpha \times x + (1 - \alpha) \times y) \leq \alpha \times f(x) + (1 - \alpha) \times f(y).\] | ||
|
|
||
| <p>With \(\alpha \in \mathbb{R} \mid 0 \leq \alpha \leq 1\). What makes this | ||
| second order is the quantification over \(f\), a function. We don't want | ||
| to define convexity for a specific function, we want to define it for | ||
| all functions, hence the need for quantification over functions.</p> | ||
|
|
||
| <h2>What about zeroth-order?</h2> | ||
|
|
||
| <p>There is no agreement on what is zeroth-order logic. It is often used to | ||
| refer to propositional logic, arguably the most primitive logic, where instead | ||
| of predicates we only have propositional symbols, e.g. \(x \land y \implies z\) | ||
| is a propositional formula with symbols \(x, y, z\). Since there are no | ||
| predicates, and thus no variables, constants, or functions, this is not really | ||
| useful to represent maths (although richer logics are often reduced to | ||
| propositional logic for inference). The other interpretation is that | ||
| zeroth-order is first-order logic without variables:</p> | ||
|
|
||
| \[CapitalOf(France) = Paris.\] | ||
| \[2^{2^2 + 2} = 64.\] | ||
| \[\neg Insect(Centipede).\] | ||
|
|
||
| <p>These formulas become first-order the second you quantify over elements, and | ||
| second-order if you quantify over sets, functions, predicates.</p> | ||
|
|
||
|
|
||
|
|
||
| <div id="hidden"> | ||
| let world = "世界" in print $ "Hello " ++ world ++ "!" | ||
| </div> | ||
| </div> | ||
|
|
||
| <script type="text/javascript" src="../js/bower/MathJax/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> | ||
| <script type="text/javascript" src="../js/highlight.pack.js"></script> | ||
| <script type="text/javascript">hljs.initHighlightingOnLoad();</script> | ||
|
|
||
| </body> | ||
| </html> |