Okay, how does it work? Good, easy. Right? We give ourselves a language, we have two

kinds of things we're modeling in this world, we have truth values, and I'll sometimes decorate

those with a quote-unquote type Omicron, and we have individuals which I'm

sometimes going to annotate with a type Iota, and then we have a signature which

is essentially the things you can write down in in this logic. We have the

connectives we all know and love from propositional logic, we have function

constants, we have predicate constants, and we have something called Scholem

constants which we'll need later. The function constants and predicate

constants we think of as being finite and of the Scholem constants we give

ourselves an infinite supply and we have variables as well which we think give

ourselves an infinite supply of as well. Okay? So those are the things we're going

to use and then we make terms. Terms are just made variables are terms and if I

have a k-ary function and k terms then I can apply the function f to k terms and

get another term. And if I have a unary function, one argument function, say the

mother function, and I have a zero-ary function Peter, right? Peter is an

individual without applying it to anything so we're then I can have mother

of Peter and that's a term. And of course by the same rule mother of mother of

mother of mother of Peter. Great great grandmother. Okay? So we can also give

ourselves propositions, another kind of objects. I do that by if I have a k-ary

predicate and apply it to k terms I'm going to get an atomic proposition and

if I have propositions then I can make new propositions by applying connectives

to them true as a composition and I can make a new given a variable X I can make

a new proposition for all XA. Okay? Now that's a very traditional way of

writing this down. What you want to think of this as a computer science is really

think of this as a grammar. Think of this as a grammar where we say well what are

the terms just the context free grammar well they're variables and a k-ary

functions. Yeah let's call this t and this n should be a k. Okay? So terms that

that's really these two productions are just these two rules. And then we have

formulae which is essentially true is a formula P of t1 to tk for a k-ary thing

and what else? A and A1, A2 or not A2 or for all XA. It's a good thing it's so

easy otherwise you wouldn't be able to see what I have read. Okay? That's a

grammar of a formal language and that's exactly what I'm doing here. And in a way

we have propositional logic as a sub language. And instead of propositional

variables which are black box propositions we have these atomic

formulae. And the only thing that's really really interesting and new is

this. There. This is new interesting for all XA where A is any kind of a

proposition which allows us to write down things like for all X even of X if

and only if even of successor of successor of X. Right? Why? Because even as

a unary predicate which I can apply to one term and variables are terms so this

is actually this is actually of type omicron. I have another one of those X is

a variable so S of X is the application of one a unary function to a term is a

term. I can do it again so S of S of X is a term. I can apply the unary predicate

I can apply the unary predicate even to it. I have another proposition here. Two

proposition joined by if and only if gives me a proposition for all X in

front of it. Wow there it is. Okay? That's exactly what we do with this kind of a

grammar. Okay. Syntax done. Oh yes and you can see I did it again. I just said well

I have true and or and for all which is kind of a minimal set of logical

constants but of course I want much more. I want to have or which I abbreviate in

the usual way implies and so on but also I want to have an existential

quantifier there is an XA and I take that to be an abbreviation of it is not