# Encoding Predicate Calculus in Propositional Logic

I'm taking a course in logic. Propositional calculus is adequate enough to represent the logical structure of truths which are stated in any language mappable to variables in the calculus.

Now it would seem to me that predicate calculus is defined based on a finite number of specifications. This should then allow me to encode the truth structure of predicate calculus using the propositional calculus. The means of doing this would be by encoding the category of a statement in the predicate calculus as a symbol in a propositional sequent.

A very simple example: for any x: if x then $$Fx$$, x, $$\implies$$ $$Fx$$.

Here I would assign to $$A$$ the prefix "for any $$x$$"
$$B$$ encodes an if statement on the same variable the statement which $$A$$ represents is conditioned on.

$$C$$ represents assigning an arbitrary proposition to the variable which $$B$$ is conditioned on.

$$D$$ represents the presence of that variable.

I would then state as a given $$A\&B\&C\&D \implies C$$

This particular encoding is not the best one because it is not necessarily consistent with all the possibilities of predicate calculus. It's beyond me at this point to determine how difficult it would be to represent the structure of some number of predicate calculus sequents using an encoding in propositional calculus but I sense it can be done. My question then is how to go about determining how to do so.

• I'm dubious that this can be done, though I might not be understanding what you are trying to accomplish. In a natural sense the predicate calculus extends and subsumes the propositional calculus. However the propositional calculus is decidable and the predicate calculus is not. Commented Aug 31, 2020 at 22:58
• I'm no expert. My problem is thinking too much prematurely. Terminating algorithms can be encoded in the propositional calculus. I'm wondering if I can encode in the propositional calculus an algorithm which can generate true statements about a sequent in the predicate calculus. I would need to manually create new variables to represent the instantiation of instances of free variables each time a new scope in the predicate calculus is entered. Commented Sep 1, 2020 at 2:55
• It would be attractive if we could somehow reduce the solution of questions in the predicate calculus to questions in the propositional calculus (although SAT is an NP-complete problem). But we cannot do this in general because the predicate calculus is undecidable. You might be interested in a decidable subset of logic called Horn clauses. Commented Sep 1, 2020 at 3:47
• A good reference and topic to look at is Herbrandization and Herbrand's theorem. (en.wikipedia.org/wiki/Herbrand%27s_theorem). They allow a kind of reduction of FOL to propositional logic. Also, I suggest you add the reference request tag to your question. Commented Sep 1, 2020 at 5:03
• you can write it as answer. thanks so much; Commented Sep 1, 2020 at 14:47