PREREQUISITE: It is recommended that you watch Part 03 before watching this video!
So, hi, I'm Daddy Bear, or you can call me Aaron. I am surprisingly nervous, even though there is literally nobody here. Normally I'd take an audience photo at this point, but because of the Coronavirus, I'm unable to book the room in the school that I normally hire. So I'm making this in my illustrious office, and I need to keep up the schedule of one talk per month. So I'm going to try to make a video every month, regardless of what happens. So this is a very long presentation. I've changed this slide to say up to 20 or 30 hours, over 20 talks, because I realize now that's how long it's going to take. And that's why I need to keep up with the schedule. Armageddon not withstanding. So, okay. Normally people would interrupt me, but there is no audience, no studio audience.
The set of real numbers is an infinite set. So we're going to remedy this deficiency by adding universal and existential quantifiers which are written as this upside down A and backwards E and they will denote "for all" and "there exists". This should become clearer as we proceed. Now, things are going to get considerably more complex as a result of these enhancements, but in the end it'll be totally worth it due to the expressive power that we will gain.
Okay. Different type of substitution now. In this case for our purposes if P is a wff and T1 and T2 are both closed terms (remember closed terms) then [P with T1 for some T2] denotes any wff obtained by substituting T1 for some occurrences of T2 in P. Basically one or more, and it's entirely up to you if there's more than one substitution possible, it's up to the context to decide which ones you want to change or not. We'll see how that works. This is specifically for handling equality, so we'll see how that works later. So here's some examples. Yes, what we've done is p(y(), x, y()) [Note: y() is a nullary function, i.e. a constant] and we're replacing f(g()) for some y() [again, y() is a function, actually a constant]. Now that may denote p(f(g())), x, y()) and we've replaced the first occurrence of y(). In this one we've replaced the second occurrence, but not the first. So in the first example, we replaced the first occurrence, not the second. In the second example, replacing the second occurrence and not the first. What do you know? In the third example, we replaced both occurrences.
Now a relation, what's a relation in mathematics? So given some set D, which we'll call the domain, a relation R over D to the n (which just means it's n-place [or n-ary, i.e. takes n arguments]) is (or may be represented by) a set of n-tuples, each element of which is a member of D. Sometimes D is called the carrier, I think, but we'll call it the domain. Now this is just a way of representing [relationships] between individual members of a set of mathematical objects. And all we do is we enumerate every single case explicitly. [EDIT: Note that, yet again, relations may be nullary, i.e. with n = 0. Such relations effectively denote a boolean constant, i.e. the empty set denotes False, and the set containing the empty tuple (and nothing else) denotes True.]Aaron Turner:
So I'm going to put a pin in that for a minute and we're going to have a look at the First Order of Logic's proof rules.
So there are two premises above the lines. So if T1 and T2 are closed terms and we've already derived that T1 = T2 and we've derived Q, then we can derive Q with T1 substituted for some instances of T2 [because we know they're equal, right?] This is the only reason we had that additional "for some" substitution rule. So here's an example [which I've fixed in the transcript!] If a() = b() and q(b()), then we know that q(a()). All we've done is we've substituted a() for b() according to the bottom line of the =-elim rule.
So for all sets of closed wffs As and all closed wffs C, C is a semantic consequence of As if and only if ... C is a syntactic consequence of As. Now if you remember earlier on, we didn't have a way of evaluating ... [whether or not] C is a semantic consequence of As because of the infinite nature of the semantics. But now, we don't have to consider an infinite number of interpretations. ... if we need to try to evaluate whether C is a semantic consequence of As, then we can try to evaluate ... if C is a syntactic consequence of As, and if it is then we know from soundness that C is a semantic consequence of As. Which brings us to theorem-proving, i.e. the practical problem of proving that C is a syntactic consequence of As.
We're building an AGI here, remember. Now we have to ask the question, how can we get a mechanical theorem-prover to sometimes return (c), just like a human. You know, if the human can do it, we can do it, or our machine can do it. How can we get a mechanical theorem prover to do that? How is the human doing that, or equivalently, how can we get a theorem-prover to think meta-mathematically? And this is a question to which we will be returning in subsequent talks, like I said. So next month is about set theory, NBG set theory, and then the month after that will be about metamathematics and how to make a theorem-prover think meta-mathematically. Exciting.
Given the global pandemic, stay safe, and thank you for your attention. Thank you.