24.2.1 Foundational things
These are the meta-definitions for any given logic (that is, they are kind of a \saytemplate for defining a specific logic). Once we answer these questions, we have a logic!
An interpretation assigns a value to specified free symbols in a formula.
An interpretation is suitable for a formula if it binds all free variables.
Given a formula (or a set of formulas), a model is an interpretation for which is true.
In formulas, this is either
Logical consequence If for every interpretation whenever is true, is too, then we write
Logical equivalence ???
Tautology notation If is a tautology (informally it is always true) then we write
That is, cannot be derived
Unsatisfiability If is unsatisfiable we write
Relation between tautology and unsatisfiability We can prove that
This apparently follows from what this means.
Normal forms The statements of the theorem is that we can always write any formula in a normal form.
Consider some formula in propositional logic, for which we have a truth table. We then consider the entries. For these rows, we might have something in the form
Then we add a term which is one if and only if . For example, in this case we would have something that looks a bit like
For conjunctive normal form, this is a little more complex, but we could do something like
then instead of making terms one when the conditions trigger, we make terms zero when the conditions are not triggered.
24.2.2 Definition of propositional logic
24.2.3 Definition of predicate logic
Syntax of predicate logic
We begin by defining the syntax of predicate logic; we have:
variables, which we can denote as (in order to ensure that we have an infinite reserve of these), but we normally write using letters (e.g. ) as it is easier for (most) humans to understand these
functions such as (where is an index used to identify a specific function, and denotes the \sayarity, aka number of arguments the function takes)
Predicates, in the form
This is not a particularly interesting language - we would ideally be able to build more complex syntactically valid objects out of these simple ones we have defined. We define a \sayterm inductively (or recursively). A term (from a purely syntactical point of view) is defined as something in the form
This is all very well, but we would also like our terms to be finite (infinitely recursive pieces of language are not particularly pleasant). We must also, therefore, define a \saybase case (i.e. some terms which are not defined in terms of other terms, so that it is at least possible for our terms to terminate). todo: finish this part (above)
We also define formulae, using these rules
is a formula,
If and are formulae, then so are , as well as
If is a formula, then and are also formulae.
The formula (in Equation 24.18, below) is not valid.
Why? Because may not be a variadic function (i.e. it may not have more than terms as arguments) but it is constructed with one term () and also with two terms which is not valid.
A syntactically valid formula in propositional logic is
Of course, we have not yet defined what this formula means (beyond whether or not we may write it), for that we require semantics.
Another syntactically valid formula is
We still have no idea what this means semantically, just that it is a valid formula.
Free variables in predicate logic
Continuing with example 24.2.3, we can make a substitution of for , which would give us
Interpretations in predicate logic
Consider the formula
we can consider this in the universe , and define
and further define
and then fix , in which case we can ask is a \saymodel for . It is, as for every , either is even, or is even.
Consider the previous example, but with a different interpretation
In this case, .
Is this a true statement:
This is not a true statement! If the right-hand side is true, this does not necessarily mean that the two separate interpretations, one for and one for are true for .
This is analogous to the fact that
is not true, as although the left-hand implies the right, the other way is not true.
A predicate logic interpretation. Let us return to the familiar formula
We would like to find an interpretation which makes this true.
For example, we could define as
But how would we define the value of
Here’s a sensible definition of what this means semantically
This might seem in some way informal, but here’s the problem; at some point we will need to introduce some axioms.
24.2.4 Logical calculi
A logical calculus is a simple thing; it’s a way to connect truth and syntax. This is especially useful in computer systems where it is easy (well, easy-ish) to carry out syntactic manipulations (this is closely related to a branch of computer science called term rewriting).