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
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.
