Is there any problem with quantifying over wff?

Nicholas Ferreira

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.

Banno

↪Nicholas Ferreira

Well, it is not possible according to the formation rules...

What occurs after ∀ is a variable, not a proposition.

Banno

↪Nicholas Ferreira

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)?

Nicholas Ferreira

↪Banno

Well, with ∀p(p∨¬p) I say that p∨¬p is true for every proposition, because p is a variable, not a specific proposition, while ☐(p∨¬p) says that "p∨¬p", which is a truth about the proposition p, is true in every possible world.
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.

Pfhorrest

A variable can stand for a proposition.

"For any proposition P, either P or not-P" is a perfectly cromulent sentence.

Nicholas Ferreira

↪Pfhorrest

Yes, in natural language it's ok to state that. But I want to know if ithere is any way of formalising that using logical or set-theoretical language.

Banno

↪Pfhorrest

Indeed, but that would take us into a second-order logic. Which is why I suggest that modality may suffice.

Banno

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. — Nicholas Ferreira

Hmmm. I'll leave you to it, then. There's too many dragons involved in having propositions range over other propositions.

quickly

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 fbfs 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. — Nicholas Ferreira

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.

alcontali

There's too many dragons involved in having propositions range over other propositions. — Banno

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 $\Bbb{N}$ .

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) ...

Deleted User

This user has been deleted and all their posts removed.

Is there any problem with quantifying over wff?

Welcome to The Philosophy Forum!

Categories

More Discussions