Is there any problem with quantifying over wff?
Is there any problem if I formalize "any proposition must be true or false" as ?p(p?¬p)?
I know that this can be formalized metalinguistically as something like ??¬?, where ? is any fbf of the object language, an I know that this is not syntatically correct in first order logic, but I want to know if I can set my domain of quantification as the set of all wff of the language in question, and, if so, if is there any problem with using logical operators over the variables being quantified.
For example, the existence of the set of all the contradictions (C) would imply that ?p((p?¬p)?C), with p varying over the set of all the well formed formulas. In this case, I use the conjunction and the negation operator in p, which is a wff and also the variable of quantification.
I know that this can be formalized metalinguistically as something like ??¬?, where ? is any fbf of the object language, an I know that this is not syntatically correct in first order logic, but I want to know if I can set my domain of quantification as the set of all wff of the language in question, and, if so, if is there any problem with using logical operators over the variables being quantified.
For example, the existence of the set of all the contradictions (C) would imply that ?p((p?¬p)?C), with p varying over the set of all the well formed formulas. In this case, I use the conjunction and the negation operator in p, which is a wff and also the variable of quantification.
Comments (10)
Well, it is not possible according to the formation rules...
What occurs after ? is a variable, not a proposition.
I wonder if what you are doing would be better served by modal logic. That is, what are you saying with ?p(p?¬p) that couldn't be said with ?(p?¬p)?
I want to formalize "to any sentence p, p is a member os S if and only if ¬p is not a member of the set S", that is, ?p(p?S?¬p?S), but I don't know how to do this.
I think I could something like ?x(Wx?(S(x)?¬S(N(x)))), with W(x) meaning "x is a well formed formula", S(x) meaning "x is a member of the set S" and N(x) meaning the definite description "the negation of x", x being a sentence. But this seems quite artifitial to me.
"For any proposition P, either P or not-P" is a perfectly cromulent sentence.
Hmmm. I'll leave you to it, then. There's too many dragons involved in having propositions range over other propositions.
A theory that permits self-referential definitions is called an impredicative theory. An example of a theory that permits defining a proposition by quantification over the set of all propositions is the calculus of inductive constructions with an impredicative sort of propositions, the basis of the proof assistant Coq. This theory is sound (and consistent) but lacks a decidable proof theory. My point is that given the right choice of logic, there is no problem with impredicative definitions. You simply have to accept the consequence that your logic might not be decidable. This isn't a huge sacrifice, as evidenced by the enormous number of people who successfully use such logics.
A set of propositions is isomorphic under encoding to the set of the Gödel numbers of these propositions, and therefore isomorophic to a set of natural numbers, i.e. a subset of [math]\Bbb{N}[/math].
So, it would be a proposition that ranges over a set of numbers.
I think that this practice could work fine, if the set's membership function is a computable function. It could conceivably just be an exercise in standard number theory (PA) ...