I was wondering if first-order logic can be reduced to propositional calculus if we eliminate quantification.

For example, instead of saying “for all x in a domain D, P(x)”, we could state “P(x)” for every element in D, with conjunction:

∀ x[P(x)] = P(x1) ∧ P(x2) ∧ P(x3) ∧ ...

I also wonder if the necessity operator of modal logic be used to define the notion of an “arbitrary constant”, in FOL; by saying “an arbitrary constant is a symbol ‘alpha’ for which, for some x in D, x necessarily equals alpha”:

α is an arbitrary constant iff ∃x[■(x = α)]

Does this definition have merit?

You can use it to prove:

P(α) → ∀x [P(x)]

which leads directly to the second rule of inference of Rosser's system RS_1.

Suppose you don't include the symbol for necessity, and define an arbitrary constant of FOL as follows:

α is an arbitrary constant iff ∃x[x= α]

Suppose P(α).

Then P(α) ∧ [x1=α ∨ x2=α ∨ ... ].

Then you only get:

P(x1) ∨ P(x2) ∨ P(x3) ∨ ...

But if you have the necessity operator then you get:

P(α) and ["x1 = α "is necessary or "x2=α " is necessary or..]

So distributing the P(α) we have for the first disjunct:

P(α) and "x1=α" is necessary.

That seems to mean P(x1).

For the second disjunct we have:

P(α) and "x2=α" is necessary.

That seems to mean P(x2).

Therefore, with the modal operator for necessity in the definition of arbitrary constant of FOL, we get the sequence:

P(x1) ∧ P(x2) ∧ P(x3) ∧..

Which is the statement in FOL, that

∀ x [P(x)].

Thus we can derive using the propositional calculus, and a few definitions, the second rule of inference R2 of Rosser's system, because we can prove

P(α) → ∀ x [P(x)]

We now only need to prove postulates 4, and 5 of RS_1, to reduce FOL to the propositional calculus.

Is there anything wrong with defining an arbitrary constant of FOL, using the necessity operator?

  • The above def of the quantifier is only intuitive. If we want to define "all" for a domain whatever, that can have an infinite number of elements, listing "all" the elements, we are not defining anything. Commented May 13 at 16:47
  • Regarding the purported def of alpha, that is not a definition. A def must allow us to replace the defined term (alpha) with its definition. In your case this is not possible. Commented May 13 at 16:49
  • 1
    You cannot eliminate the quantifiers without loss. (∀x)Px does not just amount to P(a1) ∧ P(a2) ∧ P(a3) ... To capture the sense of 'for all' we need to add at the end; "and that's all the a's there are". Furthermore, if the domain is infinite, then we cannot specify all the conjuncts, because, in standard logic, formulas are required to be of finite length.
    – Bumble
    Commented May 14 at 16:42
  • Can you provide a link or a quote about “Rosser’s system RS1”? I wasn’t able to find any good overviews. Commented May 14 at 17:24
  • 1
    @JuliusHamilton See Rosser's book, Logic for Mathematicians, page 102. Available here
    – Bumble
    Commented May 14 at 22:09

1 Answer 1


I was mistaken about the definition of an arbitrary constant. You don't need the modal operator for necessity. The following definition seems good to me currently.


α is an arbitrary constant iff ∀x [x = α] ∨ ∃!x[x= α]

This will stand up to scrutiny if you can't conclude x1=x2=x3=...

Suppose P(α), where α is an arbitrary constant, and ¬∃!x[x=α] then

P(α) ∧ [x1 = α ∧ x2 = α ∧ x3 = α ∧ ... ]

You can't use the transitive property of equality to conclude x1=x2=x3=..., because α is not necessarily a symbol in the official sense of the word symbol, and the transitive property of equality, applies only to terms that are necessarily symbols.

Transitive property of equality

For any symbols x,y,z: if x=y & y=z then x=z.

C s a symbol iff C symbolizes exactly one thing.


C is a specific constant iff ∃!x[x = C]

In the case of an arbitrary constant such as α, it doesn't necessarily symbolize exactly one thing, so the transitive property of equality simply does not apply to it.

Thus, we can get

P(x1) ∧ P(x2) ∧ P(x3) ∧...

Now using the definition of the universal quantification of a propositional function we get

∀x [P(x)]

Note: we must postulate that every thing has at least one name.

Now we close the scope of the assumption to get

P(α) ∧ ¬∃!x[x=α] → ∀x [P(x)]

Which leads to Rosser's second rule of inference R2 see my post here The smallest possible formal definition of FOL

Thus we can reduce FOL to the propositional calculus if we can prove Rosser's postulates 4 and 5.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .