Michael Jackson argues strongly that LPC is clearest language for stating and clarifying:
In MATHS (the logic I developed to help get programs that work well) we describe LPC in terms of a generic type of object. We assume that the rules can then be used any type of object at all. Further we identify the type with the set of all objects of that type (a universe of discourse). To put this another way - a type is a collection of things to which LPC with equality applies.
In practice, there is evidence that it pays to divide up the universe of discourse into objects of different types. This idea needs further work but fits with the simple model proposed here if we assume a set of predicates setting up the ontology of the domain or universe of discourse. For example we may want to distinguish animals from rocks for example, or numbers from teachers.
In essence, MATHS can talk about an infinite array of different
universes.
A natural name would be a
multiverse
perhaps. Each universe has its own type of object, its own axioms,
formulae, theorems etc. This includes objects with complex internal
structures like lists and sets. MATHS dare not talk about all of these
without getting into paradoxes. But it assumes the
(principle_of_genericity): The lower predicate calculus with equality
is a generic logic that applies to all types of objects.
In other parts of the MATHS system we make the assumption that the collection of all subsets of a type will have a similar logic. We assume that structured objects will be a type to which LPC will apply. We assume that certain families of functions and relations form a types.
The logic is based on expressing the properties of individuals of a given type. We use the term predicate for a property -- the term ultimately comes from natural language grammar and Greek philosophy. An example might be the classic argument:
|- for x:Beings, if human (x) then mortal(x).
|- human(socrates).
()|-mortal(socrates).It is rendered to look like this:
|- for x:Beings, if human (x) then mortal(x).
|- human(socrates).
()|-mortal(socrates).
Lewis Carroll gives us an example of a plausible but wrong argument:
Statements involving people's knowledge and desires (optative logic) do not always follow the generic LPC rules. They may look like predicates, but they fail to follow the rules that predicates follow. People commonly assert both that I want A(x) for all x and also `I don't want A(a)' . Logic texts use Hamlet killing Polonius as an example. In software engineering this means that a statement of requirements (What the user wants") is likely to contain inconsistencies which must be detected and removed.
Propositions are statements that are either true or false. Propositions have type @ (In script a curly P or the ΤΕΧ \pw symbol). Predicates map elements of various types into propositions. The are constructed using "and", "or", "not", "if_then_" and so on. These are the operators in the propositional calculus or PC. Phrases like "for all", "for one", "for some", "for no" etc are also used. These are quantifiers in the LPC. A typical logical text will provide one quantifier. MATHS has a great many more.
Identity and equality are two fundamental binary relations which relate expressions of a given type. Identity (==) means that the two expressions are identical in everything except their lexical layout. Identity should be treated as a meta-linguistic idea... used for discussing the logic of the type, rather than used inside the type itself.
Equality (=) is an equivalence relation that holds between two elements that can be, for this logical system, treated the same way. Two expressions of a given type are equal if and only if one can be substituted for each other, in all circumstances, without changing the meaning of the result. Each type has it's own equality relationship. It in many ways defines the properties of the type.
After this see [ logic_11_Equality_etc.html ] or return to the introduction: [ logic_0_Intro.html ] or list of logical items [ home.html#Logic ]
===========================================
P true false
--------------------------------------------
not P false true
===========================================
P true true false false
Q true false true false
--------------------------------------------
P and Q true false false false
P or Q true true true false
P iff Q true false false true
if P then Q true false true false
===========================================.
Equivalences are PARALLEL operators,
The clausal_form P:-Q is used in Prolog and some other systems:
For the lazy, Q-:P can be used for if Q then P as well. If an arrow is available then write (P->Q) but beware confusion with the notation for maps between two sets: (A->B).
Further, Since '<>' indicates the negation of '=' (in LPCe) it follows that
Since many call this the "exclusive or" operator we can define
| P | Q | P=Q | P<>Q | P and Q | P or Q |
|---|---|---|---|---|---|
| true | true | true | false | true | true |
| true | false | false | true | false | true |
| false | true | false | true | false | true |
| false | false | true | false | false | false |
Two predicates are equal when one can be written for the other in any context. This would hold when they have the same free variables and if they are true when the same values are substituted for their variables.
human(x)
x.human
older(x,y)
(x,y).older
x older y
It would be nice to allow more complex and natural syntax:
`RJBotting` has degree `Ph.D.` from `Brunel University`in place of
`RJBotting` has_degree_from( `Ph.D.` ,`Brunel University`)See [ Natural, distfix, or mixfix predicates ] below.
We can define for all as applying and:
We define no and some in terms of all
| MATHS | ΤΕΧ |
|---|---|
| and | ∧ |
| or | ∨ |
| not | not |
| if p then q | p → q |
| iff | ↔ |
| for all | ∀ |
| for some | ∃ |
We can run a series of quantifiers together:
for all x, some y, no z(F(x,y,z)) = for all x(for some y(for no z(F(x,y,z)))).
Here are a couple of classic quantified (and abbreviated) propositions
taken from automata theory:
Net
The following idiom is both common and natural:
This is taken to be an abbreviation for
Note: an abuse of notation follows. The word macro in a definition indicates an abbreviation that can be used anywhere and is always removed before any meaning or parsing etc. is applied to the formula:
. . . . . . . . . ( end of section Definitions of Quantifiers) <<Contents | End>>
I'm not sure whether the following is wise or not.
Net
Suppose that we have a Quantifier Q, a predicate (P(x)) with free variables x plus some other bound variables. The bound variables could have been bound in the context of the quantification or inside P(x). Assume that other rules also assign default types T to these free variables:
(Q P(x))::macro = (Q x:T( P(x) ).
(Q P(x) (W))::macro = (Q x:T, P(x) (W)).
For example,
Supposing further R(x,y) is another proposition with with some extra free variables y (disjoint to x!) with default types U then
P(x) ==> R(x, y) ::macro= for all x:T( if P(x) then for some y:U ( R(x, y))).
Idea a definition like this
For x:Person, y:Degree, z:College, (x has degree y from z) ::@.defines a "mixfix" or "distfix" expression. It describes a template into which expressions can be placed to create predicates:
`RJBotting` has degree `Ph.D.` from `Brunel University`
template:@TEMPLATE, for all s:#char, 0..1 template t ( s in syntax(t) ).
For example
`RJBotting` has degree `Ph.D.` from `Brunel University`has delimiters ("", "has degree", "from", "").
For example
`RJBotting` has degree `Ph.D.` from `Brunel University`has 4 delimiters (the first and last are "" null) and so a, the arity, is 3.
For example
`RJBotting` has degree `Ph.D.` from `Brunel University`has delimiters D(1)="", D(2)="has degree", D(3)="from", and D(4)="".
For example
`RJBotting` has degree `Ph.D.` from `Brunel University`has form(RJBotting, Ph.D., Brunel University).
For example
`RJBotting` has degree `Ph.D.` from `Brunel University`has syntax= expression(BEING) "has degree" expression(qualification) "from" expression(institution).
End of road works.
. . . . . . . . . ( end of section Lower Predicate Calculus(LPC)) <<Contents | End>>
Two predicates are said to be of the same type if they are defined on the same types of variables -- on the same universe of discourse. For example the predicates: even, odd, prime, composite, etc. are all of the same type because they apply to the natural numbers. Similarly: <, >, <=, >=, etc can be thought to be predicates of the same type because they apply to pairs of objects in a common domain.
On predicates of the [ same type ] we can define operations that take two predicates and generate a new predicate.
We can easily show that (&) and (|) on predicates of the same type are associative:
We can assume that (&) and (|) are serial and omit parentheses.
In fact all the properties of a Boolean Algebra will hold:
The result is suspiciously like Set Theory.
It is also a term logic. In term logic you get expressions like:
Red Boxes that are not Large
Small Red Boxesand in MATS we might have
To complete Aristotlean logic we need the following predicates that operate on predicates!
Here are some predicates that operate of predicates:
We are now ready to express (and prove) the classic medieval syllogisms [ ../samples/syllogisms.html ] in MATHS.
. . . . . . . . . ( end of section Operations on Predicates) <<Contents | End>>
Introduction to Logic: [ logic_0_Intro.html ]
Properties of Equality: [ logic_11_Equality_etc.html ]
Proofs: [ logic_2_Proofs.html ]
Sets: [ logic_30_Sets.html ]
Relations: [ logic_40_Relations.html ]
Maps and Functions: [ logic_5_Maps.html ]
Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.
The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.
For a complete listing of pages in this part of my site by topic see [ home.html ]
For a more rigorous description of the standard notations see