.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 http://www/dick/maths/logic_11_Equality_etc.html or return to the introduction: .See http://www/dick/maths/logic_0_Intro.html or list of logical items .See http://www/dick/maths/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 http://www/dick/maths/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 | "any", definite_description::= "the" set_expression | "the" structured_class_name "(" ( expression(@) | L(key_component"=>"value") ")" |"the" "(" loose_binding "||" proposition")"|"the" loose_binding "(" proposition")". .See http://www/dick/maths/notn_12_Expressions.html#loose_binding .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_'. In this table t=true, f=false. .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). ()|- (P iff Q) iff (P=Q). ()|- (P iff Q) = (P=Q). Equivalent propositions can be substituted for each other. . 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)) Definition of the .Key big O notation. 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 template:@TEMPLATE, for all s:#char, 0..1 template t ( s in syntax(t) ). fits_template::= |[t:template](syntax(t)). TEMPLATE::=Net{ 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", and "". 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 and so `a`, the arity, is 2. (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