Equational Logic and First Order Predicate Logic

[026...@dit.ie]

"
Hi,
I am interested in using Equational Theories together with Equational Logic (EL) found in algebraic specification languages (CafeOBJ[1]) to represent and prove sentences in First Order Predicate Logic.
The advantage of such an approach is that one can easily map loose theories written pseudo-FOPL to more concrete theories which may have initial models (using views).
Translating FOPL to EL seems to require auxiliary techniques such as Skolemization and sentences splitting.
I am concerned that there maybe some FOPL sentences which cannot be represented using EL even using these auxiliary techniques.
I am aware that in general EL is regarded as a sub-logic of FOPL and any valid EL theorem is a valid FOPL theorem (but not vice versa).
Goguen and Malcolm [2] describe FOPL as the *background* for equational proof scores in OBJ which was a predecessor of CafeOBJ[1]/Maude. They also provide general advice on how use EL to prove FOPL theorems.

I am using an example from COQ[3] which I have written as two CafeOBJ theories or loose specifications.
They are my two attempts to represent FOPL in EL. I am not sure if the approaches are valid.

Here is the description of the relation R from [3].
Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.
Prove that R is reflexive in any point x which has an R successor.
For any x and y, R x y implies R y x by symmetry, then by transitivity, we have R x x.
Symmetry and transitivity are not enough to prove reflexivity, we must also assume the x is related to something (e.g R x ? or R ? x exists).


Consider the 2 equations labelled PROPERTY in the module TRANSITIVE1 and EQUATION in the module TRANSITIVE2.

My questions are these:
Q1.
Does the PROPERTY equation and its reduction represent and prove reflexivity? The results of the reductions would appear to represent a proof.

Q2
Does the reduction of the EQUATION in TRANSITIVE2 prove reflexivity? I use a form selective application of bi-directional rewriting.
This form of rewriting is highly controller by the user.
Space does not permit a full description, but in this case the condition in the EQUATION is executed first and the assumption R x Y is applied during the rewriting process.
We could describe this as a manual proof with some machine support.

Q3
How do these approaches differ? Form my web searches I get *implicit* and *explicit* as follows:
The implicitly specification of function or relation asserts property that its value must satisfy.
Implicit definitions take the form of a logical predicate over the input and result variables gives the result's properties.
This approach seems to be distinct from the normal Peano style equational axioms (e.g. N + 0 = N).
The PROPERTY approach seems to fit this description.
Explicitly defined functions or relations are those where the definition can be used to to calculate an output from the arguments.
The EQUATION approach seems to fit this description.
Are these reasonable distinctions?

Regards,
Pat Browne

[1] CafeOBJ http://www.ldl.jaist.ac.jp/cafeobj/
[2] Algebraic Semantics of Imperative Programs, by Joseph Goguen and Grant Malcolm, page 85, http://cseweb.ucsd.edu/~goguen/sys/objcourse.html
[3] 1.4 predicate Calculus. http://coq.inria.fr/1-basic-predicate-calculus
"

**> This is a loose module describing all models where the equation labelled PROPERTY holds.
mod* TRANSITIVE1 {
**> One sort or type called D.
[ D ]
**> A constant which ensures that transitivity holds
op Y : -> D
**> The symmetric property is asserted by CafeOBJ's commutativity property.
op R__ : D D -> Bool {comm}
op P : D D D -> Bool
vars x y z : D
eq [PROPERTY] : P(x,z,y) = ((R x y) implies (R y z)) implies (R x z) .
}
**> Normal rewriting
open TRANSITIVE1 .
red P(x,x,Y) . -- Gives R x x
red P(x,x,Y) implies R x x . -- Gives true
close

**> A loose module describing all models where the equation labelled EQUATION holds.
mod* TRANSITIVE2 {
[ D ]
op R__ : D D -> Bool {comm}
op P : D D D -> Bool
vars x y z : D
**> Normal rewriting cannot deal with extra variable y in the condition on the RHS.
ceq [EQUATION] : R x z = true if ((R x y) implies (R y z)) .
}

open TRANSITIVE2 .
**> Using start/apply
op X : -> D .
**> If any variable x is related to arbitrary constant X
eq [e1] : R x X = true .
**> Then the arbitrary constant is related to itself.
**> CafeOBJ's start/apply commands allow selective bi-directional rewriting
start R X X .
apply .EQUATION at term .
apply .e1 at ( 1 ) .
apply .e1 at ( 2 ) .
apply reduce at term .
**> Result true : Bool
**> Apply/start is not available in Maude but I imagine the Maude's ITP could be used to prove the above.
eof

--


This email originated from DIT. If you received this email in error, please
delete it from your system. Please note that if you are not the named
addressee, disclosing, copying, distributing or taking any action based on
the contents of this email or attachments is prohibited. www.dit.ie

Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí
earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an
seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon
dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa
ríomhphost nó sna hiatáin seo. www.dit.ie

Tá ITBÁC ag aistriú go Gráinseach Ghormáin - DIT is on the move to
Grangegorman <http://www.dit.ie/grangegorman>