According to Wikipedia, an open formula is a WFF without quantifiers.
I have read that a propositional function is the same as open formula.
Are both of these statements correct? Is it true that one can't have a propositional function with quantifiers?
On
There does exist such a thing as propositional calculi with quantifiers. This got explored by logicians such as Lesniewski, Lukasiewicz, and Meredith.
Basically, $\forall$p p is equivalent to K01, which is equivalent to 0.
$\exists$p p is equivalent to A01, which is equivalent to 1.
$\forall$p Cpq is equivalent to K C0q C1q.
$\exists$p Cpq is equivalent to A C0q C1q.
Or more generally if we let F(x) stand for any sentence of propositional calculus, then $\forall$xF(x) means K F(0) F(1), where F(0) means that all instances of x in the formula get substituted by 0, and F(1) means that all instances of x in the formula get substituted by 1, and $\exists$F(x) means
A F(0) F(1).
So, as another example let's consider $\forall$pCpC$\forall$qqp. It stands as equivalent to K [C 0 C $\forall$q q 0] [C 1 C $\forall$q q 1] which is equivalent to K C0CK010 C1CK011. Both C0CK010 =1 and C1CK011 = 1, and thus $\forall$pCpC$\forall$qqp is a tautology.
No, propositional calculus does not allow for existential or universal quantification. The reason being propositional calculus is supposed to be "the most bare boned calculus" you can construct to derive "useful" things with. Interestingly enough, even solving for this simple a system is NP-complete, which means that given a formula, finding solutions take exponential time with respect to formula length.
If you want more power, then first-order logic or something similar is the way to go.