Is a logic system with predicate symbols, individual constants, negation, and conjunction (no variables and no quantification) decidable?

Question

Suppose I have a logical system with predicate/relation symbols and individual constants symbols, negation and conjunction, but no variables or quantification. For instance, suppose I have the individual constants a and b, and a 2-place predicate P, in the language. I can formulate atomic sentences like P(a, b) or P(b, a). Suppose also that negation and conjunction are available, so I can formulate complex sentences like P(a, b) & P(b, a) or -P(a, b) (where & is the conjunction symbol and - is the negation symbol).

Is this decidable, in the way that propositional logic is? Or do I need to add variables and quantification before it becomes undecidable?

(How would this be different from propositional logic, anyway?)

Answer 1

You need quantification to make your system essentially different from propositional logic. Given a formula $\phi$ with no quantifiers, pick a distinct propositional variable $v_{xy}$ for each atomic predicate $P(x,y)$ occurring in $\phi$. Let $\phi'$ be the formula of propositional logic obtained by replacing $P(x, y)$ by $v_{xy}$ throughout $\phi$. Then $\phi$ is valid iff $\phi'$ is valid.

Answer 2

In order for the structure to be valid, the initial sentence (if A then B), and the inverse, converse, and contrapositive would have to bear their correct truths. If you observe an event, and it is true, but its contrapositive is false, then your original event was either the inverse or converse of a different truth table. In short, your whole axiomatic structure has to be consistent. As for your abbreviated syntax, what I see is a computer application, in that: The statement -P(a,b) can be read "If -P(a,b) exists (as input or output), then TRUE." But in that case, your statement is the Predicate in another structure.

So I'd say that if you can't pull out of your structure any theorems that are amalgams of your atomic statements which would negate the axioms/atomic statements, AND there are no other theorems which can be assembled within your structure from your statements and operators that would afford 'floating' answers ( like in buffers), then it would be decidable by definition, though I would look for reducibility. Karnaugh maps are nice because they do it ( reducing a logic structure to the fewest gates {or least number of embedded theorems}) in a third-grade chart. Consider the T/F status for 2=2 and x=2: the first is an atomic statement that is always true. The second is true IFF x has the value of 2.