4
$\begingroup$

There may be some theoretical literature, unknown to me, that addresses this question. If possible, I would like a practical approach to this problem. My attempt involves the use of an equational specification language called CafeOBJ (see introduction). In particular, the BOOL module can be viewed as a formalisation of propositional logic defined by a set of equations. My basic idea is to transform First Order Predicate Logic sentences (FOPL) into order-sorted equations consisting of Boolean valued functions (BVF). Then in proofs the BVF are instantiated with constants and proofs are executed using term rewriting. See related question. My main concern with the proposed approach is that variables are in scope for the entire transformed sentence. There can be no nested or local quantifiers within a sentence. It seems that equational deduction used in the proposed proofs is sound and complete.

Below, I present my proposed translation, proof method, and an example.

Translation

FOPL sentences are transformed to equational form as follows.

  • Predicates are converted to BVFs.
  • All variables are assumed to be universally quantified.
  • Skolem constants and functions are used to represent existential quantified variables.
  • The translated sentences are written on the right hand side of equations.
  • The left side of the equations is a named BVF whose arguments are the variables necessary for the right hand side translated sentence.

For example the FOPL sentence

$\forall x (\forall y (Animal(y) \implies Loves(x,y)) \implies (\exists z Loves(z,x)))$

Would be translated in the following order-sorted CafeOBJ equation:

eq s1(x:Person,y:Animal)  = loves(x,y) implies loves(G(x),x)  .

The variables are each given a sort or type. Note, the Skolem function $G(x)$ has only one argument because the $y$ in the antecedent is not in scope in the consequent. The general form of which is $LeftEqName_1(Args)=Expression_{BVF}$. Because we have sorts (or types) in CafeOBJ, we do not need the predicate $Animal(y)$.

Proof

A combination of Equational Logic, Boolean Algebra, and order sorted term rewriting is used for proof. The general form of the proof is:

$(LeftEqName_1(InstantiatedArgs) \land LeftEqName_2(InstantiatedArgs) \land \dots \land LeftEqName_n(InstantiatedArgs)) \implies BVF$ .

This is intended to represents an implication whose antecedent is the conjunction of the original FOPL sentences. The consequent ($BVF$) is the Boolean valued function to be proved. I have only considered this idea for single $BVF$s, I have not considered more complex expressions in the consequent. Universal quantified variables in the original equations are replaced by fresh constants in the proofs.Universal quantified variables can also be instantiated by constants from the original set of FOPL sentences. The Theorem of Constants states that universal variables in the original equations can be replaced by fresh constants in a proof. The Theorem of Constants is broadly similar to universal elimination. Perhaps the Deduction Theorem might provide the formal basis of my proposed proof method.

I use CafeOBJ's term rewriting command called reduce , which recursively matches each term with the appropriate left-hand side of an equation and replaces it with the right-hand side, CafeOBJ reduces a logical formula into an exclusive-or normal. A term of Bool reduces to an exclusive disjunction of conjunction. It is known that the exclusive-or normal form is true if the input term is valid, and false if it is unsatisfiable.

Example

Below is a CafeOBJ order sorted example of the proposed method. In this case no universals are needed in the proof, we only need constants from the original FOPL sentences. I also include a single-sorted FOPL version that uses natural deduction in its proof.

   mod* CURIOSITY-EQL-OSA {
    [Cat < Animal Person < Thing ]
    pred    kills  : Person Animal
    pred   loves : Thing Thing
    op tuna  : -> Cat 
    ops jack  curiosity : -> Person
      
    preds  s3 s6 : Thing
    preds s4 s5 :
    pred s1   : Person  Animal
    pred s2   : Person  Person 
    op G : Person   -> Person
    op F : Person   -> Animal
    -- Everyone who loves all animals is loved by someone.
    eq s1(x:Person,y:Animal)  = loves(x,y) implies loves(G(x),x)  .
    -- Anyone who kills an animal is loved by no one.                      
    eq s2(x:Person,y:Person)  =    kills(x,F(x)) implies (not (loves(y,x))) .                      
    -- Jack loves all animals.
    eq s3(x:Animal) = loves(jack,x)  . 
   -- Either jack or curiosity killed tuna the cat
    eq s4 =   kills(curiosity,tuna) or kills(jack,tuna) .
    }
    
    open CURIOSITY-EQL-OSA .
    --> Show that jack did not kill any animal
    red (s1(jack,F(jack)) and s2(jack,G(jack))  and s3(F(jack))) implies (not (kills(jack,F(jack)) )) .
    --> Use existential generalization (existential introduction).
    let s4a =   kills(curiosity,tuna) or kills(jack,F(jack)) .
    red ((not kills(jack,F(jack))) and s4a) implies kills(curiosity,tuna) .
    --> Gives true
    close
    -- Alternatively
    open CURIOSITY-EQL-OSA .
    eq F(jack) = tuna . -- assume tuna is the animal jack kills (a contradiction).
    red (s1(jack,tuna) and s2(jack,G(jack)) and s4 and s3(tuna)) implies (kills(curiosity,tuna) ) .
    --> Gives true
    close

Single sorted first order sentences and proof

First Order Formalisation and proof

The FOPL proof uses natural deduction. Lines 1-6 are axioms which are assumed to be true. The justification for each proof step are listed on the right. The text ‘FO Con’ means first order consequence, which uses well known FOL proof techniques e.g. Line 16 is justified by disjunctive syllogism from lines 4 and 15.

$\endgroup$
5
  • $\begingroup$ Having asked someone in the know, I believe that my translation is satisfiable if and only if the original FOLis satisfiable (equisatisfiable). $\endgroup$ Oct 12 '20 at 18:00
  • 1
    $\begingroup$ Yes, they are equisatisfiable. $\endgroup$
    – ShyPerson
    Oct 13 '20 at 5:24
  • 1
    $\begingroup$ But equisatisfiability is not enough. The problem that remains is to show that the subsystem of CafeOBJ3 in question has the same deductive power as first order logic. In particular, first order logic is complete, so this subsystem of CafeOBJ3 must be shown to be complete. $\endgroup$
    – ShyPerson
    Oct 14 '20 at 0:45
  • $\begingroup$ @ShyPerson Equisatisfiability of the translation may be enough for my purposes. I wish to prove certain first order axioms hold in some model. I wish to show that certain ontological axioms hold in CafeOBJ's functional programming sub-language (an initial algebra). I suppose I should re-ask the question in terms of equisatisfiability. $\endgroup$ Oct 14 '20 at 10:44
  • 1
    $\begingroup$ Yes, probably best to ask a new separate question. $\endgroup$
    – ShyPerson
    Oct 14 '20 at 23:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.