.Open Lower Predicate Calculus
The lower predicate calculus ($LPC) with equality is a standard logic that
can be applied to a wide range of situations where we have objects
or individuals to talk about.
Michael Jackson argues strongly that
$LPC is clearest language for stating and clarifying:
.Set
Domain knowledge that is assumed about the world in which software is placed.
Things that a client or user requires to be true when the software is in place.
Specifying how the software should work.
How a program behaves.
How the platform (machine) works.
.Close.Set
For an extended and readable discussion see
.See [Jackson95]
and the following references
.Find Jackson.*9
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
.Key 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:
.Box
All humans are Mortal.
Socrates is a human.
Therefore:
Socrates is mortal.
.Close.Box
In the MATHS notation and assuming a domain of discourse or type
symbolized by `Being`, then $LPC is input like this:
.As_is |- for x:Beings, if human (x) then mortal(x).
.As_is |- human(socrates).
.As_is ()|-mortal(socrates).
It is rendered to look like this:
.Box
.As_is |- for x:Beings, if human (x) then mortal(x).
.As_is |- human(socrates).
.As_is ()|-mortal(socrates).
.Close.Box
Lewis Carroll gives us an example of a plausible but wrong
argument:
.Box
Alice saw nobody on the road.
The mad hatter arrived before nobody did.
Therefore
Nobody is slower than the mad hatter.
.Close.Box
In $LPC the error is exposed:
.Box
for no x:Beings ( saw(alice, x) ).
for no x:Beings ( before(the_mad_hatter, x) ).
slower(nobody, the_mad_hatter)
.Close.Box
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 \TeX \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
.See ./logic_11_Equality_etc.html
or return to the introduction:
.See ./logic_0_Intro.html
or list of logical items
.See ./home.html#Logic
. Syntax
|- (basis): $PROPOSITIONS.
|- $LPC.
PROPOSITIONS::=following,
.Net
simple_proposition::@#lexemes, given.
formula_in_a_different_language::@#char, given.
proposition::= $equivalences |$implication,
equivalences::= $implication #( "iff" $implication),
implication::= disjunction |"if" $proposition "then" disjunction O("else" $implication)|$clausal_form,
clausal_form::=disjunction ":-" conjunction | conjunction "-:" disjunction,
|-(dis_syn): $SERIAL(disjunction, conjunction, "or", or, @),
() |- disjunction = conjunction #("or" conjunction)
|-(con_syn): $SERIAL(conjunction, $elementary_proposition, "and", and, @),
() |- conjunction = $elementary_proposition #("or" $elementary_proposition)
elementary_proposition::= $O("not")( "(" $proposition ")" | $simple_proposition | $formula_in_a_different_language),
.Close.Net
PC::=$Propositional_Calculus.
Propositional_calculus::= $PROPOSITIONS( simple_proposition= propositional_variable, formula_in_a_different_language=>{}).
LPC::=$Lower_Predicate_Calculus_with_equality.
Lower_Predicate_Calculus_with_equality::=following,
.Net
|-(LPC1): $PROPOSITIONS(simple_proposition=>predicate).
predicate::= propositional_function | $equality | $parallel_form | $set_theoretical_proposition | $relational_proposition | $quantified_proposition |...,
propositional_function::= expression(@) | natural_predicate | formula_in_a_different_language,
natural_predicate::=#(word_in_dictionary | expression) & $fits_template.
equality::= expression "=" expression #("=" expression) & $correct_types,
Equality is only defined between objects of the same type:
correct_types::= |[T:Types] (expression(T) "=" expression(T) #("=" expression(T))).
|-(LPC2): $PARALLEL(expression,"=").
. Note
The alternative of defining `x=y` to be false unless they have the same type leads to a paradox:
PARADOX::=Net{
|- For T1,T2:Types, x:T1, y:T2, if T1<>T2 then (x=y)=false.
T1,T2:Types, t:T1,
|- T1<>T2.
F::@^T2=not((_)=t).
G::@^T1=not((_)=t).
F has type @^T2 and G type @^T1 and so not(F=G) and yet they have the same expression.
(F)|-For all x:T2 ( F(x) ).
(G)|-For all x:T1( G(x) iff x<>t ).
}=::PARADOX.
parallel_form::= (expression relation expression #(relation expression) ) & correct_typed_relations,
|- For e:#(relation expression), R, S:relation, x, y:expression, x R y S e in correct_typed_relations iff x in dom(R) and y in cod(R)=dom(S) and e in cod(S),
|- For e:#(relation expression), R, S:relation, x, y:expression, if x R y S e in correct_typed_relation then x R y S e = (x R y) and (y S e).
quantified_proposition::= ("for"|"For") quantified_variable #( "," quantified_variable) ( "(" proposition ")" | implication ).
quantified_variable::= quantifier binding,
.See ./notn_12_Expressions.html#binding
quantifier::= ((|"all") |"some" |"no" |"one" | $number |$set_of_numbers |"abf" |"most" | "(" expression "%)" | "generic" ,
number::= digit #digit | "("expression(Nat0)")",
set_of_numbers::= "("expression(@Nat0)")" |$number ".." | ".." $number |$number"..*" | "*.." $number | $number".."$number | "any",
definite_description::= "the" set_expression | "the" structured_class_name "(" ( expression(@) | L(key_component"=>"value") ")" |"the" "(" $loose_binding "||" proposition")"|"the" $loose_binding "(" proposition")".
loose_biding::=http://www/dick/maths/notn_12_Expressions.html#loose_binding.
. More on equality quantifiers descriptions
.See ./logic_11_Equality_etc.html
. Lexemes
all::lexeme="all", universal $quantifier.
some::lexeme="some", existential $quantifier.
no::lexeme="no", negative universal $quantifier.
one::lexeme="one", unique $quantifier.
most::lexeme="most", mathematical $quantifier.
generic::lexeme="generic", mathematical $quantifier.
the::lexeme="the", definite article, only used when a unique object fits.
.Close.Net
. Meta-language
The following are meta-linguistic ideas. They are used, privately,
to discuss the properties of equality:
META_LPC::= $LPC with (predicate:=definition(predicate) | identity, identity ::= expression "==" expression).
. Semantics
|- $LPC.
Propositions have two possible meanings - true and false. The following tables
summarizes how these values combine with respect to the operators
of 'not' 'and', 'or' 'iff' 'if__then_'.
.As_is ===========================================
.As_is P true false
.As_is --------------------------------------------
.As_is not P false true
.As_is ===========================================
.As_is P true true false false
.As_is Q true false true false
.As_is --------------------------------------------
.As_is P and Q true false false false
.As_is P or Q true true true false
.As_is P iff Q true false false true
.As_is if P then Q true false true false
.As_is ===========================================
.
(above)|- (@,or,false,and,true,not) in Boolean_algebra.
Equivalences are PARALLEL operators,
(above)|- P iff Q iff R ... ::= (P iff Q) and (Q iff R) and...
|-(if P then Q else R) = (if P then Q) and (if not P then R)
(previous, boolean algebra)|- if P then Q else R = (P and Q) or ((not P) and R).
The $clausal_form `P:-Q` is used in Prolog and some other systems:
For P:disjunction, Q:conjunction, (P:-Q) ::= if Q then P.
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)`.
. Equality of propositions
LPCe::=http://www/dick/maths/logic_11_Equality_etc.html
(LPCe)|- if (P=Q) then (P iff Q).
|-(PC_equal): if (P iff Q) then (P=Q).
(-1)|- (P iff Q) iff (P=Q).
(-1)|- (P iff Q) = (P=Q).
So equivalent propositions can be substituted for each other.
(This rule is listed separately in the section on proofs).
Further, Since '<>' indicates the negation of '=' (in $LPCe) it follows that
(-1, LPCe)|- (P<>Q) = not(P iff Q).
Since many call this the "exclusive or" operator we can define
P xor Q::@= (P<>Q).
. Summary of Logical operators
.Table P Q P=Q P<>Q P and Q P or Q
.Row true true true false true true
.Row true false false true false true
.Row false true false true false true
.Row false false true false false false
.Close.Table
. Predicates
Informally a predicate is a proposition with zero or more variables in it.
These variables can be be of different types. To be able to determine
whether or not a predicate is true or false all its variables must be given
values. Associated with any predicate is function of type
@^(T1>=n then for some x, y, z(w=x y z and y<>"" and |x y| <=n and for all k:0..* (x y^k z in L))
For all CFL L, some n, all z:L, if |z| >=n then for some u, v, w, x, y (z=u v w x y and v x<>"" and |v w x| <=n and for all i:0..* (u v^i w x^i y in L))
.Close.Net
Definition of the
.Key big O
.Key asymptotic
notation for functions.
.Net
For f,g:Nat0->Positive & Nat0, f is_big_O g::= for some c:Nat0,n0:Nat0, all n > n0 ( f(n) <= c* g(n) ).
For f:Nat0->Positive & Nat0, bigO(f)::= {g:f:Nat0->Positive & Nat0. for some c:Nat0,n0:Nat0, all n > n0 ( f(n) <= c* g(n) )}.
.Close.Net
. Tight bindings
A tight binding introduces a variable with a fixed values. They are
an abbreviation:
For x:variables, W : propositions, e:expressions, (for x:=e (W)) ::= (e.[x]W), (e.[x]W) extracts the free 'x's in W and replaces them by 'e's.
|-(example) for x:=2(x*x=4) = (2*2=4) = true.
(def)|- For x:variable,W:propositions, e, (for x:=e(W)) = e.[x](W).
For Q1,Q2:quantifiers, x, x1, x2:variables, W: propositions, e:expressions, (for x1:=e, Q2 x2:X2 (W)) ::= for x1:=e ( for Q2 x2:X2(W)),
For Q1,Q2, x, x1, x2, W, e, (for Q1 x1:X1, x2:=e (W)) ::= for Q1 x1:X1 (for x2:=e (W)).
For x:variables, W1(x),W2(x) : propositions, (for x:X,if W1(x) then W2(x)) ::= for all x:X(if W1(x) then W2(x)).
. Natural Abuses of Notation
For x:variables, W1(x),W2(x) : propositions, (for x:X, W1(x)(W2(x))) ::= for all x:X(if W1(x) then W2(x)).
The following idiom is both common and natural:
`For all Real x, some Real \epsilon where \epsilon>0, all Real \delta where \delta<\epsilon....`
This is taken to be an abbreviation for
`For all x:Real, some \epsilon:{ x:Real || \epsilon>0}, all \delta:{ x:Real ||\delta< \epsilon},...`
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:
For Q:quantifiers, x: variables, W: propositions, S: name_of_set, (Q S x where W) ::macro= Q x:{x:S|| W},
For Q:quantifiers, x: variables, S: name_of_set,(Q S x) ::macro= Q x:S.
.Close Definitions of Quantifiers
. Very abreviated quantifiers
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,
for all 2*i=j, one 4*k=2*j.
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))).
.Close.Net
Roadworks::=following,
.Net
This is experimental: If you have any better ideas about ways to make
formal the way we normally write things I would be interested in
hearing about them.
. Natural, distfix, or mixfix predicates
Idea a definition like this
.As_is 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:
.As_is `RJBotting` has degree `Ph.D.` from `Brunel University`
template:@TEMPLATE,
for all s:#char, 0..1 template t ( s in syntax(t) ).
fits_template::= |[t:template](syntax(t)).
TEMPLATE::=Net{
A template is a sequence of delimeters and arguments.
delimiters::%delimiter.
d:=delimiters.
delimiter::=%( word_in_dictionary ~ ("and" | "or" | "not" | "if" | "then" | "else" | "the" |"a" | "for" |"For" | "set" | "map" | "Net" | "Let" ) ).
For example
.As_is `RJBotting` has degree `Ph.D.` from `Brunel University`
has delimiters ("", "has degree", "from", "").
example0::=`sort (2,1,4,3) into (1,2,3,4)`.
example1::=Net{ delimiters=("sort", "into", ""). ...}.
types::%(Types~{@}). --to avoid ambiguities no Boolean arguments.
example2::=Net{ delimiters=("sort", "into", "").
types=(%Nat, %Nat).
...
}=::example2.
arity::0..* = |types|, -- the term arity comes from Prolog.
a:=arity.
For example
.As_is `RJBotting` has degree `Ph.D.` from `Brunel University`
has 4 delimiters (the first and last are "" null) and so `a`, the arity, is
3.
(nbr_of_delimiters): |d|=a+1. -- d for number of delimiters
(no_empty_delimiters): not ( "" in d(2..a) ) -- only the first and last delimiters can be null.
example3::=Net{ $example2.
delimiters=("sort", "into", ""). types=(%Nat, %Nat).
a=2, |d|=3, ""=delimiters(3).
...
}=::example3.
D::1..a+1->@#lexeme=map[i:1..a+1] (! [w:pre(d(i))](d(i)(w) ) ).
For example
.As_is `RJBotting` has degree `Ph.D.` from `Brunel University`
has delimiters D(1)="", D(2)="has degree", D(3)="from", and D(4)="".
example4::=Net{ $example3.
D(1)={"sort"}, D(2)={"into"}, D(3)={""}.
...
}=::example4.
form::(1..a->@#lexeme)->@#lexeme= fun[v](D(1) ! v(1) ! ![i:2..a](D(i) v(i)) ! D(a+1) ) ).
For example
.As_is `RJBotting` has degree `Ph.D.` from `Brunel University`
has form(`RJBotting`, `Ph.D.`, `Brunel University`).
example5::=Net{ $example4.
form( e1, e2 )={"sort"} e1 {"into"} e2 {""}.
...
}=::example5.
syntax::@#lexeme= form(expression o types).
example6::=Net{ $example5.
syntax={"sort"} expression(%Nat) {"into"}expression(%Nat) {""}.
...
}=::example6.
For example
.As_is `RJBotting` has degree `Ph.D.` from `Brunel University`
has syntax= expression($BEING) "has degree" expression(qualification) "from" expression(institution).
meaning:: >@.
|-for v1:types(1),v2:types(2),...v(a) :types(a), meaning(v1, v2,...v(a)) in @.
example7::=Net{ example6.
meaning::(%Nat)><(%Nat) -> @. meaning( (2,3,4,1), (1,2,3,4) ) :@.
...
}=::example7.
definitions::@#lexeme= | [v:(1..a-->variable), p:1..a---1..a]( "For" v(p(1)) ":" representation(t(p(1))) ! ![i:1..a]("," v(p(i)) ":" representation(t(p(i))) "," ! form(v) ":"":""=" representation(meaning(v)) ).
End of road works.
}=::TEMPLATE.
.Close.Net Roadworks
.Close Lower Predicate Calculus(LPC)
.Open Operations on Predicates
These ideas are new and untried but seem to be natural and
sanctioned by a long tradition in formal logic going back to
Aristotle. Indeed Fred Sommers and others have been championing
$TFL:
TFL::="Term Functor Logic".
Two predicates are said to be of the
.Key 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
.See same type
we can define
operations that take two predicates and generate a new predicate.
For T:Types, F,G: @^T.
F & G ::= map[x:T](F(x) and G(x)).
F | G ::= map[x:T](F(x) or G(x)).
~F ::= map[x:T](not F(x)).
F ~ G ::= F & (~G).
We can easily show that (&) and (|) on predicates of the same type
are associative:
F & (G & H) = (F & G) & H.
F | (G | H) = (F | G) | H.
We can assume that (&) and (|) are serial and omit parentheses.
In fact all the properties of a Boolean Algebra will hold:
()|- BOOLEAN_ALGEBRA(@^T, &, |, ~, ...).
The result is suspiciously like Set Theory.
It is also a term logic.
In term logic you get expressions like:
[R+B-L]
.As_is Red Boxes that are not Large
.As_is Small Red Boxes
and in MATS we might have
R & B ~ L.
To complete
.Key Aristotlean logic
we need the following
predicates that operate on predicates!
Here are some predicates that operate of predicates:
no F ::@ = for no x(F(x)).
all F ::@ = for all x(F(x)).
some F ::@ = for some x(F(x)).
F==>G ::@= for all x(if F(x) then G(x)).
F overlaps G ::@= some(F&G).
We are now ready to express (and prove) the classic medieval syllogisms
.See ../samples/syllogisms.html
in MATHS.
.Close Operations on Predicates
. See Also
Notations:
O::=optional
SERIAL::=http://www/dick/maths/math_11_STANDARD.html#SERIAL
PARALLEL::=http://www/dick/maths/math_11_STANDARD.html#PARALLEL
Introduction to Logic:
.See http://www/dick/maths/logic_0_Intro.html
Properties of Equality:
.See http://www/dick/maths/logic_11_Equality_etc.html
Proofs:
.See http://www/dick/maths/logic_2_Proofs.html
Sets:
.See http://www/dick/maths/logic_30_Sets.html
Relations:
.See http://www/dick/maths/logic_40_Relations.html
Maps and Functions:
.See http://www/dick/maths/logic_5_Maps.html